Theory Lexicographic_Extension

theory Lexicographic_Extension
imports List_Order
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2010-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2010-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Lexicographic_Extension
imports
  Matrix.Utility
  List_Order
begin

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"
  hence 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 True note s1 = this
    show ?thesis 
    proof (cases "(a2,a3) ∈ s1")
      case True note s2 = this
      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 True note s2 = this
      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 True note s1 = this
    show ?thesis 
    proof (cases "(a2,a3) ∈ s1")
      case True note s2 = this
      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 True note s2 = this
      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)"
  apply (rule refl_onI) using refl_onD[OF r1] refl_onD[OF r2] by 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
  note this [unfolded trans_O_iff]
  show ?thesis
    apply standard
    apply(rule lex_two_refl; fact)
    unfolding trans_O_iff
    by (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.
  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


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 thus ?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]

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_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 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_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
        hence 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
          hence "?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
            hence "?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
          hence 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
        hence 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
        hence 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
          hence "?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
            hence "?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
          hence 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
        hence 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
        hence 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
          hence "?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
            hence "?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
          hence 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
        hence 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_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_unbounded f ss ts) ∧ fst (lex_ext_unbounded f ts us) ⟶ fst (lex_ext_unbounded f ss us)) ∧ 
  (fst (lex_ext_unbounded f ss ts) ∧ snd (lex_ext_unbounded f ts us) ⟶ fst (lex_ext_unbounded f ss us)) ∧ 
  (snd (lex_ext_unbounded f ss ts) ∧ snd (lex_ext_unbounded f ts us) ⟶ snd (lex_ext_unbounded f ss us)) ∧
  (fst (lex_ext_unbounded f ss ts) ∧ fst (lex_ext_unbounded f ts us) ⟶ fst (lex_ext_unbounded f ss us))
  "
  using lex_ext_compat[of ss ts us f "length ss + length ts + length us", OF assms]
  unfolding lex_ext_def Let_def by simp
  

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

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)

lemma lex_ext_SN:
  assumes stri_imp_nstri: "⋀ x y. fst (g x y) ⟹ snd (g x y)" 
  (* stri_imp_nstri is not really needed, but simplifies the proof;
     if someone wants to proof the result without this assumption, go ahead *)
    and 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"
    thus "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"
    hence "¬ length (f n) ≤ m" by auto
    thus "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
	hence "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
  thus False
  proof (induct m')
    case 0
    from this obtain f where "?confn 0 f 0" by auto	
    hence "?lexgr [] (f (Suc 0))" by force
    thus 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) thus ?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))"
    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 stri_imp_nstri have "?ge a b" 
      proof (cases "?gr a b", simp, cases "?ge a b", simp)
	assume "¬ ?gr a b" and "¬ ?ge a b" 
	hence 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" by simp
      qed
      with n sn show "?ge (?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
      hence "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)
      hence "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

lemma lex_ext_SN_2: assumes stri_imp_nstri: "⋀ x y. fst (g x y) ⟹ snd (g x y)" 
  (* stri_imp_nstri is not really needed, but simplifies the proof;
     if someone wants to proof the result without this assumption, go ahead *)
  and 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 stri_imp_nstri compat] 
  have "SN { (ys, xs). (∀ y ∈ set ys. SN_on { (s,t). fst (g s t) } {y}) ∧ fst (lex_ext g m ys xs) }" .
  thus ?thesis using SN unfolding SN_on_def by fastforce
qed

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_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



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

lemma pointwise_ext_iff: "(pointwise_ext f xs ys) = (length xs = length ys ∧ 
  ((∃ i < length ys. fst (f (xs ! i) (ys !i))) ∧ 
  (∀ i < length ys. snd (f (xs ! i) (ys ! i)))),
  length xs = length ys ∧ 
  (∀ i < length ys. snd (f (xs ! i) (ys ! i))))
  " (is "?pw xs ys = (?stri xs ys, ?nstri xs ys)")
proof (induct xs arbitrary: ys)
  case Nil thus ?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) note oPair = this
      show ?thesis
      proof (cases nstri)
        case False
        with Pair Cons show ?thesis by auto
      next
        case True
        show ?thesis 
        proof (cases "?pw as bs")
          case (Pair strir nstrir)
          note IH = Pair[unfolded oCons, simplified]
          note strir = IH[THEN conjunct1, symmetric]
          note nstrir = IH[THEN conjunct2, symmetric]
          show ?thesis 
            by (simp add: Cons oPair Pair all_Suc_conv ex_Suc_conv nstrir strir)
        qed
      qed
    qed
  qed
qed

lemma pointwise_ext_imp_lex_ext:
  "fst (pointwise_ext f xs ys) ⟹ fst (lex_ext f m xs ys)"
  unfolding pointwise_ext_iff lex_ext_iff by auto

