# Theory Containers_Auxiliary

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

theory Containers_Auxiliary imports
begin

chapter ‹An executable linear order on sets›
text_raw ‹\label{chapter:linear:order:set}›

section ‹Auxiliary definitions›

lemma insert_bind_set: "insert a A ⤜ f = f a ∪ (A ⤜ f)"

lemma set_bind_iff:
"set (List.bind xs f) = Set.bind (set xs) (set ∘ f)"

lemma set_bind_conv_fold: "set xs ⤜ f = fold ((∪) ∘ f) xs {}"
by(induct xs rule: rev_induct)(simp_all add: insert_bind_set)

lemma card_gt_1D:
assumes "card A > 1"
shows "∃x y. x ∈ A ∧ y ∈ A ∧ x ≠ y"
proof(rule ccontr)
from assms have "A ≠ {}" by auto
then obtain x where "x ∈ A" by auto
moreover
assume "¬ ?thesis"
ultimately have "A = {x}" by auto
with assms show False by simp
qed

lemma card_eq_1_iff: "card A = 1 ⟷ (∃x. A = {x})"
proof
assume card: "card A = 1"
hence [simp]: "finite A" using card_gt_0_iff[of A] by simp
have "A = {THE x. x ∈ A}"
proof(intro equalityI subsetI)
fix x
assume x: "x ∈ A"
hence "(THE x. x ∈ A) = x"
proof(rule the_equality)
fix x'
assume x': "x' ∈ A"
show "x' = x"
proof(rule ccontr)
assume neq: "x' ≠ x"
from x x' have eq: "A = insert x (insert x' (A - {x, x'}))" by auto
have "card A = 2 + card (A - {x, x'})" using neq by(subst eq)(simp)
with card show False by simp
qed
qed
thus "x ∈ {THE x. x ∈ A}" by simp
next
fix x
assume "x ∈ {THE x. x ∈ A}"
hence x: "x = (THE x. x ∈ A)" by simp
from card have "A ≠ {}" by auto
then obtain x' where x': "x' ∈ A" by blast
thus "x ∈ A" unfolding x
proof(rule theI)
fix x
assume x: "x ∈ A"
show "x = x'"
proof(rule ccontr)
assume neq: "x ≠ x'"
from x x' have eq: "A = insert x (insert x' (A - {x, x'}))" by auto
have "card A = 2 + card (A - {x, x'})" using neq by(subst eq)(simp)
with card show False by simp
qed
qed
qed
thus "∃x. A = {x}" ..
qed auto

lemma card_eq_Suc_0_ex1: "card A = Suc 0 ⟷ (∃!x. x ∈ A)"
by(auto simp only: One_nat_def[symmetric] card_eq_1_iff)

context linorder begin

lemma sorted_last: "⟦ sorted xs; x ∈ set xs ⟧ ⟹ x ≤ last xs"
by(cases xs rule: rev_cases)(auto simp add: sorted_append)

end

lemma empty_filter_conv: "[] = filter P xs ⟷ (∀x∈set xs. ¬ P x)"
by(auto dest: sym simp add: filter_empty_conv)

definition ID :: "'a ⇒ 'a" where "ID = id"

lemma ID_code [code, code_unfold]: "ID = (λx. x)"

lemma ID_Some: "ID (Some x) = Some x"

lemma ID_None: "ID None = None"

text ‹lexicographic order on pairs›

context
fixes leq_a :: "'a ⇒ 'a ⇒ bool" (infix "⊑⇩a" 50)
and less_a :: "'a ⇒ 'a ⇒ bool" (infix "⊏⇩a" 50)
and leq_b :: "'b ⇒ 'b ⇒ bool" (infix "⊑⇩b" 50)
and less_b :: "'b ⇒ 'b ⇒ bool" (infix "⊏⇩b" 50)
begin

definition less_eq_prod :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊑" 50)
where "less_eq_prod = (λ(x1, x2) (y1, y2). x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊑⇩b y2)"

definition less_prod :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊏" 50)
where "less_prod = (λ(x1, x2) (y1, y2). x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊏⇩b y2)"

lemma less_eq_prod_simps [simp]:
"(x1, x2) ⊑ (y1, y2) ⟷ x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊑⇩b y2"

lemma less_prod_simps [simp]:
"(x1, x2) ⊏ (y1, y2) ⟷ x1 ⊏⇩a y1 ∨ x1 ⊑⇩a y1 ∧ x2 ⊏⇩b y2"

end

context
fixes leq_a :: "'a ⇒ 'a ⇒ bool" (infix "⊑⇩a" 50)
and less_a :: "'a ⇒ 'a ⇒ bool" (infix "⊏⇩a" 50)
and leq_b :: "'b ⇒ 'b ⇒ bool" (infix "⊑⇩b" 50)
and less_b :: "'b ⇒ 'b ⇒ bool" (infix "⊏⇩b" 50)
assumes lin_a: "class.linorder leq_a less_a"
and lin_b: "class.linorder leq_b less_b"
begin

abbreviation (input) less_eq_prod' :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊑" 50)
where "less_eq_prod' ≡ less_eq_prod leq_a less_a leq_b"

abbreviation (input) less_prod' :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" (infix "⊏" 50)
where "less_prod' ≡ less_prod leq_a less_a less_b"

lemma linorder_prod:
"class.linorder (⊑) (⊏)"
proof -
interpret a: linorder "(⊑⇩a)" "(⊏⇩a)" by(fact lin_a)
interpret b: linorder "(⊑⇩b)" "(⊏⇩b)" by(fact lin_b)
show ?thesis by unfold_locales auto
qed

end

hide_const less_eq_prod' less_prod'

end


# Theory Card_Datatype

(*  Title:      Containers/Card_Datatype.thy
Author:     Andreas Lochbihler, ETH Zurich *)

theory Card_Datatype
imports "HOL-Library.Cardinality"
begin

section ‹Definitions to prove equations about the cardinality of data types›

subsection ‹Specialised @{term range} constants›

definition rangeIt :: "'a ⇒ ('a ⇒ 'a) ⇒ 'a set"
where "rangeIt x f = range (λn. (f ^^ n) x)"

definition rangeC :: "('a ⇒ 'b) set ⇒ 'b set"
where "rangeC F = (⋃f ∈ F. range f)"

lemma infinite_rangeIt:
assumes inj: "inj f"
and x: "∀y. x ≠ f y"
shows "¬ finite (rangeIt x f)"
proof -
have "inj (λn. (f ^^ n) x)"
proof(rule injI)
fix n m
assume "(f ^^ n) x = (f ^^ m) x"
thus "n = m"
proof(induct n arbitrary: m)
case 0
thus ?case using x by(cases m)(auto intro: sym)
next
case (Suc n)
thus ?case using x by(cases m)(auto intro: sym dest: injD[OF inj])
qed
qed
thus ?thesis
by(auto simp add: rangeIt_def dest: finite_imageD)
qed

lemma in_rangeC: "f ∈ A ⟹ f x ∈ rangeC A"

lemma in_rangeCE: assumes "y ∈ rangeC A"
obtains f x where "f ∈ A" "y = f x"
using assms by(auto simp add: rangeC_def)

lemma in_rangeC_singleton: "f x ∈ rangeC {f}"

lemma in_rangeC_singleton_const: "x ∈ rangeC {λ_. x}"
by(rule in_rangeC_singleton)

lemma rangeC_rangeC: "f ∈ rangeC A ⟹ f x ∈ rangeC (rangeC A)"

lemma rangeC_eq_empty: "rangeC A = {} ⟷ A = {}"

lemma Ball_rangeC_iff:
"(∀x ∈ rangeC A. P x) ⟷ (∀f ∈ A. ∀x. P (f x))"
by(auto intro: in_rangeC elim: in_rangeCE)

lemma Ball_rangeC_singleton:
"(∀x ∈ rangeC {f}. P x) ⟷ (∀x. P (f x))"

lemma Ball_rangeC_rangeC:
"(∀x ∈ rangeC (rangeC A). P x) ⟷ (∀f ∈ rangeC A. ∀x. P (f x))"

lemma finite_rangeC:
assumes inj: "∀f ∈ A. inj f"
and disjoint: "∀f ∈ A. ∀g ∈ A. f ≠ g ⟶ (∀x y. f x ≠ g y)"
shows "finite (rangeC (A :: ('a ⇒ 'b) set)) ⟷ finite A ∧ (A ≠ {} ⟶ finite (UNIV :: 'a set))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
thus ?rhs using inj disjoint
proof(induct "rangeC A" arbitrary: A rule: finite_psubset_induct)
case (psubset A)
show ?case
proof(cases "A = {}")
case True thus ?thesis by simp
next
case False
then obtain f A' where A: "A = insert f A'" and f: "f ∈ A" "f ∉ A'"
by(fastforce dest: mk_disjoint_insert)
from A have rA: "rangeC A = rangeC A' ∪ range f"

have "¬ range f ⊆ rangeC A'"
proof
assume "range f ⊆ rangeC A'"
moreover obtain x where x: "x ∈ range f" by auto
ultimately have "x ∈ rangeC A'" by auto
then obtain g where "g ∈ A'" "x ∈ range g" by(auto simp add: rangeC_def)
with ‹f ∉ A'› A have "g ∈ A" "f ≠ g" by auto
with ‹f ∈ A› have "⋀x y. f x ≠ g y" by(rule psubset.prems[rule_format])
thus False using x ‹x ∈ range g› by auto
qed
hence "rangeC A' ⊂ rangeC A" unfolding rA by auto
hence "finite A' ∧ (A' ≠ {} ⟶ finite (UNIV :: 'a set))"
using psubset.prems
by -(erule psubset.hyps, auto simp add: A)
with A have "finite A" by simp
moreover with ‹finite (rangeC A)› A ‹∀f ∈ A. inj f›
have "finite (UNIV :: 'a set)"
by(auto simp add: rangeC_def dest: finite_imageD)
ultimately show ?thesis by blast
qed
qed

lemma finite_rangeC_singleton_const:
"finite (rangeC {λ_. x})"

lemma card_Un:
"⟦ finite A; finite B ⟧ ⟹ card (A ∪ B) = card (A) + card (B) - card(A ∩ B)"
by(subst card_Un_Int) simp_all

lemma card_rangeC_singleton_const:
"card (rangeC {λ_. f}) = 1"

lemma card_rangeC:
assumes inj: "∀f ∈ A. inj f"
and disjoint: "∀f ∈ A. ∀g ∈ A. f ≠ g ⟶ (∀x y. f x ≠ g y)"
shows "card (rangeC (A :: ('a ⇒ 'b) set)) = CARD('a) * card A"
(is "?lhs = ?rhs")
proof(cases "finite (UNIV :: 'a set) ∧ finite A")
case False
thus ?thesis using False finite_rangeC[OF assms]
next
case True
{ fix f
assume "f ∈ A"
hence "card (range f) = CARD('a)" using inj by(simp add: card_image) }
thus ?thesis using disjoint True unfolding rangeC_def
by(subst card_UN_disjoint) auto
qed

lemma rangeC_Int_rangeC:
"⟦ ∀f ∈ A. ∀g ∈ B. ∀x y. f x ≠ g y ⟧ ⟹ rangeC A ∩ rangeC B = {}"

lemmas rangeC_simps =
in_rangeC_singleton
in_rangeC_singleton_const
rangeC_rangeC
rangeC_eq_empty
Ball_rangeC_singleton
Ball_rangeC_rangeC
finite_rangeC
finite_rangeC_singleton_const
card_rangeC_singleton_const
card_rangeC
rangeC_Int_rangeC

bundle card_datatype =
rangeC_simps [simp]
card_Un [simp]
fun_eq_iff [simp]
Int_Un_distrib [simp]
Int_Un_distrib2 [simp]
card_eq_0_iff [simp]
imageI [simp] image_eqI [simp del]
conj_cong [cong]
infinite_rangeIt [simp]

subsection ‹Cardinality primitives for polymorphic HOL types›

ML ‹
structure Card_Simp_Rules = Named_Thms
(
val name = @{binding card_simps}
val description = "Simplification rules for cardinality of types"
)
›
setup ‹Card_Simp_Rules.setup›

definition card_fun :: "nat ⇒ nat ⇒ nat"
where "card_fun a b = (if a ≠ 0 ∧ b ≠ 0 ∨ b = 1 then b ^ a else 0)"

lemma CARD_fun [card_simps]:
"CARD('a ⇒ 'b) = card_fun CARD('a) CARD('b)"

definition card_sum :: "nat ⇒ nat ⇒ nat"
where "card_sum a b = (if a = 0 ∨ b = 0 then 0 else a + b)"

lemma CARD_sum [card_simps]:
"CARD('a + 'b) = card_sum CARD('a) CARD('b)"

definition card_option :: "nat ⇒ nat"
where "card_option n = (if n = 0 then 0 else Suc n)"

lemma CARD_option [card_simps]:
"CARD('a option) = card_option CARD('a)"

definition card_prod :: "nat ⇒ nat ⇒ nat"
where "card_prod a b = a * b"

lemma CARD_prod [card_simps]:
"CARD('a * 'b) = card_prod CARD('a) CARD('b)"

definition card_list :: "nat ⇒ nat"
where "card_list _ = 0"

lemma CARD_list [card_simps]: "CARD('a list) = card_list CARD('a)"

end


# Theory List_Fusion

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

theory List_Fusion
imports
Main
begin

section ‹Shortcut fusion for lists›

lemma Option_map_mono [partial_function_mono]:
"mono_option f ⟹ mono_option (λx. map_option g (f x))"
apply(rule monotoneI)
apply(drule (1) monotoneD)
apply(auto simp add: map_option_case flat_ord_def split: option.split)
done

lemma list_all2_coinduct [consumes 1, case_names Nil Cons, case_conclusion Cons hd tl, coinduct pred: list_all2]:
assumes X: "X xs ys"
and Nil': "⋀xs ys. X xs ys ⟹ xs = [] ⟷ ys = []"
and Cons': "⋀xs ys. ⟦ X xs ys; xs ≠ []; ys ≠ [] ⟧ ⟹ A (hd xs) (hd ys) ∧ (X (tl xs) (tl ys) ∨ list_all2 A (tl xs) (tl ys))"
shows "list_all2 A xs ys"
using X
proof(induction xs arbitrary: ys)
case Nil
from Nil'[OF this] show ?case by simp
next
case (Cons x xs)
from Nil'[OF Cons.prems] Cons'[OF Cons.prems] Cons.IH
show ?case by(auto simp add: neq_Nil_conv)
qed

subsection ‹The type of generators for finite lists›

type_synonym ('a, 's) raw_generator = "('s ⇒ bool) × ('s ⇒ 'a × 's)"

inductive_set terminates_on :: "('a, 's) raw_generator ⇒ 's set"
for g :: "('a, 's) raw_generator"
where
stop: "¬ fst g s ⟹ s ∈ terminates_on g"
| unfold: "⟦ fst g s; snd (snd g s) ∈ terminates_on g ⟧ ⟹ s ∈ terminates_on g"

definition terminates :: "('a, 's) raw_generator ⇒ bool"
where "terminates g ⟷ (terminates_on g = UNIV)"

lemma terminatesI [intro?]:
"(⋀s. s ∈ terminates_on g) ⟹ terminates g"

lemma terminatesD:
"terminates g ⟹ s ∈ terminates_on g"

lemma terminates_on_stop:
"terminates_on (λ_. False, next) = UNIV"
by(auto intro: terminates_on.stop)

lemma wf_terminates:
assumes "wf R"
and step: "⋀s. fst g s ⟹ (snd (snd g s), s) ∈ R"
shows "terminates g"
proof(rule terminatesI)
fix s
from ‹wf R› show "s ∈ terminates_on g"
proof(induction rule: wf_induct[rule_format, consumes 1, case_names wf])
case (wf s)
show ?case
proof(cases "fst g s")
case True
hence "(snd (snd g s), s) ∈ R" by(rule step)
hence "snd (snd g s) ∈ terminates_on g" by(rule wf.IH)
with True show ?thesis by(rule terminates_on.unfold)
qed(rule terminates_on.stop)
qed
qed

lemma terminates_wfD:
assumes "terminates g"
shows "wf {(snd (snd g s), s) | s . fst g s}"
proof(rule wfUNIVI)
fix thesis s
assume wf [rule_format]: "∀s. (∀s'. (s', s) ∈ {(snd (snd g s), s) |s. fst g s} ⟶ thesis s') ⟶ thesis s"
from assms have "s ∈ terminates_on g" by(auto simp add: terminates_def)
thus "thesis s" by induct (auto intro: wf)
qed

lemma terminates_wfE:
assumes "terminates g"
obtains R where "wf R" "⋀s. fst g s ⟹ (snd (snd g s), s) ∈ R"
by(rule that)(rule terminates_wfD[OF assms], simp)

context fixes g :: "('a, 's) raw_generator" begin

partial_function (option) terminates_within :: "'s ⇒ nat option"
where
"terminates_within s =
(let (has_next, next) = g
in if has_next s then
map_option (λn. n + 1) (terminates_within (snd (next s)))
else Some 0)"

lemma terminates_on_conv_dom_terminates_within:
"terminates_on g = dom terminates_within"
proof(safe)
fix s
assume "s ∈ terminates_on g"
then show "∃n. terminates_within s = Some n"
next
fix s n
assume "terminates_within s = Some n"
then show "s ∈ terminates_on g"
by(induct rule: terminates_within.raw_induct[rotated 1, consumes 1])(auto simp add: split_beta split: if_split_asm intro: terminates_on.intros)
qed

end

lemma terminates_within_unfold:
"has_next s ⟹
terminates_within (has_next, next) s = map_option (λn. n + 1) (terminates_within (has_next, next) (snd (next s)))"

typedef ('a, 's) generator = "{g :: ('a, 's) raw_generator. terminates g}"
morphisms generator Generator
proof
show "(λ_. False, undefined) ∈ ?generator"
qed

setup_lifting type_definition_generator

lemma terminates_on_generator_eq_UNIV:
"terminates_on (generator g) = UNIV"

lemma terminates_within_stop:
"terminates_within (λ_. False, next) s = Some 0"

lemma terminates_within_generator_neq_None:
"terminates_within (generator g) s ≠ None"

locale list =
fixes g :: "('a, 's) generator" begin

definition has_next :: "'s ⇒ bool"
where "has_next = fst (generator g)"

definition "next" :: "'s ⇒ 'a × 's"
where "next = snd (generator g)"

function unfoldr :: "'s ⇒ 'a list"
where "unfoldr s = (if has_next s then let (a, s') = next s in a # unfoldr s' else [])"
by pat_completeness auto
termination
proof -
have "terminates (generator g)" using generator[of g] by simp
thus ?thesis
by(rule terminates_wfE)(erule "termination", metis has_next_def next_def snd_conv)
qed

declare unfoldr.simps [simp del]

lemma unfoldr_simps:
"has_next s ⟹ unfoldr s = fst (next s) # unfoldr (snd (next s))"
"¬ has_next s ⟹ unfoldr s = []"

end

declare
list.has_next_def[code]
list.next_def[code]
list.unfoldr.simps[code]

context includes lifting_syntax
begin

lemma generator_has_next_transfer [transfer_rule]:
"(pcr_generator (=) (=) ===> (=)) fst list.has_next"
by(auto simp add: generator.pcr_cr_eq cr_generator_def list.has_next_def dest: sym)

lemma generator_next_transfer [transfer_rule]:
"(pcr_generator (=) (=) ===> (=)) snd list.next"
by(auto simp add: generator.pcr_cr_eq cr_generator_def list.next_def)

end

lemma unfoldr_eq_Nil_iff [iff]:
"list.unfoldr g s = [] ⟷ ¬ list.has_next g s"

lemma Nil_eq_unfoldr_iff [simp]:
"[] = list.unfoldr g s ⟷ ¬ list.has_next g s"
by(auto intro: sym dest: sym)

subsection ‹Generators for @{typ "'a list"}›

primrec list_has_next :: "'a list ⇒ bool"
where
"list_has_next [] ⟷ False"
| "list_has_next (x # xs) ⟷ True"

primrec list_next :: "'a list ⇒ 'a × 'a list"
where
"list_next (x # xs) = (x, xs)"

lemma terminates_list_generator: "terminates (list_has_next, list_next)"
proof
fix xs
show "xs ∈ terminates_on (list_has_next, list_next)"
by(induct xs)(auto intro: terminates_on.intros)
qed

lift_definition list_generator :: "('a, 'a list) generator"
is "(list_has_next, list_next)"
by(rule terminates_list_generator)

lemma has_next_list_generator [simp]:
"list.has_next list_generator = list_has_next"
by transfer simp

lemma next_list_generator [simp]:
"list.next list_generator = list_next"
by transfer simp

lemma unfoldr_list_generator:
"list.unfoldr list_generator xs = xs"

lemma terminates_replicate_generator:
"terminates (λn :: nat. 0 < n, λn. (a, n - 1))"
by(rule wf_terminates)(lexicographic_order)

lift_definition replicate_generator :: "'a ⇒ ('a, nat) generator"
is "λa. (λn. 0 < n, λn. (a, n - 1))"
by(rule terminates_replicate_generator)

lemma has_next_replicate_generator [simp]:
"list.has_next (replicate_generator a) n ⟷ 0 < n"
by transfer simp

lemma next_replicate_generator [simp]:
"list.next (replicate_generator a) n = (a, n - 1)"
by transfer simp

lemma unfoldr_replicate_generator:
"list.unfoldr (replicate_generator a) n = replicate n a"

context fixes f :: "'a ⇒ 'b" begin

lift_definition map_generator :: "('a, 's) generator ⇒ ('b, 's) generator"
is "λ(has_next, next). (has_next, λs. let (a, s') = next s in (f a, s'))"
by(erule terminates_wfE)(erule wf_terminates, auto simp add: split_beta)

lemma has_next_map_generator [simp]:
"list.has_next (map_generator g) = list.has_next g"
by transfer clarsimp

lemma next_map_generator [simp]:
"list.next (map_generator g) = apfst f ∘ list.next g"
by transfer(simp add: fun_eq_iff split_beta apfst_def map_prod_def)

lemma unfoldr_map_generator:
"list.unfoldr (map_generator g) = map f ∘ list.unfoldr g"
(is "?lhs = ?rhs")
proof(rule ext)
fix s
show "?lhs s = ?rhs s"
by(induct s taking: "map_generator g" rule: list.unfoldr.induct)
(subst (1 2) list.unfoldr.simps, auto simp add: split_beta apfst_def map_prod_def)
qed

end

context fixes g1 :: "('a, 's1) raw_generator"
and g2 :: "('a, 's2) raw_generator"
begin

fun append_has_next :: "'s1 × 's2 + 's2 ⇒ bool"
where
"append_has_next (Inl (s1, s2)) ⟷ fst g1 s1 ∨ fst g2 s2"
| "append_has_next (Inr s2) ⟷ fst g2 s2"

fun append_next :: "'s1 × 's2 + 's2 ⇒ 'a × ('s1 × 's2 + 's2)"
where
"append_next (Inl (s1, s2)) =
(if fst g1 s1 then
let (x, s1') = snd g1 s1 in (x, Inl (s1', s2))
else append_next (Inr s2))"
| "append_next (Inr s2) = (let (x, s2') = snd g2 s2 in (x, Inr s2'))"

end

lift_definition append_generator :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ ('a, 's1 × 's2 + 's2) generator"
is "λg1 g2. (append_has_next g1 g2, append_next g1 g2)"
proof(rule terminatesI, safe)
fix has_next1 and next1 :: "'s1 ⇒ 'a × 's1"
and has_next2 and next2 :: "'s2 ⇒ 'a × 's2"
and s
assume t1: "terminates (has_next1, next1)"
and t2: "terminates (has_next2, next2)"
let ?has_next = "append_has_next (has_next1, next1) (has_next2, next2)"
let ?next = "append_next (has_next1, next1) (has_next2, next2)"
note [simp] = split_beta
and [intro] = terminates_on.intros
{ fix s2 :: 's2
from t2 have "s2 ∈ terminates_on (has_next2, next2)" by(rule terminatesD)
hence "Inr s2 ∈ terminates_on (?has_next, ?next)" by induct auto }
note Inr' = this

show "s ∈ terminates_on (?has_next, ?next)"
proof(cases s)
case Inr thus ?thesis by(simp add: Inr')
next
case (Inl s1s2)
moreover obtain s1 s2 where "s1s2 = (s1, s2)" by(cases s1s2)
ultimately have s: "s = Inl (s1, s2)" by simp
from t1 have "s1 ∈ terminates_on (has_next1, next1)" by(rule terminatesD)
thus ?thesis unfolding s
proof induct
case stop thus ?case
by(cases "has_next2 s2")(auto simp add: Inr')
qed auto
qed
qed

definition append_init :: "'s1 ⇒ 's2 ⇒ 's1 × 's2 + 's2"
where "append_init s1 s2 = Inl (s1, s2)"

lemma has_next_append_generator [simp]:
"list.has_next (append_generator g1 g2) (Inl (s1, s2)) ⟷
list.has_next g1 s1 ∨ list.has_next g2 s2"
"list.has_next (append_generator g1 g2) (Inr s2) ⟷ list.has_next g2 s2"
by(transfer, simp)+

lemma next_append_generator [simp]:
"list.next (append_generator g1 g2) (Inl (s1, s2)) =
(if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1 in (x, Inl (s1', s2))
else list.next (append_generator g1 g2) (Inr s2))"
"list.next (append_generator g1 g2) (Inr s2) = apsnd Inr (list.next g2 s2)"

lemma unfoldr_append_generator_Inr:
"list.unfoldr (append_generator g1 g2) (Inr s2) = list.unfoldr g2 s2"
by(induct s2 taking: g2 rule: list.unfoldr.induct)(subst (1 2) list.unfoldr.simps, auto split: prod.splits)

lemma unfoldr_append_generator_Inl:
"list.unfoldr (append_generator g1 g2) (Inl (s1, s2)) =
list.unfoldr g1 s1 @ list.unfoldr g2 s2"
apply(induct s1 taking: g1 rule: list.unfoldr.induct)
apply(subst (1 2 3) list.unfoldr.simps)
apply(auto split: prod.splits simp add: apsnd_def map_prod_def unfoldr_append_generator_Inr)
done

lemma unfoldr_append_generator:
"list.unfoldr (append_generator g1 g2) (append_init s1 s2) =
list.unfoldr g1 s1 @ list.unfoldr g2 s2"

lift_definition zip_generator :: "('a, 's1) generator ⇒ ('b, 's2) generator ⇒ ('a × 'b, 's1 × 's2) generator"
is "λ(has_next1, next1) (has_next2, next2).
(λ(s1, s2). has_next1 s1 ∧ has_next2 s2,
λ(s1, s2). let (x, s1') = next1 s1; (y, s2') = next2 s2
in ((x, y), (s1', s2')))"
proof(rule terminatesI, safe)
fix has_next1 next1 has_next2 next2 s1 s2
assume t1: "terminates (has_next1, next1)"
and t2: "terminates (has_next2, next2)"
have "s1 ∈ terminates_on (has_next1, next1)" "s2 ∈ terminates_on (has_next2, next2)"
using t1 t2 by(simp_all add: terminatesD)
thus "(s1, s2) ∈ terminates_on (λ(s1, s2). has_next1 s1 ∧ has_next2 s2, λ(s1, s2). let (x, s1') = next1 s1; (y, s2') = next2 s2 in ((x, y), (s1', s2')))"
by(induct arbitrary: s2)(auto 4 3 elim: terminates_on.cases intro: terminates_on.intros simp add: split_beta Let_def)
qed

abbreviation (input) zip_init :: "'s1 ⇒ 's2 ⇒ 's1 × 's2"
where "zip_init ≡ Pair"

lemma has_next_zip_generator [simp]:
"list.has_next (zip_generator g1 g2) (s1, s2) ⟷
list.has_next g1 s1 ∧ list.has_next g2 s2"
by transfer clarsimp

lemma next_zip_generator [simp]:
"list.next (zip_generator g1 g2) (s1, s2) =
((fst (list.next g1 s1), fst (list.next g2 s2)),
(snd (list.next g1 s1), snd (list.next g2 s2)))"

lemma unfoldr_zip_generator:
"list.unfoldr (zip_generator g1 g2) (zip_init s1 s2) =
zip (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
by(induct "(s1, s2)" arbitrary: s1 s2 taking: "zip_generator g1 g2" rule: list.unfoldr.induct)
(subst (1 2 3) list.unfoldr.simps, auto 9 2 simp add: split_beta)

context fixes bound :: nat begin

lift_definition upt_generator :: "(nat, nat) generator"
is "(λn. n < bound, λn. (n, Suc n))"
by(rule wf_terminates)(relation "measure (λn. bound - n)", auto)

lemma has_next_upt_generator [simp]:
"list.has_next upt_generator n ⟷ n < bound"
by transfer simp

lemma next_upt_generator [simp]:
"list.next upt_generator n = (n, Suc n)"
by transfer simp

lemma unfoldr_upt_generator:
"list.unfoldr upt_generator n = [n..<bound]"
by(induct "bound - n" arbitrary: n)(simp_all add: list.unfoldr_simps upt_conv_Cons)

end

context fixes bound :: int begin

lift_definition upto_generator :: "(int, int) generator"
is "(λn. n ≤ bound, λn. (n, n + 1))"
by(rule wf_terminates)(relation "measure (λn. nat (bound + 1 - n))", auto)

lemma has_next_upto_generator [simp]:
"list.has_next upto_generator n ⟷ n ≤ bound"
by transfer simp

lemma next_upto_generator [simp]:
"list.next upto_generator n = (n, n + 1)"
by transfer simp

lemma unfoldr_upto_generator:
"list.unfoldr upto_generator n = [n..bound]"
by(induct n taking: upto_generator rule: list.unfoldr.induct)(subst list.unfoldr.simps, subst upto.simps, auto)

end

context
fixes P :: "'a ⇒ bool"
begin

context
fixes g :: "('a, 's) raw_generator"
begin

inductive filter_has_next :: "'s ⇒ bool"
where
"⟦ fst g s; P (fst (snd g s)) ⟧ ⟹ filter_has_next s"
| "⟦ fst g s; ¬ P (fst (snd g s)); filter_has_next (snd (snd g s)) ⟧ ⟹ filter_has_next s"

partial_function (tailrec) filter_next :: "'s ⇒ 'a × 's"
where
"filter_next s = (let (x, s') = snd g s in if P x then (x, s') else filter_next s')"

end

lift_definition filter_generator :: "('a, 's) generator ⇒ ('a, 's) generator"
is "λg. (filter_has_next g, filter_next g)"
proof(rule wf_terminates)
fix g :: "('a, 's) raw_generator" and s
let ?R = "{(snd (snd g s), s) | s. fst g s}"
let ?g = "(filter_has_next g, filter_next g)"
assume "terminates g"
thus "wf (?R⇧+)" by(rule terminates_wfD[THEN wf_trancl])
assume "fst ?g s"
hence "filter_has_next g s" by simp
thus "(snd (snd ?g s), s) ∈ ?R⇧+"
by induct(subst filter_next.simps, auto simp add: split_beta filter_next.simps split del: if_split intro: trancl_into_trancl)
qed

lemma has_next_filter_generator:
"list.has_next (filter_generator g) s ⟷
list.has_next g s ∧ (let (x, s') = list.next g s in if P x then True else list.has_next (filter_generator g) s')"
apply(transfer)
apply simp
apply(subst filter_has_next.simps)
apply auto
done

lemma next_filter_generator:
"list.next (filter_generator g) s =
(let (x, s') = list.next g s
in if P x then (x, s') else list.next (filter_generator g) s')"
apply transfer
apply simp
apply(subst filter_next.simps)
apply(simp cong: if_cong)
done

lemma has_next_filter_generator_induct [consumes 1, case_names find step]:
assumes "list.has_next (filter_generator g) s"
and find: "⋀s. ⟦ list.has_next g s; P (fst (list.next g s)) ⟧ ⟹ Q s"
and step: "⋀s. ⟦ list.has_next g s; ¬ P (fst (list.next g s)); Q (snd (list.next g s)) ⟧ ⟹ Q s"
shows "Q s"
using assms by transfer(auto elim: filter_has_next.induct)

lemma filter_generator_empty_conv:
"list.has_next (filter_generator g) s ⟷ (∃x∈set (list.unfoldr g s). P x)" (is "?lhs ⟷ ?rhs")
proof
assume "?lhs"
thus ?rhs
proof(induct rule: has_next_filter_generator_induct)
case (find s)
thus ?case
by(cases "list.next g s")(subst list.unfoldr.simps, auto)
next
case (step s)
thus ?case
by(cases "list.next g s")(subst list.unfoldr.simps, auto)
qed
next
assume ?rhs
then obtain x where "x ∈ set (list.unfoldr g s)" "P x" by blast
thus ?lhs
proof(induct xs≡"list.unfoldr g s" arbitrary: s)
case Nil thus ?case by(simp del: Nil_eq_unfoldr_iff)
next
case (Cons x' xs)
from ‹x' # xs = list.unfoldr g s›[symmetric, simp]
have [simp]: "fst (list.next g s) = x' ∧ list.has_next g s ∧ list.unfoldr g (snd (list.next g s)) = xs"
by(subst (asm) list.unfoldr.simps)(simp add: split_beta split: if_split_asm)
from Cons.hyps(1)[of "snd (list.next g s)"] ‹x ∈ set (list.unfoldr g s)› ‹P x› show ?case
qed
qed

lemma unfoldr_filter_generator:
"list.unfoldr (filter_generator g) s = filter P (list.unfoldr g s)"
unfolding list_all2_eq
proof(coinduction arbitrary: s)
case Nil
thus ?case by(simp add: filter_empty_conv filter_generator_empty_conv)
next
case (Cons s)
hence "list.has_next (filter_generator g) s" by simp
thus ?case
proof(induction rule: has_next_filter_generator_induct)
case (find s)
thus ?case
apply(subst (1 2 3 5) list.unfoldr.simps)
apply(subst (1 2) has_next_filter_generator)
apply(subst next_filter_generator)
apply(rule disjI1 exI conjI refl)+
apply(subst next_filter_generator)
done
next
case (step s)
from step.hyps
have "list.unfoldr (filter_generator g) s = list.unfoldr (filter_generator g) (snd (list.next g s))"
apply(subst (1 2) list.unfoldr.simps)
apply(subst has_next_filter_generator)
apply(subst next_filter_generator)
done
moreover from step.hyps
have "filter P (list.unfoldr g (snd (list.next g s))) = filter P (list.unfoldr g s)"
by(subst (2) list.unfoldr.simps)(auto simp add: split_beta)
ultimately show ?case using step.IH by simp
qed
qed

end

subsection ‹Destroying lists›

definition hd_fusion :: "('a, 's) generator ⇒ 's ⇒ 'a"
where "hd_fusion g s = hd (list.unfoldr g s)"

lemma hd_fusion_code [code]:
"hd_fusion g s = (if list.has_next g s then fst (list.next g s) else undefined)"
unfolding hd_fusion_def

declare hd_fusion_def [symmetric, code_unfold]

definition fold_fusion :: "('a, 's) generator ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ 's ⇒ 'b ⇒ 'b"
where "fold_fusion g f s = fold f (list.unfoldr g s)"

lemma fold_fusion_code [code]:
"fold_fusion g f s b =
(if list.has_next g s then
let (x, s') = list.next g s
in fold_fusion g f s' (f x b)
else b)"
unfolding fold_fusion_def

declare fold_fusion_def[symmetric, code_unfold]

definition gen_length_fusion :: "('a, 's) generator ⇒ nat ⇒ 's ⇒ nat"
where "gen_length_fusion g n s = n + length (list.unfoldr g s)"

lemma gen_length_fusion_code [code]:
"gen_length_fusion g n s =
(if list.has_next g s then gen_length_fusion g (Suc n) (snd (list.next g s)) else n)"
unfolding gen_length_fusion_def

definition length_fusion :: "('a, 's) generator ⇒ 's ⇒ nat"
where "length_fusion g s = length (list.unfoldr g s)"

lemma length_fusion_code [code]:
"length_fusion g = gen_length_fusion g 0"

declare length_fusion_def[symmetric, code_unfold]

definition map_fusion :: "('a ⇒ 'b) ⇒ ('a, 's) generator ⇒ 's ⇒ 'b list"
where "map_fusion f g s = map f (list.unfoldr g s)"

lemma map_fusion_code [code]:
"map_fusion f g s =
(if list.has_next g s then
let (x, s') = list.next g s
in f x # map_fusion f g s'
else [])"
unfolding map_fusion_def

declare map_fusion_def[symmetric, code_unfold]

definition append_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ 'a list"
where "append_fusion g1 g2 s1 s2 = list.unfoldr g1 s1 @ list.unfoldr g2 s2"

lemma append_fusion [code]:
"append_fusion g1 g2 s1 s2 =
(if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1
in x # append_fusion g1 g2 s1' s2
else list.unfoldr g2 s2)"
unfolding append_fusion_def

declare append_fusion_def[symmetric, code_unfold]

definition zip_fusion :: "('a, 's1) generator ⇒ ('b, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ ('a × 'b) list"
where "zip_fusion g1 g2 s1 s2 = zip (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma zip_fusion_code [code]:
"zip_fusion g1 g2 s1 s2 =
(if list.has_next g1 s1 ∧ list.has_next g2 s2 then
let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in (x, y) # zip_fusion g1 g2 s1' s2'
else [])"
unfolding zip_fusion_def
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)

declare zip_fusion_def[symmetric, code_unfold]

definition list_all_fusion :: "('a, 's) generator ⇒ ('a ⇒ bool) ⇒ 's ⇒ bool"
where "list_all_fusion g P s = List.list_all P (list.unfoldr g s)"

lemma list_all_fusion_code [code]:
"list_all_fusion g P s ⟷
(list.has_next g s ⟶
(let (x, s') = list.next g s
in P x ∧ list_all_fusion g P s'))"
unfolding list_all_fusion_def

declare list_all_fusion_def[symmetric, code_unfold]

definition list_all2_fusion :: "('a ⇒ 'b ⇒ bool) ⇒ ('a, 's1) generator ⇒ ('b, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where
"list_all2_fusion P g1 g2 s1 s2 =
list_all2 P (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma list_all2_fusion_code [code]:
"list_all2_fusion P g1 g2 s1 s2 =
(if list.has_next g1 s1 then
list.has_next g2 s2 ∧
(let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in P x y ∧ list_all2_fusion P g1 g2 s1' s2')
else ¬ list.has_next g2 s2)"
unfolding list_all2_fusion_def
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)

declare list_all2_fusion_def[symmetric, code_unfold]

definition singleton_list_fusion :: "('a, 'state) generator ⇒ 'state ⇒ bool"
where "singleton_list_fusion gen state = (case list.unfoldr gen state of [_] ⇒ True | _ ⇒ False)"

lemma singleton_list_fusion_code [code]:
"singleton_list_fusion g s ⟷
list.has_next g s ∧ ¬ list.has_next g (snd (list.next g s))"
by(auto 4 5 simp add: singleton_list_fusion_def split: list.split if_split_asm prod.splits elim: list.unfoldr.elims dest: sym)

end


# Theory Lexicographic_Order

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

theory Lexicographic_Order imports
List_Fusion
"HOL-Library.Char_ord"
begin

hide_const (open) List.lexordp

section ‹List fusion for lexicographic order›

context linorder begin

lemma lexordp_take_index_conv:
"lexordp xs ys ⟷
(length xs < length ys ∧ take (length xs) ys = xs) ∨
(∃i < min (length xs) (length ys). take i xs = take i ys ∧ xs ! i < ys ! i)"
(is "?lhs = ?rhs")
proof
assume ?lhs thus ?rhs
by induct (auto 4 3 del: disjCI intro: disjI2 exI[where x="Suc i" for i])
next
assume ?rhs (is "?prefix ∨ ?less") thus ?lhs
proof
assume "?prefix"
hence "ys = xs @ hd (drop (length xs) ys) # tl (drop (length xs) ys)"
by (metis append_Nil2 append_take_drop_id less_not_refl list.collapse)
thus ?thesis unfolding lexordp_iff by blast
next
assume "?less"
then obtain i where "i < min (length xs) (length ys)"
and "take i xs = take i ys" and nth: "xs ! i < ys ! i" by blast
hence "xs = take i xs @ xs ! i # drop (Suc i) xs" "ys = take i xs @ ys ! i # drop (Suc i) ys"
by -(subst append_take_drop_id[symmetric, of _ i], simp_all add: Cons_nth_drop_Suc)
with nth show ?thesis unfolding lexordp_iff by blast
qed
qed

― ‹lexord is extension of partial ordering List.lex›
lemma lexordp_lex: "(xs, ys) ∈ lex {(xs, ys). xs < ys} ⟷ lexordp xs ys ∧ length xs = length ys"
proof(induct xs arbitrary: ys)
case Nil thus ?case by clarsimp
next
case Cons thus ?case by(cases ys)(simp_all, safe, simp)
qed

end

subsection ‹Setup for list fusion›

context ord begin

definition lexord_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where [code del]: "lexord_fusion g1 g2 s1 s2 = lexordp (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition lexord_eq_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where [code del]: "lexord_eq_fusion g1 g2 s1 s2 = lexordp_eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma lexord_fusion_code:
"lexord_fusion g1 g2 s1 s2 ⟷
(if list.has_next g1 s1 then
if list.has_next g2 s2 then
let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in x < y ∨ ¬ y < x ∧ lexord_fusion g1 g2 s1' s2'
else False
else list.has_next g2 s2)"
unfolding lexord_fusion_def
by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm)

lemma lexord_eq_fusion_code:
"lexord_eq_fusion g1 g2 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 x < y ∨ ¬ y < x ∧ lexord_eq_fusion g1 g2 s1' s2'))"
unfolding lexord_eq_fusion_def
by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm)

end

lemmas [code] =
lexord_fusion_code ord.lexord_fusion_code
lexord_eq_fusion_code ord.lexord_eq_fusion_code

lemmas [symmetric, code_unfold] =
lexord_fusion_def ord.lexord_fusion_def
lexord_eq_fusion_def ord.lexord_eq_fusion_def

end


# Theory Extend_Partial_Order

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

theory Extend_Partial_Order
imports Main
begin

section ‹Every partial order can be extended to a total order›

lemma ChainsD: "⟦ x ∈ C; C ∈ Chains r; y ∈ C ⟧ ⟹ (x, y) ∈ r ∨ (y, x) ∈ r"

lemma Chains_Field: "⟦ C ∈ Chains r; x ∈ C ⟧ ⟹ x ∈ Field r"

lemma total_onD:
"⟦ total_on A r; x ∈ A; y ∈ A ⟧ ⟹ (x, y) ∈ r ∨ x = y ∨ (y, x) ∈ r"
unfolding total_on_def by blast

lemma linear_order_imp_linorder: "linear_order {(A, B). leq A B} ⟹ class.linorder leq (λx y. leq x y ∧ ¬ leq y x)"
by(unfold_locales)(auto 4 4 simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD antisymD transD total_onD)

lemma (in linorder) linear_order: "linear_order {(A, B). A ≤ B}"
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def total_on_def intro: refl_onI antisymI transI)

definition order_consistent :: "('a × 'a) set ⇒ ('a × 'a) set ⇒ bool"
where "order_consistent r s ⟷ (∀a a'. (a, a') ∈ r ⟶ (a', a) ∈ s ⟶ a = a')"

lemma order_consistent_sym:
"order_consistent r s ⟹ order_consistent s r"

lemma antisym_order_consistent_self:
"antisym r ⟹ order_consistent r r"
by(auto simp add: order_consistent_def dest: antisymD)

lemma refl_on_trancl:
assumes "refl_on A r"
shows "refl_on A (r^+)"
proof(rule refl_onI, safe del: conjI)
fix a b
assume "(a, b) ∈ r^+"
thus "a ∈ A ∧ b ∈ A"
by induct(blast intro: refl_onD1[OF assms] refl_onD2[OF assms])+
qed(blast dest: refl_onD[OF assms])

lemma total_on_refl_on_consistent_into:
assumes r: "total_on A r" "refl_on A r"
and consist: "order_consistent r s"
and x: "x ∈ A" and y: "y ∈ A" and s: "(x, y) ∈ s"
shows "(x, y) ∈ r"
proof(cases "x = y")
case False
with r x y have "(x, y) ∈ r ∨ (y, x) ∈ r" unfolding total_on_def by blast
thus ?thesis
proof
assume "(y, x) ∈ r"
with s consist have "x = y" unfolding order_consistent_def by blast
with False show ?thesis by contradiction
qed
qed(blast intro: refl_onD r x y)

lemma porder_linorder_tranclpE [consumes 5, case_names base step]:
assumes r: "partial_order_on A r"
and s: "linear_order_on B s"
and consist: "order_consistent r s"
and B_subset_A: "B ⊆ A"
and trancl: "(x, y) ∈ (r ∪ s)^+"
obtains "(x, y) ∈ r"
| u v where "(x, u) ∈ r" "(u, v) ∈ s" "(v, y) ∈ r"
proof(atomize_elim)
from r have "refl_on A r" "trans r" by(simp_all add: partial_order_on_def preorder_on_def)
from s have "refl_on B s" "total_on B s" "trans s"

from trancl show "(x, y) ∈ r ∨ (∃u v. (x, u) ∈ r ∧ (u, v) ∈ s ∧ (v, y) ∈ r)"
proof(induction)
case (base y)
thus ?case
proof
assume "(x, y) ∈ s"
with ‹refl_on B s› have "x ∈ B" "y ∈ B"
by(blast dest: refl_onD1 refl_onD2)+
with B_subset_A have "x ∈ A" "y ∈ A" by blast+
hence "(x, x) ∈ r" "(y, y) ∈ r"
using ‹refl_on A r› by(blast intro: refl_onD)+
with ‹(x, y) ∈ s› show ?thesis by blast
qed(simp)
next
case (step y z)
from ‹(y, z) ∈ r ∪ s› show ?case
proof
assume "(y, z) ∈ s"
with ‹refl_on B s› have "y ∈ B" "z ∈ B"
by(blast dest: refl_onD2 refl_onD1)+
from step.IH show ?thesis
proof
assume "(x, y) ∈ r"
moreover from ‹z ∈ B› B_subset_A ‹refl_on A r›
have "(z, z) ∈ r" by(blast dest: refl_onD)
ultimately show ?thesis using ‹(y, z) ∈ s› by blast
next
assume "∃u v. (x, u) ∈ r ∧ (u, v) ∈ s ∧ (v, y) ∈ r"
then obtain u v where "(x, u) ∈ r" "(u, v) ∈ s" "(v, y) ∈ r" by blast
from ‹refl_on B s› ‹(u, v) ∈ s› have "v ∈ B" by(rule refl_onD2)
with ‹total_on B s› ‹refl_on B s› order_consistent_sym[OF consist]
have "(v, y) ∈ s" using ‹y ∈ B› ‹(v, y) ∈ r›
by(rule total_on_refl_on_consistent_into)
with ‹trans s› have "(v, z) ∈ s" using ‹(y, z) ∈ s› by(rule transD)
with ‹trans s› ‹(u, v) ∈ s› have "(u, z) ∈ s" by(rule transD)
moreover from ‹z ∈ B› B_subset_A have "z ∈ A" ..
with ‹refl_on A r› have "(z, z) ∈ r" by(rule refl_onD)
ultimately show ?thesis using ‹(x, u) ∈ r› by blast
qed
next
assume "(y, z) ∈ r"
with step.IH show ?thesis
by(blast intro: transD[OF ‹trans r›])
qed
qed
qed

lemma porder_on_consistent_linorder_on_trancl_antisym:
assumes r: "partial_order_on A r"
and s: "linear_order_on B s"
and consist: "order_consistent r s"
and B_subset_A: "B ⊆ A"
shows "antisym ((r ∪ s)^+)"
proof(rule antisymI)
fix x y
let ?rs = "(r ∪ s)^+"
assume "(x, y) ∈ ?rs" "(y, x) ∈ ?rs"
from r have "antisym r" "trans r" by(simp_all add: partial_order_on_def preorder_on_def)
from s have "total_on B s" "refl_on B s" "trans s" "antisym s"

from r s consist B_subset_A ‹(x, y) ∈ ?rs›
show "x = y"
proof(cases rule: porder_linorder_tranclpE)
case base
from r s consist B_subset_A ‹(y, x) ∈ ?rs›
show ?thesis
proof(cases rule: porder_linorder_tranclpE)
case base
with ‹antisym r› ‹(x, y) ∈ r› show ?thesis by(rule antisymD)
next
case (step u v)
from ‹(v, x) ∈ r› ‹(x, y) ∈ r› ‹(y, u) ∈ r› have "(v, u) ∈ r"
by(blast intro: transD[OF ‹trans r›])
with consist have "v = u" using ‹(u, v) ∈ s›
with ‹(y, u) ∈ r› ‹(v, x) ∈ r› have "(y, x) ∈ r"
by(blast intro: transD[OF ‹trans r›])
with ‹antisym r› ‹(x, y) ∈ r› show ?thesis by(rule antisymD)
qed
next
case (step u v)
from r s consist B_subset_A ‹(y, x) ∈ ?rs›
show ?thesis
proof(cases rule: porder_linorder_tranclpE)
case base
from ‹(v, y) ∈ r› ‹(y, x) ∈ r› ‹(x, u) ∈ r› have "(v, u) ∈ r"
by(blast intro: transD[OF ‹trans r›])
with consist ‹(u, v) ∈ s›
have "u = v" by(auto simp add: order_consistent_def)
with ‹(v, y) ∈ r› ‹(x, u) ∈ r› have "(x, y) ∈ r"
by(blast intro: transD[OF ‹trans r›])
with ‹antisym r› show ?thesis using ‹(y, x) ∈ r› by(rule antisymD)
next
case (step u' v')
note r_into_s = total_on_refl_on_consistent_into[OF ‹total_on B s› ‹refl_on B s› order_consistent_sym[OF consist]]
from ‹refl_on B s› ‹(u, v) ∈ s› ‹(u', v') ∈ s›
have "u ∈ B" "v ∈ B" "u' ∈ B" "v' ∈ B" by(blast dest: refl_onD1 refl_onD2)+
from ‹trans r› ‹(v', x) ∈ r› ‹(x, u) ∈ r› have "(v', u) ∈ r" by(rule transD)
with ‹v' ∈ B› ‹u ∈ B› have "(v', u) ∈ s" by(rule r_into_s)
also note ‹(u, v) ∈ s› also (transD[OF ‹trans s›])
from ‹trans r› ‹(v, y) ∈ r› ‹(y, u') ∈ r› have "(v, u') ∈ r" by(rule transD)
with ‹v ∈ B› ‹u' ∈ B› have "(v, u') ∈ s" by(rule r_into_s)
finally (transD[OF ‹trans s›])
have "v' = u'" using ‹(u', v') ∈ s› by(rule antisymD[OF ‹antisym s›])
moreover with ‹(v, u') ∈ s› ‹(v', u) ∈ s› have "(v, u) ∈ s"
by(blast intro: transD[OF ‹trans s›])
with ‹antisym s› ‹(u, v) ∈ s› have "u = v" by(rule antisymD)
ultimately have "(x, y) ∈ r" "(y, x) ∈ r"
using ‹(x, u) ∈ r› ‹(v, y) ∈ r› ‹(y, u') ∈ r› ‹(v', x) ∈ r›
by(blast intro: transD[OF ‹trans r›])+
with ‹antisym r› show ?thesis by(rule antisymD)
qed
qed
qed

lemma porder_on_linorder_on_tranclp_porder_onI:
assumes r: "partial_order_on A r"
and s: "linear_order_on B s"
and consist: "order_consistent r s"
and subset: "B ⊆ A"
shows "partial_order_on A ((r ∪ s)^+)"
unfolding partial_order_on_def preorder_on_def
proof(intro conjI)
let ?rs = "r ∪ s"
from r have "refl_on A r" by(simp add: partial_order_on_def preorder_on_def)
moreover from s have "refl_on B s"
ultimately have "refl_on (A ∪ B) ?rs" by(rule refl_on_Un)
also from subset have "A ∪ B = A" by blast
finally show "refl_on A (?rs^+)" by(rule refl_on_trancl)

show "trans (?rs^+)" by(rule trans_trancl)

from r s consist subset show "antisym (?rs^+)"
by(rule porder_on_consistent_linorder_on_trancl_antisym)
qed

lemma porder_extend_to_linorder:
assumes r: "partial_order_on A r"
obtains s where "linear_order_on A s" "order_consistent r s"
proof(atomize_elim)
define S where "S = {s. partial_order_on A s ∧ r ⊆ s}"
from r have r_in_S: "r ∈ S" unfolding S_def by auto

have "∃y∈S. ∀x∈S. y ⊆ x ⟶ x = y"
proof(rule Zorn_Lemma2[rule_format])
fix c
assume "c ∈ chains S"
hence "c ⊆ S" by(rule chainsD2)

show "∃y∈S. ∀x∈c. x ⊆ y"
proof(cases "c = {}")
case True
with r_in_S show ?thesis by blast
next
case False
then obtain s where "s ∈ c" by blast
hence s: "partial_order_on A s"
and r_in_s: "r ⊆ s"
using ‹c ⊆ S› unfolding S_def by blast+

have "partial_order_on A (⋃c)"
unfolding partial_order_on_def preorder_on_def
proof(intro conjI)
show "refl_on A (⋃c)"
proof(rule refl_onI[OF subsetI])
fix x
assume "x ∈ ⋃c"
then obtain X where "X ∈ c" and "x ∈ X" by blast
from ‹X ∈ c› ‹c ⊆ S› have "X ∈ S" ..
hence "partial_order_on A X" unfolding S_def by simp
with ‹x ∈ X› show "x ∈ A × A"
by(cases x)(auto simp add: partial_order_on_def preorder_on_def dest: refl_onD1 refl_onD2)
next
fix x
assume "x ∈ A"
with s have "(x, x) ∈ s" unfolding partial_order_on_def preorder_on_def
by(blast dest: refl_onD)
with ‹s ∈ c› show "(x, x) ∈ ⋃c" by(rule UnionI)
qed

show "antisym (⋃c)"
proof(rule antisymI)
fix x y
assume "(x, y) ∈ ⋃c" "(y, x) ∈ ⋃c"
then obtain X Y where "X ∈ c" "Y ∈ c" "(x, y) ∈ X" "(y, x) ∈ Y" by blast
from ‹X ∈ c› ‹Y ∈ c› ‹c ⊆ S› have "antisym X" "antisym Y"
unfolding S_def by(auto simp add: partial_order_on_def)
moreover from ‹c ∈ chains S› ‹X ∈ c› ‹Y ∈ c›
have "X ⊆ Y ∨ Y ⊆ X" by(rule chainsD)
ultimately show "x = y" using ‹(x, y) ∈ X› ‹(y, x) ∈ Y›
by(auto dest: antisymD)
qed

show "trans (⋃c)"
proof(rule transI)
fix x y z
assume "(x, y) ∈ ⋃c" "(y, z) ∈ ⋃c"
then obtain X Y where "X ∈ c" "Y ∈ c" "(x, y) ∈ X" "(y, z) ∈ Y" by blast
from ‹X ∈ c› ‹Y ∈ c› ‹c ⊆ S› have "trans X" "trans Y"
unfolding S_def by(auto simp add: partial_order_on_def preorder_on_def)
from ‹c ∈ chains S› ‹X ∈ c› ‹Y ∈ c›
have "X ⊆ Y ∨ Y ⊆ X" by(rule chainsD)
thus "(x, z) ∈ ⋃c"
proof
assume "X ⊆ Y"
with ‹trans Y› ‹(x, y) ∈ X› ‹(y, z) ∈ Y›
have "(x, z) ∈ Y" by(blast dest: transD)
with ‹Y ∈ c› show ?thesis by(rule UnionI)
next
assume "Y ⊆ X"
with ‹trans X› ‹(x, y) ∈ X› ‹(y, z) ∈ Y›
have "(x, z) ∈ X" by(blast dest: transD)
with ‹X ∈ c› show ?thesis by(rule UnionI)
qed
qed
qed
moreover
have "r ⊆ ⋃c" using r_in_s ‹s ∈ c› by blast
ultimately have "⋃c ∈ S" unfolding S_def by simp
thus ?thesis by blast
qed
qed
then obtain s where "s ∈ S" and y_max: "⋀t. ⟦ t ∈ S; s ⊆ t ⟧ ⟹ s = t" by blast

have "partial_order_on A s" using ‹s ∈ S›
unfolding S_def by simp
moreover
have r_in_s: "r ⊆ s" using ‹s ∈ S› unfolding S_def by blast

have "total_on A s"
unfolding total_on_def
proof(intro strip)
fix x y
assume "x ∈ A" "y ∈ A" "x ≠ y"
show "(x, y) ∈ s ∨ (y, x) ∈ s"
proof(rule ccontr)
assume "¬ ?thesis"
hence xy: "(x, y) ∉ s" "(y, x) ∉ s" by simp_all

define s' where "s' = {(a, b). a = x ∧ (b = y ∨ b = x) ∨ a = y ∧ b = y}"
let ?s' = "(s ∪ s')^+"
note ‹partial_order_on A s›
moreover have "linear_order_on {x, y} s'" unfolding s'_def
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def total_on_def intro: refl_onI transI antisymI)
moreover have "order_consistent s s'"
unfolding s'_def using xy unfolding order_consistent_def by blast
moreover have "{x, y} ⊆ A" using ‹x ∈ A› ‹y ∈ A› by blast
ultimately have "partial_order_on A ?s'"
by(rule porder_on_linorder_on_tranclp_porder_onI)
moreover have "r ⊆ ?s'" using r_in_s by auto
ultimately have "?s' ∈ S" unfolding S_def by simp
moreover have "s ⊆ ?s'" by auto
ultimately have "s = ?s'" by(rule y_max)
moreover have "(x, y) ∈ ?s'" by(auto simp add: s'_def)
ultimately show False using ‹(x, y) ∉ s› by simp
qed
qed
ultimately have "linear_order_on A s" by(simp add: linear_order_on_def)
moreover have "order_consistent r s" unfolding order_consistent_def
proof(intro strip)
fix a a'
assume "(a, a') ∈ r" "(a', a) ∈ s"
from ‹(a, a') ∈ r› have "(a, a') ∈ s" using r_in_s by blast
with ‹partial_order_on A s› ‹(a', a) ∈ s›
show "a = a'" unfolding partial_order_on_def by(blast dest: antisymD)
qed
ultimately show "∃s. linear_order_on A s ∧ order_consistent r s" by blast
qed

end


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

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

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"

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"

lemma set_less_aux_insert_same:
"x ∈ A ⟷ x ∈ B ⟹ insert x A ⊏' insert x B ⟷ A ⊏' B"

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"

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"

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

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"

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"

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"

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"

lemma infinite_set_less_eq_Complement:
"⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ A ⊑ - B"

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"
with A have A_eq: "A ∩ above ao = A"
from z_ao z B have B_eq: "B ∩ above ao = B"
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'"
note xxs = ‹sorted (x # xs)› ‹distinct (x # xs)›
hence xs: "sorted xs" "distinct xs" and x_Min: "∀x' ∈ set xs. x < x'"
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'"
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'"
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'"
note yys = ‹sorted (y # ys)› ‹distinct (y # ys)›
hence ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
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)"
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)"

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'"
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
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'"
from ‹sorted (y # ys)› ‹distinct (y # ys)›
have ys: "sorted ys" "distinct ys" and y: "∀y'∈set ys. y < y'"
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)"
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"
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"
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'"
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'"
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'"
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'"
from yys have ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"

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"
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))"
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"
with False xxs_above subset have "x ∈ A"
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}"
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"
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))"
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"

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"

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"
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"
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)"
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"
moreover have "?YS ≠ {}" using True y_Min yys_above ‹x = y›
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"
moreover have "?XS ≠ {}" using True x_Min xxs_above
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