354 ) |
354 ) |
355 *} |
355 *} |
356 |
356 |
357 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
357 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
358 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
358 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
359 |
359 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
360 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
360 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
361 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *} |
361 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
362 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
362 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l *} |
363 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
|
364 done |
|
365 |
|
366 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
|
367 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
|
368 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
|
369 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
|
370 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
|
371 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
363 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
372 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
364 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
373 ML {* val defs_sym = add_lower_defs @{context} defs *} |
365 ML {* val defs_sym = add_lower_defs @{context} defs *} |
374 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *} |
366 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *} |
375 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
367 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |