equal
deleted
inserted
replaced
119 |
119 |
120 lemma fsingleton_eq[simp]: |
120 lemma fsingleton_eq[simp]: |
121 shows "{|x|} = {|y|} \<longleftrightarrow> x = y" |
121 shows "{|x|} = {|y|} \<longleftrightarrow> x = y" |
122 by (lifting singleton_list_eq) |
122 by (lifting singleton_list_eq) |
123 |
123 |
|
124 section {* Union *} |
|
125 |
|
126 quotient_definition |
|
127 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65) |
|
128 as |
|
129 "op @" |
124 |
130 |
125 section {* Cardinality of finite sets *} |
131 section {* Cardinality of finite sets *} |
126 |
132 |
127 fun |
133 fun |
128 fcard_raw :: "'a list \<Rightarrow> nat" |
134 fcard_raw :: "'a list \<Rightarrow> nat" |
211 quotient_definition |
217 quotient_definition |
212 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
218 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
213 as |
219 as |
214 "map" |
220 "map" |
215 |
221 |
216 (* PROPBLEM |
|
217 quotient_definition |
222 quotient_definition |
218 "fconcat :: ('a fset) fset => 'a fset" |
223 "fconcat :: ('a fset) fset => 'a fset" |
219 as |
224 as |
220 "concat" |
225 "concat" |
221 |
226 |
222 term concat |
227 lemma fconcat_rsp[quot_respect]: |
223 term fconcat |
228 shows "((list_rel op \<approx>) ===> op \<approx>) concat concat" |
224 *) |
229 apply(auto) |
225 |
230 sorry |
226 consts |
231 |
227 fconcat :: "('a fset) fset => 'a fset" |
232 (* PROBLEM: these lemmas needs to be restated, since *) |
|
233 (* concat.simps(1) and concat.simps(2) contain the *) |
|
234 (* type variables ?'a1.0 (which are turned into frees *) |
|
235 (* 'a_1 *) |
|
236 lemma concat1: |
|
237 shows "concat [] = []" |
|
238 by (simp) |
|
239 |
|
240 lemma concat2: |
|
241 shows "concat (x # xs) = x @ concat xs" |
|
242 by (simp) |
|
243 |
|
244 lemma fconcat_empty: |
|
245 shows "fconcat {||} = {||}" |
|
246 apply(lifting concat1) |
|
247 apply(injection) |
|
248 defer |
|
249 apply(cleaning) |
|
250 apply(simp add: comp_def) |
|
251 apply(cleaning) |
|
252 apply(fold fempty_def[simplified id_simps]) |
|
253 apply(rule refl) |
|
254 sorry |
|
255 |
|
256 lemma fconcat_insert: |
|
257 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
|
258 apply(lifting concat2) |
|
259 apply(injection) |
|
260 defer |
|
261 apply(cleaning) |
|
262 apply(simp add: comp_def) |
|
263 apply(cleaning) |
|
264 sorry |
228 |
265 |
229 text {* raw section *} |
266 text {* raw section *} |
230 |
267 |
231 lemma map_rsp_aux: |
268 lemma map_rsp_aux: |
232 assumes a: "a \<approx> b" |
269 assumes a: "a \<approx> b" |