theory Set_Linorder
imports
Containers_Auxiliary
Lexicographic_Order
Extend_Partial_Order
"HOL-Library.Cardinality"
begin
section {* An executable linear order on sets *}
subsection {* Definition of the linear order *}
subsubsection {* Extending finite and cofinite sets *}
text {*
Partition sets into finite and cofinite sets and distribute the rest arbitrarily such that
complement switches between the two.
*}
consts infinite_complement_partition :: "'a set set"
specification (infinite_complement_partition)
finite_complement_partition: "finite (A :: 'a set) ⟹ A ∈ infinite_complement_partition"
complement_partition: "¬ finite (UNIV :: 'a set)
⟹ (A :: 'a set) ∈ infinite_complement_partition ⟷ - A ∉ infinite_complement_partition"
proof(cases "finite (UNIV :: 'a set)")
case False
define Field_r where "Field_r = {𝒫 :: 'a set set. (∀C ∈ 𝒫. - C ∉ 𝒫) ∧ (∀A. finite A ⟶ A ∈ 𝒫)}"
define r where "r = {(𝒫1, 𝒫2). 𝒫1 ⊆ 𝒫2 ∧ 𝒫1 ∈ Field_r ∧ 𝒫2 ∈ Field_r}"
have in_Field_r [simp]: "⋀𝒫. 𝒫 ∈ Field_r ⟷ (∀C ∈ 𝒫. - C ∉ 𝒫) ∧ (∀A. finite A ⟶ A ∈ 𝒫)"
unfolding Field_r_def by simp
have in_r [simp]: "⋀𝒫1 𝒫2. (𝒫1, 𝒫2) ∈ r ⟷ 𝒫1 ⊆ 𝒫2 ∧ 𝒫1 ∈ Field_r ∧ 𝒫2 ∈ Field_r"
unfolding r_def by simp
have Field_r [simp]: "Field r = Field_r" by(auto simp add: Field_def Field_r_def)
have "Partial_order r"
by(auto simp add: Field_def r_def partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI)
moreover have "∀ℭ ∈ Chains r. ∃ℬ ∈ Field r. ∀𝒜 ∈ ℭ. (𝒜, ℬ) ∈ r"
proof
fix ℭ
assume ℭ: "ℭ ∈ Chains r"
let ?ℬ = "⋃ℭ ∪ {A. finite A}"
have *: "?ℬ ∈ Field r" using False ℭ
by clarsimp(safe, drule (2) ChainsD, auto 4 4 dest: Chains_Field)
hence "⋀𝒜. 𝒜 ∈ ℭ ⟹ (𝒜, ?ℬ) ∈ r"
using ℭ by(auto simp del: in_Field_r dest: Chains_Field)
with * show "∃ℬ ∈ Field r. ∀𝒜 ∈ ℭ. (𝒜, ℬ) ∈ r" by blast
qed
ultimately have "∃𝒫 ∈ Field r. ∀𝒜 ∈ Field r. (𝒫, 𝒜) ∈ r ⟶ 𝒜 = 𝒫"
by(rule Zorns_po_lemma)
then obtain 𝒫 where 𝒫: "𝒫 ∈ Field r"
and max: "⋀𝒜. ⟦ 𝒜 ∈ Field r; (𝒫, 𝒜) ∈ r ⟧ ⟹ 𝒜 = 𝒫" by blast
have "∀A. finite A ⟶ A ∈ 𝒫" using 𝒫 by simp
moreover {
fix C
have "C ∈ 𝒫 ∨ - C ∈ 𝒫"
proof(rule ccontr)
assume "¬ ?thesis"
hence C: "C ∉ 𝒫" "- C ∉ 𝒫" by simp_all
let ?𝒜 = "insert C 𝒫"
have *: "?𝒜 ∈ Field r" using C 𝒫 by auto
hence "(𝒫, ?𝒜) ∈ r" using 𝒫 by auto
with * have "?𝒜 = 𝒫" by(rule max)
thus False using C by auto
qed
hence "C ∈ 𝒫 ⟷ - C ∉ 𝒫" using 𝒫 by auto }
ultimately have "∃𝒫 :: 'a set set. (∀A. finite A ⟶ A ∈ 𝒫) ∧ (∀C. C ∈ 𝒫 ⟷ - C ∉ 𝒫)"
by blast
thus ?thesis by metis
qed auto
lemma not_in_complement_partition:
"¬ finite (UNIV :: 'a set)
⟹ (A :: 'a set) ∉ infinite_complement_partition ⟷ - A ∈ infinite_complement_partition"
by(metis complement_partition)
lemma not_in_complement_partition_False:
"⟦ (A :: 'a set) ∈ infinite_complement_partition; ¬ finite (UNIV :: 'a set) ⟧
⟹ - A ∈ infinite_complement_partition = False"
by(simp add: not_in_complement_partition)
lemma infinite_complement_partition_finite [simp]:
"finite (UNIV :: 'a set) ⟹ infinite_complement_partition = (UNIV :: 'a set set)"
by(auto intro: finite_subset finite_complement_partition)
lemma Compl_eq_empty_iff: "- A = {} ⟷ A = UNIV"
by auto
subsubsection {* A lexicographic-style order on finite subsets *}
context ord begin
definition set_less_aux :: "'a set ⇒ 'a set ⇒ bool" (infix "⊏''" 50)
where "A ⊏' B ⟷ finite A ∧ finite B ∧ (∃y ∈ B - A. ∀z ∈ (A - B) ∪ (B - A). y ≤ z ∧ (z ≤ y ⟶ y = z))"
definition set_less_eq_aux :: "'a set ⇒ 'a set ⇒ bool" (infix "⊑''" 50)
where "A ⊑' B ⟷ A ∈ infinite_complement_partition ∧ A = B ∨ A ⊏' B"
lemma set_less_aux_irrefl [iff]: "¬ A ⊏' A"
by(auto simp add: set_less_aux_def)
lemma set_less_eq_aux_refl [iff]: "A ⊑' A ⟷ A ∈ infinite_complement_partition"
by(simp add: set_less_eq_aux_def)
lemma set_less_aux_empty [simp]: "¬ A ⊏' {}"
by(auto simp add: set_less_aux_def intro: finite_subset finite_complement_partition)
lemma set_less_eq_aux_empty [simp]: "A ⊑' {} ⟷ A = {}"
by(auto simp add: set_less_eq_aux_def finite_complement_partition)
lemma set_less_aux_antisym: "⟦ A ⊏' B; B ⊏' A ⟧ ⟹ False"
by(auto simp add: set_less_aux_def split: if_split_asm)
lemma set_less_aux_conv_set_less_eq_aux:
"A ⊏' B ⟷ A ⊑' B ∧ ¬ B ⊑' A"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym)
lemma set_less_eq_aux_antisym: "⟦ A ⊑' B; B ⊑' A ⟧ ⟹ A = B"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym)
lemma set_less_aux_finiteD: "A ⊏' B ⟹ finite A ∧ B ∈ infinite_complement_partition"
by(auto simp add: set_less_aux_def finite_complement_partition)
lemma set_less_eq_aux_infinite_complement_partitionD:
"A ⊑' B ⟹ A ∈ infinite_complement_partition ∧ B ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_finiteD intro: finite_complement_partition)
lemma Compl_set_less_aux_Compl:
"finite (UNIV :: 'a set) ⟹ - A ⊏' - B ⟷ B ⊏' A"
by(auto simp add: set_less_aux_def finite_subset[OF subset_UNIV])
lemma Compl_set_less_eq_aux_Compl:
"finite (UNIV :: 'a set) ⟹ - A ⊑' - B ⟷ B ⊑' A"
by(auto simp add: set_less_eq_aux_def Compl_set_less_aux_Compl)
lemma set_less_aux_insert_same:
"x ∈ A ⟷ x ∈ B ⟹ insert x A ⊏' insert x B ⟷ A ⊏' B"
by(auto simp add: set_less_aux_def)
lemma set_less_eq_aux_insert_same:
"⟦ A ∈ infinite_complement_partition; insert x B ∈ infinite_complement_partition;
x ∈ A ⟷ x ∈ B ⟧
⟹ insert x A ⊑' insert x B ⟷ A ⊑' B"
by(auto simp add: set_less_eq_aux_def set_less_aux_insert_same)
end
context order begin
lemma set_less_aux_singleton_iff: "A ⊏' {x} ⟷ finite A ∧ (∀a∈A. x < a)"
by(auto simp add: set_less_aux_def less_le Bex_def)
end
context linorder begin
lemma wlog_le [case_names sym le]:
assumes "⋀a b. P a b ⟹ P b a"
and "⋀a b. a ≤ b ⟹ P a b"
shows "P b a"
by (metis assms linear)
lemma empty_set_less_aux [simp]: "{} ⊏' A ⟷ A ≠ {} ∧ finite A"
by(auto 4 3 simp add: set_less_aux_def intro!: Min_eqI intro: bexI[where x="Min A"] order_trans[where y="Min A"] Min_in)
lemma empty_set_less_eq_aux [simp]: "{} ⊑' A ⟷ finite A"
by(auto simp add: set_less_eq_aux_def finite_complement_partition)
lemma set_less_aux_trans:
assumes AB: "A ⊏' B" and BC: "B ⊏' C"
shows "A ⊏' C"
proof -
from AB BC have A: "finite A" and B: "finite B" and C: "finite C"
by(auto simp add: set_less_aux_def)
from AB A B obtain ab where ab: "ab ∈ B - A"
and minAB: "⋀x. ⟦ x ∈ A; x ∉ B ⟧ ⟹ ab ≤ x ∧ (x ≤ ab ⟶ ab = x)"
and minBA: "⋀x. ⟦ x ∈ B; x ∉ A ⟧ ⟹ ab ≤ x ∧ (x ≤ ab ⟶ ab = x)"
unfolding set_less_aux_def by auto
from BC B C obtain bc where bc: "bc ∈ C - B"
and minBC: "⋀x. ⟦ x ∈ B; x ∉ C ⟧ ⟹ bc ≤ x ∧ (x ≤ bc ⟶ bc = x)"
and minCB: "⋀x. ⟦ x ∈ C; x ∉ B ⟧ ⟹ bc ≤ x ∧ (x ≤ bc ⟶ bc = x)"
unfolding set_less_aux_def by auto
show ?thesis
proof(cases "ab ≤ bc")
case True
hence "ab ∈ C - A" "ab ∉ A - C"
using ab bc by(auto dest: minBC antisym)
moreover {
fix x
assume x: "x ∈ (C - A) ∪ (A - C)"
hence "ab ≤ x"
by(cases "x ∈ B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF True])
moreover hence "ab ≠ x ⟶ ¬ x ≤ ab" using ab bc x
by(cases "x ∈ B")(auto dest: antisym)
moreover note calculation }
ultimately show ?thesis using A C unfolding set_less_aux_def by auto
next
case False
with linear[of ab bc] have "bc ≤ ab" by simp
with ab bc have "bc ∈ C - A" "bc ∉ A - C" by(auto dest: minAB antisym)
moreover {
fix x
assume x: "x ∈ (C - A) ∪ (A - C)"
hence "bc ≤ x"
by(cases "x ∈ B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF `bc ≤ ab`])
moreover hence "bc ≠ x ⟶ ¬ x ≤ bc" using ab bc x
by(cases "x ∈ B")(auto dest: antisym)
moreover note calculation }
ultimately show ?thesis using A C unfolding set_less_aux_def by auto
qed
qed
lemma set_less_eq_aux_trans [trans]:
"⟦ A ⊑' B; B ⊑' C ⟧ ⟹ A ⊑' C"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans)
lemma set_less_trans_set_less_eq [trans]:
"⟦ A ⊏' B; B ⊑' C ⟧ ⟹ A ⊏' C"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans)
lemma set_less_eq_aux_porder: "partial_order_on infinite_complement_partition {(A, B). A ⊑' B}"
by(auto simp add: preorder_on_def partial_order_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux_infinite_complement_partitionD intro: set_less_eq_aux_antisym set_less_eq_aux_trans del: equalityI)
lemma psubset_finite_imp_set_less_aux:
assumes AsB: "A ⊂ B" and B: "finite B"
shows "A ⊏' B"
proof -
from AsB B have A: "finite A" by(auto intro: finite_subset)
moreover from AsB B have "Min (B - A) ∈ B - A" by - (rule Min_in, auto)
ultimately show ?thesis using B AsB
by(auto simp add: set_less_aux_def intro!: rev_bexI[where x="Min (B - A)"] Min_eqI dest: Min_ge_iff[THEN iffD1, rotated 2])
qed
lemma subset_finite_imp_set_less_eq_aux:
"⟦ A ⊆ B; finite B ⟧ ⟹ A ⊑' B"
by(cases "A = B")(auto simp add: set_less_eq_aux_def finite_complement_partition intro: psubset_finite_imp_set_less_aux)
lemma empty_set_less_aux_finite_iff:
"finite A ⟹ {} ⊏' A ⟷ A ≠ {}"
by(auto intro: psubset_finite_imp_set_less_aux)
lemma set_less_aux_finite_total:
assumes A: "finite A" and B: "finite B"
shows "A ⊏' B ∨ A = B ∨ B ⊏' A"
proof(cases "A ⊆ B ∨ B ⊆ A")
case True thus ?thesis
using A B psubset_finite_imp_set_less_aux[of A B] psubset_finite_imp_set_less_aux[of B A]
by auto
next
case False
hence A': "¬ A ⊆ B" and B': "¬ B ⊆ A" and AnB: "A ≠ B" by auto
thus ?thesis using A B
proof(induct "Min (B - A)" "Min (A - B)" arbitrary: A B rule: wlog_le)
case (sym m n)
from sym.hyps[OF refl refl] sym.prems show ?case by blast
next
case (le A B)
note A = `finite A` and B = `finite B`
and A' = `¬ A ⊆ B` and B' = `¬ B ⊆ A`
{ fix z
assume z: "z ∈ (A - B) ∪ (B - A)"
hence "Min (B - A) ≤ z ∧ (z ≤ Min (B - A) ⟶ Min (B - A) = z)"
proof
assume "z ∈ B - A"
hence "Min (B - A) ≤ z" by(simp add: B)
thus ?thesis by auto
next
assume "z ∈ A - B"
hence "Min (A - B) ≤ z" by(simp add: A)
with le.hyps show ?thesis by(auto)
qed }
moreover have "Min (B - A) ∈ B - A" by(rule Min_in)(simp_all add: B B')
ultimately have "A ⊏' B" using A B by(auto simp add: set_less_aux_def)
thus ?case ..
qed
qed
lemma set_less_eq_aux_finite_total:
"⟦ finite A; finite B ⟧ ⟹ A ⊑' B ∨ A = B ∨ B ⊑' A"
by(drule (1) set_less_aux_finite_total)(auto simp add: set_less_eq_aux_def)
lemma set_less_eq_aux_finite_total2:
"⟦ finite A; finite B ⟧ ⟹ A ⊑' B ∨ B ⊑' A"
by(drule (1) set_less_eq_aux_finite_total)(auto simp add: finite_complement_partition)
lemma set_less_aux_rec:
assumes A: "finite A" and B: "finite B"
and A': "A ≠ {}" and B': "B ≠ {}"
shows "A ⊏' B ⟷ Min B < Min A ∨ Min A = Min B ∧ A - {Min A} ⊏' B - {Min A}"
proof(cases "Min A = Min B")
case True
from A A' B B' have "insert (Min A) A = A" "insert (Min B) B = B"
by(auto simp add: ex_in_conv[symmetric] exI)
with True show ?thesis
by(subst (2) set_less_aux_insert_same[symmetric, where x="Min A"]) simp_all
next
case False
have "A ⊏' B ⟷ Min B < Min A"
proof
assume AB: "A ⊏' B"
with B A obtain ab where ab: "ab ∈ B - A"
and AB: "⋀x. ⟦ x ∈ A; x ∉ B ⟧ ⟹ ab ≤ x"
by(auto simp add: set_less_aux_def)
{ fix a assume "a ∈ A"
hence "Min B ≤ a" using A A' B B' ab
by(cases "a ∈ B")(auto intro: order_trans[where y=ab] dest: AB) }
hence "Min B ≤ Min A" using A A' by simp
with False show "Min B < Min A" using False by auto
next
assume "Min B < Min A"
hence "∀z∈A - B ∪ (B - A). Min B ≤ z ∧ (z ≤ Min B ⟶ Min B = z)"
using A B A' B' by(auto 4 4 intro: Min_in Min_eqI dest: bspec bspec[where x="Min B"])
moreover have "Min B ∉ A" using `Min B < Min A` by (metis A Min_le not_less)
ultimately show "A ⊏' B" using A B A' B' by(simp add: set_less_aux_def bexI[where x="Min B"])
qed
thus ?thesis using False by simp
qed
lemma set_less_eq_aux_rec:
assumes "finite A" "finite B" "A ≠ {}" "B ≠ {}"
shows "A ⊑' B ⟷ Min B < Min A ∨ Min A = Min B ∧ A - {Min A} ⊑' B - {Min A}"
proof(cases "A = B")
case True thus ?thesis using assms by(simp add: finite_complement_partition)
next
case False
moreover
hence "Min A = Min B ⟹ A - {Min A} ≠ B - {Min B}"
by (metis (lifting) assms Min_in insert_Diff)
ultimately show ?thesis using set_less_aux_rec[OF assms]
by(simp add: set_less_eq_aux_def cong: conj_cong)
qed
lemma set_less_aux_Min_antimono:
"⟦ Min A < Min B; finite A; finite B; A ≠ {} ⟧ ⟹ B ⊏' A"
using set_less_aux_rec[of B A]
by(cases "B = {}")(simp_all add: empty_set_less_aux_finite_iff)
lemma sorted_Cons_Min: "sorted (x # xs) ⟹ Min (insert x (set xs)) = x"
by(auto simp add: intro: Min_eqI)
lemma set_less_aux_code:
"⟦ sorted xs; distinct xs; sorted ys; distinct ys ⟧
⟹ set xs ⊏' set ys ⟷ ord.lexordp (>) xs ys"
apply(induct xs ys rule: splice.induct)
apply(simp_all add: empty_set_less_aux_finite_iff sorted_Cons_Min set_less_aux_rec neq_Nil_conv)
apply(auto simp add: cong: conj_cong)
done
lemma set_less_eq_aux_code:
assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys"
shows "set xs ⊑' set ys ⟷ ord.lexordp_eq (>) xs ys"
proof -
have dual: "class.linorder (≥) (>)"
by(rule linorder.dual_linorder) unfold_locales
from assms show ?thesis
by(auto simp add: set_less_eq_aux_def finite_complement_partition linorder.lexordp_eq_conv_lexord[OF dual] set_less_aux_code intro: sorted_distinct_set_unique)
qed
end
subsubsection {* Extending @{term set_less_eq_aux} to have @{term "{}"} as least element *}
context ord begin
definition set_less_eq_aux' :: "'a set ⇒ 'a set ⇒ bool" (infix "⊑''''" 50)
where "A ⊑'' B ⟷ A ⊑' B ∨ A = {} ∧ B ∈ infinite_complement_partition"
lemma set_less_eq_aux'_refl:
"A ⊑'' A ⟷ A ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux'_def)
lemma set_less_eq_aux'_antisym: "⟦ A ⊑'' B; B ⊑'' A ⟧ ⟹ A = B"
by(auto simp add: set_less_eq_aux'_def intro: set_less_eq_aux_antisym del: equalityI)
lemma set_less_eq_aux'_infinite_complement_partitionD:
"A ⊑'' B ⟹ A ∈ infinite_complement_partition ∧ B ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux'_def intro: finite_complement_partition dest: set_less_eq_aux_infinite_complement_partitionD)
lemma empty_set_less_eq_def [simp]: "{} ⊑'' B ⟷ B ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux'_def dest: set_less_eq_aux_infinite_complement_partitionD)
end
context linorder begin
lemma set_less_eq_aux'_trans: "⟦ A ⊑'' B; B ⊑'' C ⟧ ⟹ A ⊑'' C"
by(auto simp add: set_less_eq_aux'_def del: equalityI intro: set_less_eq_aux_trans dest: set_less_eq_aux_infinite_complement_partitionD)
lemma set_less_eq_aux'_porder: "partial_order_on infinite_complement_partition {(A, B). A ⊑'' B}"
by(auto simp add: partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux'_antisym set_less_eq_aux'_infinite_complement_partitionD simp add: set_less_eq_aux'_refl intro: set_less_eq_aux'_trans)
end
subsubsection {* Extend @{term set_less_eq_aux'} to a total order on @{term infinite_complement_partition} *}
context ord begin
definition set_less_eq_aux'' :: "'a set ⇒ 'a set ⇒ bool" (infix "⊑''''''" 50)
where "set_less_eq_aux'' =
(SOME sleq.
(linear_order_on UNIV {(a, b). a ≤ b} ⟶ linear_order_on infinite_complement_partition {(A, B). sleq A B}) ∧ order_consistent {(A, B). A ⊑'' B} {(A, B). sleq A B})"
lemma set_less_eq_aux''_spec:
shows "linear_order {(a, b). a ≤ b} ⟹ linear_order_on infinite_complement_partition {(A, B). A ⊑''' B}"
(is "PROP ?thesis1")
and "order_consistent {(A, B). A ⊑'' B} {(A, B). A ⊑''' B}" (is ?thesis2)
proof -
let ?P = "λsleq. (linear_order {(a, b). a ≤ b} ⟶ linear_order_on infinite_complement_partition {(A, B). sleq A B}) ∧
order_consistent {(A, B). A ⊑'' B} {(A, B). sleq A B}"
have "Ex ?P"
proof(cases "linear_order {(a, b). a ≤ b}")
case False
have "antisym {(a, b). a ⊑'' b}"
by (rule antisymI) (simp add: set_less_eq_aux'_antisym)
then show ?thesis using False
by (auto intro: antisym_order_consistent_self)
next
case True
hence "partial_order_on infinite_complement_partition {(A, B). A ⊑'' B}"
by(rule linorder.set_less_eq_aux'_porder[OF linear_order_imp_linorder])
then obtain s where "linear_order_on infinite_complement_partition s"
and "order_consistent {(A, B). A ⊑'' B} s" by(rule porder_extend_to_linorder)
thus ?thesis by(auto intro: exI[where x="λA B. (A, B) ∈ s"])
qed
hence "?P (Eps ?P)" by(rule someI_ex)
thus "PROP ?thesis1" ?thesis2 by(simp_all add: set_less_eq_aux''_def)
qed
end
context linorder begin
lemma set_less_eq_aux''_linear_order:
"linear_order_on infinite_complement_partition {(A, B). A ⊑''' B}"
by(rule set_less_eq_aux''_spec)(rule linear_order)
lemma set_less_eq_aux''_refl [iff]: "A ⊑''' A ⟷ A ∈ infinite_complement_partition"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD refl_onD1)
lemma set_less_eq_aux'_into_set_less_eq_aux'':
assumes "A ⊑'' B"
shows "A ⊑''' B"
proof(rule ccontr)
assume nleq: "¬ ?thesis"
moreover from assms have A: "A ∈ infinite_complement_partition"
and B: "B ∈ infinite_complement_partition"
by(auto dest: set_less_eq_aux'_infinite_complement_partitionD)
with set_less_eq_aux''_linear_order have "A ⊑''' B ∨ A = B ∨ B ⊑''' A"
by(auto simp add: linear_order_on_def dest: total_onD)
ultimately have "B ⊑''' A" using B by auto
with assms have "A = B" using set_less_eq_aux''_spec(2)
by(simp add: order_consistent_def)
with A nleq show False by simp
qed
lemma finite_set_less_eq_aux''_finite:
assumes "finite A" and "finite B"
shows "A ⊑''' B ⟷ A ⊑'' B"
proof
assume "A ⊑''' B"
from assms have "A ⊑' B ∨ B ⊑' A" by(rule set_less_eq_aux_finite_total2)
hence "A ⊑'' B ∨ B ⊑'' A" by(auto simp add: set_less_eq_aux'_def)
thus "A ⊑'' B"
proof
assume "B ⊑'' A"
hence "B ⊑''' A" by(rule set_less_eq_aux'_into_set_less_eq_aux'')
with `A ⊑''' B` set_less_eq_aux''_linear_order have "A = B"
by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD)
thus ?thesis using assms by(simp add: finite_complement_partition set_less_eq_aux'_def)
qed
qed(rule set_less_eq_aux'_into_set_less_eq_aux'')
lemma set_less_eq_aux''_finite:
"finite (UNIV :: 'a set) ⟹ set_less_eq_aux'' = set_less_eq_aux"
by(auto simp add: fun_eq_iff finite_set_less_eq_aux''_finite set_less_eq_aux'_def finite_subset[OF subset_UNIV])
lemma set_less_eq_aux''_antisym:
"⟦ A ⊑''' B; B ⊑''' A;
A ∈ infinite_complement_partition; B ∈ infinite_complement_partition ⟧
⟹ A = B"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD del: equalityI)
lemma set_less_eq_aux''_trans: "⟦ A ⊑''' B; B ⊑''' C ⟧ ⟹ A ⊑''' C"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: transD)
lemma set_less_eq_aux''_total:
"⟦ A ∈ infinite_complement_partition; B ∈ infinite_complement_partition ⟧
⟹ A ⊑''' B ∨ B ⊑''' A"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def dest: total_onD)
end
subsubsection {* Extend @{term set_less_eq_aux''} to cofinite sets *}
context ord begin
definition set_less_eq :: "'a set ⇒ 'a set ⇒ bool" (infix "⊑" 50)
where
"A ⊑ B ⟷
(if A ∈ infinite_complement_partition then A ⊑''' B ∨ B ∉ infinite_complement_partition
else B ∉ infinite_complement_partition ∧ - B ⊑''' - A)"
definition set_less :: "'a set ⇒ 'a set ⇒ bool" (infix "⊏" 50)
where "A ⊏ B ⟷ A ⊑ B ∧ ¬ B ⊑ A"
lemma set_less_eq_def2:
"A ⊑ B ⟷
(if finite (UNIV :: 'a set) then A ⊑''' B
else if A ∈ infinite_complement_partition then A ⊑''' B ∨ B ∉ infinite_complement_partition
else B ∉ infinite_complement_partition ∧ - B ⊑''' - A)"
by(simp add: set_less_eq_def)
end
context linorder begin
lemma set_less_eq_refl [iff]: "A ⊑ A"
by(auto simp add: set_less_eq_def2 not_in_complement_partition)
lemma set_less_eq_antisym: "⟦ A ⊑ B; B ⊑ A ⟧ ⟹ A = B"
by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False del: equalityI split: if_split_asm dest: set_less_eq_aux_antisym set_less_eq_aux''_antisym)
lemma set_less_eq_trans: "⟦ A ⊑ B; B ⊑ C ⟧ ⟹ A ⊑ C"
by(auto simp add: set_less_eq_def split: if_split_asm intro: set_less_eq_aux''_trans)
lemma set_less_eq_total: "A ⊑ B ∨ B ⊑ A"
by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False intro: set_less_eq_aux_finite_total2 finite_subset[OF subset_UNIV] del: disjCI dest: set_less_eq_aux''_total)
lemma set_less_eq_linorder: "class.linorder (⊑) (⊏)"
by(unfold_locales)(auto simp add: set_less_def set_less_eq_antisym set_less_eq_total intro: set_less_eq_trans)
lemma set_less_eq_conv_set_less: "set_less_eq A B ⟷ A = B ∨ set_less A B"
by(auto simp add: set_less_def del: equalityI dest: set_less_eq_antisym)
lemma Compl_set_less_eq_Compl: "- A ⊑ - B ⟷ B ⊑ A"
by(auto simp add: set_less_eq_def2 not_in_complement_partition_False not_in_complement_partition set_less_eq_aux''_finite Compl_set_less_eq_aux_Compl)
lemma Compl_set_less_Compl: "- A ⊏ - B ⟷ B ⊏ A"
by(simp add: set_less_def Compl_set_less_eq_Compl)
lemma set_less_eq_finite_iff: "⟦ finite A; finite B ⟧ ⟹ A ⊑ B ⟷ A ⊑' B"
by(auto simp add: set_less_eq_def finite_complement_partition set_less_eq_aux'_def finite_set_less_eq_aux''_finite)
lemma set_less_finite_iff: "⟦ finite A; finite B ⟧ ⟹ A ⊏ B ⟷ A ⊏' B"
by(simp add: set_less_def set_less_aux_conv_set_less_eq_aux set_less_eq_finite_iff)
lemma infinite_set_less_eq_Complement:
"⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ A ⊑ - B"
by(simp add: set_less_eq_def finite_complement_partition not_in_complement_partition)
lemma infinite_set_less_Complement:
"⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ A ⊏ - B"
by(auto simp add: set_less_def dest: set_less_eq_antisym intro: infinite_set_less_eq_Complement)
lemma infinite_Complement_set_less_eq:
"⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ ¬ - A ⊑ B"
using infinite_set_less_eq_Complement[of A B] Compl_set_less_eq_Compl[of A "- B"]
by(auto dest: set_less_eq_antisym)
lemma infinite_Complement_set_less:
"⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ ¬ - A ⊏ B"
using infinite_Complement_set_less_eq[of A B]
by(simp add: set_less_def)
lemma empty_set_less_eq [iff]: "{} ⊑ A"
by(auto simp add: set_less_eq_def finite_complement_partition intro: set_less_eq_aux'_into_set_less_eq_aux'')
lemma set_less_eq_empty [iff]: "A ⊑ {} ⟷ A = {}"
by (metis empty_set_less_eq set_less_eq_antisym)
lemma empty_set_less_iff [iff]: "{} ⊏ A ⟷ A ≠ {}"
by(simp add: set_less_def)
lemma not_set_less_empty [simp]: "¬ A ⊏ {}"
by(simp add: set_less_def)
lemma set_less_eq_UNIV [iff]: "A ⊑ UNIV"
using Compl_set_less_eq_Compl[of "- A" "{}"] by simp
lemma UNIV_set_less_eq [iff]: "UNIV ⊑ A ⟷ A = UNIV"
using Compl_set_less_eq_Compl[of "{}" "- A"]
by(simp add: Compl_eq_empty_iff)
lemma set_less_UNIV_iff [iff]: "A ⊏ UNIV ⟷ A ≠ UNIV"
by(simp add: set_less_def)
lemma not_UNIV_set_less [simp]: "¬ UNIV ⊏ A"
by(simp add: set_less_def)
end
subsection {* Implementation based on sorted lists *}
type_synonym 'a proper_interval = "'a option ⇒ 'a option ⇒ bool"
class proper_intrvl = ord +
fixes proper_interval :: "'a proper_interval"
class proper_interval = proper_intrvl +
assumes proper_interval_simps:
"proper_interval None None = True"
"proper_interval None (Some y) = (∃z. z < y)"
"proper_interval (Some x) None = (∃z. x < z)"
"proper_interval (Some x) (Some y) = (∃z. x < z ∧ z < y)"
context proper_intrvl begin
function set_less_eq_aux_Compl :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"set_less_eq_aux_Compl ao [] ys ⟷ True"
| "set_less_eq_aux_Compl ao xs [] ⟷ True"
| "set_less_eq_aux_Compl ao (x # xs) (y # ys) ⟷
(if x < y then proper_interval ao (Some x) ∨ set_less_eq_aux_Compl (Some x) xs (y # ys)
else if y < x then proper_interval ao (Some y) ∨ set_less_eq_aux_Compl (Some y) (x # xs) ys
else proper_interval ao (Some y))"
by(pat_completeness) simp_all
termination by(lexicographic_order)
fun Compl_set_less_eq_aux :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"Compl_set_less_eq_aux ao [] [] ⟷ ¬ proper_interval ao None"
| "Compl_set_less_eq_aux ao [] (y # ys) ⟷ ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux (Some y) [] ys"
| "Compl_set_less_eq_aux ao (x # xs) [] ⟷ ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux (Some x) xs []"
| "Compl_set_less_eq_aux ao (x # xs) (y # ys) ⟷
(if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux (Some x) xs (y # ys)
else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux (Some y) (x # xs) ys
else ¬ proper_interval ao (Some y))"
fun set_less_aux_Compl :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool" where
"set_less_aux_Compl ao [] [] ⟷ proper_interval ao None"
| "set_less_aux_Compl ao [] (y # ys) ⟷ proper_interval ao (Some y) ∨ set_less_aux_Compl (Some y) [] ys"
| "set_less_aux_Compl ao (x # xs) [] ⟷ proper_interval ao (Some x) ∨ set_less_aux_Compl (Some x) xs []"
| "set_less_aux_Compl ao (x # xs) (y # ys) ⟷
(if x < y then proper_interval ao (Some x) ∨ set_less_aux_Compl (Some x) xs (y # ys)
else if y < x then proper_interval ao (Some y) ∨ set_less_aux_Compl (Some y) (x # xs) ys
else proper_interval ao (Some y))"
function Compl_set_less_aux :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool" where
"Compl_set_less_aux ao [] ys ⟷ False"
| "Compl_set_less_aux ao xs [] ⟷ False"
| "Compl_set_less_aux ao (x # xs) (y # ys) ⟷
(if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_aux (Some x) xs (y # ys)
else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_aux (Some y) (x # xs) ys
else ¬ proper_interval ao (Some y))"
by pat_completeness simp_all
termination by lexicographic_order
end
lemmas [code] =
proper_intrvl.set_less_eq_aux_Compl.simps
proper_intrvl.set_less_aux_Compl.simps
proper_intrvl.Compl_set_less_eq_aux.simps
proper_intrvl.Compl_set_less_aux.simps
class linorder_proper_interval = linorder + proper_interval
begin
theorem assumes fin: "finite (UNIV :: 'a set)"
and xs: "sorted xs" "distinct xs"
and ys: "sorted ys" "distinct ys"
shows set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl:
"set xs ⊑' - set ys ⟷ set_less_eq_aux_Compl None xs ys" (is ?Compl2)
and Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux:
"- set xs ⊑' set ys ⟷ Compl_set_less_eq_aux None xs ys" (is ?Compl1)
proof -
note fin' [simp] = finite_subset[OF subset_UNIV fin]
define above where "above = case_option UNIV (Collect ∘ less)"
have above_simps [simp]: "above None = UNIV" "⋀x. above (Some x) = {y. x < y}"
and above_upclosed: "⋀x y ao. ⟦ x ∈ above ao; x < y ⟧ ⟹ y ∈ above ao"
and proper_interval_Some2: "⋀x ao. proper_interval ao (Some x) ⟷ (∃z∈above ao. z < x)"
and proper_interval_None2: "⋀ao. proper_interval ao None ⟷ above ao ≠ {}"
by(simp_all add: proper_interval_simps above_def split: option.splits)
{ fix ao x A B
assume ex: "proper_interval ao (Some x)"
and A: "∀a ∈ A. x ≤ a"
and B: "∀b ∈ B. x ≤ b"
from ex obtain z where z_ao: "z ∈ above ao" and z: "z < x"
by(auto simp add: proper_interval_Some2)
with A have A_eq: "A ∩ above ao = A"
by(auto simp add: above_upclosed)
from z_ao z B have B_eq: "B ∩ above ao = B"
by(auto simp add: above_upclosed)
define w where "w = Min (above ao)"
with z_ao have "w ≤ z" "∀z ∈ above ao. w ≤ z" "w ∈ above ao"
by(auto simp add: Min_le_iff intro: Min_in)
hence "A ∩ above ao ⊏' (- B) ∩ above ao" (is "?lhs ⊏' ?rhs")
using A B z by(auto simp add: set_less_aux_def intro!: bexI[where x="w"])
hence "A ⊑' ?rhs" unfolding A_eq by(simp add: set_less_eq_aux_def)
moreover
from z_ao z A B have "z ∈ - A ∩ above ao" "z ∉ B" by auto
hence neq: "- A ∩ above ao ≠ B ∩ above ao" by auto
have "¬ - A ∩ above ao ⊏' B ∩ above ao" (is "¬ ?lhs' ⊏' ?rhs'")
using A B z z_ao by(force simp add: set_less_aux_def not_less dest: bspec[where x=z])
with neq have "¬ ?lhs' ⊑' B" unfolding B_eq by(auto simp add: set_less_eq_aux_def)
moreover note calculation }
note proper_interval_set_less_eqI = this(1)
and proper_interval_not_set_less_eq_auxI = this(2)
{ fix ao
assume "set xs ∪ set ys ⊆ above ao"
with xs ys
have "set_less_eq_aux_Compl ao xs ys ⟷ set xs ⊑' (- set ys) ∩ above ao"
proof(induction ao xs ys rule: set_less_eq_aux_Compl.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by(auto intro: subset_finite_imp_set_less_eq_aux)
next
case (3 ao x xs y ys)
note ao = `set (x # xs) ∪ set (y # ys) ⊆ above ao`
hence x_ao: "x ∈ above ao" and y_ao: "y ∈ above ao" by simp_all
note yys = `sorted (y # ys)` `distinct (y # ys)`
hence ys: "sorted ys" "distinct ys" and y_Min: "∀y' ∈ set ys. y < y'"
by(auto simp add: less_le)
note xxs = `sorted (x # xs)` `distinct (x # xs)`
hence xs: "sorted xs" "distinct xs" and x_Min: "∀x' ∈ set xs. x < x'"
by(auto simp add: less_le)
let ?lhs = "set (x # xs)" and ?rhs = "- set (y # ys) ∩ above ao"
show ?case
proof(cases "x < y")
case True
show ?thesis
proof(cases "proper_interval ao (Some x)")
case True
hence "?lhs ⊑' ?rhs" using x_Min y_Min `x < y`
by(auto intro!: proper_interval_set_less_eqI)
with True show ?thesis using `x < y` by simp
next
case False
have "set xs ∪ set (y # ys) ⊆ above (Some x)" using True x_Min y_Min by auto
with True xs yys
have IH: "set_less_eq_aux_Compl (Some x) xs (y # ys) =
(set xs ⊑' - set (y # ys) ∩ above (Some x))"
by(rule "3.IH")
from True y_Min x_ao have "x ∈ - set (y # ys) ∩ above ao" by auto
hence "?rhs ≠ {}" by blast
moreover have "Min ?lhs = x" using x_Min x_ao by(auto intro!: Min_eqI)
moreover have "Min ?rhs = x" using `x < y` y_Min x_ao False
by(auto intro!: Min_eqI simp add: proper_interval_Some2)
moreover have "set xs = set xs - {x}"
using ao x_Min by auto
moreover have "- set (y # ys) ∩ above (Some x) = - set (y # ys) ∩ above ao - {x}"
using False x_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed)
ultimately show ?thesis using True False IH
by(simp del: set_simps)(subst (2) set_less_eq_aux_rec, simp_all add: x_ao)
qed
next
case False
show ?thesis
proof(cases "y < x")
case True
show ?thesis
proof(cases "proper_interval ao (Some y)")
case True
hence "?lhs ⊑' ?rhs" using x_Min y_Min `¬ x < y`
by(auto intro!: proper_interval_set_less_eqI)
with True show ?thesis using `¬ x < y` by simp
next
case False
have "set (x # xs) ∪ set ys ⊆ above (Some y)"
using `y < x` x_Min y_Min by auto
with `¬ x < y` `y < x` xxs ys
have IH: "set_less_eq_aux_Compl (Some y) (x # xs) ys =
(set (x # xs) ⊑' - set ys ∩ above (Some y))"
by(rule "3.IH")
moreover have "- set ys ∩ above (Some y) = ?rhs"
using y_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2)
ultimately show ?thesis using `¬ x < y` True False by simp
qed
next
case False with `¬ x < y` have "x = y" by auto
{ assume "proper_interval ao (Some y)"
hence "?lhs ⊑' ?rhs" using x_Min y_Min `x = y`
by(auto intro!: proper_interval_set_less_eqI) }
moreover
{ assume "?lhs ⊑' ?rhs"
moreover have "?lhs ≠ ?rhs"
proof
assume eq: "?lhs = ?rhs"
have "x ∈ ?lhs" using x_ao by simp
also note eq also note `x = y`
finally show False by simp
qed
ultimately obtain z where "z ∈ above ao" "z < y" using `x = y` y_ao
by(fastforce simp add: set_less_eq_aux_def set_less_aux_def not_le dest!: bspec[where x=y])
hence "proper_interval ao (Some y)" by(auto simp add: proper_interval_Some2) }
ultimately show ?thesis using `x = y` `¬ x < y` `¬ y < x` by auto
qed
qed
qed }
from this[of None] show ?Compl2 by simp
{ fix ao
assume "set xs ∪ set ys ⊆ above ao"
with xs ys
have "Compl_set_less_eq_aux ao xs ys ⟷ (- set xs) ∩ above ao ⊑' set ys"
proof(induction ao xs ys rule: Compl_set_less_eq_aux.induct)
case 1 thus ?case by(simp add: proper_interval_None2)
next
case (2 ao y ys)
from `sorted (y # ys)` `distinct (y # ys)`
have ys: "sorted ys" "distinct ys" and y_Min: "∀y' ∈ set ys. y < y'"
by(auto simp add: less_le)
show ?case
proof(cases "proper_interval ao (Some y)")
case True
hence "¬ - set [] ∩ above ao ⊑' set (y # ys)" using y_Min
by -(erule proper_interval_not_set_less_eq_auxI, auto)
thus ?thesis using True by simp
next
case False
note ao = `set [] ∪ set (y # ys) ⊆ above ao`
hence y_ao: "y ∈ above ao" by simp
from ao y_Min have "set [] ∪ set ys ⊆ above (Some y)" by auto
with `sorted []` `distinct []` ys
have "Compl_set_less_eq_aux (Some y) [] ys ⟷ - set [] ∩ above (Some y) ⊑' set ys"
by(rule "2.IH")
moreover have "above ao ≠ {}" using y_ao by auto
moreover have "Min (above ao) = y"
and "Min (set (y # ys)) = y"
using y_ao False ao by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less)
moreover have "above ao - {y} = above (Some y)" using False y_ao
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
moreover have "set ys - {y} = set ys"
using y_Min y_ao by(auto)
ultimately show ?thesis using False y_ao
by(simp)(subst (2) set_less_eq_aux_rec, simp_all)
qed
next
case (3 ao x xs)
from `sorted (x # xs)` `distinct (x # xs)`
have xs: "sorted xs" "distinct xs" and x_Min: "∀x'∈set xs. x < x'"
by(auto simp add: less_le)
show ?case
proof(cases "proper_interval ao (Some x)")
case True
then obtain z where "z ∈ above ao" "z < x" by(auto simp add: proper_interval_Some2)
hence "z ∈ - set (x # xs) ∩ above ao" using x_Min by auto
thus ?thesis using True by auto
next
case False
note ao = `set (x # xs) ∪ set [] ⊆ above ao`
hence x_ao: "x ∈ above ao" by simp
from ao have "set xs ∪ set [] ⊆ above (Some x)" using x_Min by auto
with xs `sorted []` `distinct []`
have "Compl_set_less_eq_aux (Some x) xs [] ⟷
- set xs ∩ above (Some x) ⊑' set []"
by(rule "3.IH")
moreover have "- set (x # xs) ∩ above ao = - set xs ∩ above (Some x)"
using False x_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed)
ultimately show ?thesis using False by simp
qed
next
case (4 ao x xs y ys)
note ao = `set (x # xs) ∪ set (y # ys) ⊆ above ao`
hence x_ao: "x ∈ above ao" and y_ao: "y ∈ above ao" by simp_all
note xxs = `sorted (x # xs)` `distinct (x # xs)`
hence xs: "sorted xs" "distinct xs" and x_Min: "∀x'∈set xs. x < x'"
by(auto simp add: less_le)
note yys = `sorted (y # ys)` `distinct (y # ys)`
hence ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
by(auto simp add: less_le)
let ?lhs = "- set (x # xs) ∩ above ao" and ?rhs = "set (y # ys)"
show ?case
proof(cases "x < y")
case True
show ?thesis
proof(cases "proper_interval ao (Some x)")
case True
hence "¬ ?lhs ⊑' ?rhs" using x_Min y_Min `x < y`
by -(erule proper_interval_not_set_less_eq_auxI, auto)
thus ?thesis using True `x < y` by simp
next
case False
have "set xs ∪ set (y # ys) ⊆ above (Some x)"
using ao x_Min y_Min True by auto
with True xs yys
have "Compl_set_less_eq_aux (Some x) xs (y # ys) ⟷
- set xs ∩ above (Some x) ⊑' set (y # ys)"
by(rule "4.IH")
moreover have "- set xs ∩ above (Some x) = ?lhs"
using x_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2)
ultimately show ?thesis using False True by simp
qed
next
case False
show ?thesis
proof(cases "y < x")
case True
show ?thesis
proof(cases "proper_interval ao (Some y)")
case True
hence "¬ ?lhs ⊑' ?rhs" using x_Min y_Min `y < x`
by -(erule proper_interval_not_set_less_eq_auxI, auto)
thus ?thesis using True `y < x` `¬ x < y` by simp
next
case False
from ao True x_Min y_Min
have "set (x # xs) ∪ set ys ⊆ above (Some y)" by auto
with `¬ x < y` True xxs ys
have "Compl_set_less_eq_aux (Some y) (x # xs) ys ⟷
- set (x # xs) ∩ above (Some y) ⊑' set ys"
by(rule "4.IH")
moreover have "y ∈ ?lhs" using True x_Min y_ao by auto
hence "?lhs ≠ {}" by auto
moreover have "Min ?lhs = y" using True False x_Min y_ao
by(auto intro!: Min_eqI simp add: not_le not_less proper_interval_Some2)
moreover have "Min ?rhs = y" using y_Min y_ao by(auto intro!: Min_eqI)
moreover have "- set (x # xs) ∩ above (Some y) = ?lhs - {y}"
using y_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2)
moreover have "set ys = set ys - {y}"
using y_ao y_Min by(auto intro: above_upclosed)
ultimately show ?thesis using True False `¬ x < y` y_ao
by(simp)(subst (2) set_less_eq_aux_rec, simp_all)
qed
next
case False
with `¬ x < y` have "x = y" by auto
{ assume "proper_interval ao (Some y)"
hence "¬ ?lhs ⊑' ?rhs" using x_Min y_Min `x = y`
by -(erule proper_interval_not_set_less_eq_auxI, auto) }
moreover
{ assume "¬ ?lhs ⊑' ?rhs"
also have "?rhs = set (y # ys) ∩ above ao"
using ao by auto
finally obtain z where "z ∈ above ao" "z < y"
using `x = y` x_ao x_Min[unfolded Ball_def]
by(fastforce simp add: set_less_eq_aux_def set_less_aux_def simp add: less_le not_le dest!: bspec[where x=y])
hence "proper_interval ao (Some y)"
by(auto simp add: proper_interval_Some2) }
ultimately show ?thesis using `x = y` by auto
qed
qed
qed }
from this[of None] show ?Compl1 by simp
qed
lemma set_less_aux_Compl_iff:
"set_less_aux_Compl ao xs ys ⟷ set_less_eq_aux_Compl ao xs ys ∧ ¬ Compl_set_less_eq_aux ao ys xs"
by(induct ao xs ys rule: set_less_aux_Compl.induct)(auto simp add: not_less_iff_gr_or_eq)
lemma Compl_set_less_aux_Compl_iff:
"Compl_set_less_aux ao xs ys ⟷ Compl_set_less_eq_aux ao xs ys ∧ ¬ set_less_eq_aux_Compl ao ys xs"
by(induct ao xs ys rule: Compl_set_less_aux.induct)(auto simp add: not_less_iff_gr_or_eq)
theorem assumes fin: "finite (UNIV :: 'a set)"
and xs: "sorted xs" "distinct xs"
and ys: "sorted ys" "distinct ys"
shows set_less_aux_Compl2_conv_set_less_aux_Compl:
"set xs ⊏' - set ys ⟷ set_less_aux_Compl None xs ys" (is ?Compl2)
and Compl1_set_less_aux_conv_Compl_set_less_aux:
"- set xs ⊏' set ys ⟷ Compl_set_less_aux None xs ys" (is ?Compl1)
using assms
by(simp_all only: set_less_aux_conv_set_less_eq_aux set_less_aux_Compl_iff Compl_set_less_aux_Compl_iff set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux)
end
subsection {* Implementation of proper intervals for sets *}
definition length_last :: "'a list ⇒ nat × 'a"
where "length_last xs = (length xs, last xs)"
lemma length_last_Nil [code]: "length_last [] = (0, undefined)"
by(simp add: length_last_def last_def)
lemma length_last_Cons_code [symmetric, code]:
"fold (λx (n, _) . (n + 1, x)) xs (1, x) = length_last (x # xs)"
by(induct xs rule: rev_induct)(simp_all add: length_last_def)
context proper_intrvl begin
fun exhaustive_above :: "'a ⇒ 'a list ⇒ bool" where
"exhaustive_above x [] ⟷ ¬ proper_interval (Some x) None"
| "exhaustive_above x (y # ys) ⟷ ¬ proper_interval (Some x) (Some y) ∧ exhaustive_above y ys"
fun exhaustive :: "'a list ⇒ bool" where
"exhaustive [] = False"
| "exhaustive (x # xs) ⟷ ¬ proper_interval None (Some x) ∧ exhaustive_above x xs"
fun proper_interval_set_aux :: "'a list ⇒ 'a list ⇒ bool"
where
"proper_interval_set_aux xs [] ⟷ False"
| "proper_interval_set_aux [] (y # ys) ⟷ ys ≠ [] ∨ proper_interval (Some y) None"
| "proper_interval_set_aux (x # xs) (y # ys) ⟷
(if x < y then False
else if y < x then proper_interval (Some y) (Some x) ∨ ys ≠ [] ∨ ¬ exhaustive_above x xs
else proper_interval_set_aux xs ys)"
fun proper_interval_set_Compl_aux :: "'a option ⇒ nat ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"proper_interval_set_Compl_aux ao n [] [] ⟷
CARD('a) > n + 1"
| "proper_interval_set_Compl_aux ao n [] (y # ys) ⟷
(let m = CARD('a) - n; (len_y, y') = length_last (y # ys)
in m ≠ len_y ∧ (m = len_y + 1 ⟶ ¬ proper_interval (Some y') None))"
| "proper_interval_set_Compl_aux ao n (x # xs) [] ⟷
(let m = CARD('a) - n; (len_x, x') = length_last (x # xs)
in m ≠ len_x ∧ (m = len_x + 1 ⟶ ¬ proper_interval (Some x') None))"
| "proper_interval_set_Compl_aux ao n (x # xs) (y # ys) ⟷
(if x < y then
proper_interval ao (Some x) ∨
proper_interval_set_Compl_aux (Some x) (n + 1) xs (y # ys)
else if y < x then
proper_interval ao (Some y) ∨
proper_interval_set_Compl_aux (Some y) (n + 1) (x # xs) ys
else proper_interval ao (Some x) ∧
(let m = card (UNIV :: 'a set) - n in m - length ys ≠ 2 ∨ m - length xs ≠ 2))"
fun proper_interval_Compl_set_aux :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"proper_interval_Compl_set_aux ao (x # xs) (y # ys) ⟷
(if x < y then
¬ proper_interval ao (Some x) ∧
proper_interval_Compl_set_aux (Some x) xs (y # ys)
else if y < x then
¬ proper_interval ao (Some y) ∧
proper_interval_Compl_set_aux (Some y) (x # xs) ys
else ¬ proper_interval ao (Some x) ∧ (ys = [] ⟶ xs ≠ []))"
| "proper_interval_Compl_set_aux ao _ _ ⟷ False"
end
lemmas [code] =
proper_intrvl.exhaustive_above.simps
proper_intrvl.exhaustive.simps
proper_intrvl.proper_interval_set_aux.simps
proper_intrvl.proper_interval_set_Compl_aux.simps
proper_intrvl.proper_interval_Compl_set_aux.simps
context linorder_proper_interval begin
lemma exhaustive_above_iff:
"⟦ sorted xs; distinct xs; ∀x'∈set xs. x < x' ⟧ ⟹ exhaustive_above x xs ⟷ set xs = {z. z > x}"
proof(induction x xs rule: exhaustive_above.induct)
case 1 thus ?case by(simp add: proper_interval_simps)
next
case (2 x y ys)
from `sorted (y # ys)` `distinct (y # ys)`
have ys: "sorted ys" "distinct ys" and y: "∀y'∈set ys. y < y'"
by(auto simp add: less_le)
hence "exhaustive_above y ys = (set ys = {z. y < z})" by(rule "2.IH")
moreover from `∀y'∈set (y # ys). x < y'` have "x < y" by simp
ultimately show ?case using y
by(fastforce simp add: proper_interval_simps)
qed
lemma exhaustive_correct:
assumes "sorted xs" "distinct xs"
shows "exhaustive xs ⟷ set xs = UNIV"
proof(cases xs)
case Nil thus ?thesis by auto
next
case Cons
show ?thesis using assms unfolding Cons exhaustive.simps
apply(subst exhaustive_above_iff)
apply(auto simp add: less_le proper_interval_simps not_less)
by (metis List.set_simps(2) UNIV_I eq_iff set_ConsD)
qed
theorem proper_interval_set_aux:
assumes fin: "finite (UNIV :: 'a set)"
and xs: "sorted xs" "distinct xs"
and ys: "sorted ys" "distinct ys"
shows "proper_interval_set_aux xs ys ⟷ (∃A. set xs ⊏' A ∧ A ⊏' set ys)"
proof -
note [simp] = finite_subset[OF subset_UNIV fin]
show ?thesis using xs ys
proof(induction xs ys rule: proper_interval_set_aux.induct)
case 1 thus ?case by simp
next
case (2 y ys)
hence "∀y'∈set ys. y < y'" by(auto simp add: less_le)
thus ?case
by(cases ys)(auto simp add: proper_interval_simps set_less_aux_singleton_iff intro: psubset_finite_imp_set_less_aux)
next
case (3 x xs y ys)
from `sorted (x # xs)` `distinct (x # xs)`
have xs: "sorted xs" "distinct xs" and x: "∀x'∈set xs. x < x'"
by(auto simp add: less_le)
from `sorted (y # ys)` `distinct (y # ys)`
have ys: "sorted ys" "distinct ys" and y: "∀y'∈set ys. y < y'"
by(auto simp add: less_le)
have Minxxs: "Min (set (x # xs)) = x" and xnxs: "x ∉ set xs"
using x by(auto intro!: Min_eqI)
have Minyys: "Min (set (y # ys)) = y" and ynys: "y ∉ set ys"
using y by(auto intro!: Min_eqI)
show ?case
proof(cases "x < y")
case True
hence "set (y # ys) ⊏' set (x # xs)" using Minxxs Minyys
by -(rule set_less_aux_Min_antimono, simp_all)
thus ?thesis using True by(auto dest: set_less_aux_trans set_less_aux_antisym)
next
case False
show ?thesis
proof(cases "y < x")
case True
{ assume "proper_interval (Some y) (Some x)"
then obtain z where z: "y < z" "z < x" by(auto simp add: proper_interval_simps)
hence "set (x # xs) ⊏' {z}" using x
by -(rule set_less_aux_Min_antimono, auto)
moreover have "{z} ⊏' set (y # ys)" using z y Minyys
by -(rule set_less_aux_Min_antimono, auto)
ultimately have "∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys)" by blast }
moreover
{ assume "ys ≠ []"
hence "{y} ⊏' set (y # ys)" using y
by -(rule psubset_finite_imp_set_less_aux, auto simp add: neq_Nil_conv)
moreover have "set (x # xs) ⊏' {y}" using False True x
by -(rule set_less_aux_Min_antimono, auto)
ultimately have "∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys)" by blast }
moreover
{ assume "¬ exhaustive_above x xs"
then obtain z where z: "z > x" "z ∉ set xs" using x
by(auto simp add: exhaustive_above_iff[OF xs x])
let ?A = "insert z (set (x # xs))"
have "set (x # xs) ⊏' ?A" using z
by -(rule psubset_finite_imp_set_less_aux, auto)
moreover have "?A ⊏' set (y # ys)" using Minyys False True z x
by -(rule set_less_aux_Min_antimono, auto)
ultimately have "∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys)" by blast }
moreover
{ fix A
assume A: "set (x # xs) ⊏' A" and A': "A ⊏' {y}"
and pi: "¬ proper_interval (Some y) (Some x)"
from A have nempty: "A ≠ {}" by auto
have "y ∉ A"
proof
assume "y ∈ A"
moreover with A' have "A ≠ {y}" by auto
ultimately have "{y} ⊏' A" by -(rule psubset_finite_imp_set_less_aux, auto)
with A' show False by(rule set_less_aux_antisym)
qed
have "y < Min A" unfolding not_le[symmetric]
proof
assume "Min A ≤ y"
moreover have "Min A ≠ y" using `y ∉ A` nempty by clarsimp
ultimately have "Min A < Min {y}" by simp
hence "{y} ⊏' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
with A' show False by(rule set_less_aux_antisym)
qed
with pi nempty have "x ≤ Min A" by(auto simp add: proper_interval_simps)
moreover
from A obtain z where z: "z ∈ A" "z ∉ set (x # xs)"
by(auto simp add: set_less_aux_def)
with `x ≤ Min A` nempty have "x < z" by auto
with z have "¬ exhaustive_above x xs"
by(auto simp add: exhaustive_above_iff[OF xs x]) }
ultimately show ?thesis using True False by fastforce
next
case False
with `¬ x < y` have "x = y" by auto
from `¬ x < y` False
have "proper_interval_set_aux xs ys = (∃A. set xs ⊏' A ∧ A ⊏' set ys)"
using xs ys by(rule "3.IH")
also have "… = (∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then obtain A where A: "set xs ⊏' A"
and A': "A ⊏' set ys" by blast
hence nempty: "A ≠ {}" "ys ≠ []" by auto
let ?A = "insert y A"
{ assume "Min A ≤ y"
also from y nempty have "y < Min (set ys)" by auto
finally have "set ys ⊏' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
with A' have False by(rule set_less_aux_antisym) }
hence MinA: "y < Min A" by(metis not_le)
with nempty have "y ∉ A" by auto
moreover
with MinA nempty have MinyA: "Min ?A = y" by -(rule Min_eqI, auto)
ultimately have A1: "set (x # xs) ⊏' ?A" using `x = y` A Minxxs xnxs
by(subst set_less_aux_rec) simp_all
moreover
have "?A ⊏' set (y # ys)" using `x = y` MinyA `y ∉ A` A' Minyys ynys
by(subst set_less_aux_rec) simp_all
ultimately show ?rhs by blast
next
assume "?rhs"
then obtain A where A: "set (x # xs) ⊏' A"
and A': "A ⊏' set (y # ys)" by blast
let ?A = "A - {x}"
from A have nempty: "A ≠ {}" by auto
{ assume "x < Min A"
hence "Min (set (x # xs)) < Min A" unfolding Minxxs .
hence "A ⊏' set (x # xs)"
by(rule set_less_aux_Min_antimono) simp_all
with A have False by(rule set_less_aux_antisym) }
moreover
{ assume "Min A < x"
hence "Min A < Min (set (y # ys))" unfolding `x = y` Minyys .
hence "set (y # ys) ⊏' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
with A' have False by(rule set_less_aux_antisym) }
ultimately have MinA: "Min A = x" by(metis less_linear)
hence "x ∈ A" using nempty by(metis Min_in `finite A`)
from A nempty Minxxs xnxs have "set xs ⊏' ?A"
by(subst (asm) set_less_aux_rec)(auto simp add: MinA)
moreover from A' `x = y` nempty Minyys MinA ynys have "?A ⊏' set ys"
by(subst (asm) set_less_aux_rec) simp_all
ultimately show ?lhs by blast
qed
finally show ?thesis using `x = y` by simp
qed
qed
qed
qed
lemma proper_interval_set_Compl_aux:
assumes fin: "finite (UNIV :: 'a set)"
and xs: "sorted xs" "distinct xs"
and ys: "sorted ys" "distinct ys"
shows "proper_interval_set_Compl_aux None 0 xs ys ⟷ (∃A. set xs ⊏' A ∧ A ⊏' - set ys)"
proof -
note [simp] = finite_subset[OF subset_UNIV fin]
define above where "above = case_option UNIV (Collect ∘ less)"
have above_simps [simp]: "above None = UNIV" "⋀x. above (Some x) = {y. x < y}"
and above_upclosed: "⋀x y ao. ⟦ x ∈ above ao; x < y ⟧ ⟹ y ∈ above ao"
and proper_interval_Some2: "⋀x ao. proper_interval ao (Some x) ⟷ (∃z∈above ao. z < x)"
by(simp_all add: proper_interval_simps above_def split: option.splits)
{ fix ao n
assume "set xs ⊆ above ao" "set ys ⊆ above ao"
from xs `set xs ⊆ above ao` ys `set ys ⊆ above ao`
have "proper_interval_set_Compl_aux ao (card (UNIV - above ao)) xs ys ⟷
(∃A ⊆ above ao. set xs ⊏' A ∧ A ⊏' - set ys ∩ above ao)"
proof(induct ao n≡"card (UNIV - above ao)" xs ys rule: proper_interval_set_Compl_aux.induct)
case (1 ao)
have "card (UNIV - above ao) + 1 < CARD('a) ⟷ (∃A ⊆ above ao. A ≠ {} ∧ A ⊏' above ao)"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
hence "card (UNIV - (UNIV - above ao)) > 1" by(simp add: card_Diff_subset)
from card_gt_1D[OF this]
obtain x y where above: "x ∈ above ao" "y ∈ above ao"
and neq: "x ≠ y" by blast
hence "{x} ⊏' {x, y} ∩ above ao"
by(simp_all add: psubsetI psubset_finite_imp_set_less_aux)
also have "… ⊑' above ao"
by(auto intro: subset_finite_imp_set_less_eq_aux)
finally show ?rhs using above by blast
next
assume ?rhs
then obtain A where nempty: "A ∩ above ao ≠ {}"
and subset: "A ⊆ above ao"
and less: "A ⊏' above ao" by blast
from nempty obtain x where x: "x ∈ A" "x ∈ above ao" by blast
show ?lhs
proof(rule ccontr)
assume "¬ ?lhs"
moreover have "CARD('a) ≥ card (UNIV - above ao)" by(rule card_mono) simp_all
moreover from card_Un_disjoint[of "UNIV - above ao" "above ao"]
have "CARD('a) = card (UNIV - above ao) + card (above ao)" by auto
ultimately have "card (above ao) = 1" using x
by(cases "card (above ao)")(auto simp add: not_less_eq less_Suc_eq_le)
with x have "above ao = {x}" unfolding card_eq_1_iff by auto
moreover with x subset have A: "A = {x}" by auto
ultimately show False using less by simp
qed
qed
thus ?case by simp
next
case (2 ao y ys)
note ys = `sorted (y # ys)` `distinct (y # ys)` `set (y # ys) ⊆ above ao`
have len_ys: "length ys = card (set ys)"
using ys by(auto simp add: List.card_set intro: sym)
define m where "m = CARD('a) - card (UNIV - above ao)"
have "CARD('a) = card (above ao) + card (UNIV - above ao)"
using card_Un_disjoint[of "above ao" "UNIV - above ao"] by auto
hence m_eq: "m = card (above ao)" unfolding m_def by simp
have "m ≠ length ys + 1 ∧ (m = length ys + 2 ⟶ ¬ proper_interval (Some (last (y # ys))) None) ⟷
(∃A ⊆ above ao. A ≠ {} ∧ A ⊏' - set (y # ys) ∩ above ao)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
hence m: "m ≠ length ys + 1"
and pi: "m = length ys + 2 ⟹ ¬ proper_interval (Some (last (y # ys))) None"
by simp_all
have "length ys + 1 = card (set (y # ys))" using ys len_ys by simp
also have "… ≤ m" unfolding m_eq by(rule card_mono)(simp, rule ys)
finally have "length ys + 2 ≤ m" using m by simp
show ?rhs
proof(cases "m = length ys + 2")
case True
hence "card (UNIV - (UNIV - above ao) - set (y # ys)) = 1"
using ys len_ys
by(subst card_Diff_subset)(auto simp add: m_def card_Diff_subset)
then obtain z where z: "z ∈ above ao" "z ≠ y" "z ∉ set ys"
unfolding card_eq_1_iff by auto
from True have "¬ proper_interval (Some (last (y # ys))) None" by(rule pi)
hence "z ≤ last (y # ys)" by(simp add: proper_interval_simps not_less del: last.simps)
moreover have ly: "last (y # ys) ∈ set (y # ys)" by(rule last_in_set) simp
with z have "z ≠ last (y # ys)" by auto
ultimately have "z < last (y # ys)" by simp
hence "{last (y # ys)} ⊏' {z}"
using z ly ys by(auto 4 3 simp add: set_less_aux_def)
also have "… ⊑' - set (y # ys) ∩ above ao"
using z by(auto intro: subset_finite_imp_set_less_eq_aux)
also have "{last (y # ys)} ≠ {}" using ly ys by blast
moreover have "{last (y # ys)} ⊆ above ao" using ys by auto
ultimately show ?thesis by blast
next
case False
with `length ys + 2 ≤ m` ys len_ys
have "card (UNIV - (UNIV - above ao) - set (y # ys)) > 1"
by(subst card_Diff_subset)(auto simp add: card_Diff_subset m_def)
from card_gt_1D[OF this]
obtain x x' where x: "x ∈ above ao" "x ≠ y" "x ∉ set ys"
and x': "x' ∈ above ao" "x' ≠ y" "x' ∉ set ys"
and neq: "x ≠ x'" by auto
hence "{x} ⊏' {x, x'} ∩ above ao"
by(simp_all add: psubsetI psubset_finite_imp_set_less_aux)
also have "… ⊑' - set (y # ys) ∩ above ao" using x x' ys
by(auto intro: subset_finite_imp_set_less_eq_aux)
also have "{x} ∩ above ao ≠ {}" using x by simp
ultimately show ?rhs by blast
qed
next
assume ?rhs
then obtain A where nempty: "A ≠ {}"
and less: "A ⊏' - set (y # ys) ∩ above ao"
and subset: "A ⊆ above ao" by blast
have "card (set (y # ys)) ≤ card (above ao)" using ys(3) by(simp add: card_mono)
hence "length ys + 1 ≤ m" unfolding m_eq using ys by(simp add: len_ys)
have "m ≠ length ys + 1"
proof
assume "m = length ys + 1"
hence "card (above ao) ≤ card (set (y # ys))"
unfolding m_eq using ys len_ys by auto
from card_seteq[OF _ _ this] ys have "set (y # ys) = above ao" by simp
with nempty less show False by(auto simp add: set_less_aux_def)
qed
moreover
{ assume "m = length ys + 2"
hence "card (above ao - set (y # ys)) = 1"
using ys len_ys m_eq by(auto simp add: card_Diff_subset)
then obtain z where z: "above ao - set (y # ys) = {z}"
unfolding card_eq_1_iff ..
hence eq_z: "- set (y # ys) ∩ above ao = {z}" by auto
with less have "A ⊏' {z}" by simp
have "¬ proper_interval (Some (last (y # ys))) None"
proof
assume "proper_interval (Some (last (y # ys))) None"
then obtain z' where z': "last (y # ys) < z'"
by(clarsimp simp add: proper_interval_simps)
have "last (y # ys) ∈ set (y # ys)" by(rule last_in_set) simp
with ys z' have "z' ∈ above ao" "z' ∉ set (y # ys)"
by(auto simp del: last.simps sorted.simps(2) intro: above_upclosed dest: sorted_last)
with eq_z have "z = z'" by fastforce
from z' have "⋀x. x ∈ set (y # ys) ⟹ x < z'" using ys
by(auto dest: sorted_last simp del: sorted.simps(2))
with eq_z `z = z'`
have "⋀x. x ∈ above ao ⟹ x ≤ z'" by(fastforce)
with `A ⊏' {z}` nempty `z = z'` subset
show False by(auto simp add: set_less_aux_def)
qed }
ultimately show ?lhs by simp
qed
thus ?case by(simp add: length_last_def m_def Let_def)
next
case (3 ao x xs)
note xs = `sorted (x # xs)` `distinct (x # xs)` `set (x # xs) ⊆ above ao`
have len_xs: "length xs = card (set xs)"
using xs by(auto simp add: List.card_set intro: sym)
define m where "m = CARD('a) - card (UNIV - above ao)"
have "CARD('a) = card (above ao) + card (UNIV - above ao)"
using card_Un_disjoint[of "above ao" "UNIV - above ao"] by auto
hence m_eq: "m = card (above ao)" unfolding m_def by simp
have "m ≠ length xs + 1 ∧ (m = length xs + 2 ⟶ ¬ proper_interval (Some (last (x # xs))) None) ⟷
(∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' above ao)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
hence m: "m ≠ length xs + 1"
and pi: "m = length xs + 2 ⟹ ¬ proper_interval (Some (last (x # xs))) None"
by simp_all
have "length xs + 1 = card (set (x # xs))" using xs len_xs by simp
also have "… ≤ m" unfolding m_eq by(rule card_mono)(simp, rule xs)
finally have "length xs + 2 ≤ m" using m by simp
show ?rhs
proof(cases "m = length xs + 2")
case True
hence "card (UNIV - (UNIV - above ao) - set (x # xs)) = 1"
using xs len_xs
by(subst card_Diff_subset)(auto simp add: m_def card_Diff_subset)
then obtain z where z: "z ∈ above ao" "z ≠ x" "z ∉ set xs"
unfolding card_eq_1_iff by auto
define A where "A = insert z {y. y ∈ set (x # xs) ∧ y < z}"
from True have "¬ proper_interval (Some (last (x # xs))) None" by(rule pi)
hence "z ≤ last (x # xs)" by(simp add: proper_interval_simps not_less del: last.simps)
moreover have lx: "last (x # xs) ∈ set (x # xs)" by(rule last_in_set) simp
with z have "z ≠ last (x # xs)" by auto
ultimately have "z < last (x # xs)" by simp
hence "set (x # xs) ⊏' A"
using z xs by(auto simp add: A_def set_less_aux_def intro: rev_bexI[where x=z])
moreover have "last (x # xs) ∉ A" using xs `z < last (x # xs)`
by(auto simp add: A_def simp del: last.simps)
hence "A ⊂ insert (last (x # xs)) A" by blast
hence less': "A ⊏' insert (last (x # xs)) A"
by(rule psubset_finite_imp_set_less_aux) simp
have "… ⊆ above ao" using xs lx z
by(auto simp del: last.simps simp add: A_def)
hence "insert (last (x # xs)) A ⊑' above ao"
by(auto intro: subset_finite_imp_set_less_eq_aux)
with less' have "A ⊏' above ao"
by(rule set_less_trans_set_less_eq)
moreover have "A ⊆ above ao" using xs z by(auto simp add: A_def)
ultimately show ?thesis by blast
next
case False
with `length xs + 2 ≤ m` xs len_xs
have "card (UNIV - (UNIV - above ao) - set (x # xs)) > 1"
by(subst card_Diff_subset)(auto simp add: card_Diff_subset m_def)
from card_gt_1D[OF this]
obtain y y' where y: "y ∈ above ao" "y ≠ x" "y ∉ set xs"
and y': "y' ∈ above ao" "y' ≠ x" "y' ∉ set xs"
and neq: "y ≠ y'" by auto
define A where "A = insert y (set (x # xs) ∩ above ao)"
hence "set (x # xs) ⊂ A" using y xs by auto
hence "set (x # xs) ⊏' …"
by(fastforce intro: psubset_finite_imp_set_less_aux)
moreover have *: "… ⊂ above ao"
using y y' neq by(auto simp add: A_def)
moreover from * have "A ⊏' above ao"
by(auto intro: psubset_finite_imp_set_less_aux)
ultimately show ?thesis by blast
qed
next
assume ?rhs
then obtain A where lessA: "set (x # xs) ⊏' A"
and Aless: "A ⊏' above ao" and subset: "A ⊆ above ao" by blast
have "card (set (x # xs)) ≤ card (above ao)" using xs(3) by(simp add: card_mono)
hence "length xs + 1 ≤ m" unfolding m_eq using xs by(simp add: len_xs)
have "m ≠ length xs + 1"
proof
assume "m = length xs + 1"
hence "card (above ao) ≤ card (set (x # xs))"
unfolding m_eq using xs len_xs by auto
from card_seteq[OF _ _ this] xs have "set (x # xs) = above ao" by simp
with lessA Aless show False by(auto dest: set_less_aux_antisym)
qed
moreover
{ assume "m = length xs + 2"
hence "card (above ao - set (x # xs)) = 1"
using xs len_xs m_eq by(auto simp add: card_Diff_subset)
then obtain z where z: "above ao - set (x # xs) = {z}"
unfolding card_eq_1_iff ..
have "¬ proper_interval (Some (last (x # xs))) None"
proof
assume "proper_interval (Some (last (x # xs))) None"
then obtain z' where z': "last (x # xs) < z'"
by(clarsimp simp add: proper_interval_simps)
have "last (x # xs) ∈ set (x # xs)" by(rule last_in_set) simp
with xs z' have "z' ∈ above ao" "z' ∉ set (x # xs)"
by(auto simp del: last.simps sorted.simps(2) intro: above_upclosed dest: sorted_last)
with z have "z = z'" by fastforce
from z' have y_less: "⋀y. y ∈ set (x # xs) ⟹ y < z'" using xs
by(auto simp del: sorted.simps(2) dest: sorted_last)
with z `z = z'` have "⋀y. y ∈ above ao ⟹ y ≤ z'" by(fastforce)
from lessA subset obtain y where y: "y ∈ A" "y ∈ above ao" "y ∉ set (x # xs)"
and min: "⋀y'. ⟦ y' ∈ set (x # xs); y' ∈ above ao; y' ∉ A ⟧ ⟹ y ≤ y'"
by(auto simp add: set_less_aux_def)
with z `z = z'` have "y = z'" by auto
have "set (x # xs) ⊆ A"
proof
fix y'
assume y': "y' ∈ set (x # xs)"
show "y' ∈ A"
proof(rule ccontr)
assume "y' ∉ A"
from y' xs have "y' ∈ above ao" by auto
with y' have "y ≤ y'" using `y' ∉ A` by(rule min)
moreover from y' have "y' < z'" by(rule y_less)
ultimately show False using `y = z'` by simp
qed
qed
moreover from z xs have "above ao = insert z (set (x # xs))" by auto
ultimately have "A = above ao" using y `y = z'` `z = z'` subset by auto
with Aless show False by simp
qed }
ultimately show ?lhs by simp
qed
thus ?case by(simp add: length_last_def m_def Let_def del: last.simps)
next
case (4 ao x xs y ys)
note xxs = `sorted (x # xs)` `distinct (x # xs)`
and yys = `sorted (y # ys)` `distinct (y # ys)`
and xxs_above = `set (x # xs) ⊆ above ao`
and yys_above = `set (y # ys) ⊆ above ao`
from xxs have xs: "sorted xs" "distinct xs" and x_Min: "∀x'∈set xs. x < x'"
by(auto simp add: less_le)
from yys have ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
by(auto simp add: less_le)
have len_xs: "length xs = card (set xs)"
using xs by(auto simp add: List.card_set intro: sym)
have len_ys: "length ys = card (set ys)"
using ys by(auto simp add: List.card_set intro: sym)
show ?case
proof(cases "x < y")
case True
have "proper_interval ao (Some x) ∨
proper_interval_set_Compl_aux (Some x) (card (UNIV - above ao) + 1) xs (y # ys) ⟷
(∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' - set (y # ys) ∩ above ao)"
(is "?lhs ⟷ ?rhs")
proof(cases "proper_interval ao (Some x)")
case True
then obtain z where z: "z ∈ above ao" "z < x"
by(clarsimp simp add: proper_interval_Some2)
moreover with xxs have "∀x'∈set xs. z < x'" by(auto)
ultimately have "set (x # xs) ⊏' {z}"
by(auto simp add: set_less_aux_def intro!: bexI[where x=z])
moreover {
from z yys `x < y` have "z < y" "∀y'∈set ys. z < y'"
by(auto)
hence subset: "{z} ⊆ - set (y # ys) ∩ above ao"
using ys `x < y` z by auto
moreover have "x ∈ …" using yys xxs `x < y` xxs_above by(auto)
ultimately have "{z} ⊂ …" using `z < x` by fastforce
hence "{z} ⊏' …"
by(fastforce intro: psubset_finite_imp_set_less_aux) }
moreover have "{z} ⊆ above ao" using z by simp
ultimately have ?rhs by blast
thus ?thesis using True by simp
next
case False
hence above_eq: "above ao = insert x (above (Some x))" using xxs_above
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
moreover have "card (above (Some x)) < CARD('a)"
by(rule psubset_card_mono)(auto)
ultimately have card_eq: "card (UNIV - above ao) + 1 = card (UNIV - above (Some x))"
by(simp add: card_Diff_subset)
from xxs_above x_Min have xs_above: "set xs ⊆ above (Some x)" by(auto)
from `x < y` y_Min have "set (y # ys) ⊆ above (Some x)" by(auto)
with `x < y` card_eq xs xs_above yys
have "proper_interval_set_Compl_aux (Some x) (card (UNIV - above ao) + 1) xs (y # ys) ⟷
(∃A ⊆ above (Some x). set xs ⊏' A ∧ A ⊏' - set (y # ys) ∩ above (Some x))"
by(subst card_eq)(rule 4)
also have "… ⟷ ?rhs" (is "?lhs' ⟷ _")
proof
assume ?lhs'
then obtain A where less_A: "set xs ⊏' A"
and A_less: "A ⊏' - set (y # ys) ∩ above (Some x)"
and subset: "A ⊆ above (Some x)" by blast
let ?A = "insert x A"
have Min_A': "Min ?A = x" using xxs_above False subset
by(auto intro!: Min_eqI simp add: proper_interval_Some2)
moreover have "Min (set (x # xs)) = x"
using x_Min by(auto intro!: Min_eqI)
moreover have Amx: "A - {x} = A"
using False subset
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
moreover have "set xs - {x} = set xs" using x_Min by auto
ultimately have less_A': "set (x # xs) ⊏' ?A"
using less_A xxs_above x_Min by(subst set_less_aux_rec) simp_all
have "x ∈ - insert y (set ys) ∩ above ao"
using `x < y` xxs_above y_Min by auto
hence "- insert y (set ys) ∩ above ao ≠ {}" by auto
moreover have "Min (- insert y (set ys) ∩ above ao) = x"
using yys y_Min xxs_above `x < y` False
by(auto intro!: Min_eqI simp add: proper_interval_Some2)
moreover have "- set (y # ys) ∩ above ao - {x} = - set (y # ys) ∩ above (Some x)"
using yys_above False xxs_above
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
ultimately have A'_less: "?A ⊏' - set (y # ys) ∩ above ao"
using Min_A' A_less Amx xxs_above by(subst set_less_aux_rec) simp_all
moreover have "?A ⊆ above ao" using subset xxs_above by(auto intro: above_upclosed)
ultimately show ?rhs using less_A' by blast
next
assume ?rhs
then obtain A where less_A: "set (x # xs) ⊏' A"
and A_less: "A ⊏' - set (y # ys) ∩ above ao"
and subset: "A ⊆ above ao" by blast
let ?A = "A - {x}"
from less_A subset xxs_above have "set (x # xs) ∩ above ao ⊏' A ∩ above ao"
by(simp add: Int_absorb2)
with False xxs_above subset have "x ∈ A"
by(auto simp add: set_less_aux_def proper_interval_Some2)
hence "… ≠ {}" by auto
moreover from `x ∈ A` False subset
have Min_A: "Min A = x"
by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less)
moreover have "Min (set (x # xs)) = x"
using x_Min by(auto intro!: Min_eqI)
moreover have eq_A: "?A ⊆ above (Some x)"
using xxs_above False subset
by(fastforce simp add: proper_interval_Some2 not_less intro: above_upclosed)
moreover have "set xs - {x} = set xs"
using x_Min by(auto)
ultimately have less_A': "set xs ⊏' ?A"
using xxs_above less_A by(subst (asm) set_less_aux_rec)(simp_all cong: conj_cong)
have "x ∈ - insert y (set ys) ∩ above ao"
using `x < y` xxs_above y_Min by auto
hence "- insert y (set ys) ∩ above ao ≠ {}" by auto
moreover have "Min (- set (y # ys) ∩ above ao) = x"
using yys y_Min xxs_above `x < y` False
by(auto intro!: Min_eqI simp add: proper_interval_Some2)
moreover have "- set (y # ys) ∩ above (Some x) = - set (y # ys) ∩ above ao - {x}"
by(auto simp add: above_eq)
ultimately have "?A ⊏' - set (y # ys) ∩ above (Some x)"
using A_less `A ≠ {}` eq_A Min_A
by(subst (asm) set_less_aux_rec) simp_all
with less_A' eq_A show ?lhs' by blast
qed
finally show ?thesis using False by simp
qed
thus ?thesis using True by simp
next
case False
show ?thesis
proof(cases "y < x")
case True
have "proper_interval ao (Some y) ∨
proper_interval_set_Compl_aux (Some y) (card (UNIV - above ao) + 1) (x # xs) ys ⟷
(∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' - set (y # ys) ∩ above ao)"
(is "?lhs ⟷ ?rhs")
proof(cases "proper_interval ao (Some y)")
case True
then obtain z where z: "z ∈ above ao" "z < y"
by(clarsimp simp add: proper_interval_Some2)
from xxs `y < x` have "∀x'∈set (x # xs). y < x'" by(auto)
hence less_A: "set (x # xs) ⊏' {y}"
by(auto simp add: set_less_aux_def intro!: bexI[where x=y])
have "{y} ⊏' {z}"
using z y_Min by(auto simp add: set_less_aux_def intro: bexI[where x=z])
also have "… ⊆ - set (y # ys) ∩ above ao" using z y_Min by auto
hence "{z} ⊑' …" by(auto intro: subset_finite_imp_set_less_eq_aux)
finally have "{y} ⊏' …" .
moreover have "{y} ⊆ above ao" using yys_above by auto
ultimately have ?rhs using less_A by blast
thus ?thesis using True by simp
next
case False
hence above_eq: "above ao = insert y (above (Some y))" using yys_above
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
moreover have "card (above (Some y)) < CARD('a)"
by(rule psubset_card_mono)(auto)
ultimately have card_eq: "card (UNIV - above ao) + 1 = card (UNIV - above (Some y))"
by(simp add: card_Diff_subset)
from yys_above y_Min have ys_above: "set ys ⊆ above (Some y)" by(auto)
have eq_ys: "- set ys ∩ above (Some y) = - set (y # ys) ∩ above ao"
by(auto simp add: above_eq)
from `y < x` x_Min have "set (x # xs) ⊆ above (Some y)" by(auto)
with `¬ x < y` `y < x` card_eq xxs ys ys_above
have "proper_interval_set_Compl_aux (Some y) (card (UNIV - above ao) + 1) (x # xs) ys ⟷
(∃A ⊆ above (Some y). set (x # xs) ⊏' A ∧ A ⊏' - set ys ∩ above (Some y))"
by(subst card_eq)(rule 4)
also have "… ⟷ ?rhs" (is "?lhs' ⟷ _")
proof
assume ?lhs'
then obtain A where "set (x # xs) ⊏' A" and subset: "A ⊆ above (Some y)"
and "A ⊏' - set ys ∩ above (Some y)" by blast
moreover from subset have "A - {y} = A" by auto
ultimately have "set (x # xs) ⊏' A - {y}"
and "A - {y} ⊏' - set (y # ys) ∩ above ao"
using eq_ys by simp_all
moreover from subset have "A - {y} ⊆ above ao"
using yys_above by(auto intro: above_upclosed)
ultimately show ?rhs by blast
next
assume ?rhs
then obtain A where "set (x # xs) ⊏' A"
and A_less: "A ⊏' - set (y # ys) ∩ above ao"
and subset: "A ⊆ above ao" by blast
moreover
from A_less False yys_above have "y ∉ A"
by(auto simp add: set_less_aux_def proper_interval_Some2 not_less)
ultimately have "set (x # xs) ⊏' A"
and "A ⊏' - set ys ∩ above (Some y)"
using eq_ys by simp_all
moreover from `y ∉ A` subset above_eq have "A ⊆ above (Some y)" by auto
ultimately show ?lhs' by blast
qed
finally show ?thesis using False by simp
qed
with False True show ?thesis by simp
next
case False
with `¬ x < y` have "x = y" by simp
have "proper_interval ao (Some x) ∧
(CARD('a) - (card (UNIV - above ao) + length ys) ≠ 2 ∨
CARD('a) - (card (UNIV - above ao) + length xs) ≠ 2) ⟷
(∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' - set (y # ys) ∩ above ao)"
(is "?below ∧ ?card ⟷ ?rhs")
proof(cases "?below")
case False
hence "- set (y # ys) ∩ above ao ⊏' set (x # xs)"
using `x = y` yys_above xxs_above y_Min
by(auto simp add: not_less set_less_aux_def proper_interval_Some2 intro!: bexI[where x=y])
with False show ?thesis by(auto dest: set_less_aux_trans)
next
case True
then obtain z where z: "z ∈ above ao" "z < x"
by(clarsimp simp add: proper_interval_Some2)
have "?card ⟷ ?rhs"
proof
assume ?rhs
then obtain A where less_A: "set (x # xs) ⊏' A"
and A_less: "A ⊏' - set (y # ys) ∩ above ao"
and subset: "A ⊆ above ao" by blast
{
assume c_ys: "CARD('a) - (card (UNIV - above ao) + length ys) = 2"
and c_xs: "CARD('a) - (card (UNIV - above ao) + length xs) = 2"
from c_ys yys_above len_ys y_Min have "card (UNIV - (UNIV - above ao) - set (y # ys)) = 1"
by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
then obtain z' where eq_y: "- set (y # ys) ∩ above ao = {z'}"
unfolding card_eq_1_iff by auto
moreover from z have "z ∉ set (y # ys)" using `x = y` y_Min by auto
ultimately have "z' = z" using z by fastforce
from c_xs xxs_above len_xs x_Min have "card (UNIV - (UNIV - above ao) - set (x # xs)) = 1"
by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
then obtain z'' where eq_x: "- set (x # xs) ∩ above ao = {z''}"
unfolding card_eq_1_iff by auto
moreover from z have "z ∉ set (x # xs)" using x_Min by auto
ultimately have "z'' = z" using z by fastforce
from less_A subset obtain q where "q ∈ A" "q ∈ above ao" "q ∉ set (x # xs)"
by(auto simp add: set_less_aux_def)
hence "q ∈ {z''}" unfolding eq_x[symmetric] by simp
hence "q = z''" by simp
with `q ∈ A` `z' = z` `z'' = z` z
have "- set (y # ys) ∩ above ao ⊆ A"
unfolding eq_y by simp
hence "- set (y # ys) ∩ above ao ⊑' A"
by(auto intro: subset_finite_imp_set_less_eq_aux)
with A_less have False by(auto dest: set_less_trans_set_less_eq) }
thus ?card by auto
next
assume ?card (is "?card_ys ∨ ?card_xs")
thus ?rhs
proof
assume ?card_ys
let ?YS = "UNIV - (UNIV - above ao) - set (y # ys)"
from `?card_ys` yys_above len_ys y_Min have "card ?YS ≠ 1"
by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
moreover have "?YS ≠ {}" using True y_Min yys_above `x = y`
by(fastforce simp add: proper_interval_Some2)
hence "card ?YS ≠ 0" by simp
ultimately have "card ?YS > 1" by(cases "card ?YS") simp_all
from card_gt_1D[OF this] obtain x' y'
where x': "x' ∈ above ao" "x' ∉ set (y # ys)"
and y': "y' ∈ above ao" "y' ∉ set (y # ys)"
and neq: "x' ≠ y'" by auto
let ?A = "{z}"
have "set (x # xs) ⊏' ?A" using z x_Min
by(auto simp add: set_less_aux_def intro!: rev_bexI)
moreover
{ have "?A ⊆ - set (y # ys) ∩ above ao"
using z `x = y` y_Min by(auto)
moreover have "x' ∉ ?A ∨ y' ∉ ?A" using neq by auto
with x' y' have "?A ≠ - set (y # ys) ∩ above ao" by auto
ultimately have "?A ⊂ - set (y # ys) ∩ above ao" by(rule psubsetI)
hence "?A ⊏' …" by(fastforce intro: psubset_finite_imp_set_less_aux) }
ultimately show ?thesis using z by blast
next
assume ?card_xs
let ?XS = "UNIV - (UNIV - above ao) - set (x # xs)"
from `?card_xs` xxs_above len_xs x_Min have "card ?XS ≠ 1"
by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
moreover have "?XS ≠ {}" using True x_Min xxs_above
by(fastforce simp add: proper_interval_Some2)
hence "card ?XS ≠ 0" by simp
ultimately have "card ?XS > 1" by(cases "card ?XS") simp_all
from card_gt_1D[OF this] obtain x' y'
where x': "x' ∈ above ao" "x' ∉ set (x # xs)"
and y': "y' ∈ above ao" "y' ∉ set (x # xs)"
and neq: "x' ≠ y'" by auto
define A
where "A = (if x' = Min (above ao) then insert y' (set (x # xs)) else insert x' (set (x # xs)))"
hence "set (x # xs) ⊆ A" by auto
moreover have "set (x # xs) ≠ …"
using neq x' y' by(auto simp add: A_def)
ultimately have "set (x # xs) ⊂ A" ..
hence "set (x # xs) ⊏' …"
by(fastforce intro: psubset_finite_imp_set_less_aux)
moreover {
have nempty: "above ao ≠ {}" using z by auto
have "A ⊏' {Min (above ao)}"
using z x' y' neq `x = y` x_Min xxs_above
by(auto 6 4 simp add: set_less_aux_def A_def nempty intro!: rev_bexI Min_eqI)
also have "Min (above ao) ≤ z" using z by(simp)
hence "Min (above ao) < x" using `z < x` by(rule le_less_trans)
with `x = y` y_Min have "Min (above ao) ∉ set (y # ys)" by auto
hence "{Min (above ao)} ⊆ - set (y # ys) ∩ above ao"
by(auto simp add: nempty)
hence "{Min (above ao)} ⊑' …" by(auto intro: subset_finite_imp_set_less_eq_aux)
finally have "A ⊏' …" . }
moreover have "A ⊆ above ao" using xxs_above yys_above x' y'
by(auto simp add: A_def)
ultimately show ?rhs by blast
qed
qed
thus ?thesis using True by simp
qed
thus ?thesis using `x = y` by simp
qed
qed
qed }
from this[of None]
show ?thesis by(simp)
qed
lemma proper_interval_Compl_set_aux:
assumes fin: "finite (UNIV :: 'a set)"
and xs: "sorted xs" "distinct xs"
and ys: "sorted ys" "distinct ys"
shows "proper_interval_Compl_set_aux None xs ys ⟷ (∃A. - set xs ⊏' A ∧ A ⊏' set ys)"
proof -
note [simp] = finite_subset[OF subset_UNIV fin]
define above where "above = case_option UNIV (Collect ∘ less)"
have above_simps [simp]: "above None = UNIV" "⋀x. above (Some x) = {y. x < y}"
and above_upclosed: "⋀x y ao. ⟦ x ∈ above ao; x < y ⟧ ⟹ y ∈ above ao"
and proper_interval_Some2: "⋀x ao. proper_interval ao (Some x) ⟷ (∃z∈above ao. z < x)"
by(simp_all add: proper_interval_simps above_def split: option.splits)
{ fix ao n
assume "set xs ⊆ above ao" "set ys ⊆ above ao"
from xs `set xs ⊆ above ao` ys `set ys ⊆ above ao`
have "proper_interval_Compl_set_aux ao xs ys ⟷
(∃A. - set xs ∩ above ao ⊏' A ∩ above ao ∧ A ∩ above ao ⊏' set ys ∩ above ao)"
proof(induction ao xs ys rule: proper_interval_Compl_set_aux.induct)
case ("2_1" ao ys)
{ fix A
assume "above ao ⊏' A ∩ above ao"
also have "… ⊆ above ao" by simp
hence "A ∩ above ao ⊑' above ao"
by(auto intro: subset_finite_imp_set_less_eq_aux)
finally have False by simp }
thus ?case by auto
next
case ("2_2" ao xs) thus ?case by simp
next
case (1 ao x xs y ys)
note xxs = `sorted (x # xs)` `distinct (x # xs)`
hence xs: "sorted xs" "distinct xs" and x_Min: "∀x' ∈ set xs. x < x'"
by(auto simp add: less_le)
note yys = `sorted (y # ys)` `distinct (y # ys)`
hence ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
by(auto simp add: less_le)
note xxs_above = `set (x # xs) ⊆ above ao`
note yys_above = `set (y # ys) ⊆ above ao`
show ?case
proof(cases "x < y")
case True
have "¬ proper_interval ao (Some x) ∧ proper_interval_Compl_set_aux (Some x) xs (y # ys) ⟷
(∃A. - set (x # xs) ∩ above ao ⊏' A ∩ above ao ∧ A ∩ above ao ⊏' set (y # ys) ∩ above ao)"
(is "?lhs ⟷ ?rhs")
proof(cases "proper_interval ao (Some x)")
case True
then obtain z where z: "z < x" "z ∈ above ao"
by(auto simp add: proper_interval_Some2)
hence nempty: "above ao ≠ {}" by auto
with z have "Min (above ao) ≤ z" by auto
hence "Min (above ao) < x" using `z < x` by(rule le_less_trans)
hence "set (y # ys) ∩ above ao ⊏' - set (x # xs) ∩ above ao"
using y_Min x_Min z `x < y`
by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
thus ?thesis using True by(auto dest: set_less_aux_trans set_less_aux_antisym)
next
case False
hence above_eq: "above ao = insert x (above (Some x))"
using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed)
from x_Min have xs_above: "set xs ⊆ above (Some x)" by auto
from `x < y` y_Min have ys_above: "set (y # ys) ⊆ above (Some x)" by auto
have eq_xs: "- set xs ∩ above (Some x) = - set (x # xs) ∩ above ao"
using above_eq by auto
have eq_ys: "set (y # ys) ∩ above (Some x) = set (y # ys) ∩ above ao"
using y_Min `x < y` xxs_above by(auto intro: above_upclosed)
from `x < y` xs xs_above yys ys_above
have "proper_interval_Compl_set_aux (Some x) xs (y # ys) ⟷
(∃A. - set xs ∩ above (Some x) ⊏' A ∩ above (Some x) ∧
A ∩ above (Some x) ⊏' set (y # ys) ∩ above (Some x))"
by(rule "1.IH")
also have "… ⟷ ?rhs" (is "?lhs ⟷ _")
proof
assume ?lhs
then obtain A where "- set xs ∩ above (Some x) ⊏' A ∩ above (Some x)"
and "A ∩ above (Some x) ⊏' set (y # ys) ∩ above (Some x)" by blast
moreover have "A ∩ above (Some x) = (A - {x}) ∩ above ao"
using above_eq by auto
ultimately have "- set (x # xs) ∩ above ao ⊏' (A - {x}) ∩ above ao"
and "(A - {x}) ∩ above ao ⊏' set (y # ys) ∩ above ao"
using eq_xs eq_ys by simp_all
thus ?rhs by blast
next
assume ?rhs
then obtain A where "- set (x # xs) ∩ above ao ⊏' A ∩ above ao"
and A_less: "A ∩ above ao ⊏' set (y # ys) ∩ above ao" by blast
moreover have "x ∉ A"
proof
assume "x ∈ A"
hence "set (y # ys) ∩ above ao ⊏' A ∩ above ao"
using y_Min `x < y` by(auto simp add: above_eq set_less_aux_def intro!: bexI[where x=x])
with A_less show False by(auto dest: set_less_aux_antisym)
qed
hence "A ∩ above ao = A ∩ above (Some x)" using above_eq by auto
ultimately show ?lhs using eq_xs eq_ys by auto
qed
finally show ?thesis using False by simp
qed
thus ?thesis using True by simp
next
case False
show ?thesis
proof(cases "y < x")
case True
show ?thesis (is "?lhs ⟷ ?rhs")
proof(cases "proper_interval ao (Some y)")
case True
then obtain z where z: "z < y" "z ∈ above ao"
by(auto simp add: proper_interval_Some2)
hence nempty: "above ao ≠ {}" by auto
with z have "Min (above ao) ≤ z" by auto
hence "Min (above ao) < y" using `z < y` by(rule le_less_trans)
hence "set (y # ys) ∩ above ao ⊏' - set (x # xs) ∩ above ao"
using y_Min x_Min z `y < x`
by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
thus ?thesis using True `y < x` by(auto dest: set_less_aux_trans set_less_aux_antisym)
next
case False
hence above_eq: "above ao = insert y (above (Some y))"
using yys_above by(auto simp add: proper_interval_Some2 intro: above_upclosed)
from y_Min have ys_above: "set ys ⊆ above (Some y)" by auto
from `y < x` x_Min have xs_above: "set (x # xs) ⊆ above (Some y)" by auto
have "y ∈ - set (x # xs) ∩ above ao" using `y < x` x_Min yys_above by auto
hence nempty: "- set (x # xs) ∩ above ao ≠ {}" by auto
have Min_x: "Min (- set (x # xs) ∩ above ao) = y"
using above_eq `y < x` x_Min by(auto intro!: Min_eqI)
have Min_y: "Min (set (y # ys) ∩ above ao) = y"
using y_Min above_eq by(auto intro!: Min_eqI)
have eq_xs: "- set (x # xs) ∩ above ao - {y} = - set (x # xs) ∩ above (Some y)"
by(auto simp add: above_eq)
have eq_ys: "set ys ∩ above ao - {y} = set ys ∩ above (Some y)"
using y_Min above_eq by auto
from `¬ x < y` `y < x` xxs xs_above ys ys_above
have "proper_interval_Compl_set_aux (Some y) (x # xs) ys ⟷
(∃A. - set (x # xs) ∩ above (Some y) ⊏' A ∩ above (Some y) ∧
A ∩ above (Some y) ⊏' set ys ∩ above (Some y))"
by(rule "1.IH")
also have "… ⟷ ?rhs" (is "?lhs' ⟷ _")
proof
assume ?lhs'
then obtain A where less_A: "- set (x # xs) ∩ above (Some y) ⊏' A ∩ above (Some y)"
and A_less: "A ∩ above (Some y) ⊏' set ys ∩ above (Some y)" by blast
let ?A = "insert y A"
have Min_A: "Min (?A ∩ above ao) = y"
using above_eq by(auto intro!: Min_eqI)
moreover have A_eq: "A ∩ above ao - {y} = A ∩ above (Some y)"
using above_eq by auto
ultimately have less_A': "- set (x # xs) ∩ above ao ⊏' ?A ∩ above ao"
using nempty yys_above less_A Min_x eq_xs by(subst set_less_aux_rec) simp_all
have A'_less: "?A ∩ above ao ⊏' set (y # ys) ∩ above ao"
using yys_above nempty Min_A A_eq A_less Min_y eq_ys
by(subst set_less_aux_rec) simp_all
with less_A' show ?rhs by blast
next
assume ?rhs
then obtain A where less_A: "- set (x # xs) ∩ above ao ⊏' A ∩ above ao"
and A_less: "A ∩ above ao ⊏' set (y # ys) ∩ above ao" by blast
from less_A have nempty': "A ∩ above ao ≠ {}" by auto
moreover have A_eq: "A ∩ above ao - {y} = A ∩ above (Some y)"
using above_eq by auto
moreover have y_in_xxs: "y ∈ - set (x # xs) ∩ above ao"
using `y < x` x_Min yys_above by auto
moreover have "y ∈ A"
proof(rule ccontr)
assume "y ∉ A"
hence "A ∩ above ao ⊏' - set (x # xs) ∩ above ao"
using `y < x` x_Min y_in_xxs
by(auto simp add: set_less_aux_def above_eq intro: bexI[where x=y])
with less_A show False by(rule set_less_aux_antisym)
qed
hence Min_A: "Min (A ∩ above ao) = y" using above_eq y_Min by(auto intro!: Min_eqI)
ultimately have less_A': "- set (x # xs) ∩ above (Some y) ⊏' A ∩ above (Some y)"
using nempty less_A Min_x eq_xs
by(subst (asm) set_less_aux_rec)(auto dest: bspec[where x=y])
have A'_less: "A ∩ above (Some y) ⊏' set ys ∩ above (Some y)"
using A_less nempty' yys_above Min_A Min_y A_eq eq_ys
by(subst (asm) set_less_aux_rec) simp_all
with less_A' show ?lhs' by blast
qed
finally show ?thesis using `¬ x < y` `y < x` False by simp
qed
next
case False
with `¬ x < y` have "x = y" by auto
thus ?thesis (is "?lhs ⟷ ?rhs")
proof(cases "proper_interval ao (Some x)")
case True
then obtain z where z: "z < x" "z ∈ above ao"
by(auto simp add: proper_interval_Some2)
hence nempty: "above ao ≠ {}" by auto
with z have "Min (above ao) ≤ z" by auto
hence "Min (above ao) < x" using `z < x` by(rule le_less_trans)
hence "set (y # ys) ∩ above ao ⊏' - set (x # xs) ∩ above ao"
using y_Min x_Min z `x = y`
by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
thus ?thesis using True `x = y` by(auto dest: set_less_aux_trans set_less_aux_antisym)
next
case False
hence above_eq: "above ao = insert x (above (Some x))"
using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed)
have "(ys = [] ⟶ xs ≠ []) ⟷ ?rhs" (is "?lhs' ⟷ _")
proof(intro iffI strip notI)
assume ?lhs'
show ?rhs
proof(cases ys)
case Nil
with `?lhs'` obtain x' xs' where xs_eq: "xs = x' # xs'"
by(auto simp add: neq_Nil_conv)
with xs have x'_Min: "∀x'' ∈ set xs'. x' < x''"
by(auto simp add: less_le)
let ?A = "- set (x # xs')"
have "- set (x # xs) ∩ above ao ⊆ ?A ∩ above ao"
using xs_eq by auto
moreover have "x' ∉ - set (x # xs) ∩ above ao" "x' ∈ ?A ∩ above ao"
using xs_eq xxs_above x'_Min x_Min by auto
ultimately have "- set (x # xs) ∩ above ao ⊂ ?A ∩ above ao"
by blast
hence "- set (x # xs) ∩ above ao ⊏' … "
by(fastforce intro: psubset_finite_imp_set_less_aux)
moreover have "… ⊏' set (y # ys) ∩ above ao"
using Nil `x = y` by(auto simp add: set_less_aux_def above_eq)
ultimately show ?thesis by blast
next
case (Cons y' ys')
let ?A = "{y}"
have "- set (x # xs) ∩ above ao ⊏' ?A ∩ above ao"
using `x = y` x_Min by(auto simp add: set_less_aux_def above_eq)
moreover have "… ⊂ set (y # ys) ∩ above ao"
using yys_above yys Cons by auto
hence "?A ∩ above ao ⊏' …" by(fastforce intro: psubset_finite_imp_set_less_aux)
ultimately show ?thesis by blast
qed
next
assume Nil: "ys = []" "xs = []" and ?rhs
then obtain A where less_A: "- {x} ∩ above ao ⊏' A ∩ above ao"
and A_less: "A ∩ above ao ⊏' {x}" using `x = y` above_eq by auto
have "x ∉ A" using A_less by(auto simp add: set_less_aux_def above_eq)
hence "A ∩ above ao ⊆ - {x} ∩ above ao" by auto
hence "A ∩ above ao ⊑' …" by(auto intro: subset_finite_imp_set_less_eq_aux)
with less_A have "… ⊏' …" by(rule set_less_trans_set_less_eq)
thus False by simp
qed
with `x = y` False show ?thesis by simp
qed
qed
qed
qed }
from this[of None] show ?thesis by simp
qed
end
subsection {* Proper intervals for HOL types *}
instantiation unit :: proper_interval begin
fun proper_interval_unit :: "unit proper_interval" where
"proper_interval_unit None None = True"
| "proper_interval_unit _ _ = False"
instance by intro_classes auto
end
instantiation bool :: proper_interval begin
fun proper_interval_bool :: "bool proper_interval" where
"proper_interval_bool (Some x) (Some y) ⟷ False"
| "proper_interval_bool (Some x) None ⟷ ¬ x"
| "proper_interval_bool None (Some y) ⟷ y"
| "proper_interval_bool None None = True"
instance by intro_classes auto
end
instantiation nat :: proper_interval begin
fun proper_interval_nat :: "nat proper_interval" where
"proper_interval_nat no None = True"
| "proper_interval_nat None (Some x) ⟷ x > 0"
| "proper_interval_nat (Some x) (Some y) ⟷ y - x > 1"
instance by intro_classes auto
end
instantiation int :: proper_interval begin
fun proper_interval_int :: "int proper_interval" where
"proper_interval_int (Some x) (Some y) ⟷ y - x > 1"
| "proper_interval_int _ _ = True"
instance by intro_classes (auto intro: less_add_one, metis less_add_one minus_less_iff)
end
instantiation integer :: proper_interval begin
context includes integer.lifting begin
lift_definition proper_interval_integer :: "integer proper_interval" is "proper_interval" .
instance by(intro_classes)(transfer, simp only: proper_interval_simps)+
end
end
lemma proper_interval_integer_simps [code]:
includes integer.lifting fixes x y :: integer and xo yo :: "integer option" shows
"proper_interval (Some x) (Some y) = (1 < y - x)"
"proper_interval None yo = True"
"proper_interval xo None = True"
by(transfer, simp)+
instantiation natural :: proper_interval begin
context includes natural.lifting begin
lift_definition proper_interval_natural :: "natural proper_interval" is "proper_interval" .
instance by(intro_classes)(transfer, simp only: proper_interval_simps)+
end
end
lemma proper_interval_natural_simps [code]:
includes natural.lifting fixes x y :: natural and xo :: "natural option" shows
"proper_interval xo None = True"
"proper_interval None (Some y) ⟷ y > 0"
"proper_interval (Some x) (Some y) ⟷ y - x > 1"
by(transfer, simp)+
lemma char_less_iff_nat_of_char: "x < y ⟷ of_char x < (of_char y :: nat)"
by (fact less_char_def)
lemma nat_of_char_inject [simp]: "of_char x = (of_char y :: nat) ⟷ x = y"
by (fact of_char_eq_iff)
lemma char_le_iff_nat_of_char: "x ≤ y ⟷ of_char x ≤ (of_char y :: nat)"
by (fact less_eq_char_def)
instantiation char :: proper_interval
begin
fun proper_interval_char :: "char proper_interval" where
"proper_interval_char None None ⟷ True"
| "proper_interval_char None (Some x) ⟷ x ≠ CHR 0x00"
| "proper_interval_char (Some x) None ⟷ x ≠ CHR 0xFF"
| "proper_interval_char (Some x) (Some y) ⟷ of_char y - of_char x > (1 :: nat)"
instance proof
fix y :: char
{ assume "y ≠ CHR 0x00"
have "CHR 0x00 < y"
proof (rule ccontr)
assume "¬ CHR 0x00 < y"
then have "of_char y = (of_char CHR 0x00 :: nat)"
by (simp add: not_less char_le_iff_nat_of_char)
then have "y = CHR 0x00"
using nat_of_char_inject [of y "CHR 0x00"] by simp
with ‹y ≠ CHR 0x00› show False
by simp
qed }
moreover
{ fix z :: char
assume "z < CHR 0x00"
hence False
by (simp add: char_less_iff_nat_of_char of_char_eq_iff [symmetric]) }
ultimately show "proper_interval None (Some y) = (∃z. z < y)"
by auto
fix x :: char
{ assume "x ≠ CHR 0xFF"
then have "x < CHR 0xFF"
by (auto simp add: neq_iff char_less_iff_nat_of_char)
(insert nat_of_char_less_256 [of x], simp)
hence "∃z. x < z" .. }
moreover
{ fix z :: char
assume "CHR 0xFF < z"
hence "False"
by (simp add: char_less_iff_nat_of_char)
(insert nat_of_char_less_256 [of z], simp) }
ultimately show "proper_interval (Some x) None = (∃z. x < z)" by auto
{ assume gt: "of_char y - of_char x > (1 :: nat)"
let ?z = "char_of (of_char x + (1 :: nat))"
from gt nat_of_char_less_256 [of y]
have 255: "of_char x < (255 :: nat)" by arith
with gt have "x < ?z" "?z < y"
by (simp_all add: char_less_iff_nat_of_char)
hence "∃z. x < z ∧ z < y" by blast }
moreover
{ fix z
assume "x < z" "z < y"
hence "(1 :: nat) < of_char y - of_char x"
by (simp add: char_less_iff_nat_of_char) }
ultimately show "proper_interval (Some x) (Some y) = (∃z>x. z < y)"
by auto
qed simp
end
instantiation Enum.finite_1 :: proper_interval begin
definition proper_interval_finite_1 :: "Enum.finite_1 proper_interval"
where "proper_interval_finite_1 x y ⟷ x = None ∧ y = None"
instance by intro_classes (simp_all add: proper_interval_finite_1_def less_finite_1_def)
end
instantiation Enum.finite_2 :: proper_interval begin
fun proper_interval_finite_2 :: "Enum.finite_2 proper_interval" where
"proper_interval_finite_2 None None ⟷ True"
| "proper_interval_finite_2 None (Some x) ⟷ x = finite_2.a⇩2"
| "proper_interval_finite_2 (Some x) None ⟷ x = finite_2.a⇩1"
| "proper_interval_finite_2 (Some x) (Some y) ⟷ False"
instance by intro_classes (auto simp add: less_finite_2_def)
end
instantiation Enum.finite_3 :: proper_interval begin
fun proper_interval_finite_3 :: "Enum.finite_3 proper_interval" where
"proper_interval_finite_3 None None ⟷ True"
| "proper_interval_finite_3 None (Some x) ⟷ x ≠ finite_3.a⇩1"
| "proper_interval_finite_3 (Some x) None ⟷ x ≠ finite_3.a⇩3"
| "proper_interval_finite_3 (Some x) (Some y) ⟷ x = finite_3.a⇩1 ∧ y = finite_3.a⇩3"
instance
proof
fix x y :: Enum.finite_3
show "proper_interval None (Some y) = (∃z. z < y)"
by(cases y)(auto simp add: less_finite_3_def split: finite_3.split)
show "proper_interval (Some x) None = (∃z. x < z)"
by(cases x)(auto simp add: less_finite_3_def)
show "proper_interval (Some x) (Some y) = (∃z>x. z < y)"
by(auto simp add: less_finite_3_def split: finite_3.split_asm)
qed simp
end
subsection {* List fusion for the order and proper intervals on @{typ "'a set"} *}
definition length_last_fusion :: "('a, 's) generator ⇒ 's ⇒ nat × 'a"
where "length_last_fusion g s = length_last (list.unfoldr g s)"
lemma length_last_fusion_code [code]:
"length_last_fusion g s =
(if list.has_next g s then
let (x, s') = list.next g s
in fold_fusion g (λx (n, _). (n + 1, x)) s' (1, x)
else (0, undefined))"
unfolding length_last_fusion_def
by(subst list.unfoldr.simps)(simp add: length_last_Nil length_last_Cons_code fold_fusion_def split_beta)
declare length_last_fusion_def [symmetric, code_unfold]
context proper_intrvl begin
definition set_less_eq_aux_Compl_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 =
set_less_eq_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition Compl_set_less_eq_aux_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 =
Compl_set_less_eq_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition set_less_aux_Compl_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"set_less_aux_Compl_fusion g1 g2 ao s1 s2 =
set_less_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition Compl_set_less_aux_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"Compl_set_less_aux_fusion g1 g2 ao s1 s2 =
Compl_set_less_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition exhaustive_above_fusion :: "('a, 's) generator ⇒ 'a ⇒ 's ⇒ bool"
where "exhaustive_above_fusion g a s = exhaustive_above a (list.unfoldr g s)"
definition exhaustive_fusion :: "('a, 's) generator ⇒ 's ⇒ bool"
where "exhaustive_fusion g s = exhaustive (list.unfoldr g s)"
definition proper_interval_set_aux_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"proper_interval_set_aux_fusion g1 g2 s1 s2 =
proper_interval_set_aux (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition proper_interval_set_Compl_aux_fusion ::
"('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ nat ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 =
proper_interval_set_Compl_aux ao n (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition proper_interval_Compl_set_aux_fusion ::
"('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 =
proper_interval_Compl_set_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
lemma set_less_eq_aux_Compl_fusion_code:
"set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 ⟷
(list.has_next g1 s1 ⟶ list.has_next g2 s2 ⟶
(let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in if x < y then proper_interval ao (Some x) ∨ set_less_eq_aux_Compl_fusion g1 g2 (Some x) s1' s2
else if y < x then proper_interval ao (Some y) ∨ set_less_eq_aux_Compl_fusion g1 g2 (Some y) s1 s2'
else proper_interval ao (Some y)))"
unfolding set_less_eq_aux_Compl_fusion_def
by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta)
lemma Compl_set_less_eq_aux_fusion_code:
"Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 ⟷
(if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1
in if list.has_next g2 s2 then
let (y, s2') = list.next g2 s2
in if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2
else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2'
else ¬ proper_interval ao (Some y)
else ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2
else if list.has_next g2 s2 then
let (y, s2') = list.next g2 s2
in ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2'
else ¬ proper_interval ao None)"
unfolding Compl_set_less_eq_aux_fusion_def
by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta)
lemma set_less_aux_Compl_fusion_code:
"set_less_aux_Compl_fusion g1 g2 ao s1 s2 ⟷
(if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1
in if list.has_next g2 s2 then
let (y, s2') = list.next g2 s2
in if x < y then proper_interval ao (Some x) ∨ set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2
else if y < x then proper_interval ao (Some y) ∨ set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2'
else proper_interval ao (Some y)
else proper_interval ao (Some x) ∨ set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2
else if list.has_next g2 s2 then
let (y, s2') = list.next g2 s2
in proper_interval ao (Some y) ∨ set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2'
else proper_interval ao None)"
unfolding set_less_aux_Compl_fusion_def
by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta)
lemma Compl_set_less_aux_fusion_code:
"Compl_set_less_aux_fusion g1 g2 ao s1 s2 ⟷
list.has_next g1 s1 ∧ list.has_next g2 s2 ∧
(let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_aux_fusion g1 g2 (Some x) s1' s2
else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_aux_fusion g1 g2 (Some y) s1 s2'
else ¬ proper_interval ao (Some y))"
unfolding Compl_set_less_aux_fusion_def
by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta)
lemma exhaustive_above_fusion_code:
"exhaustive_above_fusion g y s ⟷
(if list.has_next g s then
let (x, s') = list.next g s
in ¬ proper_interval (Some y) (Some x) ∧ exhaustive_above_fusion g x s'
else ¬ proper_interval (Some y) None)"
unfolding exhaustive_above_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)
lemma exhaustive_fusion_code:
"exhaustive_fusion g s =
(list.has_next g s ∧
(let (x, s') = list.next g s
in ¬ proper_interval None (Some x) ∧ exhaustive_above_fusion g x s'))"
unfolding exhaustive_fusion_def exhaustive_above_fusion_def
by(subst (1) list.unfoldr.simps)(simp add: split_beta)
lemma proper_interval_set_aux_fusion_code:
"proper_interval_set_aux_fusion g1 g2 s1 s2 ⟷
list.has_next g2 s2 ∧
(let (y, s2') = list.next g2 s2
in if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1
in if x < y then False
else if y < x then proper_interval (Some y) (Some x) ∨ list.has_next g2 s2' ∨ ¬ exhaustive_above_fusion g1 x s1'
else proper_interval_set_aux_fusion g1 g2 s1' s2'
else list.has_next g2 s2' ∨ proper_interval (Some y) None)"
unfolding proper_interval_set_aux_fusion_def exhaustive_above_fusion_def
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)
lemma proper_interval_set_Compl_aux_fusion_code:
"proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 ⟷
(if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1
in if list.has_next g2 s2 then
let (y, s2') = list.next g2 s2
in if x < y then
proper_interval ao (Some x) ∨
proper_interval_set_Compl_aux_fusion g1 g2 (Some x) (n + 1) s1' s2
else if y < x then
proper_interval ao (Some y) ∨
proper_interval_set_Compl_aux_fusion g1 g2 (Some y) (n + 1) s1 s2'
else
proper_interval ao (Some x) ∧
(let m = CARD('a) - n
in m - length_fusion g2 s2' ≠ 2 ∨ m - length_fusion g1 s1' ≠ 2)
else
let m = CARD('a) - n; (len_x, x') = length_last_fusion g1 s1
in m ≠ len_x ∧ (m = len_x + 1 ⟶ ¬ proper_interval (Some x') None)
else if list.has_next g2 s2 then
let (y, s2') = list.next g2 s2;
m = CARD('a) - n;
(len_y, y') = length_last_fusion g2 s2
in m ≠ len_y ∧ (m = len_y + 1 ⟶ ¬ proper_interval (Some y') None)
else CARD('a) > n + 1)"
unfolding proper_interval_set_Compl_aux_fusion_def length_last_fusion_def length_fusion_def
by(subst (1 2 4 5 9 10) list.unfoldr.simps)(simp add: split_beta)
lemma proper_interval_Compl_set_aux_fusion_code:
"proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 ⟷
list.has_next g1 s1 ∧ list.has_next g2 s2 ∧
(let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in if x < y then
¬ proper_interval ao (Some x) ∧ proper_interval_Compl_set_aux_fusion g1 g2 (Some x) s1' s2
else if y < x then
¬ proper_interval ao (Some y) ∧ proper_interval_Compl_set_aux_fusion g1 g2 (Some y) s1 s2'
else ¬ proper_interval ao (Some x) ∧ (list.has_next g2 s2' ∨ list.has_next g1 s1'))"
unfolding proper_interval_Compl_set_aux_fusion_def
by(subst (1 2 4 5) list.unfoldr.simps)(auto simp add: split_beta)
end
lemmas [code] =
set_less_eq_aux_Compl_fusion_code proper_intrvl.set_less_eq_aux_Compl_fusion_code
Compl_set_less_eq_aux_fusion_code proper_intrvl.Compl_set_less_eq_aux_fusion_code
set_less_aux_Compl_fusion_code proper_intrvl.set_less_aux_Compl_fusion_code
Compl_set_less_aux_fusion_code proper_intrvl.Compl_set_less_aux_fusion_code
exhaustive_above_fusion_code proper_intrvl.exhaustive_above_fusion_code
exhaustive_fusion_code proper_intrvl.exhaustive_fusion_code
proper_interval_set_aux_fusion_code proper_intrvl.proper_interval_set_aux_fusion_code
proper_interval_set_Compl_aux_fusion_code proper_intrvl.proper_interval_set_Compl_aux_fusion_code
proper_interval_Compl_set_aux_fusion_code proper_intrvl.proper_interval_Compl_set_aux_fusion_code
lemmas [symmetric, code_unfold] =
set_less_eq_aux_Compl_fusion_def proper_intrvl.set_less_eq_aux_Compl_fusion_def
Compl_set_less_eq_aux_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def
set_less_aux_Compl_fusion_def proper_intrvl.set_less_aux_Compl_fusion_def
Compl_set_less_aux_fusion_def proper_intrvl.Compl_set_less_aux_fusion_def
exhaustive_above_fusion_def proper_intrvl.exhaustive_above_fusion_def
exhaustive_fusion_def proper_intrvl.exhaustive_fusion_def
proper_interval_set_aux_fusion_def proper_intrvl.proper_interval_set_aux_fusion_def
proper_interval_set_Compl_aux_fusion_def proper_intrvl.proper_interval_set_Compl_aux_fusion_def
proper_interval_Compl_set_aux_fusion_def proper_intrvl.proper_interval_Compl_set_aux_fusion_def
subsection {* Drop notation *}
context ord begin
no_notation set_less_aux (infix "⊏''" 50)
and set_less_eq_aux (infix "⊑''" 50)
and set_less_eq_aux' (infix "⊑''''" 50)
and set_less_eq_aux'' (infix "⊑''''''" 50)
and set_less_eq (infix "⊑" 50)
and set_less (infix "⊏" 50)
end
end