# Theory Containers.Set_Impl

```(*  Title:      Containers/Set_Impl.thy
Author:     Andreas Lochbihler, KIT
René Thiemann, UIBK *)

theory Set_Impl imports
Collection_Enum
DList_Set
RBT_Set2
Closure_Set
Containers_Generator
Complex_Main
begin

section ‹Different implementations of sets›

subsection ‹Auxiliary functions›

text ‹A simple quicksort implementation›

context ord begin

function (sequential) quicksort_acc :: "'a list ⇒ 'a list ⇒ 'a list"
and quicksort_part :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ 'a list ⇒ 'a list"
where
"quicksort_acc ac [] = ac"
| "quicksort_acc ac [x] = x # ac"
| "quicksort_acc ac (x # xs) = quicksort_part ac x [] [] [] xs"
| "quicksort_part ac x lts eqs gts [] = quicksort_acc (eqs @ x # quicksort_acc ac gts) lts"
| "quicksort_part ac x lts eqs gts (z # zs) =
(if z > x then quicksort_part ac x lts eqs (z # gts) zs
else if z < x then quicksort_part ac x (z # lts) eqs gts zs
else quicksort_part ac x lts (z # eqs) gts zs)"
by pat_completeness simp_all

lemma length_quicksort_accp:
"quicksort_acc_quicksort_part_dom (Inl (ac, xs)) ⟹ length (quicksort_acc ac xs) = length ac + length xs"
and length_quicksort_partp:
"quicksort_acc_quicksort_part_dom (Inr (ac, x, lts, eqs, gts, zs))
⟹ length (quicksort_part ac x lts eqs gts zs) = length ac + 1 + length lts + length eqs + length gts + length zs"
apply(induct rule: quicksort_acc_quicksort_part.pinduct)
done

termination
apply(relation "measure (case_sum (λ(_, xs). 2 * length xs ^ 2) (λ(_, _, lts, eqs, gts, zs). 2 * (length lts + length eqs + length gts + length zs) ^ 2 + length zs + 1))")
done

definition quicksort :: "'a list ⇒ 'a list"
where "quicksort = quicksort_acc []"

lemma set_quicksort_acc [simp]: "set (quicksort_acc ac xs) = set ac ∪ set xs"
and set_quicksort_part [simp]:
"set (quicksort_part ac x lts eqs gts zs) =
set ac ∪ {x} ∪ set lts ∪ set eqs ∪ set gts ∪ set zs"
by(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct)(auto split: if_split_asm)

lemma set_quicksort [simp]: "set (quicksort xs) = set xs"

lemma distinct_quicksort_acc:
"distinct (quicksort_acc ac xs) = distinct (ac @ xs)"
and distinct_quicksort_part:
"distinct (quicksort_part ac x lts eqs gts zs) = distinct (ac @ [x] @ lts @ eqs @ gts @ zs)"
by(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) auto

lemma distinct_quicksort [simp]: "distinct (quicksort xs) = distinct xs"

end

lemmas [code] =
ord.quicksort_acc.simps quicksort_acc.simps
ord.quicksort_part.simps quicksort_part.simps
ord.quicksort_def quicksort_def

context linorder begin

lemma sorted_quicksort_acc:
"⟦ sorted ac; ∀x ∈ set xs. ∀a ∈ set ac. x < a ⟧
⟹ sorted (quicksort_acc ac xs)"
and sorted_quicksort_part:
"⟦ sorted ac; ∀y ∈ set lts ∪ {x} ∪ set eqs ∪ set gts ∪ set zs. ∀a ∈ set ac. y < a;
∀y ∈ set lts. y < x; ∀y ∈ set eqs. y = x; ∀y ∈ set gts. y > x ⟧
⟹ sorted (quicksort_part ac x lts eqs gts zs)"
proof(induction ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by(auto)
next
case 3 thus ?case by simp
next
case (4 ac x lts eqs gts)
note ac_greater = ‹∀y∈set lts ∪ {x} ∪ set eqs ∪ set gts ∪ set []. ∀a∈set ac. y < a›
have "sorted eqs" "set eqs ⊆ {x}" using ‹∀y∈set eqs. y = x›
by(induct eqs)(simp_all)
moreover have "∀y ∈ set ac ∪ set gts. x ≤ y"
using ‹∀a∈set gts. x < a› ac_greater by auto
moreover have "sorted (quicksort_acc ac gts)"
using ‹sorted ac› ac_greater by(auto intro: "4.IH")
ultimately have "sorted (eqs @ x # quicksort_acc ac gts)"
moreover have "∀y∈set lts. ∀a∈set (eqs @ x # quicksort_acc ac gts). y < a"
using ‹∀y∈set lts. y < x› ac_greater ‹∀a∈set gts. x < a› ‹∀y∈set eqs. y = x›
by fastforce
ultimately show ?case by(simp add: "4.IH")
next
case 5 thus ?case by(simp add: not_less order_eq_iff)
qed

lemma sorted_quicksort [simp]: "sorted (quicksort xs)"

lemma insort_key_append1:
"∀y ∈ set ys. f x < f y ⟹ insort_key f x (xs @ ys) = insort_key f x xs @ ys"
proof(induct xs)
case Nil
thus ?case by(cases ys) auto
qed simp

lemma insort_key_append2:
"∀y ∈ set xs. f x > f y ⟹ insort_key f x (xs @ ys) = xs @ insort_key f x ys"
by(induct xs) auto

lemma sort_key_append:
"∀x∈set xs. ∀y∈set ys. f x < f y ⟹ sort_key f (xs @ ys) = sort_key f xs @ sort_key f ys"

definition single_list :: "'a ⇒ 'a list" where "single_list a = [a]"

lemma to_single_list: "x # xs = single_list x @ xs"

lemma sort_snoc: "sort (xs @ [x]) = insort x (sort xs)"

lemma sort_append_swap: "sort (xs @ ys) = sort (ys @ xs)"
by(induct xs arbitrary: ys rule: rev_induct)(simp_all add: sort_snoc[symmetric])

lemma sort_append_swap2: "sort (xs @ ys @ zs) = sort (ys @ xs @ zs)"
by(induct xs)(simp_all, subst (1 2) sort_append_swap, simp)

lemma sort_Cons_append_swap: "sort (x # xs) = sort (xs @ [x])"
by(subst sort_append_swap) simp

lemma sort_append_Cons_swap: "sort (ys @ x # xs) = sort (ys @ xs @ [x])"
apply(induct ys)
apply(simp only: append.simps sort_Cons_append_swap)
apply simp
done

lemma quicksort_acc_conv_sort:
"quicksort_acc ac xs = sort xs @ ac"
and quicksort_part_conv_sort:
"⟦ ∀y ∈ set lts. y < x; ∀y ∈ set eqs. y = x; ∀y ∈ set gts. y > x ⟧
⟹ quicksort_part ac x lts eqs gts zs = sort (lts @ eqs @ gts @ x # zs) @ ac"
proof(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by simp
next
case 3 thus ?case by simp
next
case (4 ac x lts eqs gts)
note eqs = ‹∀y∈set eqs. y = x›
{ fix eqs
assume "∀y∈set eqs. y = x"
hence "insort x eqs = x # eqs" by(induct eqs) simp_all }
note [simp] = this
from eqs have [simp]: "sort eqs = eqs" by(induct eqs) simp_all
from eqs have [simp]: "eqs @ [x] = x # eqs" by(induct eqs) simp_all

show ?case using 4
apply(subst sort_key_append)
apply(auto 4 3 dest: bspec)[1]
apply(simp add: append_assoc[symmetric] sort_snoc del: append_assoc)
apply(subst sort_key_append)
apply(auto 4 3 simp add: insort_key_append1 dest: bspec)
done
next
case (5 ac x lts eqs gts z zs)
have "⟦ ¬ z < x; ¬ x < z ⟧ ⟹ z = x" by simp
thus ?case using 5
apply(simp del: sort_key_simps)
apply(safe, simp_all del: sort_key_simps add: to_single_list)
apply(subst sort_append_swap)
apply(fold append_assoc)
apply(subst (2) sort_append_swap)
apply(subst sort_append_swap2)
apply(unfold append_assoc)
apply(rule refl)
apply(subst (1 5) append_assoc[symmetric])
apply(subst (1 2) sort_append_swap)
apply(unfold append_assoc)
apply(subst sort_append_swap2)
apply(subst (1 2) sort_append_swap)
apply(unfold append_assoc)
apply(subst sort_append_swap2)
apply(rule refl)
apply(subst (2 6) append_assoc[symmetric])
apply(subst (2 5) append_assoc[symmetric])
apply(subst (1 2) sort_append_swap2)
apply(subst (4) append_assoc)
apply(subst (2) sort_append_swap2)
apply simp
done
qed

lemma quicksort_conv_sort: "quicksort xs = sort xs"

lemma sort_remdups: "sort (remdups xs) = remdups (sort xs)"
by(rule sorted_distinct_set_unique) simp_all

end

text ‹Removing duplicates from a sorted list›

context ord begin

fun remdups_sorted :: "'a list ⇒ 'a list"
where
"remdups_sorted [] = []"
| "remdups_sorted [x] = [x]"
| "remdups_sorted (x#y#xs) = (if x < y then x # remdups_sorted (y#xs) else remdups_sorted (y#xs))"

end

lemmas [code] = ord.remdups_sorted.simps

context linorder begin

lemma [simp]:
assumes "sorted xs"
shows sorted_remdups_sorted: "sorted (remdups_sorted xs)"
and set_remdups_sorted: "set (remdups_sorted xs) = set xs"
using assms by(induct xs rule: remdups_sorted.induct)(auto)

lemma distinct_remdups_sorted [simp]: "sorted xs ⟹ distinct (remdups_sorted xs)"
by(induct xs rule: remdups_sorted.induct)(auto)

lemma remdups_sorted_conv_remdups: "sorted xs ⟹ remdups_sorted xs = remdups xs"
by(induct xs rule: remdups_sorted.induct)(auto)

end

text ‹An specialised operation to convert a finite set into a sorted list›

definition csorted_list_of_set :: "'a :: ccompare set ⇒ 'a list"
where [code del]:
"csorted_list_of_set A =
(if ID CCOMPARE('a) = None ∨ ¬ finite A then undefined else linorder.sorted_list_of_set cless_eq A)"

lemma csorted_list_of_set_set [simp]:
"⟦ ID CCOMPARE('a :: ccompare) = Some c; linorder.sorted (le_of_comp c) xs; distinct xs ⟧
⟹ linorder.sorted_list_of_set (le_of_comp c) (set xs) = xs"
by(simp add: distinct_remdups_id linorder.sorted_list_of_set_sort_remdups[OF ID_ccompare] linorder.sorted_sort_id[OF ID_ccompare])

lemma csorted_list_of_set_split:
fixes A :: "'a :: ccompare set" shows
"P (csorted_list_of_set A) ⟷
(∀xs. ID CCOMPARE('a) ≠ None ⟶ finite A ⟶ A = set xs ⟶ distinct xs ⟶ linorder.sorted cless_eq xs ⟶ P xs) ∧
(ID CCOMPARE('a) = None ∨ ¬ finite A ⟶ P undefined)"
by(auto simp add: csorted_list_of_set_def linorder.sorted_list_of_set[OF ID_ccompare])

code_identifier code_module Set ⇀ (SML) Set_Impl
| code_module Set_Impl ⇀ (SML) Set_Impl

subsection ‹Delete code equation with set as constructor›

lemma is_empty_unfold [code_unfold]:
"set_eq A {} = Set.is_empty A"
"set_eq {} A = Set.is_empty A"

definition is_UNIV :: "'a set ⇒ bool"
where [code del]: "is_UNIV A ⟷ A = UNIV"

lemma is_UNIV_unfold [code_unfold]:
"A = UNIV ⟷ is_UNIV A"
"UNIV = A ⟷ is_UNIV A"
"set_eq A UNIV ⟷ is_UNIV A"
"set_eq UNIV A ⟷ is_UNIV A"

declare [[code drop:
Set.empty
Set.is_empty
uminus_set_inst.uminus_set
Set.member
Set.insert
Set.remove
UNIV
Set.filter
image
Set.subset_eq
Ball
Bex
Set.union
minus_set_inst.minus_set
Set.inter
card
Set.bind
the_elem
Pow
sum
Gcd
Lcm
Product_Type.product
Id_on
Image
trancl
relcomp
wf
Min
Inf_fin
Max
Sup_fin
"Inf :: 'a set set ⇒ 'a set"
"Sup :: 'a set set ⇒ 'a set"
sorted_list_of_set
List.map_project
Sup_pred_inst.Sup_pred
finite
card
Inf_pred_inst.Inf_pred
pred_of_set
Wellfounded.acc
Bleast
can_select
(* "set_eq :: 'a set ⇒ 'a set ⇒ bool" *)
irrefl_on
bacc
set_of_pred
set_of_seq
]]

subsection ‹Set implementations›

definition Collect_set :: "('a ⇒ bool) ⇒ 'a set"
where [simp]: "Collect_set = Collect"

definition DList_set :: "'a :: ceq set_dlist ⇒ 'a set"
where "DList_set = Collect o DList_Set.member"

definition RBT_set :: "'a :: ccompare set_rbt ⇒ 'a set"
where "RBT_set = Collect o RBT_Set2.member"

definition Complement :: "'a set ⇒ 'a set"
where [simp]: "Complement A = - A"

definition Set_Monad :: "'a list ⇒ 'a set"

code_datatype Collect_set DList_set RBT_set Set_Monad Complement

lemma DList_set_empty [simp]: "DList_set DList_Set.empty = {}"

lemma RBT_set_empty [simp]: "RBT_set RBT_Set2.empty = {}"

lemma RBT_set_conv_keys:
"ID CCOMPARE('a :: ccompare) ≠ None
⟹ RBT_set (t :: 'a set_rbt) = set (RBT_Set2.keys t)"

subsection ‹Set operations›

text ‹
A collection of all the theorems about @{const Complement}.
›
ML ‹
structure Set_Complement_Eqs = Named_Thms
(
val name = @{binding set_complement_code}
val description = "Code equations involving set complement"
)
›
setup ‹Set_Complement_Eqs.setup›

text ‹Various fold operations over sets›

typedef ('a, 'b) comp_fun_commute = "{f :: 'a ⇒ 'b ⇒ 'b. comp_fun_commute f}"
morphisms comp_fun_commute_apply Abs_comp_fun_commute
by(rule exI[where x="λ_. id"])(simp, unfold_locales, auto)

setup_lifting type_definition_comp_fun_commute

lemma comp_fun_commute_apply' [simp]:
"comp_fun_commute_on UNIV (comp_fun_commute_apply f)"
using comp_fun_commute_apply[of f] by (simp add: comp_fun_commute_def')

lift_definition set_fold_cfc :: "('a, 'b) comp_fun_commute ⇒ 'b ⇒ 'a set ⇒ 'b" is "Finite_Set.fold" .

declare [[code drop: set_fold_cfc]]

lemma set_fold_cfc_code [code]:
fixes xs :: "'a :: ceq list"
and dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt"
shows set_fold_cfc_Complement[set_complement_code]:
"set_fold_cfc f''' b (Complement A) = Code.abort (STR ''set_fold_cfc not supported on Complement'') (λ_. set_fold_cfc f''' b (Complement A))"
and
"set_fold_cfc f''' b (Collect_set P) = Code.abort (STR ''set_fold_cfc not supported on Collect_set'') (λ_. set_fold_cfc f''' b (Collect_set P))"
"set_fold_cfc f b (Set_Monad xs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''set_fold_cfc Set_Monad: ceq = None'') (λ_. set_fold_cfc f b (Set_Monad xs))
| Some eq ⇒ List.fold (comp_fun_commute_apply f) (equal_base.list_remdups eq xs) b)"
"set_fold_cfc f' b (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''set_fold_cfc DList_set: ceq = None'') (λ_. set_fold_cfc f' b (DList_set dxs))
| Some _ ⇒ DList_Set.fold (comp_fun_commute_apply f') dxs b)"
(is ?DList_set)
"set_fold_cfc f'' b (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''set_fold_cfc RBT_set: ccompare = None'') (λ_. set_fold_cfc f'' b (RBT_set rbt))
| Some _ ⇒ RBT_Set2.fold (comp_fun_commute_apply f'') rbt b)"
(is ?RBT_set)
proof -
note fold_set_fold_remdups = comp_fun_commute_def' comp_fun_commute_on.fold_set_fold_remdups[OF _ subset_UNIV]
by(auto split: option.split dest!: Collection_Eq.ID_ceq simp add: set_fold_cfc_def fold_set_fold_remdups)
show ?DList_set
apply(auto split: option.splits simp add: DList_set_def)
apply transfer
apply(auto dest: Collection_Eq.ID_ceq simp add: List.member_def[abs_def] fold_set_fold_remdups distinct_remdups_id)
done
show ?RBT_set
apply(auto split: option.split simp add: RBT_set_conv_keys fold_conv_fold_keys)
apply transfer
apply(simp add: fold_set_fold_remdups distinct_remdups_id linorder.distinct_keys[OF ID_ccompare] ord.is_rbt_rbt_sorted)
done
qed simp_all

typedef ('a, 'b) comp_fun_idem = "{f :: 'a ⇒ 'b ⇒ 'b. comp_fun_idem f}"
morphisms comp_fun_idem_apply Abs_comp_fun_idem
by(rule exI[where x="λ_. id"])(simp, unfold_locales, auto)

setup_lifting type_definition_comp_fun_idem

lemma comp_fun_idem_apply' [simp]:
"comp_fun_idem_on UNIV (comp_fun_idem_apply f)"
using comp_fun_idem_apply[of f] by (simp add: comp_fun_idem_def')

lift_definition set_fold_cfi :: "('a, 'b) comp_fun_idem ⇒ 'b ⇒ 'a set ⇒ 'b" is "Finite_Set.fold" .

declare [[code drop: set_fold_cfi]]

lemma set_fold_cfi_code [code]:
fixes xs :: "'a list"
and dxs :: "'b :: ceq set_dlist"
and rbt :: "'c :: ccompare set_rbt" shows
"set_fold_cfi f b (Complement A) = Code.abort (STR ''set_fold_cfi not supported on Complement'') (λ_. set_fold_cfi f b (Complement A))"
"set_fold_cfi f b (Collect_set P) = Code.abort (STR ''set_fold_cfi not supported on Collect_set'') (λ_. set_fold_cfi f b (Collect_set P))"
"set_fold_cfi f b (Set_Monad xs) = List.fold (comp_fun_idem_apply f) xs b"
"set_fold_cfi f' b (DList_set dxs) =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''set_fold_cfi DList_set: ceq = None'') (λ_. set_fold_cfi f' b (DList_set dxs))
| Some _ ⇒ DList_Set.fold (comp_fun_idem_apply f') dxs b)"
(is ?DList_set)
"set_fold_cfi f'' b (RBT_set rbt) =
(case ID CCOMPARE('c) of None ⇒ Code.abort (STR ''set_fold_cfi RBT_set: ccompare = None'') (λ_. set_fold_cfi f'' b (RBT_set rbt))
| Some _ ⇒ RBT_Set2.fold (comp_fun_idem_apply f'') rbt b)"
(is ?RBT_set)
proof -
by(auto split: option.split dest!: Collection_Eq.ID_ceq simp add: set_fold_cfi_def comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV])
show ?DList_set
apply(auto split: option.split simp add: DList_set_def)
apply transfer
apply(auto dest: Collection_Eq.ID_ceq simp add: List.member_def[abs_def] comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV])
done
show ?RBT_set
apply(auto split: option.split simp add: RBT_set_conv_keys fold_conv_fold_keys)
apply transfer
apply(simp add: comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV])
done
qed simp_all

typedef 'a semilattice_set = "{f :: 'a ⇒ 'a ⇒ 'a. semilattice_set f}"
morphisms semilattice_set_apply Abs_semilattice_set
proof
show "(λx y. if x = y then x else undefined) ∈ ?semilattice_set"
unfolding mem_Collect_eq by(unfold_locales) simp_all
qed

setup_lifting type_definition_semilattice_set

lemma semilattice_set_apply' [simp]:
"semilattice_set (semilattice_set_apply f)"
using semilattice_set_apply[of f] by simp

lemma comp_fun_idem_semilattice_set_apply [simp]:
"comp_fun_idem_on UNIV (semilattice_set_apply f)"
proof -
interpret semilattice_set "semilattice_set_apply f" by simp
show ?thesis by(unfold_locales)(simp_all add: fun_eq_iff left_commute)
qed

lift_definition set_fold1 :: "'a semilattice_set ⇒ 'a set ⇒ 'a" is "semilattice_set.F" .

lemma (in semilattice_set) F_set_conv_fold:
"xs ≠ [] ⟹ F (set xs) = Finite_Set.fold f (hd xs) (set (tl xs))"

lemma set_fold1_code [code]:
fixes rbt :: "'a :: {ccompare, lattice} set_rbt"
and dxs :: "'b :: {ceq, lattice} set_dlist" shows
set_fold1_Complement[set_complement_code]:
"set_fold1 f (Complement A) = Code.abort (STR ''set_fold1: Complement'') (λ_. set_fold1 f (Complement A))"
and "set_fold1 f (Collect_set P) = Code.abort (STR ''set_fold1: Collect_set'') (λ_. set_fold1 f (Collect_set P))"
and "set_fold1 f (Set_Monad (x # xs)) = fold (semilattice_set_apply f) xs x" (is "?Set_Monad")
and
"set_fold1 f' (DList_set dxs) =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''set_fold1 DList_set: ceq = None'') (λ_. set_fold1 f' (DList_set dxs))
| Some _ ⇒ if DList_Set.null dxs then Code.abort (STR ''set_fold1 DList_set: empty set'') (λ_. set_fold1 f' (DList_set dxs))
else DList_Set.fold (semilattice_set_apply f') (DList_Set.tl dxs) (DList_Set.hd dxs))"
(is "?DList_set")
and
"set_fold1 f'' (RBT_set rbt) =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''set_fold1 RBT_set: ccompare = None'') (λ_. set_fold1 f'' (RBT_set rbt))
| Some _ ⇒ if RBT_Set2.is_empty rbt then Code.abort (STR ''set_fold1 RBT_set: empty set'') (λ_. set_fold1 f'' (RBT_set rbt))
else RBT_Set2.fold1 (semilattice_set_apply f'') rbt)"
(is "?RBT_set")
proof -
note fold_set_fold = comp_fun_idem_def' comp_fun_idem_on.fold_set_fold[OF _ subset_UNIV]
show ?DList_set
by(simp add: set_fold1_def semilattice_set.F_set_conv_fold fold_set_fold DList_set_def DList_Set.Collect_member split: option.split)(transfer, simp)
show ?RBT_set
by(simp add: set_fold1_def semilattice_set.F_set_conv_fold fold_set_fold RBT_set_def RBT_Set2.member_conv_keys RBT_Set2.fold1_conv_fold split: option.split)
qed simp_all

text ‹Implementation of set operations›

lemma Collect_code [code]:
fixes P :: "'a :: cenum ⇒ bool" shows
"Collect P =
(case ID CENUM('a) of None ⇒ Collect_set P
| Some (enum, _) ⇒ Set_Monad (filter P enum))"
by(auto split: option.split dest: in_cenum)

lemma finite_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt"
and A :: "'c :: finite_UNIV set" and P :: "'c ⇒ bool" shows
"finite (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''finite DList_set: ceq = None'') (λ_. finite (DList_set dxs))
| Some _ ⇒ True)"
"finite (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''finite RBT_set: ccompare = None'') (λ_. finite (RBT_set rbt))
| Some _ ⇒ True)"
and finite_Complement [set_complement_code]:
"finite (Complement A) ⟷
(if of_phantom (finite_UNIV :: 'c finite_UNIV) then True
else if finite A then False
else Code.abort (STR ''finite Complement: infinite set'') (λ_. finite (Complement A)))"
and
"finite (Collect_set P) ⟷
of_phantom (finite_UNIV :: 'c finite_UNIV) ∨ Code.abort (STR ''finite Collect_set'') (λ_. finite (Collect_set P))"
by(auto simp add: DList_set_def RBT_set_def member_conv_keys card_gt_0_iff finite_UNIV split: option.split elim: finite_subset[rotated 1])

lemma CARD_code [code_unfold]:
"CARD('a :: card_UNIV) = of_phantom (card_UNIV :: 'a card_UNIV)"

lemma card_code [code]:
fixes dxs :: "'a :: ceq set_dlist" and xs :: "'a list"
and rbt :: "'b :: ccompare set_rbt"
and A :: "'c :: card_UNIV set" shows
"card (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''card DList_set: ceq = None'') (λ_. card (DList_set dxs))
| Some _ ⇒ DList_Set.length dxs)"
"card (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''card RBT_set: ccompare = None'') (λ_. card (RBT_set rbt))
| Some _ ⇒ length (RBT_Set2.keys rbt))"
(case ID CEQ('a) of None ⇒ Code.abort (STR ''card Set_Monad: ceq = None'') (λ_. card (Set_Monad xs))
| Some eq ⇒ length (equal_base.list_remdups eq xs))"
and card_Complement [set_complement_code]:
"card (Complement A) =
(let a = card A; s = CARD('c)
in if s > 0 then s - a
else if finite A then 0
else Code.abort (STR ''card Complement: infinite'') (λ_. card (Complement A)))"
by(auto simp add: RBT_set_def member_conv_keys distinct_card DList_set_def Let_def card_UNIV Compl_eq_Diff_UNIV card_Diff_subset_Int card_gt_0_iff finite_subset[of A UNIV] List.card_set dest: Collection_Eq.ID_ceq split: option.split)

lemma is_UNIV_code [code]:
fixes rbt :: "'a :: {cproper_interval, finite_UNIV} set_rbt"
and A :: "'b :: card_UNIV set" shows
"is_UNIV A ⟷
(let a = CARD('b);
b = card A
in if a > 0 then a = b
else if b > 0 then False
else Code.abort (STR ''is_UNIV called on infinite type and set'') (λ_. is_UNIV A))"
(is ?generic)
"is_UNIV (RBT_set rbt) =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''is_UNIV RBT_set: ccompare = None'') (λ_. is_UNIV (RBT_set rbt))
| Some _ ⇒ of_phantom (finite_UNIV :: 'a finite_UNIV) ∧ proper_intrvl.exhaustive_fusion cproper_interval rbt_keys_generator (RBT_Set2.init rbt))"
(is ?rbt)
proof -
{
fix c
assume linorder: "ID CCOMPARE('a) = Some c"
have "is_UNIV (RBT_set rbt) =
(finite (UNIV :: 'a set) ∧ proper_intrvl.exhaustive cproper_interval (RBT_Set2.keys rbt))"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
have "finite (UNIV :: 'a set)"
unfolding ‹?lhs›[unfolded is_UNIV_def, symmetric]
using linorder
moreover
hence "proper_intrvl.exhaustive cproper_interval (RBT_Set2.keys rbt)"
using linorder ‹?lhs›
by(simp add: linorder_proper_interval.exhaustive_correct[OF ID_ccompare_interval[OF linorder]] sorted_RBT_Set_keys is_UNIV_def RBT_set_conv_keys)
ultimately show ?rhs ..
next
assume ?rhs
thus ?lhs using linorder
by(auto simp add: linorder_proper_interval.exhaustive_correct[OF ID_ccompare_interval[OF linorder]] sorted_RBT_Set_keys is_UNIV_def RBT_set_conv_keys)
qed }
thus ?rbt
by(auto simp add: finite_UNIV proper_intrvl.exhaustive_fusion_def unfoldr_rbt_keys_generator is_UNIV_def split: option.split)

show ?generic
by(auto simp add: Let_def is_UNIV_def dest: card_seteq[of UNIV A] dest!: card_ge_0_finite)
qed

lemma is_empty_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt"
and A :: "'c set" shows
"Set.is_empty (Set_Monad xs) ⟷ xs = []"
"Set.is_empty (DList_set dxs) ⟷
(case ID CEQ('a) of None ⇒ Code.abort (STR ''is_empty DList_set: ceq = None'') (λ_. Set.is_empty (DList_set dxs))
| Some _ ⇒ DList_Set.null dxs)" (is ?DList_set)
"Set.is_empty (RBT_set rbt) ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''is_empty RBT_set: ccompare = None'') (λ_. Set.is_empty (RBT_set rbt))
| Some _ ⇒ RBT_Set2.is_empty rbt)" (is ?RBT_set)
and is_empty_Complement [set_complement_code]:
"Set.is_empty (Complement A) ⟷ is_UNIV A" (is ?Complement)
proof -
show ?DList_set
by(clarsimp simp add: DList_set_def Set.is_empty_def DList_Set.member_empty_empty split: option.split)

show ?RBT_set
by(clarsimp simp add: RBT_set_def Set.is_empty_def RBT_Set2.member_empty_empty[symmetric] fun_eq_iff simp del: RBT_Set2.member_empty_empty split: option.split)

show ?Complement

lemma Set_insert_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt" shows
"⋀x. Set.insert x (Collect_set A) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''insert Collect_set: ceq = None'') (λ_. Set.insert x (Collect_set A))
| Some eq ⇒ Collect_set (equal_base.fun_upd eq A x True))"
"⋀x. Set.insert x (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''insert DList_set: ceq = None'') (λ_. Set.insert x (DList_set dxs))
| Some _ ⇒ DList_set (DList_Set.insert x dxs))"
"⋀x. Set.insert x (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''insert RBT_set: ccompare = None'') (λ_. Set.insert x (RBT_set rbt))
| Some _ ⇒ RBT_set (RBT_Set2.insert x rbt))"
and insert_Complement [set_complement_code]:
"⋀x. Set.insert x (Complement X) = Complement (Set.remove x X)"
by(auto split: option.split dest: equal.equal_eq[OF ID_ceq] simp add: DList_set_def DList_Set.member_insert RBT_set_def)

lemma Set_member_code [code]:
fixes xs :: "'a :: ceq list" shows
"⋀x. x ∈ Collect_set A ⟷ A x"
"⋀x. x ∈ DList_set dxs ⟷ DList_Set.member dxs x"
"⋀x. x ∈ RBT_set rbt ⟷ RBT_Set2.member rbt x"
and mem_Complement [set_complement_code]:
"⋀x. x ∈ Complement X ⟷ x ∉ X"
and
"⋀x. x ∈ Set_Monad xs ⟷
(case ID CEQ('a) of None ⇒ Code.abort (STR ''member Set_Monad: ceq = None'') (λ_. x ∈ Set_Monad xs)
| Some eq ⇒ equal_base.list_member eq xs x)"
by(auto simp add: DList_set_def RBT_set_def List.member_def split: option.split dest!: Collection_Eq.ID_ceq)

lemma Set_remove_code [code]:
fixes rbt :: "'a :: ccompare set_rbt"
and dxs :: "'b :: ceq set_dlist" shows
"⋀x. Set.remove x (Collect_set A) =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''remove Collect: ceq = None'') (λ_. Set.remove x (Collect_set A))
| Some eq ⇒ Collect_set (equal_base.fun_upd eq A x False))"
"⋀x. Set.remove x (DList_set dxs) =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''remove DList_set: ceq = None'') (λ_. Set.remove x (DList_set dxs))
| Some _ ⇒ DList_set (DList_Set.remove x dxs))"
"⋀x. Set.remove x (RBT_set rbt) =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''remove RBT_set: ccompare = None'') (λ_. Set.remove x (RBT_set rbt))
| Some _ ⇒ RBT_set (RBT_Set2.remove x rbt))"
and remove_Complement [set_complement_code]:
"⋀x A. Set.remove x (Complement A) = Complement (Set.insert x A)"
by(auto split: option.split if_split_asm dest: equal.equal_eq[OF ID_ceq] simp add: DList_set_def DList_Set.member_remove RBT_set_def)

lemma Set_uminus_code [code, set_complement_code]:
"- A = Complement A"
"- (Collect_set P) = Collect_set (λx. ¬ P x)"
"- (Complement B) = B"
by auto

text ‹
These equations represent complements as true complements.
If you want that the complement operations returns an explicit enumeration of the elements, use the following set of equations which use @{class cenum}.
›

lemma Set_uminus_cenum:
fixes A :: "'a :: cenum set" shows
"- A =
(case ID CENUM('a) of None ⇒ Complement A
| Some (enum, _) ⇒ Set_Monad (filter (λx. x ∉ A) enum))"
and "- (Complement B) = B"
by(auto split: option.split dest: ID_cEnum)

lemma Set_minus_code [code]:
fixes rbt1 rbt2 :: "'a :: ccompare set_rbt"
shows "A - B = A ∩ (- B)"
"RBT_set rbt1 - RBT_set rbt2 =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''minus RBT_set RBT_set: ccompare = None'') (λ_. RBT_set rbt1 - RBT_set rbt2)
| Some _ ⇒ RBT_set (RBT_Set2.minus rbt1 rbt2))"
by (auto simp: Set_member_code(3) split: option.splits)

lemma Set_union_code [code]:
fixes rbt1 rbt2 :: "'a :: ccompare set_rbt"
and rbt :: "'b :: {ccompare, ceq} set_rbt"
and dxs :: "'b set_dlist"
and dxs1 dxs2 :: "'c :: ceq set_dlist" shows
"RBT_set rbt1 ∪ RBT_set rbt2 =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''union RBT_set RBT_set: ccompare = None'') (λ_. RBT_set rbt1 ∪ RBT_set rbt2)
| Some _ ⇒ RBT_set (RBT_Set2.union rbt1 rbt2))" (is ?RBT_set_RBT_set)
"RBT_set rbt ∪ DList_set dxs =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''union RBT_set DList_set: ccompare = None'') (λ_. RBT_set rbt ∪ DList_set dxs)
| Some _ ⇒
case ID CEQ('b) of None ⇒ Code.abort (STR ''union RBT_set DList_set: ceq = None'') (λ_. RBT_set rbt ∪ DList_set dxs)
| Some _ ⇒ RBT_set (DList_Set.fold RBT_Set2.insert dxs rbt))" (is ?RBT_set_DList_set)
"DList_set dxs ∪ RBT_set rbt =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''union DList_set RBT_set: ccompare = None'') (λ_. RBT_set rbt ∪ DList_set dxs)
| Some _ ⇒
case ID CEQ('b) of None ⇒ Code.abort (STR ''union DList_set RBT_set: ceq = None'') (λ_. RBT_set rbt ∪ DList_set dxs)
| Some _ ⇒ RBT_set (DList_Set.fold RBT_Set2.insert dxs rbt))" (is ?DList_set_RBT_set)
"DList_set dxs1 ∪ DList_set dxs2 =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''union DList_set DList_set: ceq = None'') (λ_. DList_set dxs1 ∪ DList_set dxs2)
| Some _ ⇒ DList_set (DList_Set.union dxs1 dxs2))" (is ?DList_set_DList_set)
"Set_Monad zs ∪ RBT_set rbt2 =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''union Set_Monad RBT_set: ccompare = None'') (λ_. Set_Monad zs ∪ RBT_set rbt2)
| Some _ ⇒ RBT_set (fold RBT_Set2.insert zs rbt2))" (is ?Set_Monad_RBT_set)
"RBT_set rbt1 ∪ Set_Monad zs =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''union RBT_set Set_Monad: ccompare = None'') (λ_. RBT_set rbt1 ∪ Set_Monad zs)
| Some _ ⇒ RBT_set (fold RBT_Set2.insert zs rbt1))" (is ?RBT_set_Set_Monad)
"Set_Monad ws ∪ DList_set dxs2 =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''union Set_Monad DList_set: ceq = None'') (λ_. Set_Monad ws ∪ DList_set dxs2)
| Some _ ⇒ DList_set (fold DList_Set.insert ws dxs2))" (is ?Set_Monad_DList_set)
"DList_set dxs1 ∪ Set_Monad ws =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''union DList_set Set_Monad: ceq = None'') (λ_. DList_set dxs1 ∪ Set_Monad ws)
| Some _ ⇒ DList_set (fold DList_Set.insert ws dxs1))" (is ?DList_set_Set_Monad)
"Collect_set A ∪ B = Collect_set (λx. A x ∨ x ∈ B)"
"B ∪ Collect_set A = Collect_set (λx. A x ∨ x ∈ B)"
and Set_union_Complement [set_complement_code]:
"Complement B ∪ B' = Complement (B ∩ - B')"
"B' ∪ Complement B = Complement (- B' ∩ B)"
proof -
by(auto split: option.split simp add: RBT_set_def)

show ?RBT_set_DList_set ?DList_set_RBT_set
by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.fold_def DList_Set.member_def List.member_def dest: equal.equal_eq[OF ID_ceq])

by(auto split: option.split simp add: DList_set_def DList_Set.member_fold_insert)

show ?DList_set_DList_set
by(auto split: option.split simp add: DList_set_def DList_Set.member_union)
qed(auto)

lemma Set_inter_code [code]:
fixes rbt1 rbt2 :: "'a :: ccompare set_rbt"
and rbt :: "'b :: {ccompare, ceq} set_rbt"
and dxs :: "'b set_dlist"
and dxs1 dxs2 :: "'c :: ceq set_dlist"
and xs1 xs2 :: "'c list"
shows
"Collect_set A'' ∩ J = Collect_set (λx. A'' x ∧ x ∈ J)" (is ?collect1)
"J ∩ Collect_set A'' = Collect_set (λx. A'' x ∧ x ∈ J)" (is ?collect2)

"DList_set dxs1 ∩ H =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''inter DList_set1: ceq = None'') (λ_. DList_set dxs1 ∩ H)
| Some eq ⇒ DList_set (DList_Set.filter (λx. x ∈ H) dxs1))" (is ?dlist1)
"H ∩ DList_set dxs2 =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''inter DList_set2: ceq = None'') (λ_. H ∩ DList_set dxs2)
| Some eq ⇒ DList_set (DList_Set.filter (λx. x ∈ H) dxs2))" (is ?dlist2)

"RBT_set rbt1 ∩ G =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''inter RBT_set1: ccompare = None'') (λ_. RBT_set rbt1 ∩ G)
| Some _ ⇒ RBT_set (RBT_Set2.filter (λx. x ∈ G) rbt1))" (is ?rbt1)
"G ∩ RBT_set rbt2 =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''inter RBT_set2: ccompare = None'') (λ_. G ∩ RBT_set rbt2)
| Some _ ⇒ RBT_set (RBT_Set2.filter (λx. x ∈ G) rbt2))" (is ?rbt2)
and Set_inter_Complement [set_complement_code]:
"Complement B'' ∩ Complement B''' = Complement (B'' ∪ B''')" (is ?complement)
and
"Set_Monad xs ∩ RBT_set rbt1 =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''inter Set_Monad RBT_set: ccompare = None'') (λ_. RBT_set rbt1 ∩ Set_Monad xs)
| Some _ ⇒ RBT_set (RBT_Set2.inter_list rbt1 xs))" (is ?monad_rbt)
"Set_Monad xs' ∩ DList_set dxs2 =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''inter Set_Monad DList_set: ceq = None'') (λ_. Set_Monad xs' ∩ DList_set dxs2)
| Some eq ⇒ DList_set (DList_Set.filter (equal_base.list_member eq xs') dxs2))" (is ?monad_dlist)
| Some eq ⇒ Set_Monad (filter (equal_base.list_member eq xs2) xs1))" (is ?monad)

"DList_set dxs ∩ RBT_set rbt =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''inter DList_set RBT_set: ccompare = None'') (λ_. DList_set dxs ∩ RBT_set rbt)
| Some _ ⇒
case ID CEQ('b) of None ⇒ Code.abort (STR ''inter DList_set RBT_set: ceq = None'') (λ_. DList_set dxs ∩ RBT_set rbt)
| Some _ ⇒ RBT_set (RBT_Set2.inter_list rbt (list_of_dlist dxs)))" (is ?dlist_rbt)
"DList_set dxs1 ∩ DList_set dxs2 =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''inter DList_set DList_set: ceq = None'') (λ_. DList_set dxs1 ∩ DList_set dxs2)
| Some _ ⇒ DList_set (DList_Set.filter (DList_Set.member dxs2) dxs1))" (is ?dlist)
"DList_set dxs1 ∩ Set_Monad xs' =
(case ID CEQ('c) of None ⇒ Code.abort (STR ''inter DList_set Set_Monad: ceq = None'') (λ_. DList_set dxs1 ∩ Set_Monad xs')
| Some eq ⇒ DList_set (DList_Set.filter (equal_base.list_member eq xs') dxs1))" (is ?dlist_monad)

"RBT_set rbt1 ∩ RBT_set rbt2 =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''inter RBT_set RBT_set: ccompare = None'') (λ_. RBT_set rbt1 ∩ RBT_set rbt2)
| Some _ ⇒ RBT_set (RBT_Set2.inter rbt1 rbt2))" (is ?rbt_rbt)
"RBT_set rbt ∩ DList_set dxs =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''inter RBT_set DList_set: ccompare = None'') (λ_. RBT_set rbt ∩ DList_set dxs)
| Some _ ⇒
case ID CEQ('b) of None ⇒ Code.abort (STR ''inter RBT_set DList_set: ceq = None'') (λ_. RBT_set rbt ∩ DList_set dxs)
| Some _ ⇒ RBT_set (RBT_Set2.inter_list rbt (list_of_dlist dxs)))" (is ?rbt_dlist)
"RBT_set rbt1 ∩ Set_Monad xs =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''inter RBT_set Set_Monad: ccompare = None'') (λ_. RBT_set rbt1 ∩ Set_Monad xs)
| Some _ ⇒ RBT_set (RBT_Set2.inter_list rbt1 xs))" (is ?rbt_monad)
proof -
by(auto simp add: RBT_set_def DList_set_def DList_Set.member_def List.member_def dest: equal.equal_eq[OF ID_ceq] split: option.split)
by(auto simp add: DList_set_def List.member_def dest!: Collection_Eq.ID_ceq split: option.splits)
qed

lemma Set_bind_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt" shows
"Set.bind (DList_set dxs) f' =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''bind DList_set: ceq = None'') (λ_. Set.bind (DList_set dxs) f')
| Some _ ⇒ DList_Set.fold (union ∘ f') dxs {})" (is ?DList)
"Set.bind (RBT_set rbt) f'' =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''bind RBT_set: ccompare = None'') (λ_. Set.bind (RBT_set rbt) f'')
| Some _ ⇒ RBT_Set2.fold (union ∘ f'') rbt {})" (is ?RBT)
proof -
show ?DList by(auto simp add: DList_set_def DList_Set.member_def List.member_def List.member_def[abs_def] set_bind_conv_fold DList_Set.fold_def split: option.split dest: equal.equal_eq[OF ID_ceq] ID_ceq)
show ?RBT by(clarsimp split: option.split simp add: RBT_set_def RBT_Set2.fold_conv_fold_keys RBT_Set2.member_conv_keys set_bind_conv_fold)
qed

lemma UNIV_code [code]: "UNIV = - {}"
by(simp)

lift_definition inf_sls :: "'a :: lattice semilattice_set" is "inf" by unfold_locales

lemma Inf_fin_code [code]: "Inf_fin A = set_fold1 inf_sls A"

lift_definition sup_sls :: "'a :: lattice semilattice_set" is "sup" by unfold_locales

lemma Sup_fin_code [code]: "Sup_fin A = set_fold1 sup_sls A"

lift_definition inf_cfi :: "('a :: lattice, 'a) comp_fun_idem" is "inf"
by(rule comp_fun_idem_inf)

lemma Inf_code:
fixes A :: "'a :: complete_lattice set" shows
"Inf A = (if finite A then set_fold_cfi inf_cfi top A else Code.abort (STR ''Inf: infinite'') (λ_. Inf A))"

lift_definition sup_cfi :: "('a :: lattice, 'a) comp_fun_idem" is "sup"
by(rule comp_fun_idem_sup)

lemma Sup_code:
fixes A :: "'a :: complete_lattice set" shows
"Sup A = (if finite A then set_fold_cfi sup_cfi bot A else Code.abort (STR ''Sup: infinite'') (λ_. Sup A))"

lemmas Inter_code [code] = Inf_code[where ?'a = "_ :: type set"]
lemmas Union_code [code] = Sup_code[where ?'a = "_ :: type set"]
lemmas Predicate_Inf_code [code] = Inf_code[where ?'a = "_ :: type Predicate.pred"]
lemmas Predicate_Sup_code [code] = Sup_code[where ?'a = "_ :: type Predicate.pred"]
lemmas Inf_fun_code [code] = Inf_code[where ?'a = "_ :: type ⇒ _ :: complete_lattice"]
lemmas Sup_fun_code [code] = Sup_code[where ?'a = "_ :: type ⇒ _ :: complete_lattice"]

lift_definition min_sls :: "'a :: linorder semilattice_set" is min by unfold_locales

lemma Min_code [code]: "Min A = set_fold1 min_sls A"

lift_definition max_sls :: "'a :: linorder semilattice_set" is max by unfold_locales

lemma Max_code [code]: "Max A = set_fold1 max_sls A"

text ‹
We do not implement @{term Ball}, @{term Bex}, and @{term sorted_list_of_set} for @{term Collect_set} using @{term cEnum},
because it should already have been converted to an explicit list of elements if that is possible.
›

lemma Ball_code [code]:
fixes rbt :: "'a :: ccompare set_rbt"
and dxs :: "'b :: ceq set_dlist" shows
"Ball (Set_Monad xs) P = list_all P xs"
"Ball (DList_set dxs) P' =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''Ball DList_set: ceq = None'') (λ_. Ball (DList_set dxs) P')
| Some _ ⇒ DList_Set.dlist_all P' dxs)"
"Ball (RBT_set rbt) P'' =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''Ball RBT_set: ccompare = None'') (λ_. Ball (RBT_set rbt) P'')
| Some _ ⇒ RBT_Set2.all P'' rbt)"
by(simp_all add: DList_set_def RBT_set_def list_all_iff dlist_all_conv_member RBT_Set2.all_conv_all_member split: option.splits)

lemma Bex_code [code]:
fixes rbt :: "'a :: ccompare set_rbt"
and dxs :: "'b :: ceq set_dlist" shows
"Bex (Set_Monad xs) P = list_ex P xs"
"Bex (DList_set dxs) P' =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''Bex DList_set: ceq = None'') (λ_. Bex (DList_set dxs) P')
| Some _ ⇒ DList_Set.dlist_ex P' dxs)"
"Bex (RBT_set rbt) P'' =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''Bex RBT_set: ccompare = None'') (λ_. Bex (RBT_set rbt) P'')
| Some _ ⇒ RBT_Set2.ex P'' rbt)"
by(simp_all add: DList_set_def RBT_set_def list_ex_iff dlist_ex_conv_member RBT_Set2.ex_conv_ex_member split: option.splits)

lemma csorted_list_of_set_code [code]:
fixes rbt :: "'a :: ccompare set_rbt"
and dxs :: "'b :: {ccompare, ceq} set_dlist"
and xs :: "'a :: ccompare list" shows
"csorted_list_of_set (RBT_set rbt) =
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''csorted_list_of_set RBT_set: ccompare = None'') (λ_. csorted_list_of_set (RBT_set rbt))
| Some _ ⇒ RBT_Set2.keys rbt)"
"csorted_list_of_set (DList_set dxs) =
(case ID CEQ('b) of None ⇒ Code.abort (STR ''csorted_list_of_set DList_set: ceq = None'') (λ_. csorted_list_of_set (DList_set dxs))
| Some _ ⇒
case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''csorted_list_of_set DList_set: ccompare = None'') (λ_. csorted_list_of_set (DList_set dxs))
| Some c ⇒ ord.quicksort (lt_of_comp c) (list_of_dlist dxs))"
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''csorted_list_of_set Set_Monad: ccompare = None'') (λ_. csorted_list_of_set (Set_Monad xs))
| Some c ⇒ ord.remdups_sorted (lt_of_comp c) (ord.quicksort (lt_of_comp c) xs))"
by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.Collect_member member_conv_keys sorted_RBT_Set_keys linorder.sorted_list_of_set_sort_remdups[OF ID_ccompare] linorder.quicksort_conv_sort[OF ID_ccompare] distinct_remdups_id distinct_list_of_dlist linorder.remdups_sorted_conv_remdups[OF ID_ccompare] linorder.sorted_sort[OF ID_ccompare] linorder.sort_remdups[OF ID_ccompare] csorted_list_of_set_def)

lemma cless_set_code [code]:
fixes rbt rbt' :: "'a :: ccompare set_rbt"
and rbt1 rbt2 :: "'b :: cproper_interval set_rbt"
and A B :: "'a set"
and A' B' :: "'b set" shows
"cless_set A B ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cless_set: ccompare = None'') (λ_. cless_set A B)
| Some c ⇒
if finite A ∧ finite B then ord.lexordp (λx y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B)
else Code.abort (STR ''cless_set: infinite set'') (λ_. cless_set A B))"
(is "?fin_fin")
and cless_set_Complement2 [set_complement_code]:
"cless_set A' (Complement B') ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_set Complement2: ccompare = None'') (λ_. cless_set A' (Complement B'))
| Some c ⇒
if finite A' ∧ finite B' then
finite (UNIV :: 'b set) ⟶
proper_intrvl.set_less_aux_Compl (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B')
else Code.abort (STR ''cless_set Complement2: infinite set'') (λ_. cless_set A' (Complement B')))"
(is "?fin_Compl_fin")
and cless_set_Complement1 [set_complement_code]:
"cless_set (Complement A') B' ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_set Complement1: ccompare = None'') (λ_. cless_set (Complement A') B')
| Some c ⇒
if finite A' ∧ finite B' then
finite (UNIV :: 'b set) ∧
proper_intrvl.Compl_set_less_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B')
else Code.abort (STR ''cless_set Complement1: infinite set'') (λ_. cless_set (Complement A') B'))"
(is "?Compl_fin_fin")
and cless_set_Complement12 [set_complement_code]:
"cless_set (Complement A) (Complement B) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cless_set Complement Complement: ccompare = None'') (λ_. cless_set (Complement A) (Complement B))
| Some _ ⇒ cless B A)" (is ?Compl_Compl)
and
"cless_set (RBT_set rbt) (RBT_set rbt') ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cless_set RBT_set RBT_set: ccompare = None'') (λ_. cless_set (RBT_set rbt) (RBT_set rbt'))
| Some c ⇒ ord.lexord_fusion (λx y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))"
(is ?rbt_rbt)
and cless_set_rbt_Complement2 [set_complement_code]:
"cless_set (RBT_set rbt1) (Complement (RBT_set rbt2)) ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_set RBT_set (Complement RBT_set): ccompare = None'') (λ_. cless_set (RBT_set rbt1) (Complement (RBT_set rbt2)))
| Some c ⇒
finite (UNIV :: 'b set) ⟶
proper_intrvl.set_less_aux_Compl_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?rbt_Compl)
and cless_set_rbt_Complement1 [set_complement_code]:
"cless_set (Complement (RBT_set rbt1)) (RBT_set rbt2) ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_set (Complement RBT_set) RBT_set: ccompare = None'') (λ_. cless_set (Complement (RBT_set rbt1)) (RBT_set rbt2))
| Some c ⇒
finite (UNIV :: 'b set) ∧
proper_intrvl.Compl_set_less_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?Compl_rbt)
proof -
note [split] = option.split csorted_list_of_set_split
and [simp] =
le_of_comp_of_ords_linorder[OF ID_ccompare]
lt_of_comp_of_ords
finite_subset[OF subset_UNIV] ccompare_set_def ID_Some
ord.lexord_fusion_def
proper_intrvl.Compl_set_less_aux_fusion_def
proper_intrvl.set_less_aux_Compl_fusion_def
unfoldr_rbt_keys_generator
RBT_set_def sorted_RBT_Set_keys member_conv_keys
linorder.set_less_finite_iff[OF ID_ccompare]
linorder.set_less_aux_code[OF ID_ccompare, symmetric]
linorder.Compl_set_less_Compl[OF ID_ccompare]
linorder.infinite_set_less_Complement[OF ID_ccompare]
linorder.infinite_Complement_set_less[OF ID_ccompare]
linorder_proper_interval.set_less_aux_Compl2_conv_set_less_aux_Compl[OF ID_ccompare_interval, symmetric]
linorder_proper_interval.Compl1_set_less_aux_conv_Compl_set_less_aux[OF ID_ccompare_interval, symmetric]

show ?Compl_Compl by simp
show ?rbt_rbt
by auto
show ?rbt_Compl by(cases "finite (UNIV :: 'b set)") auto
show ?Compl_rbt by(cases "finite (UNIV :: 'b set)") auto
show ?fin_fin by auto
show ?fin_Compl_fin by(cases "finite (UNIV :: 'b set)", auto)
show ?Compl_fin_fin by(cases "finite (UNIV :: 'b set)") auto
qed

lemma le_of_comp_set_less_eq:
"le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le"
by (rule le_of_comp_of_ords_gen, simp add: ord.set_less_def)

lemma cless_eq_set_code [code]:
fixes rbt rbt' :: "'a :: ccompare set_rbt"
and rbt1 rbt2 :: "'b :: cproper_interval set_rbt"
and A B :: "'a set"
and A' B' :: "'b set" shows
"cless_eq_set A B ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cless_eq_set: ccompare = None'') (λ_. cless_eq_set A B)
| Some c ⇒
if finite A ∧ finite B then
ord.lexordp_eq (λx y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B)
else Code.abort (STR ''cless_eq_set: infinite set'') (λ_. cless_eq_set A B))"
(is "?fin_fin")
and cless_eq_set_Complement2 [set_complement_code]:
"cless_eq_set A' (Complement B') ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_eq_set Complement2: ccompare = None'') (λ_. cless_eq_set A' (Complement B'))
| Some c ⇒
if finite A' ∧ finite B' then
finite (UNIV :: 'b set) ⟶
proper_intrvl.set_less_eq_aux_Compl (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B')
else Code.abort (STR ''cless_eq_set Complement2: infinite set'') (λ_. cless_eq_set A' (Complement B')))"
(is "?fin_Compl_fin")
and cless_eq_set_Complement1 [set_complement_code]:
"cless_eq_set (Complement A') B' ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_eq_set Complement1: ccompare = None'') (λ_. cless_eq_set (Complement A') B')
| Some c ⇒
if finite A' ∧ finite B' then
finite (UNIV :: 'b set) ∧
proper_intrvl.Compl_set_less_eq_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B')
else Code.abort (STR ''cless_eq_set Complement1: infinite set'') (λ_. cless_eq_set (Complement A') B'))"
(is "?Compl_fin_fin")
and cless_eq_set_Complement12 [set_complement_code]:
"cless_eq_set (Complement A) (Complement B) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cless_eq_set Complement Complement: ccompare = None'') (λ_. cless_eq (Complement A) (Complement B))
| Some c ⇒ cless_eq_set B A)"
(is ?Compl_Compl)

"cless_eq_set (RBT_set rbt) (RBT_set rbt') ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cless_eq_set RBT_set RBT_set: ccompare = None'') (λ_. cless_eq_set (RBT_set rbt) (RBT_set rbt'))
| Some c ⇒ ord.lexord_eq_fusion (λx y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))"
(is ?rbt_rbt)
and cless_eq_set_rbt_Complement2 [set_complement_code]:
"cless_eq_set (RBT_set rbt1) (Complement (RBT_set rbt2)) ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_eq_set RBT_set (Complement RBT_set): ccompare = None'') (λ_. cless_eq_set (RBT_set rbt1) (Complement (RBT_set rbt2)))
| Some c ⇒
finite (UNIV :: 'b set) ⟶
proper_intrvl.set_less_eq_aux_Compl_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?rbt_Compl)
and cless_eq_set_rbt_Complement1 [set_complement_code]:
"cless_eq_set (Complement (RBT_set rbt1)) (RBT_set rbt2) ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''cless_eq_set (Complement RBT_set) RBT_set: ccompare = None'') (λ_. cless_eq_set (Complement (RBT_set rbt1)) (RBT_set rbt2))
| Some c ⇒
finite (UNIV :: 'b set) ∧
proper_intrvl.Compl_set_less_eq_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?Compl_rbt)
proof -
note [split] = option.split csorted_list_of_set_split
and [simp] =
le_of_comp_set_less_eq
finite_subset[OF subset_UNIV] ccompare_set_def ID_Some
ord.lexord_eq_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def
proper_intrvl.set_less_eq_aux_Compl_fusion_def
unfoldr_rbt_keys_generator
RBT_set_def sorted_RBT_Set_keys member_conv_keys
linorder.set_less_eq_finite_iff[OF ID_ccompare]
linorder.set_less_eq_aux_code[OF ID_ccompare, symmetric]
linorder.Compl_set_less_eq_Compl[OF ID_ccompare]
linorder.infinite_set_less_eq_Complement[OF ID_ccompare]
linorder.infinite_Complement_set_less_eq[OF ID_ccompare]
linorder_proper_interval.set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl[OF ID_ccompare_interval, symmetric]
linorder_proper_interval.Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux[OF ID_ccompare_interval, symmetric]

show ?Compl_Compl by simp
show ?rbt_rbt

by auto
show ?rbt_Compl by(cases "finite (UNIV :: 'b set)") auto
show ?Compl_rbt by(cases "finite (UNIV :: 'b set)") auto
show ?fin_fin by auto
show ?fin_Compl_fin by (cases "finite (UNIV :: 'b set)", auto)
show ?Compl_fin_fin by(cases "finite (UNIV :: 'b set)") auto
qed

lemma cproper_interval_set_Some_Some_code [code]:
fixes rbt1 rbt2 :: "'a :: cproper_interval set_rbt"
and A B :: "'a set" shows

"cproper_interval (Some A) (Some B) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval: ccompare = None'') (λ_. cproper_interval (Some A) (Some B))
| Some c ⇒
finite (UNIV :: 'a set) ∧ proper_intrvl.proper_interval_set_aux (lt_of_comp c) cproper_interval (csorted_list_of_set A) (csorted_list_of_set B))"
(is ?fin_fin)
and cproper_interval_set_Some_Some_Complement [set_complement_code]:
"cproper_interval (Some A) (Some (Complement B)) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval Complement2: ccompare = None'') (λ_. cproper_interval (Some A) (Some (Complement B)))
| Some c ⇒
finite (UNIV :: 'a set) ∧ proper_intrvl.proper_interval_set_Compl_aux (lt_of_comp c) cproper_interval None 0 (csorted_list_of_set A) (csorted_list_of_set B))"
(is ?fin_Compl_fin)
and cproper_interval_set_Some_Complement_Some [set_complement_code]:
"cproper_interval (Some (Complement A)) (Some B) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval Complement1: ccompare = None'') (λ_. cproper_interval (Some (Complement A)) (Some B))
| Some c ⇒
finite (UNIV :: 'a set) ∧ proper_intrvl.proper_interval_Compl_set_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A) (csorted_list_of_set B))"
(is ?Compl_fin_fin)
and cproper_interval_set_Some_Complement_Some_Complement [set_complement_code]:
"cproper_interval (Some (Complement A)) (Some (Complement B)) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval Complement Complement: ccompare = None'') (λ_. cproper_interval (Some (Complement A)) (Some (Complement B)))
| Some _ ⇒ cproper_interval (Some B) (Some A))"
(is ?Compl_Compl)

"cproper_interval (Some (RBT_set rbt1)) (Some (RBT_set rbt2)) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval RBT_set RBT_set: ccompare = None'') (λ_. cproper_interval (Some (RBT_set rbt1)) (Some (RBT_set rbt2)))
| Some c ⇒
finite (UNIV :: 'a set) ∧ proper_intrvl.proper_interval_set_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?rbt_rbt)
and cproper_interval_set_Some_rbt_Some_Complement [set_complement_code]:
"cproper_interval (Some (RBT_set rbt1)) (Some (Complement (RBT_set rbt2))) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval RBT_set (Complement RBT_set): ccompare = None'') (λ_. cproper_interval (Some (RBT_set rbt1)) (Some (Complement (RBT_set rbt2))))
| Some c ⇒
finite (UNIV :: 'a set) ∧ proper_intrvl.proper_interval_set_Compl_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None 0 (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?rbt_Compl_rbt)
and cproper_interval_set_Some_Complement_Some_rbt [set_complement_code]:
"cproper_interval (Some (Complement (RBT_set rbt1))) (Some (RBT_set rbt2)) ⟷
(case ID CCOMPARE('a) of None ⇒ Code.abort (STR ''cproper_interval (Complement RBT_set) RBT_set: ccompare = None'') (λ_. cproper_interval (Some (Complement (RBT_set rbt1))) (Some (RBT_set rbt2)))
| Some c ⇒
finite (UNIV :: 'a set) ∧ proper_intrvl.proper_interval_Compl_set_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))"
(is ?Compl_rbt_rbt)
proof -
note [split] = option.split csorted_list_of_set_split
and [simp] =
lt_of_comp_of_ords
finite_subset[OF subset_UNIV] ccompare_set_def ID_Some
linorder.set_less_finite_iff[OF ID_ccompare]
RBT_set_def sorted_RBT_Set_keys member_conv_keys
linorder.distinct_entries[OF ID_ccompare]
unfoldr_rbt_keys_generator
proper_intrvl.proper_interval_set_aux_fusion_def
proper_intrvl.proper_interval_set_Compl_aux_fusion_def
proper_intrvl.proper_interval_Compl_set_aux_fusion_def
linorder_proper_interval.proper_interval_set_aux[OF ID_ccompare_interval]
linorder_proper_interval.proper_interval_set_Compl_aux[OF ID_ccompare_interval]
linorder_proper_interval.proper_interval_Compl_set_aux[OF ID_ccompare_interval]
and [cong] = conj_cong

show ?Compl_Compl
by(clarsimp simp add: Complement_cproper_interval_set_Complement simp del: cproper_interval_set_Some_Some)

show ?rbt_rbt ?rbt_Compl_rbt ?Compl_rbt_rbt by auto
show ?fin_fin ?fin_Compl_fin ?Compl_fin_fin by auto
qed

context ord begin

fun sorted_list_subset :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"sorted_list_subset eq [] ys = True"
| "sorted_list_subset eq (x # xs) [] = False"
| "sorted_list_subset eq (x # xs) (y # ys) ⟷
(if eq x y then sorted_list_subset eq xs ys
else x > y ∧ sorted_list_subset eq (x # xs) ys)"

end

context linorder begin

lemma sorted_list_subset_correct:
"⟦ sorted xs; distinct xs; sorted ys; distinct ys ⟧
⟹ sorted_list_subset (=) xs ys ⟷ set xs ⊆ set ys"
apply(induct "(=) :: 'a ⇒ 'a ⇒ bool" xs ys rule: sorted_list_subset.induct)
apply(auto 6 2)
using order_antisym apply auto
done

end

context ord begin

definition sorted_list_subset_fusion :: "('a ⇒ 'a ⇒ bool) ⇒ ('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where "sorted_list_subset_fusion eq g1 g2 s1 s2 = sorted_list_subset eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma sorted_list_subset_fusion_code:
"sorted_list_subset_fusion eq g1 g2 s1 s2 =
(if list.has_next g1 s1 then
let (x, s1') = list.next g1 s1
in list.has_next g2 s2 ∧ (
let (y, s2') = list.next g2 s2
in if eq x y then sorted_list_subset_fusion eq g1 g2 s1' s2'
else y < x ∧ sorted_list_subset_fusion eq g1 g2 s1 s2')
else True)"
unfolding sorted_list_subset_fusion_def
by(subst (1 2 5) list.unfoldr.simps)(simp add: split_beta Let_def)

end

lemmas [code] = ord.sorted_list_subset_fusion_code

lemma subset_eq_code [code]:
fixes A1 A2 :: "'a set"
and rbt :: "'b :: ccompare set_rbt"
and rbt1 rbt2 :: "'d :: {ccompare, ceq} set_rbt"
and dxs :: "'c :: ceq set_dlist"
and xs :: "'c list" shows
"RBT_set rbt ⊆ B ⟷
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''subset RBT_set1: ccompare = None'') (λ_. RBT_set rbt ⊆ B)
| Some _ ⇒ list_all_fusion rbt_keys_generator (λx. x ∈ B) (RBT_Set2.init rbt))" (is ?rbt)
"DList_set dxs ⊆ C ⟷
(case ID CEQ('c) of None ⇒ Code.abort (STR ''subset DList_set1: ceq = None'') (λ_. DList_set dxs ⊆ C)
| Some _ ⇒ DList_Set.dlist_all (λx. x ∈ C) dxs)" (is ?dlist)
"Set_Monad xs ⊆ C ⟷ list_all (λx. x ∈ C) xs" (is ?Set_Monad)
and Collect_subset_eq_Complement [set_complement_code]:
"Collect_set P ⊆ Complement A ⟷ A ⊆ {x. ¬ P x}" (is ?Collect_set_Compl)
and Complement_subset_eq_Complement [set_complement_code]:
"Complement A1 ⊆ Complement A2 ⟷ A2 ⊆ A1" (is ?Compl)
and
"RBT_set rbt1 ⊆ RBT_set rbt2 ⟷
(case ID CCOMPARE('d) of None ⇒ Code.abort (STR ''subset RBT_set RBT_set: ccompare = None'') (λ_. RBT_set rbt1 ⊆ RBT_set rbt2)
| Some c ⇒
(case ID CEQ('d) of None ⇒ ord.sorted_list_subset_fusion (lt_of_comp c) (λ x y. c x y = Eq) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)
| Some eq ⇒ ord.sorted_list_subset_fusion (lt_of_comp c) eq rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)))"
(is ?rbt_rbt)
proof -
show ?rbt_rbt
by (auto simp add: comparator.eq[OF ID_ccompare'] RBT_set_def member_conv_keys unfoldr_rbt_keys_generator ord.sorted_list_subset_fusion_def linorder.sorted_list_subset_correct[OF ID_ccompare] sorted_RBT_Set_keys split: option.split dest!: ID_ceq[THEN equal.equal_eq] del: iffI)
show ?rbt
by(auto simp add: RBT_set_def member_conv_keys list_all_fusion_def unfoldr_rbt_keys_generator keys.rep_eq list_all_iff split: option.split)
show ?dlist by(auto simp add: DList_set_def dlist_all_conv_member split: option.split)
show ?Collect_set_Compl ?Compl by auto
qed

lemma set_eq_code [code]:
fixes rbt1 rbt2 :: "'b :: {ccompare, ceq} set_rbt" shows
"set_eq A B ⟷ A ⊆ B ∧ B ⊆ A"
and set_eq_Complement_Complement [set_complement_code]:
"set_eq (Complement A) (Complement B) = set_eq A B"
and
"set_eq (RBT_set rbt1) (RBT_set rbt2) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''set_eq RBT_set RBT_set: ccompare = None'') (λ_. set_eq (RBT_set rbt1) (RBT_set rbt2))
| Some c ⇒
(case ID CEQ('b) of None ⇒ list_all2_fusion (λ x y. c x y = Eq) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)
| Some eq ⇒ list_all2_fusion eq rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)))"
(is ?rbt_rbt)
proof -
show ?rbt_rbt
by (auto 4 3 split: option.split simp add: comparator.eq[OF ID_ccompare'] sorted_RBT_Set_keys list_all2_fusion_def unfoldr_rbt_keys_generator RBT_set_conv_keys set_eq_def list.rel_eq dest!: ID_ceq[THEN equal.equal_eq] intro: linorder.sorted_distinct_set_unique[OF ID_ccompare])

lemma Set_project_code [code]:
"Set.filter P A = A ∩ Collect_set P"

lemma Set_image_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt" shows
"image f (Collect_set A) = Code.abort (STR ''image Collect_set'') (λ_. image f (Collect_set A))"
and image_Complement_Complement [set_complement_code]:
"image f (Complement (Complement B)) = image f B"
and
"image g (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''image DList_set: ceq = None'') (λ_. image g (DList_set dxs))
| Some _ ⇒ DList_Set.fold (insert ∘ g) dxs {})"
(is ?dlist)
"image h (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''image RBT_set: ccompare = None'') (λ_. image h (RBT_set rbt))
| Some _ ⇒ RBT_Set2.fold (insert ∘ h) rbt {})"
(is ?rbt)
proof -
{ fix xs have "fold (insert ∘ g) xs {} = g ` set xs"
by(induct xs rule: rev_induct) simp_all }
thus ?dlist
by(simp add: DList_set_def DList_Set.fold_def DList_Set.Collect_member split: option.split)
{ fix xs have "fold (insert ∘ h) xs {} = h ` set xs"
by(induct xs rule: rev_induct) simp_all }
thus ?rbt by(auto simp add: RBT_set_def fold_conv_fold_keys member_conv_keys split: option.split)
qed simp_all

