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)
apply(simp_all add: quicksort_acc.psimps quicksort_part.psimps)
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))")
apply(simp_all add: power2_eq_square add_mult_distrib add_mult_distrib2 length_quicksort_accp)
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"
by(simp add: quicksort_def)

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"
by(simp add: quicksort_def distinct_quicksort_acc)

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)"
    by(auto simp add: sorted_append)
  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)"
by(simp add: quicksort_def sorted_quicksort_acc)

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"
by(induct xs)(simp_all add: insort_key_append1)

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

lemma to_single_list: "x # xs = single_list x @ xs"
by(simp add: single_list_def)

lemma sort_snoc: "sort (xs @ [x]) = insort x (sort xs)"
by(induct xs)(simp_all add: insort_left_comm)

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"
by(simp add: quicksort_def quicksort_acc_conv_sort)

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"
by(auto simp add: Set.is_empty_def set_eq_def)

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"
by(auto simp add: is_UNIV_def set_eq_def)

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_code
  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"
where [simp]: "Set_Monad = set"

code_datatype Collect_set DList_set RBT_set Set_Monad Complement

lemma DList_set_empty [simp]: "DList_set DList_Set.empty = {}"
by(simp add: DList_set_def)

lemma RBT_set_empty [simp]: "RBT_set RBT_Set2.empty = {}"
by(simp add: RBT_set_def)

lemma RBT_set_conv_keys: 
  "ID CCOMPARE('a :: ccompare) ≠ None 
  ⟹ RBT_set (t :: 'a set_rbt) = set (RBT_Set2.keys t)"
by(clarsimp simp add: RBT_set_def member_conv_keys)

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)"
  (is ?Set_Monad)
  "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]
  show ?Set_Monad
    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"
  (is ?Set_Monad)
  "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 -
  show ?Set_Monad
    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))"
by(clarsimp simp add: neq_Nil_conv eq_fold)

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 ?Set_Monad
    by(simp add: set_fold1_def semilattice_set.eq_fold fold_set_fold)
  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 (Set_Monad xs) = True"
  "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)"
by(simp add: 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))"
  "card (Set_Monad xs) =
  (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 
        by(simp add: finite_code)
      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
    by(auto simp add: is_UNIV_def Set.is_empty_def)
qed(simp_all add: Set.is_empty_def List.null_def)

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 (Set_Monad xs) = Set_Monad (x # xs)"
  "⋀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)
  "Set_Monad xs ∪ Set_Monad ys = Set_Monad (xs @ ys)"
  "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 -
  show ?RBT_set_RBT_set ?Set_Monad_RBT_set ?RBT_set_Set_Monad
    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])

  show ?DList_set_Set_Monad ?Set_Monad_DList_set
    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)

  "Set_Monad xs'' ∩ I = Set_Monad (filter (λx. x ∈ I) xs'')" (is ?monad1)
  "I ∩ Set_Monad xs'' = Set_Monad (filter (λx. x ∈ I) xs'')" (is ?monad2)

  "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)
  "Set_Monad xs1 ∩ Set_Monad xs2 =
  (case ID CEQ('c) of None ⇒ Code.abort (STR ''inter Set_Monad Set_Monad: ceq = None'') (λ_. Set_Monad xs1 ∩ Set_Monad xs2)
                 | 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 -
  show ?rbt_rbt ?rbt1 ?rbt2 ?rbt_dlist ?rbt_monad ?dlist_rbt ?monad_rbt
    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)
  show ?dlist ?dlist1 ?dlist2 ?dlist_monad ?monad_dlist ?monad ?monad1 ?monad2 ?collect1 ?collect2 ?complement
    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 (Set_Monad xs) f = fold ((∪) ∘ f) xs (Set_Monad [])" (is ?Set_Monad)
  "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 ?Set_Monad by(simp add: set_bind_conv_fold)
  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"
by transfer(simp add: Inf_fin_def)

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"
by transfer(simp add: Sup_fin_def)

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))"
by transfer(simp add: Inf_fold_inf)

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))"
by transfer(simp add: Sup_fold_sup)

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"
by transfer(simp add: Min_def)

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

lemma Max_code [code]: "Max A = set_fold1 max_sls A"
by transfer(simp add: Max_def)

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))"
  "csorted_list_of_set (Set_Monad xs) =
  (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 ?Set_Monad by(auto simp add: list_all_iff 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])
qed(auto simp add: set_eq_def)

lemma Set_project_code [code]:
  "Set.filter P A = A ∩ Collect_set P"
by(auto simp add: Set.filter_def)

lemma Set_image_code [code]:
  fixes dxs :: "'a :: ceq set_dlist" 
  and rbt :: "'b :: ccompare set_rbt" shows
  "image f (Set_Monad xs) = Set_Monad (map f xs)"
  "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 (Set_Monad [x]) = x"
  "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)