lemma pointwise_ext_SN_2: assumes stri_imp_nstri: "⋀ x y. fst (g x y) ⟹ snd (g x y)" 
  (* stri_imp_nstri is not really needed, but simplifies the proof;
     if someone wants to proof the result without this assumption, go ahead *)
  and 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 (pointwise_ext g ys xs) }"
  by (rule SN_subset, rule lex_ext_SN_2[OF stri_imp_nstri compat SN], auto simp: pointwise_ext_imp_lex_ext) 

lemma pointwise_ext_snd_neq_imp_fst: 
  assumes snd_neq_imp_fst: "⋀ x y. ⟦snd (g x y); x ≠ y⟧ ⟹ fst (g x y)"
  and snd: "snd (pointwise_ext g as bs)"
  and neq: "as ≠ bs"
  shows "fst (pointwise_ext g as bs)"
proof -
  from snd[unfolded pointwise_ext_iff] have ge: "⋀ j. j < length bs ⟹ snd (g (as ! j) (bs ! j))" 
        and len: "length as = length bs" by auto
  from neq len obtain j where j: "j < length bs" and neq: "as ! j ≠ bs ! j" 
    unfolding list_eq_iff_nth_eq by auto
  with ge[OF j] snd_neq_imp_fst have gt: "fst (g (as ! j) (bs ! j))" by auto
  with j have "∃ j < length bs. fst (g (as ! j) (bs ! j))" by auto
  with snd show ?thesis 
    unfolding pointwise_ext_iff by auto
qed

lemma pointwise_ext_refl:
  assumes "⋀ x. snd (g x x)"
  shows "snd (pointwise_ext g xs xs)"
using assms
by (unfold pointwise_ext_iff, auto)

lemma pointwise_ext_trans:
  assumes compat: "⋀ x y z. ⟦fst(g x y); snd(g y z)⟧ ⟹ fst(g x z)"
  assumes snd_trans: "⋀ x y z. ⟦snd(g x y); snd(g y z)⟧ ⟹ snd(g x z)"
  and one: "fst (pointwise_ext g xs ys)"
  and two: "fst (pointwise_ext g ys zs)"
  shows "fst (pointwise_ext g xs zs)"
proof -
  let ?nx = "length xs"  
  let ?ny = "length ys"
  let ?nz = "length zs"
  from one[unfolded pointwise_ext_iff] obtain i where i: "i < ?nx" and stri: "fst (g (xs ! i) (ys ! i))" and len1: "?nx = ?ny" and nstri1: "∀ i < ?nx. snd (g (xs ! i) (ys ! i))" by auto
  from two[unfolded pointwise_ext_iff] have len2: "?ny = ?nz" and nstri2: "∀ i < ?ny. snd (g (ys ! i) (zs ! i))" by auto
  from nstri1 nstri2 snd_trans have nstri: "∀ i < ?nx. snd (g (xs ! i) (zs ! i))" unfolding len1 len2 by blast
  from compat[OF stri ] nstri2[THEN spec] len1 i have stri: "fst (g (xs ! i) (zs ! i))" by simp
  from stri nstri i len2[unfolded len1[symmetric]] 
  show ?thesis unfolding pointwise_ext_iff by auto
qed

lemma pointwise_snd_trans:
  assumes snd_trans: "⋀ x y z. ⟦snd(g x y); snd(g y z)⟧ ⟹ snd(g x z)"
  and one: "snd (pointwise_ext g xs ys)"
  and two: "snd (pointwise_ext g ys zs)"
  shows "snd (pointwise_ext g xs zs)"
proof -
  let ?nx = "length xs"  
  let ?ny = "length ys"
  let ?nz = "length zs"
  from one[unfolded pointwise_ext_iff] have len1: "?nx = ?ny" and nstri1: "∀ i < ?nx. snd (g (xs ! i) (ys ! i))" by auto
  from two[unfolded pointwise_ext_iff] have len2: "?ny = ?nz" and nstri2: "∀ i < ?ny. snd (g (ys ! i) (zs ! i))" by auto
  from nstri1 nstri2 snd_trans have nstri: "∀ i < ?nx. snd (g (xs ! i) (zs ! i))" unfolding len1 len2 by blast
  from nstri len2[unfolded len1[symmetric]] 
  show ?thesis unfolding pointwise_ext_iff by auto
qed


lemma bool_pair_cases:
  obtains
    (TT) "p = (True, True)"
  | (TF) "p = (True, False)"
  | (FT) "p = (False, True)"
  | (FF) "p = (False, False)"
  apply (cases p)
  apply (case_tac a)
  apply (case_tac b)
  apply simp+
  apply (case_tac b)
  apply simp+
done

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 xP xs ys rule: lex_ext_unbounded.induct)
  note [simp] = lex_ext_unbounded.simps
  case (4 x xs y ys)
  note bool_pair_cases [cases type]
  show ?case
  proof (cases "P x y")
    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 (auto) (metis bool_pair_cases fst_conv snd_conv)
      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 (auto) (metis bool_pair_cases fst_conv snd_conv)
      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)+

end