lemma the_elem_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt" shows
"the_elem (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''the_elem DList_set: ceq = None'') (λ_. the_elem (DList_set dxs))
| Some _ ⇒
case list_of_dlist dxs of [x] ⇒ x
| _ ⇒ Code.abort (STR ''the_elem DList_set: not unique'') (λ_. the_elem (DList_set dxs)))"
"the_elem (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''the_elem RBT_set: ccompare = None'') (λ_. the_elem (RBT_set rbt))
| Some _ ⇒
case RBT_Mapping2.impl_of rbt of RBT_Impl.Branch _ RBT_Impl.Empty x _ RBT_Impl.Empty ⇒ x
| _ ⇒ Code.abort (STR ''the_elem RBT_set: not unique'') (λ_. the_elem (RBT_set rbt)))"
by(auto simp add: RBT_set_def DList_set_def DList_Set.Collect_member the_elem_def member_conv_keys split: option.split list.split rbt.split)(simp add: RBT_Set2.keys_def)

lemma Pow_set_conv_fold:
"Pow (set xs ∪ A) = fold (λx A. A ∪ insert x ` A) xs (Pow A)"
by(induct xs rule: rev_induct)(auto simp add: Pow_insert)

lemma Pow_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and rbt :: "'b :: ccompare set_rbt" shows
"Pow A = Collect_set (λB. B ⊆ A)"
"Pow (Set_Monad xs) = fold (λx A. A ∪ insert x ` A) xs {{}}"
"Pow (DList_set dxs) =
(case ID CEQ('a) of None ⇒ Code.abort (STR ''Pow DList_set: ceq = None'') (λ_. Pow (DList_set dxs))
| Some _ ⇒ DList_Set.fold (λx A. A ∪ insert x ` A) dxs {{}})"
"Pow (RBT_set rbt) =
(case ID CCOMPARE('b) of None ⇒ Code.abort (STR ''Pow RBT_set: ccompare = None'') (λ_. Pow (RBT_set rbt))
| Some _ ⇒ RBT_Set2.fold (λx A. A ∪ insert x ` A) rbt {{}})"
by(auto simp add: DList_set_def DList_Set.Collect_member DList_Set.fold_def RBT_set_def fold_conv_fold_keys member_conv_keys Pow_set_conv_fold[where A="{}", simplified] split: option.split)

lemma fold_singleton: "Finite_Set.fold f x {y} = f y x"
by(fastforce simp add: Finite_Set.fold_def intro: fold_graph.intros elim: fold_graph.cases)

lift_definition sum_cfc :: "('a ⇒ 'b :: comm_monoid_add) ⇒ ('a, 'b) comp_fun_commute"
is "λf :: 'a ⇒ 'b. plus ∘ f"

lemma sum_code [code]:
"sum f A = (if finite A then set_fold_cfc (sum_cfc f) 0 A else 0)"

lemma product_code [code]:
fixes dxs :: "'a :: ceq set_dlist"
and dys :: "'b :: ceq set_dlist"
and rbt1 :: "'c :: ccompare set_rbt"
and rbt2 :: "'d :: ccompare set_rbt" shows
"Product_Type.product A B = Collect_set (λ(x, y). x ∈ A ∧ y ∈ B)"

Set_Monad (fold (λx. fold (λy rest. (x, y) # rest) ys) xs [])"