Cset, Dlist_Cset, List_Cset: restructured
authorhaftmann
Sat Aug 27 09:44:45 2011 +0200 (2011-08-27)
changeset 44558cc878a312673
parent 44557 9ab8c88449a4
child 44559 5a12314dcf30
Cset, Dlist_Cset, List_Cset: restructured
src/HOL/Library/Cset.thy
src/HOL/Library/Dlist_Cset.thy
src/HOL/Library/List_Cset.thy
     1.1 --- a/src/HOL/Library/Cset.thy	Sat Aug 27 09:02:25 2011 +0200
     1.2 +++ b/src/HOL/Library/Cset.thy	Sat Aug 27 09:44:45 2011 +0200
     1.3 @@ -152,6 +152,10 @@
     1.4    "set xs = Set (List.set xs)"
     1.5  hide_const (open) set
     1.6  
     1.7 +definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
     1.8 +  "coset xs = Set (- List.set xs)"
     1.9 +hide_const (open) coset
    1.10 +
    1.11  text {* conversion from @{typ "'a Predicate.pred"} *}
    1.12  
    1.13  definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
    1.14 @@ -200,6 +204,21 @@
    1.15    by (simp add: set_def)
    1.16  hide_fact (open) set_def
    1.17  
    1.18 +lemma member_set [simp]:
    1.19 +  "member (Cset.set xs) = (\<lambda>x. x \<in> set xs)"
    1.20 +  by (simp add: fun_eq_iff member_def)
    1.21 +hide_fact (open) member_set
    1.22 +
    1.23 +lemma set_of_coset [simp]:
    1.24 +  "set_of (Cset.coset xs) = - set xs"
    1.25 +  by (simp add: coset_def)
    1.26 +hide_fact (open) coset_def
    1.27 +
    1.28 +lemma member_coset [simp]:
    1.29 +  "member (Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
    1.30 +  by (simp add: fun_eq_iff member_def)
    1.31 +hide_fact (open) member_coset
    1.32 +
    1.33  lemma set_simps [simp]:
    1.34    "Cset.set [] = Cset.empty"
    1.35    "Cset.set (x # xs) = insert x (Cset.set xs)"
    1.36 @@ -268,6 +287,82 @@
    1.37    "single a = insert a Cset.empty"
    1.38    by (simp add: Cset.single_def)
    1.39  
    1.40 +lemma compl_set [simp]:
    1.41 +  "- Cset.set xs = Cset.coset xs"
    1.42 +  by (simp add: Cset.set_def Cset.coset_def)
    1.43 +
    1.44 +lemma compl_coset [simp]:
    1.45 +  "- Cset.coset xs = Cset.set xs"
    1.46 +  by (simp add: Cset.set_def Cset.coset_def)
    1.47 +
    1.48 +lemma member_cset_of:
    1.49 +  "member = set_of"
    1.50 +  by (rule ext)+ (simp add: member_def mem_def)
    1.51 +
    1.52 +lemma inter_project:
    1.53 +  "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
    1.54 +  "inf A (Cset.coset xs) = foldr Cset.remove xs A"
    1.55 +proof -
    1.56 +  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
    1.57 +    by (simp add: inter project_def Cset.set_def member_def)
    1.58 +  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
    1.59 +    by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
    1.60 +  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
    1.61 +    fold More_Set.remove xs \<circ> member"
    1.62 +    by (rule fold_commute) (simp add: fun_eq_iff mem_def)
    1.63 +  then have "fold More_Set.remove xs (member A) = 
    1.64 +    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
    1.65 +    by (simp add: fun_eq_iff)
    1.66 +  then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
    1.67 +    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
    1.68 +  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
    1.69 +    by (auto simp add: More_Set.remove_def * member_cset_of)
    1.70 +  ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
    1.71 +    by (simp add: foldr_fold)
    1.72 +qed
    1.73 +
    1.74 +lemma subtract_remove:
    1.75 +  "A - Cset.set xs = foldr Cset.remove xs A"
    1.76 +  "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
    1.77 +  by (simp_all only: diff_eq compl_set compl_coset inter_project)
    1.78 +
    1.79 +lemma union_insert:
    1.80 +  "sup (Cset.set xs) A = foldr Cset.insert xs A"
    1.81 +  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
    1.82 +proof -
    1.83 +  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
    1.84 +    by (simp add: fun_eq_iff member_cset_of)
    1.85 +  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
    1.86 +    fold Set.insert xs \<circ> member"
    1.87 +    by (rule fold_commute) (simp add: fun_eq_iff mem_def)
    1.88 +  then have "fold Set.insert xs (member A) =
    1.89 +    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
    1.90 +    by (simp add: fun_eq_iff)
    1.91 +  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
    1.92 +    by (simp add: union_set * member_cset_of)
    1.93 +  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
    1.94 +    by (auto simp add: * member_cset_of)
    1.95 +  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
    1.96 +    by (simp add: foldr_fold)
    1.97 +  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
    1.98 +    by (auto simp add: Cset.coset_def member_cset_of mem_def)
    1.99 +qed
   1.100 +
   1.101 +context complete_lattice
   1.102 +begin
   1.103 +
   1.104 +lemma Infimum_inf:
   1.105 +  "Infimum (Cset.set As) = foldr inf As top"
   1.106 +  "Infimum (Cset.coset []) = bot"
   1.107 +  by (simp_all add: Inf_set_foldr)
   1.108 +
   1.109 +lemma Supremum_sup:
   1.110 +  "Supremum (Cset.set As) = foldr sup As bot"
   1.111 +  "Supremum (Cset.coset []) = top"
   1.112 +  by (simp_all add: Sup_set_foldr)
   1.113 +
   1.114 +end
   1.115 +
   1.116  lemma of_pred_code [code]:
   1.117    "of_pred (Predicate.Seq f) = (case f () of
   1.118       Predicate.Empty \<Rightarrow> Cset.empty
   1.119 @@ -287,6 +382,22 @@
   1.120    apply simp_all
   1.121    done
   1.122  
   1.123 +lemma bind_set:
   1.124 +  "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
   1.125 +  by (simp add: Cset.bind_def SUPR_set_fold)
   1.126 +hide_fact (open) bind_set
   1.127 +
   1.128 +lemma pred_of_cset_set:
   1.129 +  "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
   1.130 +proof -
   1.131 +  have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
   1.132 +    by (simp add: Cset.pred_of_cset_def member_set)
   1.133 +  moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
   1.134 +    by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI, simp add: mem_def)
   1.135 +  ultimately show ?thesis by simp
   1.136 +qed
   1.137 +hide_fact (open) pred_of_cset_set
   1.138 +
   1.139  no_notation bind (infixl "\<guillemotright>=" 70)
   1.140  
   1.141  hide_const (open) is_empty insert remove map filter forall exists card
     2.1 --- a/src/HOL/Library/Dlist_Cset.thy	Sat Aug 27 09:02:25 2011 +0200
     2.2 +++ b/src/HOL/Library/Dlist_Cset.thy	Sat Aug 27 09:44:45 2011 +0200
     2.3 @@ -3,66 +3,44 @@
     2.4  header {* Canonical implementation of sets by distinct lists *}
     2.5  
     2.6  theory Dlist_Cset
     2.7 -imports Dlist List_Cset
     2.8 +imports Dlist Cset
     2.9  begin
    2.10  
    2.11  definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    2.12    "Set dxs = Cset.set (list_of_dlist dxs)"
    2.13  
    2.14  definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    2.15 -  "Coset dxs = List_Cset.coset (list_of_dlist dxs)"
    2.16 +  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    2.17  
    2.18  code_datatype Set Coset
    2.19  
    2.20 -declare member_code [code del]
    2.21 -declare List_Cset.is_empty_set [code del]
    2.22 -declare List_Cset.empty_set [code del]
    2.23 -declare List_Cset.UNIV_set [code del]
    2.24 -declare insert_set [code del]
    2.25 -declare remove_set [code del]
    2.26 -declare compl_set [code del]
    2.27 -declare compl_coset [code del]
    2.28 -declare map_set [code del]
    2.29 -declare filter_set [code del]
    2.30 -declare forall_set [code del]
    2.31 -declare exists_set [code del]
    2.32 -declare card_set [code del]
    2.33 -declare List_Cset.single_set [code del]
    2.34 -declare List_Cset.bind_set [code del]
    2.35 -declare List_Cset.pred_of_cset_set [code del]
    2.36 -declare inter_project [code del]
    2.37 -declare subtract_remove [code del]
    2.38 -declare union_insert [code del]
    2.39 -declare Infimum_inf [code del]
    2.40 -declare Supremum_sup [code del]
    2.41 -
    2.42  lemma Set_Dlist [simp]:
    2.43 -  "Set (Dlist xs) = Cset.Set (set xs)"
    2.44 +  "Set (Dlist xs) = Cset.set xs"
    2.45    by (rule Cset.set_eqI) (simp add: Set_def)
    2.46  
    2.47  lemma Coset_Dlist [simp]:
    2.48 -  "Coset (Dlist xs) = Cset.Set (- set xs)"
    2.49 +  "Coset (Dlist xs) = Cset.coset xs"
    2.50    by (rule Cset.set_eqI) (simp add: Coset_def)
    2.51  
    2.52  lemma member_Set [simp]:
    2.53    "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
    2.54 -  by (simp add: Set_def member_set)
    2.55 +  by (simp add: Set_def fun_eq_iff List.member_def)
    2.56  
    2.57  lemma member_Coset [simp]:
    2.58    "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    2.59 -  by (simp add: Coset_def member_set not_set_compl)
    2.60 +  by (simp add: Coset_def fun_eq_iff List.member_def)
    2.61  
    2.62  lemma Set_dlist_of_list [code]:
    2.63    "Cset.set xs = Set (dlist_of_list xs)"
    2.64    by (rule Cset.set_eqI) simp
    2.65  
    2.66  lemma Coset_dlist_of_list [code]:
    2.67 -  "List_Cset.coset xs = Coset (dlist_of_list xs)"
    2.68 +  "Cset.coset xs = Coset (dlist_of_list xs)"
    2.69    by (rule Cset.set_eqI) simp
    2.70  
    2.71  lemma is_empty_Set [code]:
    2.72    "Cset.is_empty (Set dxs) \<longleftrightarrow> Dlist.null dxs"
    2.73 -  by (simp add: Dlist.null_def List.null_def member_set)
    2.74 +  by (simp add: Dlist.null_def List.null_def Set_def)
    2.75  
    2.76  lemma bot_code [code]:
    2.77    "bot = Set Dlist.empty"
    2.78 @@ -70,47 +48,47 @@
    2.79  
    2.80  lemma top_code [code]:
    2.81    "top = Coset Dlist.empty"
    2.82 -  by (simp add: empty_def)
    2.83 +  by (simp add: empty_def Cset.coset_def)
    2.84  
    2.85  lemma insert_code [code]:
    2.86    "Cset.insert x (Set dxs) = Set (Dlist.insert x dxs)"
    2.87    "Cset.insert x (Coset dxs) = Coset (Dlist.remove x dxs)"
    2.88 -  by (simp_all add: Dlist.insert_def Dlist.remove_def member_set not_set_compl)
    2.89 +  by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def)
    2.90  
    2.91  lemma remove_code [code]:
    2.92    "Cset.remove x (Set dxs) = Set (Dlist.remove x dxs)"
    2.93    "Cset.remove x (Coset dxs) = Coset (Dlist.insert x dxs)"
    2.94 -  by (auto simp add: Dlist.insert_def Dlist.remove_def member_set not_set_compl)
    2.95 +  by (simp_all add: Dlist.insert_def Dlist.remove_def Cset.set_def Cset.coset_def Set_def Coset_def Compl_insert)
    2.96  
    2.97  lemma member_code [code]:
    2.98    "Cset.member (Set dxs) = Dlist.member dxs"
    2.99    "Cset.member (Coset dxs) = Not \<circ> Dlist.member dxs"
   2.100 -  by (simp_all add: member_def)
   2.101 +  by (simp_all add: List.member_def member_def fun_eq_iff Dlist.member_def)
   2.102  
   2.103  lemma compl_code [code]:
   2.104    "- Set dxs = Coset dxs"
   2.105    "- Coset dxs = Set dxs"
   2.106 -  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
   2.107 +  by (rule Cset.set_eqI, simp add: fun_eq_iff List.member_def Set_def Coset_def)+
   2.108  
   2.109  lemma map_code [code]:
   2.110    "Cset.map f (Set dxs) = Set (Dlist.map f dxs)"
   2.111 -  by (rule Cset.set_eqI) (simp add: member_set)
   2.112 +  by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def)
   2.113    
   2.114  lemma filter_code [code]:
   2.115    "Cset.filter f (Set dxs) = Set (Dlist.filter f dxs)"
   2.116 -  by (rule Cset.set_eqI) (simp add: member_set)
   2.117 +  by (rule Cset.set_eqI) (simp add: fun_eq_iff List.member_def Set_def)
   2.118  
   2.119  lemma forall_Set [code]:
   2.120    "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   2.121 -  by (simp add: member_set list_all_iff)
   2.122 +  by (simp add: Set_def list_all_iff)
   2.123  
   2.124  lemma exists_Set [code]:
   2.125    "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   2.126 -  by (simp add: member_set list_ex_iff)
   2.127 +  by (simp add: Set_def list_ex_iff)
   2.128  
   2.129  lemma card_code [code]:
   2.130    "Cset.card (Set dxs) = Dlist.length dxs"
   2.131 -  by (simp add: length_def member_set distinct_card)
   2.132 +  by (simp add: length_def Set_def distinct_card)
   2.133  
   2.134  lemma inter_code [code]:
   2.135    "inf A (Set xs) = Set (Dlist.filter (Cset.member A) xs)"
   2.136 @@ -143,13 +121,15 @@
   2.137  declare Cset.single_code[code]
   2.138  
   2.139  lemma bind_set [code]:
   2.140 -  "Cset.bind (Dlist_Cset.Set xs) f = foldl (\<lambda>A x. sup A (f x)) Cset.empty (list_of_dlist xs)"
   2.141 -by(simp add: List_Cset.bind_set Dlist_Cset.Set_def)
   2.142 +  "Cset.bind (Dlist_Cset.Set xs) f = fold (sup \<circ> f) (list_of_dlist xs) Cset.empty"
   2.143 +  by (simp add: Cset.bind_set Set_def)
   2.144  hide_fact (open) bind_set
   2.145  
   2.146  lemma pred_of_cset_set [code]:
   2.147    "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot"
   2.148 -by(simp add: List_Cset.pred_of_cset_set Dlist_Cset.Set_def)
   2.149 +  by (simp add: Cset.pred_of_cset_set Dlist_Cset.Set_def)
   2.150  hide_fact (open) pred_of_cset_set
   2.151  
   2.152 +export_code "Cset._" in Haskell
   2.153 +
   2.154  end
     3.1 --- a/src/HOL/Library/List_Cset.thy	Sat Aug 27 09:02:25 2011 +0200
     3.2 +++ b/src/HOL/Library/List_Cset.thy	Sat Aug 27 09:44:45 2011 +0200
     3.3 @@ -7,28 +7,12 @@
     3.4  imports Cset
     3.5  begin
     3.6  
     3.7 -declare mem_def [simp]
     3.8 -declare Cset.set_code [code del]
     3.9 -
    3.10 -definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    3.11 -  "coset xs = Set (- set xs)"
    3.12 -hide_const (open) coset
    3.13 -
    3.14 -lemma set_of_coset [simp]:
    3.15 -  "set_of (List_Cset.coset xs) = - set xs"
    3.16 -  by (simp add: coset_def)
    3.17 -
    3.18 -lemma member_coset [simp]:
    3.19 -  "member (List_Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
    3.20 -  by (simp add: coset_def fun_eq_iff)
    3.21 -hide_fact (open) member_coset
    3.22 -
    3.23 -code_datatype Cset.set List_Cset.coset
    3.24 +code_datatype Cset.set Cset.coset
    3.25  
    3.26  lemma member_code [code]:
    3.27    "member (Cset.set xs) = List.member xs"
    3.28 -  "member (List_Cset.coset xs) = Not \<circ> List.member xs"
    3.29 -  by (simp_all add: fun_eq_iff member_def fun_Compl_def member_set)
    3.30 +  "member (Cset.coset xs) = Not \<circ> List.member xs"
    3.31 +  by (simp_all add: fun_eq_iff List.member_def)
    3.32  
    3.33  definition (in term_syntax)
    3.34    setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    3.35 @@ -60,24 +44,27 @@
    3.36  
    3.37  lemma empty_set [code]:
    3.38    "Cset.empty = Cset.set []"
    3.39 -  by (simp add: set_def)
    3.40 +  by simp
    3.41  hide_fact (open) empty_set
    3.42  
    3.43  lemma UNIV_set [code]:
    3.44 -  "top = List_Cset.coset []"
    3.45 -  by (simp add: coset_def)
    3.46 +  "top = Cset.coset []"
    3.47 +  by (simp add: Cset.coset_def)
    3.48  hide_fact (open) UNIV_set
    3.49  
    3.50  lemma remove_set [code]:
    3.51    "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)"
    3.52 -  "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
    3.53 -by (simp_all add: Cset.set_def coset_def)
    3.54 -  (metis List.set_insert More_Set.remove_def remove_set_compl)
    3.55 +  "Cset.remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
    3.56 +  by (simp_all add: Cset.set_def Cset.coset_def Compl_insert)
    3.57  
    3.58  lemma insert_set [code]:
    3.59    "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)"
    3.60 -  "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
    3.61 -  by (simp_all add: Cset.set_def coset_def)
    3.62 +  "Cset.insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
    3.63 +  by (simp_all add: Cset.set_def Cset.coset_def)
    3.64 +
    3.65 +declare compl_set [code]
    3.66 +declare compl_coset [code]
    3.67 +declare subtract_remove [cpde]
    3.68  
    3.69  lemma map_set [code]:
    3.70    "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
    3.71 @@ -103,26 +90,11 @@
    3.72    then show ?thesis by (simp add: Cset.set_def)
    3.73  qed
    3.74  
    3.75 -lemma compl_set [simp, code]:
    3.76 -  "- Cset.set xs = List_Cset.coset xs"
    3.77 -  by (simp add: Cset.set_def coset_def)
    3.78 -
    3.79 -lemma compl_coset [simp, code]:
    3.80 -  "- List_Cset.coset xs = Cset.set xs"
    3.81 -  by (simp add: Cset.set_def coset_def)
    3.82 -
    3.83  context complete_lattice
    3.84  begin
    3.85  
    3.86 -lemma Infimum_inf [code]:
    3.87 -  "Infimum (Cset.set As) = foldr inf As top"
    3.88 -  "Infimum (List_Cset.coset []) = bot"
    3.89 -  by (simp_all add: Inf_set_foldr)
    3.90 -
    3.91 -lemma Supremum_sup [code]:
    3.92 -  "Supremum (Cset.set As) = foldr sup As bot"
    3.93 -  "Supremum (List_Cset.coset []) = top"
    3.94 -  by (simp_all add: Sup_set_foldr)
    3.95 +declare Infimum_inf [code]
    3.96 +declare Supremum_sup [code]
    3.97  
    3.98  end
    3.99  
   3.100 @@ -132,20 +104,8 @@
   3.101  by(simp add: Cset.single_code)
   3.102  hide_fact (open) single_set
   3.103  
   3.104 -lemma bind_set [code]:
   3.105 -  "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
   3.106 -  by (simp add: Cset.bind_def SUPR_set_fold)
   3.107 -
   3.108 -lemma pred_of_cset_set [code]:
   3.109 -  "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
   3.110 -proof -
   3.111 -  have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
   3.112 -    by (simp add: Cset.pred_of_cset_def member_code member_set)
   3.113 -  moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
   3.114 -    by (induct xs) (auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
   3.115 -  ultimately show ?thesis by simp
   3.116 -qed
   3.117 -hide_fact (open) pred_of_cset_set
   3.118 +declare Cset.bind_set [code]
   3.119 +declare Cset.pred_of_cset_set [code]
   3.120  
   3.121  
   3.122  subsection {* Derived operations *}
   3.123 @@ -165,7 +125,7 @@
   3.124    "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
   3.125  
   3.126  instance proof
   3.127 -qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff fun_eq_iff member_def)
   3.128 +qed (auto simp add: equal_set_def Cset.set_eq_iff Cset.member_def fun_eq_iff mem_def)
   3.129  
   3.130  end
   3.131  
   3.132 @@ -176,59 +136,7 @@
   3.133  
   3.134  subsection {* Functorial operations *}
   3.135  
   3.136 -lemma member_cset_of:
   3.137 -  "member = set_of"
   3.138 -  by (rule ext)+ (simp add: member_def)
   3.139 -
   3.140 -lemma inter_project [code]:
   3.141 -  "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   3.142 -  "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
   3.143 -proof -
   3.144 -  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   3.145 -    by (simp add: inter project_def Cset.set_def member_cset_of)
   3.146 -  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   3.147 -    by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
   3.148 -  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   3.149 -    fold More_Set.remove xs \<circ> member"
   3.150 -    by (rule fold_commute) (simp add: fun_eq_iff)
   3.151 -  then have "fold More_Set.remove xs (member A) = 
   3.152 -    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
   3.153 -    by (simp add: fun_eq_iff)
   3.154 -  then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
   3.155 -    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
   3.156 -  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   3.157 -    by (auto simp add: More_Set.remove_def * member_cset_of intro: ext)
   3.158 -  ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
   3.159 -    by (simp add: foldr_fold)
   3.160 -qed
   3.161 -
   3.162 -lemma subtract_remove [code]:
   3.163 -  "A - Cset.set xs = foldr Cset.remove xs A"
   3.164 -  "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)"
   3.165 -  by (simp_all only: diff_eq compl_set compl_coset inter_project)
   3.166 -
   3.167 -lemma union_insert [code]:
   3.168 -  "sup (Cset.set xs) A = foldr Cset.insert xs A"
   3.169 -  "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   3.170 -proof -
   3.171 -  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   3.172 -    by (simp add: fun_eq_iff member_cset_of)
   3.173 -  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
   3.174 -    fold Set.insert xs \<circ> member"
   3.175 -    by (rule fold_commute) (simp add: fun_eq_iff)
   3.176 -  then have "fold Set.insert xs (member A) =
   3.177 -    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   3.178 -    by (simp add: fun_eq_iff)
   3.179 -  then have "sup (Cset.set xs) A = fold Cset.insert xs A"
   3.180 -    by (simp add: union_set * member_cset_of)
   3.181 -  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   3.182 -    by (auto simp add: * member_cset_of intro: ext)
   3.183 -  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
   3.184 -    by (simp add: foldr_fold)
   3.185 -  show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
   3.186 -    by (auto simp add: coset_def member_cset_of)
   3.187 -qed
   3.188 -
   3.189 -declare mem_def[simp del]
   3.190 +declare inter_project [code]
   3.191 +declare union_insert [code]
   3.192  
   3.193  end