Theory 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 = yset lts  {x}  set eqs  set gts  set []. aset ac. y < a
  have "sorted eqs" "set eqs  {x}" using yset eqs. y = x 
    by(induct eqs)(simp_all)
  moreover have "y  set ac  set gts. x  y"
    using aset 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 "yset lts. aset (eqs @ x # quicksort_acc ac gts). y < a"
    using yset lts. y < x ac_greater aset gts. x < a yset 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:
  "xset xs. yset 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 = yset eqs. y = x
  { fix eqs
    assume "yset 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
  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
  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) =
  (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"
by(unfold_locales)(simp add: fun_eq_iff add.left_commute)

lemma sum_code [code]:
  "sum f A = (if finite A then set_fold_cfc (sum_cfc f) 0 A else 0)"
  by transfer(simp add: sum.eq_fold)

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

  "Product_Type.product (Set_Monad xs) (Set_Monad ys) = 
   Set_Monad (fold (λx. fold (λy rest. (x, y) # rest) ys) xs [])"
  (is ?Set_Monad)

  "Product_Type.product (DList_set dxs) B1 = 
   (case ID CEQ('a) of None  Code.abort (STR ''product DList_set1: ceq = None'') (λ_. Product_Type.product (DList_set dxs) B1)
                   | Some _   DList_Set.fold (λx rest. Pair x ` B1  rest) dxs {})" 
  (is "?dlist1")

  "Product_Type.product A1 (DList_set dys) = 
   (case ID CEQ('b) of None  Code.abort (STR ''product DList_set2: ceq = None'') (λ_. Product_Type.product A1 (DList_set dys))
                   | Some _  DList_Set.fold (λy rest. (λx. (x, y)) ` A1  rest) dys {})"
  (is "?dlist2")

  "Product_Type.product (DList_set dxs) (DList_set dys) = 
  (case ID CEQ('a) of None  Code.abort (STR ''product DList_set DList_set: ceq1 = None'') (λ_. Product_Type.product (DList_set dxs) (DList_set dys))
                  | Some _  
     case ID CEQ('b) of None  Code.abort (STR ''product DList_set DList_set: ceq2 = None'') (λ_. Product_Type.product (DList_set dxs) (DList_set dys))
                    | Some _  DList_set (DList_Set.product dxs dys))"

  "Product_Type.product (RBT_set rbt1) B2 =
  (case ID CCOMPARE('c) of None  Code.abort (STR ''product RBT_set: ccompare1 = None'') (λ_. Product_Type.product (RBT_set rbt1) B2)
                     | Some _  RBT_Set2.fold (λx rest. Pair x ` B2  rest) rbt1 {})"
  (is "?rbt1")

  "Product_Type.product A2 (RBT_set rbt2) =
  (case ID CCOMPARE('d) of None  Code.abort (STR ''product RBT_set: ccompare2 = None'') (λ_. Product_Type.product A2 (RBT_set rbt2))
                     | Some _  RBT_Set2.fold (λy rest. (λx. (x, y)) ` A2  rest) rbt2 {})"
  (is "?rbt2")

  "Product_Type.product (RBT_set rbt1) (RBT_set rbt2) =
  (case ID CCOMPARE('c) of None  Code.abort (STR ''product RBT_set RBT_set: ccompare1 = None'') (λ_<