34 |
36 |
35 |
37 |
36 subsection {* Basic operations *} |
38 subsection {* Basic operations *} |
37 |
39 |
38 definition is_empty :: "'a fset \<Rightarrow> bool" where |
40 definition is_empty :: "'a fset \<Rightarrow> bool" where |
39 "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)" |
41 [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)" |
40 |
42 |
41 lemma is_empty_Set [code]: |
43 lemma is_empty_Set [code]: |
42 "is_empty (Set xs) \<longleftrightarrow> null xs" |
44 "is_empty (Set xs) \<longleftrightarrow> null xs" |
43 by (simp add: is_empty_def is_empty_set) |
45 by (simp add: is_empty_set) |
44 |
46 |
45 definition empty :: "'a fset" where |
47 definition empty :: "'a fset" where |
46 "empty = Fset {}" |
48 [simp]: "empty = Fset {}" |
47 |
49 |
48 lemma empty_Set [code]: |
50 lemma empty_Set [code]: |
49 "empty = Set []" |
51 "empty = Set []" |
50 by (simp add: empty_def Set_def) |
52 by (simp add: Set_def) |
51 |
53 |
52 definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
54 definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
53 "insert x A = Fset (Set.insert x (member A))" |
55 [simp]: "insert x A = Fset (Set.insert x (member A))" |
54 |
56 |
55 lemma insert_Set [code]: |
57 lemma insert_Set [code]: |
56 "insert x (Set xs) = Set (List_Set.insert x xs)" |
58 "insert x (Set xs) = Set (List_Set.insert x xs)" |
57 by (simp add: insert_def Set_def insert_set) |
59 by (simp add: Set_def insert_set) |
58 |
60 |
59 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
61 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
60 "remove x A = Fset (List_Set.remove x (member A))" |
62 [simp]: "remove x A = Fset (List_Set.remove x (member A))" |
61 |
63 |
62 lemma remove_Set [code]: |
64 lemma remove_Set [code]: |
63 "remove x (Set xs) = Set (remove_all x xs)" |
65 "remove x (Set xs) = Set (remove_all x xs)" |
64 by (simp add: remove_def Set_def remove_set) |
66 by (simp add: Set_def remove_set) |
65 |
67 |
66 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where |
68 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where |
67 "map f A = Fset (image f (member A))" |
69 [simp]: "map f A = Fset (image f (member A))" |
68 |
70 |
69 lemma map_Set [code]: |
71 lemma map_Set [code]: |
70 "map f (Set xs) = Set (remdups (List.map f xs))" |
72 "map f (Set xs) = Set (remdups (List.map f xs))" |
71 by (simp add: map_def Set_def) |
73 by (simp add: Set_def) |
72 |
74 |
73 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
75 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
74 "project P A = Fset (List_Set.project P (member A))" |
76 [simp]: "project P A = Fset (List_Set.project P (member A))" |
75 |
77 |
76 lemma project_Set [code]: |
78 lemma project_Set [code]: |
77 "project P (Set xs) = Set (filter P xs)" |
79 "project P (Set xs) = Set (filter P xs)" |
78 by (simp add: project_def Set_def project_set) |
80 by (simp add: Set_def project_set) |
79 |
81 |
80 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
82 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
81 "forall P A \<longleftrightarrow> Ball (member A) P" |
83 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P" |
82 |
84 |
83 lemma forall_Set [code]: |
85 lemma forall_Set [code]: |
84 "forall P (Set xs) \<longleftrightarrow> list_all P xs" |
86 "forall P (Set xs) \<longleftrightarrow> list_all P xs" |
85 by (simp add: forall_def Set_def ball_set) |
87 by (simp add: Set_def ball_set) |
86 |
88 |
87 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
89 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where |
88 "exists P A \<longleftrightarrow> Bex (member A) P" |
90 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P" |
89 |
91 |
90 lemma exists_Set [code]: |
92 lemma exists_Set [code]: |
91 "exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
93 "exists P (Set xs) \<longleftrightarrow> list_ex P xs" |
92 by (simp add: exists_def Set_def bex_set) |
94 by (simp add: Set_def bex_set) |
|
95 |
|
96 |
|
97 subsection {* Derived operations *} |
|
98 |
|
99 lemma member_exists [code]: |
|
100 "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A" |
|
101 by simp |
|
102 |
|
103 definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
104 [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B" |
|
105 |
|
106 lemma subfset_eq_forall [code]: |
|
107 "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A" |
|
108 by (simp add: subset_eq) |
|
109 |
|
110 definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
|
111 [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B" |
|
112 |
|
113 lemma subfset_subfset_eq [code]: |
|
114 "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A" |
|
115 by (simp add: subset) |
|
116 |
|
117 lemma eq_fset_subfset_eq [code]: |
|
118 "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A" |
|
119 by (cases A, cases B) (simp add: eq set_eq) |
|
120 |
|
121 definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
|
122 [simp]: "inter A B = Fset (List_Set.project (member A) (member B))" |
|
123 |
|
124 lemma inter_project [code]: |
|
125 "inter A B = project (member A) B" |
|
126 by (simp add: inter) |
93 |
127 |
94 |
128 |
95 subsection {* Functorial operations *} |
129 subsection {* Functorial operations *} |
96 |
130 |
97 definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
131 definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
98 "union A B = Fset (member A \<union> member B)" |
132 [simp]: "union A B = Fset (member A \<union> member B)" |
99 |
133 |
100 lemma union_insert [code]: |
134 lemma union_insert [code]: |
101 "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
135 "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
102 proof - |
136 proof - |
103 have "foldl (\<lambda>A x. Set.insert x A) (member A) xs = |
137 have "foldl (\<lambda>A x. Set.insert x A) (member A) xs = |
104 member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)" |
138 member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)" |
105 by (rule foldl_apply_inv) simp |
139 by (rule foldl_apply_inv) simp |
106 then show ?thesis by (simp add: union_def union_set insert_def) |
140 then show ?thesis by (simp add: union_set) |
107 qed |
141 qed |
108 |
142 |
109 definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
143 definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
110 "subtract A B = Fset (member B - member A)" |
144 [simp]: "subtract A B = Fset (member B - member A)" |
111 |
145 |
112 lemma subtract_remove [code]: |
146 lemma subtract_remove [code]: |
113 "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" |
147 "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" |
114 proof - |
148 proof - |
115 have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs = |
149 have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs = |
116 member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)" |
150 member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)" |
117 by (rule foldl_apply_inv) simp |
151 by (rule foldl_apply_inv) simp |
118 then show ?thesis by (simp add: subtract_def minus_set remove_def) |
152 then show ?thesis by (simp add: minus_set) |
119 qed |
153 qed |
120 |
154 |
121 |
155 definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where |
122 subsection {* Derived operations *} |
156 [simp]: "Inter A = Fset (Set.Inter (member ` member A))" |
123 |
157 |
124 lemma member_exists [code]: |
158 lemma Inter_inter [code]: |
125 "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A" |
159 "Inter (Set (A # As)) = foldl inter A As" |
126 by (simp add: exists_def mem_def) |
160 proof - |
127 |
161 note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del] |
128 definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
162 have "foldl (op \<inter>) (member A) (List.map member As) = |
129 "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B" |
163 member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))" |
130 |
164 by (rule foldl_apply_inv) simp |
131 lemma subfset_eq_forall [code]: |
165 then show ?thesis |
132 "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A" |
166 by (simp add: Inter_set image_set inter_def_raw inter foldl_map) |
133 by (simp add: subfset_eq_def subset_eq forall_def mem_def) |
167 qed |
134 |
168 |
135 definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where |
169 definition Union :: "'a fset fset \<Rightarrow> 'a fset" where |
136 "subfset A B \<longleftrightarrow> member A \<subset> member B" |
170 [simp]: "Union A = Fset (Set.Union (member ` member A))" |
137 |
171 |
138 lemma subfset_subfset_eq [code]: |
172 lemma Union_union [code]: |
139 "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A" |
173 "Union (Set As) = foldl union empty As" |
140 by (simp add: subfset_def subfset_eq_def subset) |
174 proof - |
141 |
175 note Union_image_eq [simp del] set_map [simp del] |
142 lemma eq_fset_subfset_eq [code]: |
176 have "foldl (op \<union>) (member empty) (List.map member As) = |
143 "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A" |
177 member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))" |
144 by (cases A, cases B) (simp add: eq subfset_eq_def set_eq) |
178 by (rule foldl_apply_inv) simp |
145 |
179 then show ?thesis |
146 definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where |
180 by (simp add: Union_set image_set union_def_raw foldl_map) |
147 "inter A B = Fset (List_Set.project (member A) (member B))" |
181 qed |
148 |
|
149 lemma inter_project [code]: |
|
150 "inter A B = project (member A) B" |
|
151 by (simp add: inter_def project_def inter) |
|
152 |
182 |
153 |
183 |
154 subsection {* Misc operations *} |
184 subsection {* Misc operations *} |
155 |
185 |
156 lemma size_fset [code]: |
186 lemma size_fset [code]: |