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)"
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)"
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)"
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 x≡P 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