diff -r 9163c0f9830d -r c0f2db9a243b IntEx.thy --- a/IntEx.thy Mon Oct 26 19:35:30 2009 +0100 +++ b/IntEx.thy Tue Oct 27 07:46:52 2009 +0100 @@ -132,6 +132,10 @@ ML {* val quot = @{thm QUOTIENT_my_int} *} ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} +ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} +ML {* val t_defs = @{thms PLUS_def} *} + + ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} @@ -150,24 +154,6 @@ ) *} -ML {* -fun make_simp_lam_prs_thm lthy quot_thm typ = - let - val (_, [lty, rty]) = dest_Type typ; - val thy = ProofContext.theory_of lthy; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [SOME lcty, NONE, SOME rcty]; - val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; - val tac = - (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW - (quotient_tac quot_thm); - val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); - val ts = @{thm HOL.sym} OF [t] - in - MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts - end -*} - ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} @@ -180,25 +166,11 @@ ML {* t_t2 *} ML {* val t_l = simp_lam_prs @{context} t_t2 *} -ML {* - fun simp_allex_prs lthy quot thm = - let - val rwf = @{thm FORALL_PRS} OF [quot]; - val rwfs = @{thm "HOL.sym"} OF [rwf]; - val rwe = @{thm EXISTS_PRS} OF [quot]; - val rwes = @{thm "HOL.sym"} OF [rwe] - in - (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm)) - end - handle _ => thm -*} - ML {* val t_a = simp_allex_prs @{context} quot t_l *} -ML {* val t_defs = @{thms PLUS_def} *} ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} -ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *} +ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} ML {* ObjectLogic.rulify t_r *} lemma