equal
deleted
inserted
replaced
331 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
331 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
332 |
332 |
333 term list_rec |
333 term list_rec |
334 |
334 |
335 quotient_def |
335 quotient_def |
336 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'b" |
336 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
337 where |
337 where |
338 "fset_rec \<equiv> list_rec" |
338 "fset_rec \<equiv> list_rec" |
339 |
339 |
340 thm list.recs(2) |
340 thm list.recs(2) |
341 thm list.cases |
341 thm list.cases |
349 ML {* val defs_sym = add_lower_defs @{context} defs *} |
349 ML {* val defs_sym = add_lower_defs @{context} defs *} |
350 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
350 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
351 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
351 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
352 |
352 |
353 |
353 |
354 ML {* val ind_r_a = atomize_thm @{thm card1_suc} *} |
354 ML {* val ind_r_a = atomize_thm @{thm map_append} *} |
355 (* prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
355 prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
356 ML_prf {* fun tac ctxt = |
356 ML_prf {* fun tac ctxt = |
357 (FIRST' [ |
357 (FIRST' [ |
358 rtac rel_refl, |
358 rtac rel_refl, |
359 atac, |
359 atac, |
360 rtac @{thm get_rid}, |
360 rtac @{thm get_rid}, |