diff -r 14682786c356 -r 06e54c862a39 QuotMain.thy --- a/QuotMain.thy Sun Dec 06 06:39:32 2009 +0100 +++ b/QuotMain.thy Sun Dec 06 06:41:52 2009 +0100 @@ -740,12 +740,17 @@ then rtrm else mk_repabs lthy (T, T') rtrm - | (Const (_, T), Const (_, T')) => - if T = T' + | (_, Const (@{const_name "op ="}, _)) => rtrm + + (* FIXME: check here that rtrm is the corresponding definition for teh const *) + | (_, Const (_, T')) => + let + val rty = fastype_of rtrm + in + if rty = T' then rtrm - else mk_repabs lthy (T, T') rtrm - - | (_, Const (@{const_name "op ="}, _)) => rtrm + else mk_repabs lthy (rty, T') rtrm + end | _ => raise (LIFT_MATCH "injection") *} @@ -773,6 +778,12 @@ resolve_tac (quotient_rules_get ctxt)]) *} +(* solver for the simplifier *) +ML {* +fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) +val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac +*} + definition "QUOT_TRUE x \ True" @@ -1041,92 +1052,77 @@ *} ML {* -fun lambda_allex_prs_simple_conv ctxt ctrm = +fun lambda_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 fun_map}, _) $ r1 $ a2) $ (Abs _)) => + let + val thy = ProofContext.theory_of ctxt + val (ty_b, ty_a) = dest_fun_type (fastype_of r1) + val (ty_c, ty_d) = dest_fun_type (fastype_of a2) + 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 + (*val _ = tracing "lambda_prs" + val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))) + val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*) + 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 +val lambda_prs_conv = + More_Conv.top_conv lambda_prs_simple_conv -fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) +fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) *} (* - Cleaning the theorem consists of 6 kinds of rewrites. + Cleaning the theorem consists of three rewriting steps. The first two need to be done before fun_map is unfolded - - lambda_prs: + 1) lambda_prs: (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f - - all_prs (and the same for exists: ex_prs) - \x\Respects R. (abs ---> id) f ----> \x. f - - - Rewriting with definitions from the argument defs - NewConst ----> (rep ---> abs) oldConst + Implemented as conversion since it is not a pattern. - - Quotient_rel_rep: - Rel (Rep x) (Rep y) ----> x = y + 2) all_prs (the same for exists): + Ball (Respects R) ((abs ---> id) f) ----> All f - - ABS_REP - Abs (Rep x) ----> x + Rewriting with definitions from the argument defs + (rep ---> abs) oldConst ----> newconst - - id_simps; fun_map.simps + 3) Quotient_rel_rep: + Rel (Rep x) (Rep y) ----> x = y - The first one is implemented as a conversion (fast). - The second one is an EqSubst (slow). - The rest are a simp_tac and are fast. + Quotient_abs_rep: + Abs (Rep x) ----> x + + id_simps; fun_map.simps *) ML {* -fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) -val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac -*} - -ML {* fun clean_tac lthy = let val thy = ProofContext.theory_of lthy; val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) + (* FIXME: shouldn't the definitions already be varified? *) val thms1 = @{thms all_prs ex_prs} @ defs val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} - fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver - (* FIXME: use of someting smaller than HOL_basic_ss *) + fun simps 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 "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" (simp_tac (simp_ctxt thms2)), - - (* final step *) - NDT lthy "d" (TRY o rtac refl) - ] + EVERY' [lambda_prs_tac lthy, + simp_tac (simps thms1), + simp_tac (simps thms2), + TRY o rtac refl] end *}