Theory Knuth_Bendix_Order.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}" 
        by (simp add: h n)
      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)
        by (simp add: lex_ext_unbounded_iff)
      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 [])"
  by (simp add: lex_ext_iff)

lemma lex_ext_least_2: "¬ fst (lex_ext f m [] ys)"
  by (simp add: lex_ext_iff)

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)"
        by (simp add: FT *)
      moreover
      have "?l2 (x#xs) (y#ys) ⟶ ?r2 (x#xs) (y#ys)"
        by (simp add: *)
      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
qed (simp add: lex_ext_unbounded.simps)+

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