# HG changeset patch # User Christian Urban # Date 1260049122 -3600 # Node ID 96c241932603bf085bd398582e149a2eed408082 # Parent ff37ffbb128a2d893cdddd95e36690060b1179f5 moved all_prs and ex_prs out from the conversion into the simplifier diff -r ff37ffbb128a -r 96c241932603 IntEx.thy --- a/IntEx.thy Sat Dec 05 22:16:17 2009 +0100 +++ b/IntEx.thy Sat Dec 05 22:38:42 2009 +0100 @@ -154,10 +154,12 @@ abbreviation "Resp \ Respects" + lemma "PLUS a b = PLUS a b" apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* simp_tac (HOL_basic_ss addSolver quotient_solver addsimps @{thms all_prs}) 1 *}) apply(tactic {* clean_tac @{context} 1 *}) done diff -r ff37ffbb128a -r 96c241932603 QuotMain.thy --- a/QuotMain.thy Sat Dec 05 22:16:17 2009 +0100 +++ b/QuotMain.thy Sat Dec 05 22:38:42 2009 +0100 @@ -1044,54 +1044,28 @@ fun lambda_allex_prs_simple_conv ctxt ctrm = case (term_of ctrm) of ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => - let - val (ty_b, ty_a) = dest_fun_type (fastype_of r1); - val (ty_c, ty_d) = dest_fun_type (fastype_of a2); - val thy = ProofContext.theory_of ctxt; - val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] - val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] - val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; - val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] - val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te - val tl = Thm.lhs_of ts; - val (insp, inst) = make_inst (term_of tl) (term_of ctrm); - val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; - in - Conv.rewr_conv ti ctrm - end - | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ - (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => - let - val (ty_a, ty_b) = dest_fun_type (fastype_of absf); - val thy = ProofContext.theory_of ctxt; - val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; - val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; - val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; - val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; - in - Conv.rewr_conv ti ctrm - end - | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ - (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => - let - val (ty_a, ty_b) = dest_fun_type (fastype_of absf); - val thy = ProofContext.theory_of ctxt; - val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; - val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; - val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; - val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; - in - Conv.rewr_conv ti ctrm - end + let + val (ty_b, ty_a) = dest_fun_type (fastype_of r1); + val (ty_c, ty_d) = dest_fun_type (fastype_of a2); + val thy = ProofContext.theory_of ctxt; + val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; + val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] + val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val tl = Thm.lhs_of ts; + val (insp, inst) = make_inst (term_of tl) (term_of ctrm); + val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; + in + Conv.rewr_conv ti ctrm + end | _ => Conv.all_conv ctrm *} ML {* val lambda_allex_prs_conv = More_Conv.top_conv lambda_allex_prs_simple_conv -*} -ML {* fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) *} @@ -1121,7 +1095,6 @@ The rest are a simp_tac and are fast. *) -ML {* fun OF1 thm1 thm2 = thm2 RS thm1 *} ML {* fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac @@ -1132,21 +1105,25 @@ let val thy = ProofContext.theory_of lthy; val defs = map (Thm.varifyT o #def) (qconsts_dest thy) - val thms = @{thms eq_reflection[OF fun_map.simps]} - @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} - @ defs - val simp_ctxt = HOL_basic_ss addsimps thms addSolver quotient_solver + val thms1 = @{thms all_prs ex_prs} + val thms2 = @{thms eq_reflection[OF fun_map.simps]} + @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} + @ defs + fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver + (* FIXME: use of someting smaller than HOL_basic_ss *) in EVERY' [ (* (rep1 ---> abs2) (\x. rep2 (f (abs1 x))) ----> f *) + NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), + (* Ball (Respects R) ((abs ---> id) f) ----> All f *) - NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), + NDT lthy "b" (simp_tac (simp_ctxt thms1)), (* NewConst -----> (rep ---> abs) oldConst *) (* abs (rep x) -----> x *) (* R (Rep x) (Rep y) -----> x = y *) (* id_simps; fun_map.simps *) - NDT lthy "c" (TRY o simp_tac simp_ctxt), + NDT lthy "c" (simp_tac (simp_ctxt thms2)), (* final step *) NDT lthy "d" (TRY o rtac refl) @@ -1225,11 +1202,11 @@ val reg_goal = Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = tracing "Regularization done." + val _ = warning "Regularization done." val inj_goal = Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = tracing "RepAbs Injection done." + val _ = warning "RepAbs Injection done." in Drule.instantiate' [] [SOME (cterm_of thy rtrm'),