|
1 (* Title: HOL/Library/Crude_Executable_Set.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} |
|
6 |
|
7 theory Crude_Executable_Set |
|
8 imports List_Set |
|
9 begin |
|
10 |
|
11 declare mem_def [code del] |
|
12 declare Collect_def [code del] |
|
13 declare insert_code [code del] |
|
14 declare vimage_code [code del] |
|
15 |
|
16 subsection {* Set representation *} |
|
17 |
|
18 setup {* |
|
19 Code.add_type_cmd "set" |
|
20 *} |
|
21 |
|
22 definition Set :: "'a list \<Rightarrow> 'a set" where |
|
23 [simp]: "Set = set" |
|
24 |
|
25 definition Coset :: "'a list \<Rightarrow> 'a set" where |
|
26 [simp]: "Coset xs = - set xs" |
|
27 |
|
28 setup {* |
|
29 Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set") |
|
30 #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set") |
|
31 #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set") |
|
32 #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool") |
|
33 *} |
|
34 |
|
35 code_datatype Set Coset |
|
36 |
|
37 |
|
38 subsection {* Basic operations *} |
|
39 |
|
40 lemma [code]: |
|
41 "set xs = Set (remdups xs)" |
|
42 by simp |
|
43 |
|
44 lemma [code]: |
|
45 "x \<in> Set xs \<longleftrightarrow> member x xs" |
|
46 "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs" |
|
47 by (simp_all add: mem_iff) |
|
48 |
|
49 definition is_empty :: "'a set \<Rightarrow> bool" where |
|
50 [simp]: "is_empty A \<longleftrightarrow> A = {}" |
|
51 |
|
52 lemma [code_inline]: |
|
53 "A = {} \<longleftrightarrow> is_empty A" |
|
54 by simp |
|
55 |
|
56 definition empty :: "'a set" where |
|
57 [simp]: "empty = {}" |
|
58 |
|
59 lemma [code_inline]: |
|
60 "{} = empty" |
|
61 by simp |
|
62 |
|
63 setup {* |
|
64 Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool") |
|
65 #> Code.add_signature_cmd ("empty", "'a set") |
|
66 #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
67 #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
68 #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set") |
|
69 #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
70 #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
|
71 #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
|
72 #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat") |
|
73 *} |
|
74 |
|
75 lemma is_empty_Set [code]: |
|
76 "is_empty (Set xs) \<longleftrightarrow> null xs" |
|
77 by (simp add: empty_null) |
|
78 |
|
79 lemma empty_Set [code]: |
|
80 "empty = Set []" |
|
81 by simp |
|
82 |
|
83 lemma insert_Set [code]: |
|
84 "insert x (Set xs) = Set (List_Set.insert x xs)" |
|
85 "insert x (Coset xs) = Coset (remove_all x xs)" |
|
86 by (simp_all add: insert_set insert_set_compl) |
|
87 |
|
88 lemma remove_Set [code]: |
|
89 "remove x (Set xs) = Set (remove_all x xs)" |
|
90 "remove x (Coset xs) = Coset (List_Set.insert x xs)" |
|
91 by (simp_all add:remove_set remove_set_compl) |
|
92 |
|
93 lemma image_Set [code]: |
|
94 "image f (Set xs) = Set (remdups (map f xs))" |
|
95 by simp |
|
96 |
|
97 lemma project_Set [code]: |
|
98 "project P (Set xs) = Set (filter P xs)" |
|
99 by (simp add: project_set) |
|
100 |
|
101 lemma Ball_Set [code]: |
|
102 "Ball (Set xs) P \<longleftrightarrow> list_all P xs" |
|
103 by (simp add: ball_set) |
|
104 |
|
105 lemma Bex_Set [code]: |
|
106 "Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
|
107 by (simp add: bex_set) |
|
108 |
|
109 lemma card_Set [code]: |
|
110 "card (Set xs) = length (remdups xs)" |
|
111 proof - |
|
112 have "card (set (remdups xs)) = length (remdups xs)" |
|
113 by (rule distinct_card) simp |
|
114 then show ?thesis by simp |
|
115 qed |
|
116 |
|
117 |
|
118 subsection {* Derived operations *} |
|
119 |
|
120 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
121 [simp]: "set_eq = op =" |
|
122 |
|
123 lemma [code_inline]: |
|
124 "op = = set_eq" |
|
125 by simp |
|
126 |
|
127 definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
128 [simp]: "subset_eq = op \<subseteq>" |
|
129 |
|
130 lemma [code_inline]: |
|
131 "op \<subseteq> = subset_eq" |
|
132 by simp |
|
133 |
|
134 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
135 [simp]: "subset = op \<subset>" |
|
136 |
|
137 lemma [code_inline]: |
|
138 "op \<subset> = subset" |
|
139 by simp |
|
140 |
|
141 setup {* |
|
142 Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
143 #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
144 #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
145 *} |
|
146 |
|
147 lemma set_eq_subset_eq [code]: |
|
148 "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A" |
|
149 by auto |
|
150 |
|
151 lemma subset_eq_forall [code]: |
|
152 "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
153 by (simp add: subset_eq) |
|
154 |
|
155 lemma subset_subset_eq [code]: |
|
156 "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A" |
|
157 by (simp add: subset) |
|
158 |
|
159 |
|
160 subsection {* Functorial operations *} |
|
161 |
|
162 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
163 [simp]: "inter = op \<inter>" |
|
164 |
|
165 lemma [code_inline]: |
|
166 "op \<inter> = inter" |
|
167 by simp |
|
168 |
|
169 definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
170 [simp]: "subtract A B = B - A" |
|
171 |
|
172 lemma [code_inline]: |
|
173 "B - A = subtract A B" |
|
174 by simp |
|
175 |
|
176 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
177 [simp]: "union = op \<union>" |
|
178 |
|
179 lemma [code_inline]: |
|
180 "op \<union> = union" |
|
181 by simp |
|
182 |
|
183 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
184 [simp]: "Inf = Complete_Lattice.Inf" |
|
185 |
|
186 lemma [code_inline]: |
|
187 "Complete_Lattice.Inf = Inf" |
|
188 by simp |
|
189 |
|
190 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
191 [simp]: "Sup = Complete_Lattice.Sup" |
|
192 |
|
193 lemma [code_inline]: |
|
194 "Complete_Lattice.Sup = Sup" |
|
195 by simp |
|
196 |
|
197 definition Inter :: "'a set set \<Rightarrow> 'a set" where |
|
198 [simp]: "Inter = Inf" |
|
199 |
|
200 lemma [code_inline]: |
|
201 "Inf = Inter" |
|
202 by simp |
|
203 |
|
204 definition Union :: "'a set set \<Rightarrow> 'a set" where |
|
205 [simp]: "Union = Sup" |
|
206 |
|
207 lemma [code_inline]: |
|
208 "Sup = Union" |
|
209 by simp |
|
210 |
|
211 setup {* |
|
212 Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
213 #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
214 #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
215 #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a") |
|
216 #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a") |
|
217 #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set") |
|
218 #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set") |
|
219 *} |
|
220 |
|
221 lemma inter_project [code]: |
|
222 "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
223 "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs" |
|
224 by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set) |
|
225 |
|
226 lemma subtract_remove [code]: |
|
227 "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs" |
|
228 "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
229 by (auto simp add: minus_set) |
|
230 |
|
231 lemma union_insert [code]: |
|
232 "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs" |
|
233 "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
|
234 by (auto simp add: union_set) |
|
235 |
|
236 lemma Inf_inf [code]: |
|
237 "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs" |
|
238 "Inf (Coset []) = (bot :: 'a::complete_lattice)" |
|
239 by (simp_all add: Inf_Univ bot_def [symmetric] Inf_set_fold) |
|
240 |
|
241 lemma Sup_sup [code]: |
|
242 "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs" |
|
243 "Sup (Coset []) = (top :: 'a::complete_lattice)" |
|
244 by (simp_all add: Sup_Univ top_def [symmetric] Sup_set_fold) |
|
245 |
|
246 lemma Inter_inter [code]: |
|
247 "Inter (Set xs) = foldl inter (Coset []) xs" |
|
248 "Inter (Coset []) = empty" |
|
249 unfolding Inter_def Inf_inf by simp_all |
|
250 |
|
251 lemma Union_union [code]: |
|
252 "Union (Set xs) = foldl union empty xs" |
|
253 "Union (Coset []) = Coset []" |
|
254 unfolding Union_def Sup_sup by simp_all |
|
255 |
|
256 hide (open) const is_empty empty remove |
|
257 set_eq subset_eq subset inter union subtract Inf Sup Inter Union |
|
258 |
|
259 end |