equal
deleted
inserted
replaced
42 term Nil |
42 term Nil |
43 term EMPTY |
43 term EMPTY |
44 thm EMPTY_def |
44 thm EMPTY_def |
45 |
45 |
46 quotient_def (for "'a fset") |
46 quotient_def (for "'a fset") |
47 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet" |
47 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
48 where |
48 where |
49 "INSERT \<equiv> op #" |
49 "INSERT \<equiv> op #" |
50 |
50 |
51 term Cons |
51 term Cons |
52 term INSERT |
52 term INSERT |
166 term fold1 |
166 term fold1 |
167 term fold |
167 term fold |
168 thm fold_def |
168 thm fold_def |
169 |
169 |
170 (* FIXME: does not work yet for all types*) |
170 (* FIXME: does not work yet for all types*) |
171 quotient_def (for "'a fset") |
171 quotient_def (for "'a fset" "'b fset") |
172 fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
172 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
173 where |
173 where |
174 "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
174 "fmap \<equiv> map" |
175 |
175 |
176 term map |
176 term map |
177 term fmap |
177 term fmap |
178 thm fmap_def |
178 thm fmap_def |
179 |
179 |
292 |
292 |
293 lemma map_append : |
293 lemma map_append : |
294 "(map f ((a::'a list) @ b)) \<approx> |
294 "(map f ((a::'a list) @ b)) \<approx> |
295 ((map f a) ::'a list) @ (map f b)" |
295 ((map f a) ::'a list) @ (map f b)" |
296 by simp (rule list_eq_refl) |
296 by simp (rule list_eq_refl) |
|
297 |
|
298 |
|
299 print_quotients |
297 |
300 |
298 |
301 |
299 ML {* val qty = @{typ "'a fset"} *} |
302 ML {* val qty = @{typ "'a fset"} *} |
300 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
303 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
301 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} |
304 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} |