equal
deleted
inserted
replaced
156 |
156 |
157 term fold1 |
157 term fold1 |
158 term fold |
158 term fold |
159 thm fold_def |
159 thm fold_def |
160 |
160 |
161 local_setup {* |
161 quotient_def (for "'a fset") |
162 old_make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn |
162 fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
163 @{typ "'a list"} @{typ "'a fset"} #> snd |
163 where |
164 *} |
164 "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
165 |
165 |
166 term map |
166 term map |
167 term fmap |
167 term fmap |
168 thm fmap_def |
168 thm fmap_def |
169 |
|
170 |
169 |
171 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
170 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
172 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
171 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
173 |
172 |
174 ML {* |
173 ML {* |