# Theory Lexicographic_Extension

```section ‹Lexicographic Extension›

theory Lexicographic_Extension
imports
Matrix.Utility
Order_Pair
begin

text ‹
In this theory we define the lexicographic extension of an order pair, so that it generalizes
the existing notion @{const lex_prod} which is based on a single order only.

Our main result is that this extension yields again an order pair.
›

fun lex_two :: "'a rel ⇒ 'a rel ⇒ 'b rel ⇒ ('a × 'b) rel"
where
"lex_two s ns s2 = {((a1, b1), (a2, b2)) . (a1, a2) ∈ s ∨ (a1, a2) ∈ ns ∧ (b1, b2) ∈ s2}"

lemma lex_two:
assumes compat: "ns O s ⊆ s"
and SN_s: "SN s"
and SN_s2: "SN s2"
shows "SN (lex_two s ns s2)" (is "SN ?r")
proof
fix f
assume "∀ i. (f i, f (Suc i)) ∈ ?r"
then have steps: "⋀ i. (f i, f (Suc i)) ∈ ?r" ..
let ?a = "λ i. fst (f i)"
let ?b = "λ i. snd (f i)"
{
fix i
from steps[of i]
have "(?a i, ?a (Suc i)) ∈ s ∨ (?a i, ?a (Suc i)) ∈ ns ∧ (?b i, ?b (Suc i)) ∈ s2"
by (cases "f i", cases "f (Suc i)", auto)
}
note steps = this
have "∃ j. ∀ i ≥ j. (?a i, ?a (Suc i)) ∈ ns - s"
by (rule non_strict_ending[OF _ compat], insert steps SN_s, unfold SN_on_def, auto)
with steps obtain j where steps: "⋀ i. i ≥ j ⟹ (?b i, ?b (Suc i)) ∈ s2" by auto
obtain g where g: "g = (λ i. ?b (j + i))" by auto
from steps have "⋀ i. (g i, g (Suc i)) ∈ s2" unfolding g by auto
with SN_s2 show False unfolding SN_defs by auto
qed

lemma lex_two_compat:
assumes compat1: "ns1 O s1 ⊆ s1"
and compat1': "s1 O ns1 ⊆ s1"
and trans1: "s1 O s1 ⊆ s1"
and trans1': "ns1 O ns1 ⊆ ns1"
and compat2: "ns2 O s2 ⊆ s2"
and ns: "(ab1, ab2) ∈ lex_two s1 ns1 ns2"
and s: "(ab2, ab3) ∈ lex_two s1 ns1 s2"
shows "(ab1, ab3) ∈ lex_two s1 ns1 s2"
proof -
obtain a1 b1 where ab1: "ab1 = (a1, b1)" by force
obtain a2 b2 where ab2: "ab2 = (a2, b2)" by force
obtain a3 b3 where ab3: "ab3 = (a3, b3)" by force
note id = ab1 ab2 ab3
show ?thesis
proof (cases "(a1, a2) ∈ s1")
case s1: True
show ?thesis
proof (cases "(a2, a3) ∈ s1")
case s2: True
from trans1 s1 s2 show ?thesis unfolding id by auto
next
case False with s have "(a2, a3) ∈ ns1" unfolding id by simp
from compat1' s1 this show ?thesis unfolding id by auto
qed
next
case False
with ns have ns: "(a1, a2) ∈ ns1" "(b1, b2) ∈ ns2" unfolding id by auto
show ?thesis
proof (cases "(a2, a3) ∈ s1")
case s2: True
from compat1 ns(1) s2 show ?thesis unfolding id by auto
next
case False
with s have nss: "(a2, a3) ∈ ns1" "(b2, b3) ∈ s2" unfolding id by auto
from trans1' ns(1) nss(1) compat2 ns(2) nss(2)
show ?thesis unfolding id by auto
qed
qed
qed

lemma lex_two_compat':
assumes compat1: "ns1 O s1 ⊆ s1"
and compat1': "s1 O ns1 ⊆ s1"
and trans1: "s1 O s1 ⊆ s1"
and trans1': "ns1 O ns1 ⊆ ns1"
and compat2': "s2 O ns2 ⊆ s2"
and s: "(ab1, ab2) ∈ lex_two s1 ns1 s2"
and ns: "(ab2, ab3) ∈ lex_two s1 ns1 ns2"
shows "(ab1, ab3) ∈ lex_two s1 ns1 s2"
proof -
obtain a1 b1 where ab1: "ab1 = (a1, b1)" by force
obtain a2 b2 where ab2: "ab2 = (a2, b2)" by force
obtain a3 b3 where ab3: "ab3 = (a3, b3)" by force
note id = ab1 ab2 ab3
show ?thesis
proof (cases "(a1, a2) ∈ s1")
case s1: True
show ?thesis
proof (cases "(a2, a3) ∈ s1")
case s2: True
from trans1 s1 s2 show ?thesis unfolding id by auto
next
case False with ns have "(a2, a3) ∈ ns1" unfolding id by simp
from compat1' s1 this show ?thesis unfolding id by auto
qed
next
case False
with s have s: "(a1, a2) ∈ ns1" "(b1, b2) ∈ s2" unfolding id by auto
show ?thesis
proof (cases "(a2, a3) ∈ s1")
case s2: True
from compat1 s(1) s2 show ?thesis unfolding id by auto
next
case False
with ns have nss: "(a2, a3) ∈ ns1" "(b2, b3) ∈ ns2" unfolding id by auto
from trans1' s(1) nss(1) compat2' s(2) nss(2)
show ?thesis unfolding id by auto
qed
qed
qed

lemma lex_two_compat2:
assumes "ns1 O s1 ⊆ s1" "s1 O ns1 ⊆ s1" "s1 O s1 ⊆ s1" "ns1 O ns1 ⊆ ns1" "ns2 O s2 ⊆ s2"
shows "lex_two s1 ns1 ns2 O lex_two s1 ns1 s2 ⊆ lex_two s1 ns1 s2"
using lex_two_compat[OF assms] by (intro subsetI, elim relcompE, fast)

lemma lex_two_compat'2:
assumes "ns1 O s1 ⊆ s1" "s1 O ns1 ⊆ s1" "s1 O s1 ⊆ s1" "ns1 O ns1 ⊆ ns1" "s2 O ns2 ⊆ s2"
shows "lex_two s1 ns1 s2 O lex_two s1 ns1 ns2 ⊆ lex_two s1 ns1 s2"
using lex_two_compat'[OF assms] by (intro subsetI, elim relcompE, fast)

lemma lex_two_refl:
assumes r1: "refl ns1" and r2: "refl ns2"
shows "refl (lex_two s1 ns1 ns2)"
using refl_onD[OF r1] and refl_onD[OF r2] by (intro refl_onI) auto

lemma lex_two_order_pair:
assumes o1: "order_pair s1 ns1" and o2: "order_pair s2 ns2"
shows "order_pair (lex_two s1 ns1 s2) (lex_two s1 ns1 ns2)"
proof -
interpret o1: order_pair s1 ns1 using o1.
interpret o2: order_pair s2 ns2 using o2.
note o1.trans_S o1.trans_NS o2.trans_S o2.trans_NS
o1.compat_NS_S o2.compat_NS_S o1.compat_S_NS o2.compat_S_NS
note this [unfolded trans_O_iff]
note o1.refl_NS o2.refl_NS
show ?thesis
by (unfold_locales, intro lex_two_refl, fact+, unfold trans_O_iff)
(rule lex_two_compat2 lex_two_compat'2;fact)+
qed

lemma lex_two_SN_order_pair:
assumes o1: "SN_order_pair s1 ns1" and o2: "SN_order_pair s2 ns2"
shows "SN_order_pair (lex_two s1 ns1 s2) (lex_two s1 ns1 ns2)"
proof -
interpret o1: SN_order_pair s1 ns1 using o1.
interpret o2: SN_order_pair s2 ns2 using o2.
note o1.trans_S o1.trans_NS o2.trans_S o2.trans_NS o1.SN o2.SN
o1.compat_NS_S o2.compat_NS_S o1.compat_S_NS o2.compat_S_NS
note this [unfolded trans_O_iff]
interpret order_pair "(lex_two s1 ns1 s2)" "(lex_two s1 ns1 ns2)"
by(rule lex_two_order_pair, standard)
show ?thesis by(standard, rule lex_two; fact)
qed

text ‹
In the unbounded lexicographic extension, there is no restriction on the lengths
of the lists. Therefore it is possible to compare lists of different lengths.
This usually results a non-terminating relation, e.g., \$[1] > [0, 1] > [0, 0, 1] > \ldots\$
›

fun lex_ext_unbounded :: "('a ⇒ 'a ⇒ bool × bool) ⇒ 'a list ⇒ 'a list ⇒ bool × bool"
where "lex_ext_unbounded f [] [] = (False, True)" |
"lex_ext_unbounded f (_ # _) [] = (True, True)" |
"lex_ext_unbounded f [] (_ # _) = (False, False)" |
"lex_ext_unbounded f (a # as) (b # bs) =
(let (stri, nstri) = f a b in
if stri then (True, True)
else if nstri then lex_ext_unbounded f as bs
else (False, False))"

lemma lex_ext_unbounded_iff: "(lex_ext_unbounded f xs ys) = (
((∃ i < length xs. i < length ys ∧ (∀ j < i. snd (f (xs ! j) (ys ! j))) ∧ fst (f (xs ! i) (ys !i))) ∨
(∀ i < length ys. snd (f (xs ! i) (ys ! i))) ∧ length xs > length ys),
((∃ i < length xs. i < length ys ∧ (∀ j < i. snd (f (xs ! j) (ys ! j))) ∧ fst (f (xs ! i) (ys !i))) ∨
(∀ i < length ys. snd (f (xs ! i) (ys ! i))) ∧ length xs ≥ length ys))
" (is "?lex xs ys = (?stri xs ys, ?nstri xs ys)")
proof (induct xs arbitrary: ys)
case Nil then show ?case by (cases ys, auto)
next
case (Cons a as)
note oCons = this
from oCons show ?case
proof (cases ys, simp)
case (Cons b bs)
show ?thesis
proof (cases "f a b")
case (Pair stri nstri)
show ?thesis
proof (cases stri)
case True
with Pair Cons show ?thesis by auto
next
case False
show ?thesis
proof (cases nstri)
case False
with ‹¬ stri› Pair Cons show ?thesis by force
next
case True
with False Pair have f: "f a b = (False, True)" by auto
show ?thesis by (simp add: all_Suc_conv ex_Suc_conv Cons f oCons)
qed
qed
qed
qed
qed

declare lex_ext_unbounded.simps[simp del]

text ‹
The lexicographic extension of an order pair takes a natural number as maximum bound.
A decrease with lists of unequal lengths will never be successful if the length of the
second list exceeds this bound. The bound is essential to preserve strong normalization.
›
definition lex_ext :: "('a ⇒ 'a ⇒ bool × bool) ⇒ nat ⇒ 'a list ⇒ 'a list ⇒ bool × bool"
where
"lex_ext f n ss ts =
(let lts = length ts in
if (length ss = lts ∨ lts ≤ n) then lex_ext_unbounded f ss ts
else (False, False))"

lemma lex_ext_iff: "(lex_ext f m xs ys) = (
(length xs = length ys ∨ length ys ≤ m) ∧ ((∃ i < length xs. i < length ys ∧ (∀ j < i. snd (f (xs ! j) (ys ! j))) ∧ fst (f (xs ! i) (ys !i))) ∨
(∀ i < length ys. snd (f (xs ! i) (ys ! i))) ∧ length xs > length ys),
(length xs = length ys ∨ length ys ≤ m) ∧
((∃ i < length xs. i < length ys ∧ (∀ j < i. snd (f (xs ! j) (ys ! j))) ∧ fst (f (xs ! i) (ys !i))) ∨
(∀ i < length ys. snd (f (xs ! i) (ys ! i))) ∧ length xs ≥ length ys))
"
unfolding lex_ext_def
by (simp only: lex_ext_unbounded_iff Let_def, auto)

lemma lex_ext_to_lex_ext_unbounded:
assumes "length xs ≤ n" and "length ys ≤ n"
shows "lex_ext f n xs ys = lex_ext_unbounded f xs ys"
using assms by (simp add: lex_ext_def)

lemma lex_ext_stri_imp_nstri:
assumes "fst (lex_ext f m xs ys)"
shows "snd (lex_ext f m xs ys)"
using assms by (auto simp: lex_ext_iff)

lemma nstri_lex_ext_map:
assumes "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ fst (order' (f s) (f t))"
and "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ snd (order' (f s) (f t))"
and "snd (lex_ext order n ss ts)"
shows "snd (lex_ext order' n (map f ss) (map f ts))"
using assms unfolding lex_ext_iff by auto

lemma stri_lex_ext_map:
assumes "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ fst (order' (f s) (f t))"
and "⋀s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ snd (order' (f s) (f t))"
and "fst (lex_ext order n ss ts)"
shows "fst (lex_ext order' n (map f ss) (map f ts))"
using assms unfolding lex_ext_iff by auto

lemma lex_ext_arg_empty: "snd (lex_ext f n [] xs) ⟹ xs = []"
unfolding lex_ext_iff by auto

lemma lex_ext_co_compat:
assumes "⋀ s t. s ∈ set ss ⟹ t ∈ set ts ⟹ fst (order s t) ⟹ snd (order' t s) ⟹ False"
and "⋀ s t. s ∈ set ss ⟹ t ∈ set ts ⟹ snd (order s t) ⟹ fst (order' t s) ⟹ False"
and "⋀ s t. fst (order s t) ⟹ snd (order s t)"
and "fst (lex_ext order n ss ts)"
and "snd (lex_ext order' n ts ss)"
shows False
proof -
let ?ls = "length ss"
let ?lt = "length ts"
define s where "s i = fst (order (ss ! i) (ts ! i))" for i
define ns where "ns i = snd (order (ss ! i) (ts ! i))" for i
define s' where "s' i = fst (order' (ts ! i) (ss ! i))" for i
define ns' where "ns' i = snd (order' (ts ! i) (ss ! i))" for i
have co: "i < ?ls ⟹ i < ?lt ⟹ s i ⟹ ns' i ⟹ False" for i
using assms(1) unfolding s_def ns'_def set_conv_nth by auto
have co': "i < ?ls ⟹ i < ?lt ⟹ s' i ⟹ ns i ⟹ False" for i
using assms(2) unfolding s'_def ns_def set_conv_nth by auto
from assms(4)[unfolded lex_ext_iff fst_conv, folded s_def ns_def]
have ch1: "(∃ i. i < ?ls ∧ i < ?lt ∧ (∀ j<i. ns j) ∧ s i) ∨ (∀i<?lt. ns i) ∧ ?lt < ?ls" (is "?A ∨ ?B") by auto
from assms(5)[unfolded lex_ext_iff snd_conv, folded s'_def ns'_def]
have ch2: "(∃i. i < ?ls ∧ i < ?lt ∧ (∀j<i. ns' j) ∧ s' i) ∨ (∀i<?ls. ns' i) ∧ ?ls ≤ ?lt" (is "?A' ∨ ?B'") by auto
from ch1 show False
proof
assume ?A
then obtain i where i: "i < ?ls" "i < ?lt" and s: "s i" and ns: "⋀ j. j < i ⟹ ns j" by auto
note s = co[OF i s]
have ns: "j < i ⟹ s' j ⟹ False" for j
using i ns[of j] co'[of j] by auto
from ch2 show False
proof
assume ?A'
then obtain i' where i': "i' < ?ls" "i' < ?lt" and s': "s' i'" and ns': "⋀ j'. j' < i' ⟹ ns' j'" by auto
from s ns'[of i] have "i ≥ i'" by presburger
with ns[OF _ s'] have i': "i' = i" by presburger
from ‹s i› have "ns i" using assms(3) unfolding s_def ns_def by auto
from co'[OF i s'[unfolded i'] this] show False .
next
assume ?B'
with i have "ns' i" by auto
from s[OF this] show False .
qed
next
assume B: ?B
with ch2 have ?A' by auto
then obtain i where i: "i < ?ls" "i < ?lt" and s': "s' i" and ns': "⋀ j. j < i ⟹ ns' j" by auto
from co'[OF i s'] B i show False by auto
qed
qed

lemma lex_ext_irrefl: assumes "⋀ x. x ∈ set xs ⟹ ¬ fst (rel x x)"
shows "¬ fst (lex_ext rel n xs xs)"
proof
assume "fst (lex_ext rel n xs xs)"
then obtain i where "i < length xs" and "fst (rel (xs ! i) (xs ! i))"
unfolding lex_ext_iff by auto
with assms[of "xs ! i"] show False by auto
qed

lemma lex_ext_unbounded_stri_imp_nstri:
assumes "fst (lex_ext_unbounded f xs ys)"
shows "snd (lex_ext_unbounded f xs ys)"
using assms by (auto simp: lex_ext_unbounded_iff)

lemma all_nstri_imp_lex_nstri: assumes "∀ i < length ys. snd (f (xs ! i) (ys ! i))" and "length xs ≥ length ys" and "length xs = length ys ∨ length ys ≤ m"
shows "snd (lex_ext f m xs ys)"
using assms by (auto simp: lex_ext_iff)

lemma lex_ext_cong[fundef_cong]: fixes f g m1 m2 xs1 xs2 ys1 ys2
assumes "length xs1 = length ys1" and "m1 = m2" and "length xs2 = length ys2" and "⋀ i. ⟦i < length ys1; i < length ys2⟧ ⟹ f (xs1 ! i) (xs2 ! i) = g (ys1 ! i) (ys2 ! i)"
shows "lex_ext f m1 xs1 xs2 = lex_ext g m2 ys1 ys2"
using assms by (auto simp: lex_ext_iff)

lemma lex_ext_unbounded_cong[fundef_cong]: assumes "as = as'" and "bs = bs'"
and "⋀ i. i < length as' ⟹ i < length bs' ⟹ f (as' ! i) (bs' ! i) = g (as' ! i) (bs' ! i)" shows "lex_ext_unbounded f as bs = lex_ext_unbounded g as' bs'"
unfolding assms lex_ext_unbounded_iff using assms(3) by auto

text ‹Compatibility is the key property to ensure transitivity of the order.›

text ‹
We prove compatibility locally, i.e., it only has to hold for elements
of the argument lists. Locality is essential for being applicable in recursively
defined term orders such as KBO.
›
lemma lex_ext_compat:
assumes compat: "⋀ s t u. ⟦s ∈ set ss; t ∈ set ts; u ∈ set us⟧ ⟹
(snd (f s t) ∧ fst (f t u) ⟶ fst (f s u)) ∧
(fst (f s t) ∧ snd (f t u) ⟶ fst (f s u)) ∧
(snd (f s t) ∧ snd (f t u) ⟶ snd (f s u)) ∧
(fst (f s t) ∧ fst (f t u) ⟶ fst (f s u))"
shows "
(snd (lex_ext f n ss ts) ∧ fst (lex_ext f n ts us) ⟶ fst (lex_ext f n ss us)) ∧
(fst (lex_ext f n ss ts) ∧ snd (lex_ext f n ts us) ⟶ fst (lex_ext f n ss us)) ∧
(snd (lex_ext f n ss ts) ∧ snd (lex_ext f n ts us) ⟶ snd (lex_ext f n ss us)) ∧
(fst (lex_ext f n ss ts) ∧ fst (lex_ext f n ts us) ⟶ fst (lex_ext f n ss us))
"
proof -
let ?ls = "length ss"
let ?lt = "length ts"
let ?lu = "length us"
let ?st = "lex_ext f n ss ts"
let ?tu = "lex_ext f n ts us"
let ?su = "lex_ext f n ss us"
let ?fst = "λ ss ts i. fst (f (ss ! i) (ts ! i))"
let ?snd = "λ ss ts i. snd (f (ss ! i) (ts ! i))"
let ?ex = "λ ss ts. ∃ i < length ss. i < length ts ∧ (∀ j < i. ?snd ss ts j) ∧ ?fst ss ts i"
let ?all = "λ ss ts. ∀ i < length ts. ?snd ss ts i"
have lengths: "(?ls = ?lt ∨ ?lt ≤ n) ∧ (?lt = ?lu ∨ ?lu ≤ n) ⟶
(?ls = ?lu ∨ ?lu ≤ n)" (is "?lst ∧ ?ltu ⟶ ?lsu") by arith
{
assume st: "snd ?st" and tu: "fst ?tu"
with lengths have lsu: "?lsu" by (simp add: lex_ext_iff)
from st have st: "?ex ss ts ∨ ?all ss ts ∧ ?lt ≤ ?ls" by (simp add: lex_ext_iff)
from tu have tu: "?ex ts us ∨ ?all ts us ∧ ?lu < ?lt" by (simp add: lex_ext_iff)
from st have "fst ?su"
proof
assume st: "?ex ss ts"
then obtain i1 where i1: "i1 < ?ls ∧ i1 < ?lt" and fst1: "?fst ss ts i1" and snd1: "∀ j < i1. ?snd ss ts j" by force
from tu show ?thesis
proof
assume tu: "?ex ts us"
then obtain i2 where i2: "i2 < ?lt ∧ i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "∀ j < i2. ?snd ts us j" by auto
let ?i = "min i1 i2"
from i1 i2 have i: "?i < ?ls ∧ ?i < ?lt ∧ ?i < ?lu" by auto
then have ssi: "ss ! ?i ∈ set ss" and tsi: "ts ! ?i ∈ set ts" and usi: "us ! ?i ∈ set us" by auto
have snd: "∀ j < ?i. ?snd ss us j"
proof (intro allI impI)
fix j
assume j: "j < ?i"
with snd1 snd2 have snd1: "?snd ss ts j" and snd2: "?snd ts us j" by auto
from j i have ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
have fst: "?fst ss us ?i"
proof (cases "i1 < i2")
case True
then have "?i = i1" by simp
with True fst1 snd2 have "?fst ss ts ?i" and "?snd ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
next
case False
show ?thesis
proof (cases "i2 < i1")
case True
then have "?i = i2" by simp
with True snd1 fst2 have "?snd ss ts ?i" and "?fst ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
next
case False
with ‹¬ i1 < i2› have "i1 = i2" by simp
with fst1 fst2 have "?fst ss ts ?i" and "?fst ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
qed
qed
show ?thesis by (simp add: lex_ext_iff lsu, rule disjI1, rule exI[of _ ?i], simp add: fst snd i)
next
assume tu: "?all ts us ∧ ?lu < ?lt"
show ?thesis
proof (cases "i1 < ?lu")
case True
then have usi: "us ! i1 ∈ set us" by auto
from i1 have ssi: "ss ! i1 ∈ set ss" and tsi: "ts ! i1 ∈ set ts" by auto
from True tu have "?snd ts us i1" by auto
with fst1 compat[OF ssi tsi usi] have fst: "?fst ss us i1" by auto
have snd: "∀ j < i1. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < i1"
with i1 True snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with fst lsu True i1 show ?thesis by (auto simp: lex_ext_iff)
next
case False
with i1 have lus: "?lu < ?ls" by auto
have snd: "∀ j < ?lu. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < ?lu"
with False i1 snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with lus lsu show ?thesis by (auto simp: lex_ext_iff)
qed
qed
next
assume st: "?all ss ts ∧ ?lt ≤ ?ls"
from tu
show ?thesis
proof
assume tu: "?ex ts us"
with st obtain i2 where i2: "i2 < ?lt ∧ i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "∀ j < i2. ?snd ts us j" by auto
from st i2 have i2: "i2 < ?ls ∧ i2 < ?lt ∧ i2 < ?lu" by auto
then have ssi: "ss ! i2 ∈ set ss" and tsi: "ts ! i2 ∈ set ts" and usi: "us ! i2 ∈ set us" by auto
from i2 st have "?snd ss ts i2" by auto
with fst2 compat[OF ssi tsi usi] have fst: "?fst ss us i2" by auto
have snd: "∀ j < i2. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < i2"
with i2 snd2 st have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with fst lsu i2 show ?thesis by (auto simp: lex_ext_iff)
next
assume tu: "?all ts us ∧ ?lu < ?lt"
with st have lus: "?lu < ?ls" by auto
have snd: "∀ j < ?lu. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < ?lu"
with st tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with lus lsu show ?thesis by (auto simp: lex_ext_iff)
qed
qed
}
moreover
{
assume st: "fst ?st" and tu: "snd ?tu"
with lengths have lsu: "?lsu" by (simp add: lex_ext_iff)
from st have st: "?ex ss ts ∨ ?all ss ts ∧ ?lt < ?ls" by (simp add: lex_ext_iff)
from tu have tu: "?ex ts us ∨ ?all ts us ∧ ?lu ≤ ?lt" by (simp add: lex_ext_iff)
from st have "fst ?su"
proof
assume st: "?ex ss ts"
then obtain i1 where i1: "i1 < ?ls ∧ i1 < ?lt" and fst1: "?fst ss ts i1" and snd1: "∀ j < i1. ?snd ss ts j" by force
from tu show ?thesis
proof
assume tu: "?ex ts us"
then obtain i2 where i2: "i2 < ?lt ∧ i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "∀ j < i2. ?snd ts us j" by auto
let ?i = "min i1 i2"
from i1 i2 have i: "?i < ?ls ∧ ?i < ?lt ∧ ?i < ?lu" by auto
then have ssi: "ss ! ?i ∈ set ss" and tsi: "ts ! ?i ∈ set ts" and usi: "us ! ?i ∈ set us" by auto
have snd: "∀ j < ?i. ?snd ss us j"
proof (intro allI impI)
fix j
assume j: "j < ?i"
with snd1 snd2 have snd1: "?snd ss ts j" and snd2: "?snd ts us j" by auto
from j i have ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
have fst: "?fst ss us ?i"
proof (cases "i1 < i2")
case True
then have "?i = i1" by simp
with True fst1 snd2 have "?fst ss ts ?i" and "?snd ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
next
case False
show ?thesis
proof (cases "i2 < i1")
case True
then have "?i = i2" by simp
with True snd1 fst2 have "?snd ss ts ?i" and "?fst ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
next
case False
with ‹¬ i1 < i2› have "i1 = i2" by simp
with fst1 fst2 have "?fst ss ts ?i" and "?fst ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
qed
qed
show ?thesis by (simp add: lex_ext_iff lsu, rule disjI1, rule exI[of _ ?i], simp add: fst snd i)
next
assume tu: "?all ts us ∧ ?lu ≤ ?lt"
show ?thesis
proof (cases "i1 < ?lu")
case True
then have usi: "us ! i1 ∈ set us" by auto
from i1 have ssi: "ss ! i1 ∈ set ss" and tsi: "ts ! i1 ∈ set ts" by auto
from True tu have "?snd ts us i1" by auto
with fst1 compat[OF ssi tsi usi] have fst: "?fst ss us i1" by auto
have snd: "∀ j < i1. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < i1"
with i1 True snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with fst lsu True i1 show ?thesis by (auto simp: lex_ext_iff)
next
case False
with i1 have lus: "?lu < ?ls" by auto
have snd: "∀ j < ?lu. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < ?lu"
with False i1 snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with lus lsu show ?thesis by (auto simp: lex_ext_iff)
qed
qed
next
assume st: "?all ss ts ∧ ?lt < ?ls"
from tu
show ?thesis
proof
assume tu: "?ex ts us"
with st obtain i2 where i2: "i2 < ?lt ∧ i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "∀ j < i2. ?snd ts us j" by auto
from st i2 have i2: "i2 < ?ls ∧ i2 < ?lt ∧ i2 < ?lu" by auto
then have ssi: "ss ! i2 ∈ set ss" and tsi: "ts ! i2 ∈ set ts" and usi: "us ! i2 ∈ set us" by auto
from i2 st have "?snd ss ts i2" by auto
with fst2 compat[OF ssi tsi usi] have fst: "?fst ss us i2" by auto
have snd: "∀ j < i2. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < i2"
with i2 snd2 st have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with fst lsu i2 show ?thesis by (auto simp: lex_ext_iff)
next
assume tu: "?all ts us ∧ ?lu ≤ ?lt"
with st have lus: "?lu < ?ls" by auto
have snd: "∀ j < ?lu. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < ?lu"
with st tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with lus lsu show ?thesis by (auto simp: lex_ext_iff)
qed
qed
}
moreover
{
assume st: "snd ?st" and tu: "snd ?tu"
with lengths have lsu: "?lsu" by (simp add: lex_ext_iff)
from st have st: "?ex ss ts ∨ ?all ss ts ∧ ?lt ≤ ?ls" by (simp add: lex_ext_iff)
from tu have tu: "?ex ts us ∨ ?all ts us ∧ ?lu ≤ ?lt" by (simp add: lex_ext_iff)
from st have "snd ?su"
proof
assume st: "?ex ss ts"
then obtain i1 where i1: "i1 < ?ls ∧ i1 < ?lt" and fst1: "?fst ss ts i1" and snd1: "∀ j < i1. ?snd ss ts j" by force
from tu show ?thesis
proof
assume tu: "?ex ts us"
then obtain i2 where i2: "i2 < ?lt ∧ i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "∀ j < i2. ?snd ts us j" by auto
let ?i = "min i1 i2"
from i1 i2 have i: "?i < ?ls ∧ ?i < ?lt ∧ ?i < ?lu" by auto
then have ssi: "ss ! ?i ∈ set ss" and tsi: "ts ! ?i ∈ set ts" and usi: "us ! ?i ∈ set us" by auto
have snd: "∀ j < ?i. ?snd ss us j"
proof (intro allI impI)
fix j
assume j: "j < ?i"
with snd1 snd2 have snd1: "?snd ss ts j" and snd2: "?snd ts us j" by auto
from j i have ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
have fst: "?fst ss us ?i"
proof (cases "i1 < i2")
case True
then have "?i = i1" by simp
with True fst1 snd2 have "?fst ss ts ?i" and "?snd ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
next
case False
show ?thesis
proof (cases "i2 < i1")
case True
then have "?i = i2" by simp
with True snd1 fst2 have "?snd ss ts ?i" and "?fst ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
next
case False
with ‹¬ i1 < i2› have "i1 = i2" by simp
with fst1 fst2 have "?fst ss ts ?i" and "?fst ts us ?i" by auto
with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
qed
qed
show ?thesis by (simp add: lex_ext_iff lsu, rule disjI1, rule exI[of _ ?i], simp add: fst snd i)
next
assume tu: "?all ts us ∧ ?lu ≤ ?lt"
show ?thesis
proof (cases "i1 < ?lu")
case True
then have usi: "us ! i1 ∈ set us" by auto
from i1 have ssi: "ss ! i1 ∈ set ss" and tsi: "ts ! i1 ∈ set ts" by auto
from True tu have "?snd ts us i1" by auto
with fst1 compat[OF ssi tsi usi] have fst: "?fst ss us i1" by auto
have snd: "∀ j < i1. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < i1"
with i1 True snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with fst lsu True i1 show ?thesis by (auto simp: lex_ext_iff)
next
case False
with i1 have lus: "?lu ≤ ?ls" by auto
have snd: "∀ j < ?lu. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < ?lu"
with False i1 snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with lus lsu show ?thesis by (auto simp: lex_ext_iff)
qed
qed
next
assume st: "?all ss ts ∧ ?lt ≤ ?ls"
from tu
show ?thesis
proof
assume tu: "?ex ts us"
with st obtain i2 where i2: "i2 < ?lt ∧ i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "∀ j < i2. ?snd ts us j" by auto
from st i2 have i2: "i2 < ?ls ∧ i2 < ?lt ∧ i2 < ?lu" by auto
then have ssi: "ss ! i2 ∈ set ss" and tsi: "ts ! i2 ∈ set ts" and usi: "us ! i2 ∈ set us" by auto
from i2 st have "?snd ss ts i2" by auto
with fst2 compat[OF ssi tsi usi] have fst: "?fst ss us i2" by auto
have snd: "∀ j < i2. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < i2"
with i2 snd2 st have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with fst lsu i2 show ?thesis by (auto simp: lex_ext_iff)
next
assume tu: "?all ts us ∧ ?lu ≤ ?lt"
with st have lus: "?lu ≤ ?ls" by auto
have snd: "∀ j < ?lu. ?snd ss us j"
proof (intro allI impI)
fix j
assume "j < ?lu"
with st tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and
ssj: "ss ! j ∈ set ss" and tsj: "ts ! j ∈ set ts" and usj: "us ! j ∈ set us" by auto
from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
qed
with lus lsu show ?thesis by (auto simp: lex_ext_iff)
qed
qed
}
ultimately
show ?thesis using lex_ext_stri_imp_nstri by blast
qed

lemma lex_ext_unbounded_map:
assumes S: "⋀ i. i < length ss ⟹ i < length ts ⟹ fst (r (ss ! i) (ts ! i)) ⟹ fst (r (map f ss ! i) (map f ts ! i))"
and NS: "⋀ i. i < length ss ⟹ i < length ts ⟹ snd (r (ss ! i) (ts ! i)) ⟹ snd (r (map f ss ! i) (map f ts ! i))"
shows "(fst (lex_ext_unbounded r ss ts) ⟶ fst (lex_ext_unbounded r (map f ss) (map f ts))) ∧
(snd (lex_ext_unbounded r ss ts) ⟶ snd (lex_ext_unbounded r (map f ss) (map f ts)))"
using S NS unfolding lex_ext_unbounded_iff by auto

lemma lex_ext_unbounded_map_S:
assumes S: "⋀ i. i < length ss ⟹ i < length ts ⟹ fst (r (ss ! i) (ts ! i)) ⟹ fst (r (map f ss ! i) (map f ts ! i))"
and NS: "⋀ i. i < length ss ⟹ i < length ts ⟹ snd (r (ss ! i) (ts ! i)) ⟹ snd (r (map f ss ! i) (map f ts ! i))"
and stri: "fst (lex_ext_unbounded r ss ts)"
shows "fst (lex_ext_unbounded r (map f ss) (map f ts))"
using lex_ext_unbounded_map[of ss ts r f, OF S NS] stri by blast

lemma lex_ext_unbounded_map_NS:
assumes S: "⋀ i. i < length ss ⟹ i < length ts ⟹ fst (r (ss ! i) (ts ! i)) ⟹ fst (r (map f ss ! i) (map f ts ! i))"
and NS: "⋀ i. i < length ss ⟹ i < length ts ⟹ snd (r (ss ! i) (ts ! i)) ⟹ snd (r (map f ss ! i) (map f ts ! i))"
and nstri: "snd (lex_ext_unbounded r ss ts)"
shows "snd (lex_ext_unbounded r (map f ss) (map f ts))"
using lex_ext_unbounded_map[of ss ts r f, OF S NS] nstri by blast

text ‹Strong normalization with local SN assumption›
lemma lex_ext_SN:
assumes compat: "⋀ x y z. ⟦snd (g x y); fst (g y z)⟧ ⟹ fst (g x z)"
shows "SN { (ys, xs). (∀ y ∈ set ys. SN_on { (s, t). fst (g s t) } {y}) ∧ fst (lex_ext g m ys xs) }"
(is "SN { (ys, xs). ?cond ys xs }")
proof (rule ccontr)
assume "¬ ?thesis"
from this obtain f where f: "⋀ n :: nat. ?cond (f n) (f (Suc n))" unfolding SN_defs by auto
have m_imp_m: "⋀ n. length (f n) ≤ m ⟹ length (f (Suc n)) ≤ m"
proof -
fix n
assume "length (f n) ≤ m"
then show "length (f (Suc n)) ≤ m"
using f[of n] by (auto simp: lex_ext_iff)
qed
have lm_imp_m_or_eq: "⋀ n. length (f n) > m ⟹ length (f (Suc n)) ≤ m ∨ length (f n) = length (f (Suc n))"
proof -
fix n
assume "length (f n) > m"
then have "¬ length (f n) ≤ m" by auto
then show "length (f (Suc n)) ≤ m ∨ length (f n) = length (f (Suc n))"
using f[of n] by (simp add: lex_ext_iff, blast)
qed
let ?l0 = "max (length (f 0)) m"
have "⋀ n. length (f n) ≤ ?l0"
proof -
fix n
show "length (f n) ≤ ?l0"
proof (induct n, simp)
case (Suc n)
show ?case
proof (cases "length (f n) ≤ m")
case True
with m_imp_m[of n] show ?thesis by auto
next
case False
then have "length (f n) > m" by auto
with lm_imp_m_or_eq[of n]
have "length (f n) = length (f (Suc n)) ∨ length (f (Suc n)) ≤ m" by auto
with Suc show ?thesis by auto
qed
qed
qed
from this obtain m' where len: "⋀ n. length (f n) ≤ m'" by auto
let ?lexgr = "λ ys xs. fst (lex_ext g m ys xs)"
let ?lexge = "λ ys xs. snd (lex_ext g m ys xs)"
let ?gr = "λ t s. fst (g t s)"
let ?ge = "λ t s. snd (g t s)"
let ?S = "{ (y, x). fst (g y x) }"
let ?NS = "{ (y, x). snd (g y x) }"
let ?baseSN = "λ ys. ∀ y ∈ set ys. SN_on ?S {y}"
let ?con = "λ ys xs m'. ?baseSN ys ∧ length ys ≤ m' ∧ ?lexgr ys xs"
let ?confn = "λ m' f n . ?con (f n) (f (Suc n)) m'"
from compat have compat2: "?NS O ?S ⊆ ?S" by auto
from f len have  "∃ f. ∀ n. ?confn m' f n" by auto
then show False
proof (induct m')
case 0
from this obtain f where "?confn 0 f 0" by auto
then have "?lexgr [] (f (Suc 0))" by force
then show False by (simp add: lex_ext_iff)
next
case (Suc m')
from this obtain f where confn: "⋀ n. ?confn (Suc m') f n" by auto
have ne: "⋀ n. f n ≠ []"
proof -
fix n
show "f n ≠ []"
proof (cases "f n")
case (Cons a b) then show ?thesis by auto
next
case Nil
with confn[of n] show ?thesis by (simp add: lex_ext_iff)
qed
qed
let ?hf = "λ n. hd (f n)"
have ge: "⋀ n. ?ge (?hf n) (?hf (Suc n)) ∨ ?gr (?hf n) (?hf (Suc n))"
proof -
fix n
from ne[of n] obtain a as where n: "f n = a # as" by (cases "f n", auto)
from ne[of "Suc n"] obtain b bs where sn: "f (Suc n) = b # bs" by (cases "f (Suc n)", auto)
from n sn have "?ge a b ∨ ?gr a b"
proof (cases "?gr a b", simp, cases "?ge a b", simp)
assume "¬ ?gr a b" and "¬ ?ge a b"
then have g: "g a b = (False, False)" by (cases "g a b", auto)
from confn[of n] have "fst (lex_ext g m (f n) (f (Suc n)))" (is ?fst) by simp
have "?fst = False" by (simp add: n sn lex_ext_def g lex_ext_unbounded.simps)
with ‹?fst› show "?ge a b ∨ ?gr a b" by simp
qed
with n sn show "?ge (?hf n) (?hf (Suc n)) ∨ ?gr (?hf n) (?hf (Suc n))" by simp
qed
from ge have GE: "∀ n. (?hf n, ?hf (Suc n)) ∈ ?NS ∪ ?S" by auto
from confn[of 0] ne[of 0] have SN_0: "SN_on ?S {?hf 0}" by (cases "f 0", auto )
from non_strict_ending[of ?hf, OF GE compat2 SN_0]
obtain j where j: "∀ i ≥ j. (?hf i, ?hf (Suc i)) ∈ ?NS - ?S" by auto
let ?h = "λ n. tl (f (j + n))"
obtain h where h: "h = ?h"  by auto
have "⋀ n. ?confn m' h n"
proof -
fix n
let ?nj = "j + n"
from spec[OF j, of ?nj]
have ge_not_gr: "(?hf ?nj, ?hf (Suc ?nj)) ∈ ?NS - ?S" by simp
from confn[of ?nj] have old: "?confn (Suc m') f ?nj" by simp
from ne[of ?nj] obtain a as where n: "f ?nj = a # as" by (cases "f ?nj", auto)
from ne[of "Suc ?nj"] obtain b bs where sn: "f (Suc ?nj) = b # bs" by (cases "f (Suc ?nj)", auto)
from old have one: "∀ y ∈ set (h n). SN_on ?S {y}"
from old have two: "length (h n) ≤ m'" by (simp add: j n h)
from ge_not_gr have ge_not_gr2: "g a b = (False, True)"  by (simp add: n sn, cases "g a b", auto)
from old have "fst (lex_ext g m (f (j+ n)) (f (Suc (j+n))))" (is ?fst) by simp
then have "length as = length bs ∨ length bs ≤ m" (is ?len)
by (simp add: lex_ext_def n sn, cases ?len, auto)
from ‹?fst›[simplified n sn] have "fst (lex_ext_unbounded g as bs)" (is ?fst)
by (simp add: lex_ext_def, cases "length as = length bs ∨ Suc (length bs) ≤ m", simp_all add: ge_not_gr2 lex_ext_unbounded.simps)
then have "fst (lex_ext_unbounded g as bs)" (is ?fst)
have three: "?lexgr (h n) (h (Suc n))"
by (simp add: lex_ext_def h n sn ge_not_gr2 lex_ext_unbounded.simps, simp only: Let_def, simp add: ‹?len› ‹?fst›)
from one two three show "?confn m' h n" by blast
qed
with Suc show ?thesis by blast
qed
qed

text ‹Strong normalization with global SN assumption is immediate consequence.›
lemma lex_ext_SN_2:
assumes compat: "⋀ x y z. ⟦snd (g x y); fst (g y z)⟧ ⟹ fst (g x z)"
and SN:  "SN {(s, t). fst (g s t)}"
shows "SN { (ys, xs). fst (lex_ext g m ys xs) }"
proof -
from lex_ext_SN[OF compat]
have "SN { (ys, xs). (∀ y ∈ set ys. SN_on { (s, t). fst (g s t) } {y}) ∧ fst (lex_ext g m ys xs) }" .
then show ?thesis using SN unfolding SN_on_def by fastforce
qed

text ‹The empty list is the least element in the lexicographic extension.›
lemma lex_ext_least_1: "snd (lex_ext f m xs [])"

lemma lex_ext_least_2: "¬ fst (lex_ext f m [] ys)"

text ‹Preservation of totality on lists of same length.›
lemma lex_ext_unbounded_total:
assumes "∀(s, t)∈set (zip ss ts). s = t ∨ fst (f s t) ∨ fst (f t s)"
and refl: "⋀ t. snd (f t t)"
and "length ss = length ts"
shows "ss = ts ∨ fst (lex_ext_unbounded f ss ts) ∨ fst (lex_ext_unbounded f ts ss)"
using assms(3, 1)
proof (induct ss ts rule: list_induct2)
case (Cons s ss t ts)
from Cons(3) have "s = t ∨ (fst (f s t) ∨ fst (f t s))" by auto
then show ?case
proof
assume st: "s = t"
then show ?thesis using Cons(2-3) refl[of t] by (cases "f t t", auto simp: lex_ext_unbounded.simps)
qed (auto simp: lex_ext_unbounded.simps split: prod.splits)
qed simp

lemma lex_ext_total:
assumes "∀(s, t)∈set (zip ss ts). s = t ∨ fst (f s t) ∨ fst (f t s)"
and "⋀ t. snd (f t t)"
and len: "length ss = length ts"
shows "ss = ts ∨ fst (lex_ext f n ss ts) ∨ fst (lex_ext f n ts ss)"
using lex_ext_unbounded_total[OF assms] unfolding lex_ext_def Let_def len by auto

text ‹Monotonicity of the lexicographic extension.›
lemma lex_ext_unbounded_mono:
assumes "⋀i. ⟦i < length xs; i < length ys; fst (P (xs ! i) (ys ! i))⟧ ⟹ fst (P' (xs ! i) (ys ! i))"
and   "⋀i. ⟦i < length xs; i < length ys; snd (P (xs ! i) (ys ! i))⟧ ⟹ snd (P' (xs ! i) (ys ! i))"
shows
"(fst (lex_ext_unbounded P xs ys) ⟶ fst (lex_ext_unbounded P' xs ys)) ∧
(snd (lex_ext_unbounded P xs ys) ⟶ snd (lex_ext_unbounded P' xs ys))"
(is "(?l1 xs ys ⟶ ?r1 xs ys) ∧ (?l2 xs ys ⟶ ?r2 xs ys)")
using assms
proof (induct x≡P xs ys rule: lex_ext_unbounded.induct)
note [simp] = lex_ext_unbounded.simps
case (4 x xs y ys)
consider (TT) "P x y = (True, True)"
| (TF) "P x y = (True, False)"
| (FT) "P x y = (False, True)"
| (FF) "P x y = (False, False)" by (cases "P x y", auto)
thus ?case
proof cases
case TT
moreover
with 4(2) [of 0] and 4(3) [of 0]
have "P' x y = (True, True)"
by (auto) (metis (full_types) prod.collapse)
ultimately
show ?thesis by simp
next
case TF
show ?thesis
proof (cases "snd (P' x y)")
case False
moreover
with 4(2) [of 0] and TF
have "P' x y = (True, False)"
by (cases "P' x y", auto)
ultimately
show ?thesis by simp
next
case True
with 4(2) [of 0] and TF
have "P' x y = (True, True)"
by (auto )(metis (full_types) fst_conv snd_conv surj_pair)
then show ?thesis by simp
qed
next
case FF then show ?thesis by simp
next
case FT
show ?thesis
proof (cases "fst (P' x y)")
case True
with 4(3) [of 0] and FT
have *: "P' x y = (True, True)"
by (auto) (metis (full_types) prod.collapse)
have "?l1 (x#xs) (y#ys) ⟶ ?r1 (x#xs) (y#ys)"
moreover
have "?l2 (x#xs) (y#ys) ⟶ ?r2 (x#xs) (y#ys)"
ultimately show ?thesis by blast
next
case False
with 4(3) [of 0] and FT
have *: "P' x y = (False, True)"
by (cases "P' x y", auto)
show ?thesis
using 4(1) [OF refl FT [symmetric]] and 4(2) and 4(3)
using FT *
by (auto) (metis Suc_less_eq nth_Cons_Suc)+
qed
qed

lemma lex_ext_local_mono [mono]:
assumes "⋀s t. s ∈ set ts ⟹ t ∈ set ss ⟹ ord s t ⟹ ord' s t"
shows "fst (lex_ext (λ x y. (ord x y, (x, y) ∈ ns_rel)) (length ts) ts ss) ⟶
fst (lex_ext (λ x y. (ord' x y, (x, y) ∈ ns_rel)) (length ts) ts ss)"
proof
assume ass: "fst (lex_ext (λx y. (ord x y, (x, y) ∈ ns_rel)) (length ts) ts ss)"
from assms have mono: "(⋀i. i < length ts ⟹ i < length ss ⟹ ord (ts ! i) (ss ! i) ⟹ ord' (ts ! i) (ss ! i))"
using nth_mem by blast
let ?P = "(λ x y. (ord x y, (x, y) ∈ ns_rel))"
let ?P' = "(λ x y. (ord' x y, (x, y) ∈ ns_rel))"
from ass have lex: "fst (lex_ext_unbounded ?P ts ss)" unfolding lex_ext_def Let_def if_distrib
by (auto split: if_splits)
have "fst (lex_ext_unbounded ?P' ts ss)"
by (rule lex_ext_unbounded_mono[THEN conjunct1, rule_format, OF _ _ lex], insert mono, auto)
thus "fst (lex_ext (λx y. (ord' x y, (x, y) ∈ ns_rel)) (length ts) ts ss)"
using ass unfolding lex_ext_def by (auto simp: Let_def)
qed

lemma lex_ext_mono [mono]:
assumes "⋀s t. ord s t ⟶ ord' s t"
shows "fst (lex_ext (λ x y. (ord x y, (x, y) ∈ ns)) (length ts) ts ss) ⟶
fst (lex_ext (λ x y. (ord' x y, (x, y) ∈ ns)) (length ts) ts ss)"
using assms lex_ext_local_mono[of ts ss ord ord' ns] by blast

end
```