Theory List_Lexorder_NS
theory List_Lexorder_NS
imports
"../util/Sorting_Util"
"../util/List_Slice"
"../order/List_Permutation_Util"
begin
section ‹General Non-standard Lexicographical Comparison›
text ‹ This section is based on the @{const lexord} classical lexicographical definition
in the the List library but accounts for a variant of lexicographic order defined below
that we rely on for verifying sais.
The main difference is that this ordering preferences the original string over its prefix.
For example, "aaa" is less than "aa", which in turn is less than "a".›
definition nslexord :: "('a × 'a) set ⇒ ('a list × 'a list) set" where
"nslexord r = {(x,y). (∃a v. x = y @ a # v) ∨
(∃u a b v w. (a, b) ∈ r ∧ x = u @ a # v ∧ y = u @ b # w)}"
definition nslexordp :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"nslexordp cmp xs ys ⟷
(∃b c as bs cs. xs = as @ b # bs ∧ ys = as @ c # cs ∧ cmp b c) ∨
(∃c cs. xs = ys @ c # cs)"
lemma nslexord_eq_nslexordp:
"(xs, ys) ∈ nslexord {(x, y). cmp x y} ⟷ nslexordp cmp xs ys"
"(xs, ys) ∈ nslexord r ⟷ nslexordp (λx y. (x, y) ∈ r) xs ys"
by (clarsimp simp: nslexord_def nslexordp_def; blast)+
definition nslexordeqp :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"nslexordeqp cmp xs ys ⟷ nslexordp cmp xs ys ∨ (xs = ys)"
subsection ‹Intro and Elimination›
lemma nslexordpI1:
"∃b c as bs cs. xs = as @ b # bs ∧ ys = as @ c # cs ∧ cmp b c ⟹ nslexordp cmp xs ys"
by (simp add: nslexordp_def)
lemma nslexordpI2:
"∃c cs. xs = ys @ c # cs ⟹ nslexordp cmp xs ys"
by (simp add: nslexordp_def)
lemma nslexordpE:
"nslexordp cmp xs ys ⟹
(∃b c as bs cs. xs = as @ b # bs ∧ ys = as @ c # cs ∧ cmp b c) ∨
(∃c cs. xs = ys @ c # cs)"
by (simp add: nslexordp_def)
lemma nslexordp_imp_eq:
"nslexordp cmp xs ys ⟹ nslexordeqp cmp xs ys"
by (simp add: nslexordeqp_def)
lemma nslexordeqp_imp_eq_or_less:
"nslexordeqp cmp xs ys ⟹ xs = ys ∨ nslexordp cmp xs ys"
using nslexordeqp_def by auto
subsection "Simplification"
lemma nslexord_Nil_left[simp]: "([], y) ∉ nslexord r"
by (unfold nslexord_def, induct y, auto)
lemma nslexord_Nil_right[simp]: "(y, []) ∈ nslexord r = (∃a x. y = a # x)"
by (unfold nslexord_def, induct y, auto)
lemma nslexord_cons_cons[simp]:
"(a # x, b # y) ∈ nslexord r ⟷ (a, b) ∈ r ∨ (a = b ∧ (x, y) ∈ nslexord r)" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
apply (simp add: nslexord_def)
apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
done
qed (auto simp add: nslexord_def; (blast | meson Cons_eq_appendI))
lemma nslexordp_cons_cons[simp]:
"nslexordp r (a # x) (b # y) ⟷ r a b ∨ (a = b ∧ nslexordp r x y)"
by (metis mem_Collect_eq nslexord_cons_cons nslexord_eq_nslexordp(1) prod.simps(2))
lemmas nslexord_simps = nslexord_Nil_left nslexord_Nil_right nslexord_cons_cons
lemma nslexord_same_pref_iff:
"(xs @ ys, xs @ zs) ∈ nslexord r ⟷ (∃x ∈ set xs. (x, x) ∈ r) ∨ (ys, zs) ∈ nslexord r"
by(induction xs) auto
lemma nslexord_same_pref_if_irrefl[simp]:
"irrefl r ⟹ (xs @ ys, xs @ zs) ∈ nslexord r ⟷ (ys, zs) ∈ nslexord r"
by (simp add: irrefl_def nslexord_same_pref_iff)
lemma nslexord_append_leftI:
"∃b z. y = b # z ⟹ (x @ y, x) ∈ nslexord r"
by (simp add: nslexordpI2 nslexord_eq_nslexordp(2))
lemma nslexord_append_left_rightI:
"(a ,b) ∈ r ⟹ (u @ a # x, u @ b # y) ∈ nslexord r"
by (simp add: nslexord_same_pref_iff)
lemma nslexord_append_rightI:
"(u, v) ∈ nslexord r ⟹ (x @ u, x @ v) ∈ nslexord r"
by (simp add: nslexord_same_pref_iff)
lemma nslexord_append_rightD:
"⟦(x @ u, x @ v) ∈ nslexord r; (∀a. (a,a) ∉ r) ⟧ ⟹ (u,v) ∈ nslexord r"
by (simp add: nslexord_same_pref_iff)
lemma nslexord_lex:
"(x,y) ∈ lex r = ((x,y) ∈ nslexord r ∧ length x = length y)"
proof (induction x arbitrary: y)
case (Cons a x y) then show ?case
by (cases y) (force+)
qed auto
subsection ‹Recursive version›
fun nslexordrec :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"nslexordrec P [] _ = False" |
"nslexordrec P _ [] = True" |
"nslexordrec P (x#xs) (y#ys) = (if P x y then True else if x = y then nslexordrec P xs ys else False)"
lemma nslexordp_eq_nslexordrec:
"nslexordp cmp xs ys ⟷ nslexordrec cmp xs ys"
proof (induct xs arbitrary: ys)
case Nil
then show ?case
by (simp add: nslexordp_def)
next
case (Cons a xs)
note IH = this
then show ?case
proof (cases ys)
case Nil
then show ?thesis
by (simp add: nslexordp_def)
next
case (Cons b zs)
note P = IH[of zs]
have "cmp a b ⟹ ?thesis"
by (simp add: Cons)
moreover
have "⟦¬cmp a b; a = b⟧ ⟹ ?thesis"
by (simp add: P Cons)
moreover
have "⟦¬cmp a b; a ≠ b⟧ ⟹ ?thesis"
by (simp add: local.Cons)
ultimately show ?thesis
by blast
qed
qed
lemmas nslexordp_induct = nslexordrec.induct
subsection "Properties"
text ‹Useful properties for proving things about relations,
such as what type of order is satisfied›
lemma nslexord_total_on:
assumes "total_on A R"
shows "total_on {xs. set xs ⊆ A} (nslexord R)"
proof (intro total_onI)
fix x y
assume "x ∈ {xs. set xs ⊆ A}" "y ∈ {xs. set xs ⊆ A}" "x ≠ y"
hence "set x ⊆ A" "set y ⊆ A" "x ≠ y"
by blast+
then show "(x, y) ∈ nslexord R ∨ (y, x) ∈ nslexord R"
proof (induct x arbitrary: y)
case Nil
then show ?case
by (metis list.exhaust nslexord_Nil_right)
next
case (Cons a x)
note IH = this
then show ?case
proof (cases y)
case Nil
then show ?thesis
by auto
next
case (Cons b z)
then show ?thesis
by (metis Cons.hyps IH(2-4) assms list.set_intros(1,2) nslexord_cons_cons subset_code(1)
total_on_def)
qed
qed
qed
lemma total_on_totalp_on_eq:
"total_on A {(x, y). R x y} = totalp_on A R"
by (simp add: total_on_def totalp_on_def)
lemmas nslexordp_totalp_on =
nslexord_total_on[OF total_on_totalp_on_eq[THEN iffD2],
simplified nslexord_eq_nslexordp(1) totalp_on_total_on_eq[symmetric]]
lemma nslexord_total:
"total r ⟹ total (nslexord r)"
using nslexord_total_on by fastforce
lemma nslexordp_totalp:
"totalp r ⟹ totalp (nslexordp r)"
using nslexordp_totalp_on by fastforce
corollary nslexord_linear:
"(∀a b. (a,b) ∈ r ∨ a = b ∨ (b,a) ∈ r) ⟹ (x,y) ∈ nslexord r ∨ x = y ∨ (y,x) ∈ nslexord r"
using nslexord_total by (metis UNIV_I total_on_def)
lemma nslexord_irrefl_on:
assumes "irrefl_on A R"
shows "irrefl_on {xs. set xs ⊆ A} (nslexord R)"
proof (intro irrefl_onI)
fix x
assume "x ∈ {xs. set xs ⊆ A}"
hence "set x ⊆ A"
by blast
then show "(x, x) ∉ nslexord R"
proof (induct x)
case Nil
then show ?case
by auto
next
case (Cons a x)
then show ?case
by (meson assms irrefl_onD list.set_intros(1) nslexord_cons_cons set_subset_Cons
subset_code(1))
qed
qed
lemma irrefl_on_irreflp_on_eq:
"irrefl_on A {(x, y). R x y} = irreflp_on A R"
by (simp add: irrefl_on_def irreflp_on_def)
lemmas nslexordp_irreflp_on =
nslexord_irrefl_on[OF irrefl_on_irreflp_on_eq[THEN iffD2],
simplified nslexord_eq_nslexordp(1) irreflp_on_irrefl_on_eq[symmetric]]
lemma nslexord_irreflexive:
"∀x. (x,x) ∉ r ⟹ (xs,xs) ∉ nslexord r"
by (metis lex_take_index nslexord_lex)
lemma nslexord_irrefl:
"irrefl R ⟹ irrefl (nslexord R)"
by (simp add: irrefl_def nslexord_irreflexive)
lemma nslexordp_irreflp:
assumes "irreflp R"
shows "irreflp (nslexordp R)"
using assms nslexordp_irreflp_on by force
lemma asym_on_asymp_on_eq:
"asym_on A {(x, y). R x y} = asymp_on A R"
by (simp add: asym_on_def asymp_on_def)
lemma nslexord_asym_on:
assumes "asym_on A R"
shows "asym_on {xs. set xs ⊆ A} (nslexord R)"
proof (intro asym_onI)
fix x y
assume "x ∈ {xs. set xs ⊆ A}" "y ∈ {xs. set xs ⊆ A}" "(x, y) ∈ nslexord R"
hence "set x ⊆ A" "set y ⊆ A" "(x, y) ∈ nslexord R"
by blast+
then show "(y, x) ∉ nslexord R"
proof (induct x arbitrary: y)
case Nil
then show ?case
by force
next
case (Cons a x)
note IH = this
then show ?case
proof (cases y)
case Nil
then show ?thesis
by simp
next
case (Cons b z)
hence "(a # x, b # z) ∈ nslexord R"
using IH(4) by blast
with nslexord_cons_cons[of a x b z R]
have "(a, b) ∈ R ∨ a = b ∧ (x, z) ∈ nslexord R"
by blast
moreover
have "(a, b) ∈ R ⟹ ?thesis"
by (metis IH(2,3) assms asym_onD list.set_intros(1) local.Cons nslexord_cons_cons
subset_code(1))
moreover
have "a = b ∧ (x, z) ∈ nslexord R ⟹ ?thesis"
using Cons.hyps IH(2,3) calculation(2) local.Cons by auto
ultimately show ?thesis
by blast
qed
qed
qed
lemmas nslexordp_asymp_on =
nslexord_asym_on[OF asym_on_asymp_on_eq[THEN iffD2],
simplified nslexord_eq_nslexordp(1) asymp_on_asym_on_eq[symmetric]]
lemma nslexord_asym:
assumes "asym R"
shows "asym (nslexord R)"
using assms nslexord_asym_on by force
lemma nslexordp_asymp:
assumes "asymp R"
shows "asymp (nslexordp R)"
using assms nslexordp_asymp_on by force
lemma nslexord_asymmetric:
assumes "asym R" "(a, b) ∈ nslexord R"
shows "(b, a) ∉ nslexord R"
by (simp add: assms asymD nslexord_asym)
lemma trans_on_transp_on_eq:
"trans_on A {(x, y). R x y} = transp_on A R"
by (simp add: trans_on_def transp_on_def)
lemma nslexord_trans_on:
assumes "trans_on A R"
shows "trans_on {xs. set xs ⊆ A} (nslexord R)"
proof (intro trans_onI)
fix x y z
assume "x ∈ {xs. set xs ⊆ A}" "y ∈ {xs. set xs ⊆ A}" "z ∈ {xs. set xs ⊆ A}"
"(x, y) ∈ nslexord R" "(y, z) ∈ nslexord R"
hence "set x ⊆ A" "set y ⊆ A" "set z ⊆ A" "(x, y) ∈ nslexord R" "(y, z) ∈ nslexord R"
by blast+
then show "(x, z) ∈ nslexord R"
proof (induct x arbitrary: y z)
case Nil
then show ?case
by simp
next
case (Cons a x)
note IH = this
then show ?case
proof (cases y)
case Nil
then show ?thesis
using IH(6) by auto
next
case (Cons b y')
hence "(a # x, b # y') ∈ nslexord R"
using IH(5) by blast
with nslexord_cons_cons[of a x b y' R]
have P: "(a, b) ∈ R ∨ a = b ∧ (x, y') ∈ nslexord R"
by blast
then show ?thesis
proof (cases z)
case Nil
then show ?thesis
by simp
next
case (Cons c z')
hence "(b # y', c # z') ∈ nslexord R"
using IH(6) ‹y = b # y'› by auto
with nslexord_cons_cons[of b y' c z' R]
have "(b, c) ∈ R ∨ b = c ∧ (y', z') ∈ nslexord R"
by blast
moreover
have "a ∈ A" "set x ⊆ A"
using IH(2) by auto
moreover
have "b ∈ A" "set y' ⊆ A"
using IH(3) ‹y = b # y'› by force+
moreover
have "c ∈ A" "set z' ⊆ A"
using IH(4) ‹z = c # z'› by force+
moreover
from P
have "(b, c) ∈ R ⟹ ?thesis"
by (metis assms calculation(2,4,6) local.Cons nslexord_cons_cons trans_onD)
moreover
from P
have "b = c ∧ (y', z') ∈ nslexord R ⟹ ?thesis"
by (metis Cons.hyps calculation(3,5,7) local.Cons nslexord_cons_cons)
ultimately show ?thesis
by blast
qed
qed
qed
qed
lemmas nslexordp_transp_on =
nslexord_trans_on[OF trans_on_transp_on_eq[THEN iffD2],
simplified nslexord_eq_nslexordp(1) transp_on_trans_on_eq[symmetric]]
lemma nslexord_trans:
assumes "trans R"
shows "trans (nslexord R)"
using assms nslexord_trans_on by force
lemma nslexordp_transp:
assumes "transp R"
shows "transp (nslexordp R)"
using assms nslexordp_transp_on by force
subsection ‹Monotonicity›
text ‹Properties about monotonicity›
lemma monotone_on_nslexordp:
assumes "monotone_on A orda ordb f"
shows "monotone_on {xs. set xs ⊆ A} (nslexordp orda) (nslexordp ordb) (map f)"
proof (rule monotone_onI)
fix x y
assume "x ∈ {xs. set xs ⊆ A}" "y ∈ {xs. set xs ⊆ A}" "nslexordp orda x y"
hence "set x ⊆ A" "set y ⊆ A"
by blast+
let ?c1 = "∃b c as bs cs. x = as @ b # bs ∧ y = as @ c # cs ∧ orda b c"
and ?c2 = "∃c cs. x = y @ c # cs"
let ?g = "nslexordp ordb (map f x) (map f y)"
from nslexordpE[OF ‹nslexordp orda x y›]
have "?c1 ∨ ?c2" .
moreover
have "?c2 ⟹ ?g"
using nslexordpI2 by fastforce
moreover
have "?c1 ⟹ ?g"
proof (rule nslexordpI1)
assume ?c1
then obtain b c as bs cs where
"x = as @ b # bs"
"y = as @ c # cs"
"orda b c"
by blast
moreover
have "map f x = map f as @ f b # map f bs"
by (simp add: calculation(1))
moreover
have "map f y = map f as @ f c # map f cs"
by (simp add: calculation(2))
moreover
have "ordb (f b) (f c)"
by (metis ‹set x ⊆ A› ‹set y ⊆ A› assms calculation(1-3) in_set_conv_decomp monotone_on_def
subset_code(1))
ultimately show "∃b c as bs cs. map f x = as @ b # bs ∧ map f y = as @ c # cs ∧ ordb b c"
by blast
qed
ultimately show "nslexordp ordb (map f x) (map f y)"
by blast
qed
lemma monotone_on_bij_betw_inv_nslexordp:
assumes "monotone_on A orda ordb f"
and "asymp_on A orda"
and "totalp_on A orda"
and "asymp_on B ordb"
and "totalp_on B ordb"
and "bij_betw f A B"
and "bij_betw g B A"
and "inverses_on f g A B"
shows "monotone_on {xs. set xs ⊆ B} (nslexordp ordb) (nslexordp orda) (map g)"
by (metis assms monotone_on_bij_betw_inv monotone_on_nslexordp)
lemma monotone_on_bij_betw_nslexordp:
assumes "monotone_on A orda ordb f"
and "asymp_on A orda"
and "totalp_on A orda"
and "asymp_on B ordb"
and "totalp_on B ordb"
and "bij_betw f A B"
shows "∃g. bij_betw (map g) {xs. set xs ⊆ B} {xs. set xs ⊆ A} ∧
inverses_on (map f) (map g) {xs. set xs ⊆ A} {xs. set xs ⊆ B} ∧
monotone_on {xs. set xs ⊆ B} (nslexordp ordb) (nslexordp orda) (map g)"
by (metis assms bij_betw_inv_alt bij_betw_map inverses_on_map monotone_on_bij_betw_inv_nslexordp)
lemma monotone_on_iff_nslexordp:
assumes "monotone_on A orda ordb f"
and "asymp_on A orda"
and "totalp_on A orda"
and "asymp_on B ordb"
and "totalp_on B ordb"
and "bij_betw f A B"
and "set xs ⊆ A"
and "set ys ⊆ A"
shows "nslexordp orda xs ys ⟷ nslexordp ordb (map f xs) (map f ys)"
proof
assume "nslexordp orda xs ys"
with monotone_onD[OF monotone_on_nslexordp[OF assms(1)], simplified, OF assms(7,8)]
show "nslexordp ordb (map f xs) (map f ys)"
by blast
next
assume A: "nslexordp ordb (map f xs) (map f ys)"
from monotone_on_bij_betw_nslexordp[OF assms(1-6)]
obtain g where P:
"bij_betw (map g) {xs. set xs ⊆ B} {xs. set xs ⊆ A}"
"inverses_on (map f) (map g) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
"monotone_on {xs. set xs ⊆ B} (nslexordp ordb) (nslexordp orda) (map g)"
by blast
have Q: "set (map f xs) ⊆ B"
using assms(6,7) bij_betw_imp_surj_on by fastforce
have R: "set (map f ys) ⊆ B"
using assms(6,8) bij_betw_imp_surj_on by fastforce
from monotone_onD[OF P(3), simplified, OF Q R A]
show "nslexordp orda xs ys"
by (metis P(2) assms(7,8) inverses_on_def mem_Collect_eq)
qed
subsection ‹Other›
lemma nslexordp_cons1_exE:
assumes "nslexordp cmp xs (x # xs)"
shows "∃a as bs. x # xs = as @ x # a # bs ∧ cmp a x ∧ (∀b ∈ set as. b = x)"
using assms
proof (induct xs arbitrary: x)
case Nil
then show ?case
using nslexord_Nil_left nslexord_eq_nslexordp(1) by blast
next
case (Cons a xs)
note IH = this
have "cmp a x ⟹ ?case"
by fastforce
moreover
have "⟦¬cmp a x; a ≠ x⟧ ⟹ ?case"
using IH(2) by force
moreover
have "⟦¬cmp a x; a = x⟧ ⟹ ?case"
proof -
assume "¬cmp a x" "a = x"
with IH(2)
have "nslexordp cmp xs (x # xs)"
by simp
with IH(1)[OF _] ‹a = x›
have "∃k as bs. a # xs = as @ x # k # bs ∧ cmp k x ∧ (∀b∈set as. b = x)"
by simp
then obtain k as bs where P:
"a # xs = as @ x # k # bs" "cmp k x" "∀b∈set as. b = x"
by blast
then show ?case
by (metis Cons_eq_appendI set_ConsD)
qed
ultimately show ?case
by blast
qed
lemma nslexordp_cons2_exE:
assumes "nslexordp cmp (x # xs) xs"
shows "(∀k ∈ set xs. k = x) ∨ (∃a as bs. x # xs = as @ x # a # bs ∧ cmp x a ∧ (∀b ∈ set as. b = x))"
using assms
proof (induct xs arbitrary: x)
case Nil
then show ?case
by simp
next
case (Cons a xs)
note IH = this
have "cmp x a ⟹ ?case"
by (metis append_Nil empty_iff empty_set)
moreover
have "⟦¬cmp x a; a = x⟧ ⟹ ?case"
proof -
assume "¬cmp x a" "a = x"
with IH(2)
have "nslexordp cmp (x # xs) xs"
by simp
with IH(1)[of x] ‹a = x›
have "(∀k∈set xs. k = x) ∨
(∃k as bs. a # xs = as @ x # k # bs ∧ cmp x k ∧ (∀b∈set as. b = x))"
by simp
then show ?thesis
proof
assume "∀k∈set xs. k = x"
then show ?thesis
by (simp add: ‹a = x›)
next
assume "∃k as bs. a # xs = as @ x # k # bs ∧ cmp x k ∧ (∀b∈set as. b = x)"
then obtain k as bs where P:
"a # xs = as @ x # k # bs" "cmp x k" "∀b∈set as. b = x"
by blast
then show ?thesis
by (metis Cons_eq_appendI set_ConsD)
qed
qed
moreover
have "⟦¬cmp x a; a ≠ x⟧ ⟹ ?case"
using Cons.prems by auto
ultimately show ?case
by blast
qed
section ‹Order definitions on lists of linorder elements›
definition list_less_ns :: "('a :: linorder) list ⇒ 'a list ⇒ bool"
where
"list_less_ns xs ys =
(∃n. n ≤ length xs ∧ n ≤ length ys ∧
(∀i < n. xs ! i = ys ! i) ∧
(length ys = n ⟶ n < length xs) ∧
(length ys ≠ n ⟶ length xs ≠ n ∧ xs ! n < ys ! n))"
definition list_less_eq_ns :: "('a :: linorder) list ⇒ 'a list ⇒ bool"
where
"list_less_eq_ns xs ys =
(∃n. n ≤ length xs ∧ n ≤ length ys ∧
(∀i < n. xs ! i = ys ! i) ∧
(length ys ≠ n ⟶ length xs ≠ n ∧ xs ! n < ys ! n))"
definition list_less_ns_ex :: "('a :: linorder) list ⇒ ('a :: linorder) list ⇒ bool"
where
"list_less_ns_ex xs ys ⟷
(∃b c as bs cs. xs = as @ b # bs ∧ ys = as @ c # cs ∧ b < c) ∨
(∃c cs. xs = ys @ c # cs)"
section ‹Helper list comparison theorems›
lemma list_less_ns_alt_def:
"list_less_ns xs ys = list_less_ns_ex xs ys"
proof
assume "list_less_ns xs ys"
with list_less_ns_def[THEN iffD1, of xs ys]
obtain n where P:
"n ≤ length xs" "n ≤ length ys" "∀i<n. xs ! i = ys ! i" "length ys = n ⟶ n < length xs"
"length ys ≠ n ⟶ length xs ≠ n ∧ xs ! n < ys ! n"
by blast
show "list_less_ns_ex xs ys"
proof (cases "length ys = n")
assume "length ys = n"
then show ?thesis
by (metis P(1,2,3,4) id_take_nth_drop list_less_ns_ex_def nth_take_lemma take_all)
next
assume "length ys ≠ n"
then show ?thesis
by (metis P(1,2,3,5) id_take_nth_drop le_neq_implies_less list_less_ns_ex_def nth_take_lemma)
qed
next
assume "list_less_ns_ex xs ys"
hence "(∃b c as bs cs. xs = as @ b # bs ∧ ys = as @ c # cs ∧ b < c) ∨ (∃c cs. xs = ys @ c # cs)"
using list_less_ns_ex_def by blast
then show "list_less_ns xs ys"
proof
assume "∃b c as bs cs. xs = as @ b # bs ∧ ys = as @ c # cs ∧ b < c"
then obtain b c as bs cs where P:
"xs = as @ b # bs" "ys = as @ c # cs" "b < c"
by blast
hence "length as < length xs"
by simp
moreover
have "length as < length ys"
by (simp add: P(2))
moreover
have "∀i < length as. xs ! i = ys ! i"
by (simp add: P(1) P(2) nth_append)
moreover
have "xs ! length as < ys ! length as"
by (simp add: P(1) P(2) P(3))
ultimately show "list_less_ns xs ys"
using list_less_ns_def[THEN iffD2, OF exI, of "length as" xs ys] by simp
next
assume "∃c cs. xs = ys @ c # cs"
then obtain c cs where
"xs = ys @ c # cs"
by blast
hence "length ys < length xs"
by simp
then show "list_less_ns xs ys"
using list_less_ns_def[THEN iffD2, OF exI, of "length ys" xs ys]
by (simp add: ‹xs = ys @ c # cs› nth_append)
qed
qed
lemma nslexordp_eq_list_less_ns_ex:
"nslexordp (<) = list_less_ns_ex"
by (clarsimp simp: fun_eq_iff nslexordp_def list_less_ns_ex_def)
lemma nslexordp_eq_list_less_ns_ex_apply:
"nslexordp (<) x y = list_less_ns_ex x y"
by (simp add: nslexordp_eq_list_less_ns_ex)
lemma nslexordp_eq_list_less_ns:
"nslexordp (<) = list_less_ns"
by (clarsimp simp: fun_eq_iff list_less_ns_alt_def nslexordp_eq_list_less_ns_ex)
lemma nslexordp_eq_list_less_ns_app:
"nslexordp (<) x y = list_less_ns x y"
by (simp add: nslexordp_eq_list_less_ns)
lemma nslexordeqp_eq_list_less_eq_ns_apply:
"nslexordeqp (<) x y = list_less_eq_ns x y"
proof (cases "x = y")
assume "x = y"
then show ?thesis
by (simp add: list_less_eq_ns_def nslexordeqp_def)
next
assume "x ≠ y"
hence "nslexordeqp (<) x y = nslexordp (<) x y"
by (simp add: nslexordeqp_def)
moreover
have "nslexordp (<) x y = list_less_ns x y"
by (simp add: nslexordp_eq_list_less_ns)
moreover
have "list_less_eq_ns x y = list_less_ns x y"
unfolding list_less_eq_ns_def list_less_ns_def
proof (intro iffI; elim exE conjE)
fix n
assume "n ≤ length x" "n ≤ length y" "∀i<n. x ! i = y ! i"
"length y ≠ n ⟶ length x ≠ n ∧ x ! n < y ! n"
then show "∃n≤length x. n ≤ length y ∧ (∀i<n. x ! i = y ! i) ∧
(length y = n ⟶ n < length x) ∧
(length y ≠ n ⟶ length x ≠ n ∧ x ! n < y ! n)"
by (metis ‹x ≠ y› le_eq_less_or_eq nth_equalityI)
next
fix n
assume "n ≤ length x" "n ≤ length y" "∀i<n. x ! i = y ! i" "length y = n ⟶ n < length x"
"length y ≠ n ⟶ length x ≠ n ∧ x ! n < y ! n"
then show "∃n≤length x. n ≤ length y ∧ (∀i<n. x ! i = y ! i) ∧
(length y ≠ n ⟶ length x ≠ n ∧ x ! n < y ! n)"
by blast
qed
ultimately show ?thesis
by blast
qed
section ‹@{const list_less_ns} helpers›
lemma list_less_ns_cons_same:
"list_less_ns (a # xs) (a # ys) = list_less_ns xs ys"
by (metis nslexordp_cons_cons nslexordp_eq_list_less_ns order_less_irrefl)
lemma list_less_ns_cons_diff:
"a < b ⟹ list_less_ns (a # xs) (b # ys)"
using list_less_ns_def by fastforce
lemma list_less_ns_cons:
"list_less_ns (a # xs) (b # ys) = (a ≤ b ∧ (a = b ⟶ list_less_ns xs ys))"
by (metis length_Cons list_less_ns_cons_diff list_less_ns_cons_same list_less_ns_def nat.simps(3)
not_less_iff_gr_or_eq not_less_zero nth_Cons_0 order.strict_iff_order
order_class.order_eq_iff)
lemma list_less_eq_ns_cons_same:
"list_less_eq_ns (a # xs) (a # ys) = list_less_eq_ns xs ys"
by (metis list.inject list_less_ns_cons_same nslexordeqp_def nslexordeqp_eq_list_less_eq_ns_apply
nslexordp_eq_list_less_ns_app)
lemma list_less_eq_ns_cons:
"list_less_eq_ns (a # xs) (b # ys) = (a ≤ b ∧ (a = b ⟶ list_less_eq_ns xs ys))"
by (metis list.inject list_less_ns_cons nle_le nslexordeqp_def
nslexordeqp_eq_list_less_eq_ns_apply nslexordp_eq_list_less_ns)
lemma list_less_ns_hd_same:
"⟦hd xs = hd ys; xs ≠ []; ys ≠ []⟧ ⟹ list_less_ns xs ys = list_less_ns (tl xs) (tl ys)"
by (metis list.collapse list_less_ns_cons_same)
lemma list_less_ns_recurse:
"⟦xs ≠ []; ys ≠ []⟧ ⟹
(hd xs = hd ys ⟶ list_less_ns xs ys = list_less_ns (tl xs) (tl ys)) ∧
(hd xs ≠ hd ys ⟶ list_less_ns xs ys = (hd xs < hd ys))"
by (metis list.collapse list_less_ns_cons list_less_ns_hd_same nless_le)
lemma list_less_ns_nil:
"xs ≠ [] ⟹ list_less_ns xs []"
using list_less_ns_def by auto
lemma list_less_ns_app:
"bs ≠ [] ⟹ list_less_ns (as @ bs) as"
by (metis list.collapse nslexordpI2 nslexordp_eq_list_less_ns)
section ‹Lists of linorder elements are linorders with a bottom element›
lemma list_less_ns_imp_less_eq_not_less_eq:
"list_less_ns x y ⟹ (list_less_eq_ns x y ∧ ¬ list_less_eq_ns y x)"
apply (clarsimp simp: nslexordp_eq_list_less_ns[symmetric]
nslexordeqp_eq_list_less_eq_ns_apply[symmetric]
nslexordeqp_def
nslexord_eq_nslexordp(1)[symmetric])
apply (rule conjI)
apply (erule nslexord_asymmetric[rotated], fastforce)
by (metis Product_Type.Collect_case_prodD fst_conv nslexord_irreflexive order_less_irrefl
snd_conv)
lemma list_less_eq_ns_not_less_eq_imp_less:
"list_less_eq_ns x y ∧ ¬ list_less_eq_ns y x ⟹ list_less_ns x y"
by (metis nslexordeqp_eq_list_less_eq_ns_apply nslexordeqp_imp_eq_or_less
nslexordp_eq_list_less_ns)
lemma list_less_eq_ns_trans:
"⟦list_less_eq_ns x y; list_less_eq_ns y z⟧ ⟹ list_less_eq_ns x z"
apply (clarsimp simp: nslexordp_eq_list_less_ns[symmetric]
nslexordeqp_eq_list_less_eq_ns_apply[symmetric]
nslexordeqp_def
nslexord_eq_nslexordp(1)[symmetric])
apply safe
apply (erule (1) transD[OF nslexord_trans, rotated])
by (metis order_less_trans transp_def transp_trans)
lemma list_less_eq_ns_anti_sym:
"⟦list_less_eq_ns x y; list_less_eq_ns y x⟧ ⟹ x = y"
by (metis list_less_ns_imp_less_eq_not_less_eq nslexordeqp_eq_list_less_eq_ns_apply
nslexordeqp_imp_eq_or_less nslexordp_eq_list_less_ns)
lemma list_less_eq_ns_linear:
"list_less_eq_ns x y ∨ list_less_eq_ns y x"
apply (simp add: nslexordp_eq_list_less_ns[symmetric]
nslexordeqp_eq_list_less_eq_ns_apply[symmetric]
nslexordeqp_def
nslexord_eq_nslexordp(1)[symmetric])
by (metis case_prodI linorder_neqE mem_Collect_eq nslexord_linear)