equal
deleted
inserted
replaced
175 |
175 |
176 term map |
176 term map |
177 term fmap |
177 term fmap |
178 thm fmap_def |
178 thm fmap_def |
179 |
179 |
180 ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def card_def INSERT_def fmap_def fold_def} *} |
180 ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *} |
181 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
181 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
182 |
182 |
183 ML {* |
183 ML {* |
184 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
184 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
185 @{const_name "membship"}, @{const_name "card1"}, |
185 @{const_name "membship"}, @{const_name "card1"}, |
186 @{const_name "append"}, @{const_name "fold1"}, |
186 @{const_name "append"}, @{const_name "fold1"}, |
187 @{const_name "map"}]; |
187 @{const_name "map"}]; |
188 *} |
188 *} |
189 |
189 |
190 (* FIXME: does not work anymore :o( *) |
|
191 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
190 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
192 |
191 |
193 lemma memb_rsp: |
192 lemma memb_rsp: |
194 fixes z |
193 fixes z |
195 assumes a: "list_eq x y" |
194 assumes a: "list_eq x y" |
313 ML {* val rsp_thms = |
312 ML {* val rsp_thms = |
314 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
313 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
315 @ @{thms ho_all_prs ho_ex_prs} *} |
314 @ @{thms ho_all_prs ho_ex_prs} *} |
316 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *} |
315 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *} |
317 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *} |
316 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *} |
318 ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
317 ML {* val defs = fset_defs *} |
319 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
318 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
320 ML {* |
319 ML {* |
321 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
320 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
322 @{const_name "membship"}, @{const_name "card1"}, |
321 @{const_name "membship"}, @{const_name "card1"}, |
323 @{const_name "append"}, @{const_name "fold1"}, |
322 @{const_name "append"}, @{const_name "fold1"}, |