equal
deleted
inserted
replaced
299 print_quotients |
299 print_quotients |
300 |
300 |
301 |
301 |
302 ML {* val qty = @{typ "'a fset"} *} |
302 ML {* val qty = @{typ "'a fset"} *} |
303 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 *} |
304 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} |
304 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
305 |
305 |
306 ML {* val rsp_thms = |
306 ML {* val rsp_thms = |
307 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
307 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
308 @ @{thms ho_all_prs ho_ex_prs} *} |
308 @ @{thms ho_all_prs ho_ex_prs} *} |
309 |
309 |
356 ) |
356 ) |
357 *} |
357 *} |
358 |
358 |
359 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
359 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
360 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
360 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
361 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
|
362 thm APP_PRS |
|
363 ML aps |
|
364 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
361 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
365 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
362 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
366 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} |
363 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} |
367 ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} |
364 ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} |
368 ML {* val defs_sym = add_lower_defs @{context} defs *} |
365 ML {* val defs_sym = add_lower_defs @{context} defs *} |