# Theory Set_Linorder

```(*  Title:      Containers/Set_Linorder.thy
Author:     Andreas Lochbihler, KIT *)

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 "∃ℬ ∈ Field r. ∀𝒜 ∈ ℭ. (𝒜, ℬ) ∈ r" if ℭ: "ℭ ∈ Chains r" for ℭ
proof -
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"

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"

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: list_induct2')
apply(simp_all add: empty_set_less_aux_finite_iff sorted_Cons_Min set_less_aux_rec neq_Nil_conv)
apply(auto 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)
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)"

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]

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 ≠ {}"

lemma not_set_less_empty [simp]: "¬ A ⊏ {}"

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"]

lemma set_less_UNIV_iff [iff]: "A ⊏ UNIV ⟷ A ≠ UNIV"

lemma not_UNIV_set_less [simp]: "¬ UNIV ⊏ A"

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 intro: order_antisym)
done
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 ```