1.1 --- a/src/HOL/IsaMakefile Tue Jun 07 11:11:01 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue Jun 07 11:12:05 2011 +0200
1.3 @@ -453,7 +453,7 @@
1.4 Library/Indicator_Function.thy Library/Infinite_Set.thy \
1.5 Library/Inner_Product.thy Library/Kleene_Algebra.thy \
1.6 Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
1.7 - Library/Lattice_Syntax.thy Library/Library.thy \
1.8 + Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \
1.9 Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
1.10 Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
1.11 Library/Multiset.thy Library/Nat_Bijection.thy \
2.1 --- a/src/HOL/Library/Cset.thy Tue Jun 07 11:11:01 2011 +0200
2.2 +++ b/src/HOL/Library/Cset.thy Tue Jun 07 11:12:05 2011 +0200
2.3 @@ -35,66 +35,6 @@
2.4 by (simp add: Cset.set_eq_iff)
2.5 hide_fact (open) set_eqI
2.6
2.7 -declare mem_def [simp]
2.8 -
2.9 -definition set :: "'a list \<Rightarrow> 'a Cset.set" where
2.10 - "set xs = Set (List.set xs)"
2.11 -hide_const (open) set
2.12 -
2.13 -lemma member_set [simp]:
2.14 - "member (Cset.set xs) = set xs"
2.15 - by (simp add: set_def)
2.16 -hide_fact (open) member_set
2.17 -
2.18 -definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
2.19 - "coset xs = Set (- set xs)"
2.20 -hide_const (open) coset
2.21 -
2.22 -lemma member_coset [simp]:
2.23 - "member (Cset.coset xs) = - set xs"
2.24 - by (simp add: coset_def)
2.25 -hide_fact (open) member_coset
2.26 -
2.27 -code_datatype Cset.set Cset.coset
2.28 -
2.29 -lemma member_code [code]:
2.30 - "member (Cset.set xs) = List.member xs"
2.31 - "member (Cset.coset xs) = Not \<circ> List.member xs"
2.32 - by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
2.33 -
2.34 -lemma member_image_UNIV [simp]:
2.35 - "member ` UNIV = UNIV"
2.36 -proof -
2.37 - have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
2.38 - proof
2.39 - fix A :: "'a set"
2.40 - show "A = member (Set A)" by simp
2.41 - qed
2.42 - then show ?thesis by (simp add: image_def)
2.43 -qed
2.44 -
2.45 -definition (in term_syntax)
2.46 - setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
2.47 - \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
2.48 - [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
2.49 -
2.50 -notation fcomp (infixl "\<circ>>" 60)
2.51 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
2.52 -
2.53 -instantiation Cset.set :: (random) random
2.54 -begin
2.55 -
2.56 -definition
2.57 - "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
2.58 -
2.59 -instance ..
2.60 -
2.61 -end
2.62 -
2.63 -no_notation fcomp (infixl "\<circ>>" 60)
2.64 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
2.65 -
2.66 -
2.67 subsection {* Lattice instantiation *}
2.68
2.69 instantiation Cset.set :: (type) boolean_algebra
2.70 @@ -149,185 +89,39 @@
2.71 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
2.72 [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
2.73
2.74 -lemma is_empty_set [code]:
2.75 - "is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
2.76 - by (simp add: is_empty_set)
2.77 -hide_fact (open) is_empty_set
2.78 -
2.79 -lemma empty_set [code]:
2.80 - "bot = Cset.set []"
2.81 - by (simp add: set_def)
2.82 -hide_fact (open) empty_set
2.83 -
2.84 -lemma UNIV_set [code]:
2.85 - "top = Cset.coset []"
2.86 - by (simp add: coset_def)
2.87 -hide_fact (open) UNIV_set
2.88 -
2.89 definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.90 [simp]: "insert x A = Set (Set.insert x (member A))"
2.91
2.92 -lemma insert_set [code]:
2.93 - "insert x (Cset.set xs) = Cset.set (List.insert x xs)"
2.94 - "insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
2.95 - by (simp_all add: set_def coset_def)
2.96 -
2.97 definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.98 [simp]: "remove x A = Set (More_Set.remove x (member A))"
2.99
2.100 -lemma remove_set [code]:
2.101 - "remove x (Cset.set xs) = Cset.set (removeAll x xs)"
2.102 - "remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
2.103 - by (simp_all add: set_def coset_def remove_set_compl)
2.104 - (simp add: More_Set.remove_def)
2.105 -
2.106 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
2.107 [simp]: "map f A = Set (image f (member A))"
2.108
2.109 -lemma map_set [code]:
2.110 - "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
2.111 - by (simp add: set_def)
2.112 -
2.113 enriched_type map: map
2.114 by (simp_all add: fun_eq_iff image_compose)
2.115
2.116 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
2.117 [simp]: "filter P A = Set (More_Set.project P (member A))"
2.118
2.119 -lemma filter_set [code]:
2.120 - "filter P (Cset.set xs) = Cset.set (List.filter P xs)"
2.121 - by (simp add: set_def project_set)
2.122 -
2.123 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
2.124 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
2.125
2.126 -lemma forall_set [code]:
2.127 - "forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
2.128 - by (simp add: set_def list_all_iff)
2.129 -
2.130 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
2.131 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
2.132
2.133 -lemma exists_set [code]:
2.134 - "exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
2.135 - by (simp add: set_def list_ex_iff)
2.136 -
2.137 definition card :: "'a Cset.set \<Rightarrow> nat" where
2.138 [simp]: "card A = Finite_Set.card (member A)"
2.139 -
2.140 -lemma card_set [code]:
2.141 - "card (Cset.set xs) = length (remdups xs)"
2.142 -proof -
2.143 - have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
2.144 - by (rule distinct_card) simp
2.145 - then show ?thesis by (simp add: set_def)
2.146 -qed
2.147 -
2.148 -lemma compl_set [simp, code]:
2.149 - "- Cset.set xs = Cset.coset xs"
2.150 - by (simp add: set_def coset_def)
2.151 -
2.152 -lemma compl_coset [simp, code]:
2.153 - "- Cset.coset xs = Cset.set xs"
2.154 - by (simp add: set_def coset_def)
2.155 -
2.156 -
2.157 -subsection {* Derived operations *}
2.158 -
2.159 -lemma subset_eq_forall [code]:
2.160 - "A \<le> B \<longleftrightarrow> forall (member B) A"
2.161 - by (simp add: subset_eq)
2.162 -
2.163 -lemma subset_subset_eq [code]:
2.164 - "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
2.165 - by (fact less_le_not_le)
2.166 -
2.167 -instantiation Cset.set :: (type) equal
2.168 -begin
2.169 -
2.170 -definition [code]:
2.171 - "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
2.172 -
2.173 -instance proof
2.174 -qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
2.175 -
2.176 -end
2.177 -
2.178 -lemma [code nbe]:
2.179 - "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
2.180 - by (fact equal_refl)
2.181 -
2.182 -
2.183 -subsection {* Functorial operations *}
2.184 -
2.185 -lemma inter_project [code]:
2.186 - "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
2.187 - "inf A (Cset.coset xs) = foldr remove xs A"
2.188 -proof -
2.189 - show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
2.190 - by (simp add: inter project_def set_def)
2.191 - have *: "\<And>x::'a. remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
2.192 - by (simp add: fun_eq_iff)
2.193 - have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
2.194 - fold More_Set.remove xs \<circ> member"
2.195 - by (rule fold_commute) (simp add: fun_eq_iff)
2.196 - then have "fold More_Set.remove xs (member A) =
2.197 - member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
2.198 - by (simp add: fun_eq_iff)
2.199 - then have "inf A (Cset.coset xs) = fold remove xs A"
2.200 - by (simp add: Diff_eq [symmetric] minus_set *)
2.201 - moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
2.202 - by (auto simp add: More_Set.remove_def * intro: ext)
2.203 - ultimately show "inf A (Cset.coset xs) = foldr remove xs A"
2.204 - by (simp add: foldr_fold)
2.205 -qed
2.206 -
2.207 -lemma subtract_remove [code]:
2.208 - "A - Cset.set xs = foldr remove xs A"
2.209 - "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
2.210 - by (simp_all only: diff_eq compl_set compl_coset inter_project)
2.211 -
2.212 -lemma union_insert [code]:
2.213 - "sup (Cset.set xs) A = foldr insert xs A"
2.214 - "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
2.215 -proof -
2.216 - have *: "\<And>x::'a. insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
2.217 - by (simp add: fun_eq_iff)
2.218 - have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
2.219 - fold Set.insert xs \<circ> member"
2.220 - by (rule fold_commute) (simp add: fun_eq_iff)
2.221 - then have "fold Set.insert xs (member A) =
2.222 - member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
2.223 - by (simp add: fun_eq_iff)
2.224 - then have "sup (Cset.set xs) A = fold insert xs A"
2.225 - by (simp add: union_set *)
2.226 - moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
2.227 - by (auto simp add: * intro: ext)
2.228 - ultimately show "sup (Cset.set xs) A = foldr insert xs A"
2.229 - by (simp add: foldr_fold)
2.230 - show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
2.231 - by (auto simp add: coset_def)
2.232 -qed
2.233 -
2.234 +
2.235 context complete_lattice
2.236 begin
2.237
2.238 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
2.239 [simp]: "Infimum A = Inf (member A)"
2.240
2.241 -lemma Infimum_inf [code]:
2.242 - "Infimum (Cset.set As) = foldr inf As top"
2.243 - "Infimum (Cset.coset []) = bot"
2.244 - by (simp_all add: Inf_set_foldr Inf_UNIV)
2.245 -
2.246 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
2.247 [simp]: "Supremum A = Sup (member A)"
2.248
2.249 -lemma Supremum_sup [code]:
2.250 - "Supremum (Cset.set As) = foldr sup As bot"
2.251 - "Supremum (Cset.coset []) = top"
2.252 - by (simp_all add: Sup_set_foldr Sup_UNIV)
2.253 -
2.254 end
2.255
2.256
2.257 @@ -351,7 +145,7 @@
2.258 declare mem_def [simp del]
2.259
2.260
2.261 -hide_const (open) setify is_empty insert remove map filter forall exists card
2.262 +hide_const (open) is_empty insert remove map filter forall exists card
2.263 Inter Union
2.264
2.265 end
3.1 --- a/src/HOL/Library/Dlist_Cset.thy Tue Jun 07 11:11:01 2011 +0200
3.2 +++ b/src/HOL/Library/Dlist_Cset.thy Tue Jun 07 11:12:05 2011 +0200
3.3 @@ -3,21 +3,21 @@
3.4 header {* Canonical implementation of sets by distinct lists *}
3.5
3.6 theory Dlist_Cset
3.7 -imports Dlist Cset
3.8 +imports Dlist List_Cset
3.9 begin
3.10
3.11 definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
3.12 - "Set dxs = Cset.set (list_of_dlist dxs)"
3.13 + "Set dxs = List_Cset.set (list_of_dlist dxs)"
3.14
3.15 definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
3.16 - "Coset dxs = Cset.coset (list_of_dlist dxs)"
3.17 + "Coset dxs = List_Cset.coset (list_of_dlist dxs)"
3.18
3.19 code_datatype Set Coset
3.20
3.21 declare member_code [code del]
3.22 -declare Cset.is_empty_set [code del]
3.23 -declare Cset.empty_set [code del]
3.24 -declare Cset.UNIV_set [code del]
3.25 +declare List_Cset.is_empty_set [code del]
3.26 +declare List_Cset.empty_set [code del]
3.27 +declare List_Cset.UNIV_set [code del]
3.28 declare insert_set [code del]
3.29 declare remove_set [code del]
3.30 declare compl_set [code del]
3.31 @@ -50,11 +50,11 @@
3.32 by (simp add: Coset_def member_set not_set_compl)
3.33
3.34 lemma Set_dlist_of_list [code]:
3.35 - "Cset.set xs = Set (dlist_of_list xs)"
3.36 + "List_Cset.set xs = Set (dlist_of_list xs)"
3.37 by (rule Cset.set_eqI) simp
3.38
3.39 lemma Coset_dlist_of_list [code]:
3.40 - "Cset.coset xs = Coset (dlist_of_list xs)"
3.41 + "List_Cset.coset xs = Coset (dlist_of_list xs)"
3.42 by (rule Cset.set_eqI) simp
3.43
3.44 lemma is_empty_Set [code]:
4.1 --- a/src/HOL/Library/Library.thy Tue Jun 07 11:11:01 2011 +0200
4.2 +++ b/src/HOL/Library/Library.thy Tue Jun 07 11:12:05 2011 +0200
4.3 @@ -29,6 +29,7 @@
4.4 Lattice_Algebras
4.5 Lattice_Syntax
4.6 ListVector
4.7 + List_Cset
4.8 Kleene_Algebra
4.9 Mapping
4.10 Monad_Syntax
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Library/List_Cset.thy Tue Jun 07 11:12:05 2011 +0200
5.3 @@ -0,0 +1,222 @@
5.4 +
5.5 +(* Author: Florian Haftmann, TU Muenchen *)
5.6 +
5.7 +header {* implementation of Cset.sets based on lists *}
5.8 +
5.9 +theory List_Cset
5.10 +imports Cset
5.11 +begin
5.12 +
5.13 +declare mem_def [simp]
5.14 +
5.15 +definition set :: "'a list \<Rightarrow> 'a Cset.set" where
5.16 + "set xs = Set (List.set xs)"
5.17 +hide_const (open) set
5.18 +
5.19 +lemma member_set [simp]:
5.20 + "member (List_Cset.set xs) = set xs"
5.21 + by (simp add: set_def)
5.22 +hide_fact (open) member_set
5.23 +
5.24 +definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
5.25 + "coset xs = Set (- set xs)"
5.26 +hide_const (open) coset
5.27 +
5.28 +lemma member_coset [simp]:
5.29 + "member (List_Cset.coset xs) = - set xs"
5.30 + by (simp add: coset_def)
5.31 +hide_fact (open) member_coset
5.32 +
5.33 +code_datatype List_Cset.set List_Cset.coset
5.34 +
5.35 +lemma member_code [code]:
5.36 + "member (List_Cset.set xs) = List.member xs"
5.37 + "member (List_Cset.coset xs) = Not \<circ> List.member xs"
5.38 + by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
5.39 +
5.40 +lemma member_image_UNIV [simp]:
5.41 + "member ` UNIV = UNIV"
5.42 +proof -
5.43 + have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
5.44 + proof
5.45 + fix A :: "'a set"
5.46 + show "A = member (Set A)" by simp
5.47 + qed
5.48 + then show ?thesis by (simp add: image_def)
5.49 +qed
5.50 +
5.51 +definition (in term_syntax)
5.52 + setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
5.53 + \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
5.54 + [code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\<cdot>} xs"
5.55 +
5.56 +notation fcomp (infixl "\<circ>>" 60)
5.57 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
5.58 +
5.59 +instantiation Cset.set :: (random) random
5.60 +begin
5.61 +
5.62 +definition
5.63 + "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
5.64 +
5.65 +instance ..
5.66 +
5.67 +end
5.68 +
5.69 +no_notation fcomp (infixl "\<circ>>" 60)
5.70 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
5.71 +
5.72 +subsection {* Basic operations *}
5.73 +
5.74 +lemma is_empty_set [code]:
5.75 + "Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs"
5.76 + by (simp add: is_empty_set null_def)
5.77 +hide_fact (open) is_empty_set
5.78 +
5.79 +lemma empty_set [code]:
5.80 + "bot = List_Cset.set []"
5.81 + by (simp add: set_def)
5.82 +hide_fact (open) empty_set
5.83 +
5.84 +lemma UNIV_set [code]:
5.85 + "top = List_Cset.coset []"
5.86 + by (simp add: coset_def)
5.87 +hide_fact (open) UNIV_set
5.88 +
5.89 +lemma remove_set [code]:
5.90 + "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)"
5.91 + "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
5.92 +by (simp_all add: set_def coset_def)
5.93 + (metis List.set_insert More_Set.remove_def remove_set_compl)
5.94 +
5.95 +lemma insert_set [code]:
5.96 + "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)"
5.97 + "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
5.98 + by (simp_all add: set_def coset_def)
5.99 +
5.100 +lemma map_set [code]:
5.101 + "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))"
5.102 + by (simp add: set_def)
5.103 +
5.104 +lemma filter_set [code]:
5.105 + "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)"
5.106 + by (simp add: set_def project_set)
5.107 +
5.108 +lemma forall_set [code]:
5.109 + "Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs"
5.110 + by (simp add: set_def list_all_iff)
5.111 +
5.112 +lemma exists_set [code]:
5.113 + "Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs"
5.114 + by (simp add: set_def list_ex_iff)
5.115 +
5.116 +lemma card_set [code]:
5.117 + "Cset.card (List_Cset.set xs) = length (remdups xs)"
5.118 +proof -
5.119 + have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
5.120 + by (rule distinct_card) simp
5.121 + then show ?thesis by (simp add: set_def)
5.122 +qed
5.123 +
5.124 +lemma compl_set [simp, code]:
5.125 + "- List_Cset.set xs = List_Cset.coset xs"
5.126 + by (simp add: set_def coset_def)
5.127 +
5.128 +lemma compl_coset [simp, code]:
5.129 + "- List_Cset.coset xs = List_Cset.set xs"
5.130 + by (simp add: set_def coset_def)
5.131 +
5.132 +context complete_lattice
5.133 +begin
5.134 +
5.135 +lemma Infimum_inf [code]:
5.136 + "Infimum (List_Cset.set As) = foldr inf As top"
5.137 + "Infimum (List_Cset.coset []) = bot"
5.138 + by (simp_all add: Inf_set_foldr Inf_UNIV)
5.139 +
5.140 +lemma Supremum_sup [code]:
5.141 + "Supremum (List_Cset.set As) = foldr sup As bot"
5.142 + "Supremum (List_Cset.coset []) = top"
5.143 + by (simp_all add: Sup_set_foldr Sup_UNIV)
5.144 +
5.145 +end
5.146 +
5.147 +
5.148 +subsection {* Derived operations *}
5.149 +
5.150 +lemma subset_eq_forall [code]:
5.151 + "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
5.152 + by (simp add: subset_eq)
5.153 +
5.154 +lemma subset_subset_eq [code]:
5.155 + "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
5.156 + by (fact less_le_not_le)
5.157 +
5.158 +instantiation Cset.set :: (type) equal
5.159 +begin
5.160 +
5.161 +definition [code]:
5.162 + "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
5.163 +
5.164 +instance proof
5.165 +qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
5.166 +
5.167 +end
5.168 +
5.169 +lemma [code nbe]:
5.170 + "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
5.171 + by (fact equal_refl)
5.172 +
5.173 +
5.174 +subsection {* Functorial operations *}
5.175 +
5.176 +lemma inter_project [code]:
5.177 + "inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)"
5.178 + "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
5.179 +proof -
5.180 + show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)"
5.181 + by (simp add: inter project_def set_def)
5.182 + have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
5.183 + by (simp add: fun_eq_iff More_Set.remove_def)
5.184 + have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
5.185 + fold More_Set.remove xs \<circ> member"
5.186 + by (rule fold_commute) (simp add: fun_eq_iff)
5.187 + then have "fold More_Set.remove xs (member A) =
5.188 + member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
5.189 + by (simp add: fun_eq_iff)
5.190 + then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
5.191 + by (simp add: Diff_eq [symmetric] minus_set *)
5.192 + moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
5.193 + by (auto simp add: More_Set.remove_def * intro: ext)
5.194 + ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
5.195 + by (simp add: foldr_fold)
5.196 +qed
5.197 +
5.198 +lemma subtract_remove [code]:
5.199 + "A - List_Cset.set xs = foldr Cset.remove xs A"
5.200 + "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)"
5.201 + by (simp_all only: diff_eq compl_set compl_coset inter_project)
5.202 +
5.203 +lemma union_insert [code]:
5.204 + "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
5.205 + "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
5.206 +proof -
5.207 + have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
5.208 + by (simp add: fun_eq_iff)
5.209 + have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
5.210 + fold Set.insert xs \<circ> member"
5.211 + by (rule fold_commute) (simp add: fun_eq_iff)
5.212 + then have "fold Set.insert xs (member A) =
5.213 + member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
5.214 + by (simp add: fun_eq_iff)
5.215 + then have "sup (List_Cset.set xs) A = fold Cset.insert xs A"
5.216 + by (simp add: union_set *)
5.217 + moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
5.218 + by (auto simp add: * intro: ext)
5.219 + ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
5.220 + by (simp add: foldr_fold)
5.221 + show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
5.222 + by (auto simp add: coset_def)
5.223 +qed
5.224 +
5.225 +end
5.226 \ No newline at end of file