equal
deleted
inserted
replaced
151 |
151 |
152 term membship |
152 term membship |
153 term IN |
153 term IN |
154 thm IN_def |
154 thm IN_def |
155 |
155 |
156 (* FIXME: does not work yet |
156 term fold1 |
157 quotient_def (for "'a fset") |
157 quotient_def |
158 FOLD :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
158 FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
159 where |
159 where |
160 "FOLD \<equiv> fold1" |
160 "FOLD \<equiv> fold1" |
161 *) |
|
162 local_setup {* |
|
163 old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
|
164 *} |
|
165 |
161 |
166 term fold1 |
162 term fold1 |
167 term fold |
163 term fold |
168 thm fold_def |
164 thm fold_def |
169 |
165 |
170 (* FIXME: does not work yet for all types*) |
|
171 quotient_def |
166 quotient_def |
172 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
167 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
173 where |
168 where |
174 "fmap \<equiv> map" |
169 "fmap \<equiv> map" |
175 |
170 |
176 term map |
171 term map |
177 term fmap |
172 term fmap |
178 thm fmap_def |
173 thm fmap_def |
179 |
174 |
180 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *} |
175 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} |
|
176 ML {* val consts = lookup_quot_consts defs *} |
|
177 ML {* val defs_sym = add_lower_defs @{context} defs *} |
181 |
178 |
182 lemma memb_rsp: |
179 lemma memb_rsp: |
183 fixes z |
180 fixes z |
184 assumes a: "list_eq x y" |
181 assumes a: "list_eq x y" |
185 shows "(z memb x) = (z memb y)" |
182 shows "(z memb x) = (z memb y)" |