365 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
365 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
366 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
366 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
367 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
367 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
368 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
368 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
369 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
369 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
370 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l *} |
370 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} |
371 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
371 ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} |
372 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
|
373 ML {* val defs_sym = add_lower_defs @{context} defs *} |
372 ML {* val defs_sym = add_lower_defs @{context} defs *} |
374 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *} |
373 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a *} |
375 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
374 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
376 ML {* ObjectLogic.rulify ind_r_s *} |
375 ML {* ObjectLogic.rulify ind_r_s *} |
377 |
376 |
378 ML {* |
377 ML {* |
379 fun lift_thm_fset_note name thm lthy = |
378 fun lift_thm_fset_note name thm lthy = |