diff -r a296bf1a3b09 -r 03c03e88efa9 IntEx.thy --- a/IntEx.thy Mon Oct 26 14:16:32 2009 +0100 +++ b/IntEx.thy Mon Oct 26 15:31:53 2009 +0100 @@ -142,15 +142,6 @@ repabs_eq2 @{context} (g, thm, othm) ) *} -ML {* - val lpi = Drule.instantiate' - [SOME @{ctyp "nat \ nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; -*} -prove lambda_prs_mn_b : {* concl_of lpi *} -apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) -apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) -apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) -done ML {* fun make_simp_lam_prs_thm lthy quot_thm typ = @@ -166,26 +157,23 @@ 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_def}] ts + MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts end *} - +thm id_apply 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 *} thm HOL.sym[OF lambda_prs_mn_b,simplified] ML {* fun simp_lam_prs lthy thm = - simp_lam_prs lthy (eqsubst_thm lthy - @{thms HOL.sym[OF lambda_prs_mn_b,simplified]} - thm) + simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) handle _ => thm *} ML {* t_t2 *} ML {* val t_l = simp_lam_prs @{context} t_t2 *} -ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} ML {* fun simp_allex_prs lthy thm =