615 Toplevel.program (fn () => |
615 Toplevel.program (fn () => |
616 repabs_eq2 @{context} (g, thm, othm) |
616 repabs_eq2 @{context} (g, thm, othm) |
617 ) |
617 ) |
618 *} |
618 *} |
619 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
619 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
620 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l *} |
|
621 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a *} |
|
622 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
|
623 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
620 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
624 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
621 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
625 done |
622 done |
|
623 |
|
624 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
|
625 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
|
626 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
|
627 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
|
628 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
|
629 ML {* val thm = @{thm spec[OF FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]],symmetric]} *} |
|
630 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
|
631 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
|
632 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
|
633 ML {* ObjectLogic.rulify ind_r_s *} |
626 |
634 |
627 ML {* |
635 ML {* |
628 fun lift thm = |
636 fun lift thm = |
629 let |
637 let |
630 val ind_r_a = atomize_thm thm; |
638 val ind_r_a = atomize_thm thm; |