# HG changeset patch # User Christian Urban # Date 1261608783 -3600 # Node ID bf6861ee3b900beee5b24227318a20d64f3d829d # Parent da75568e7f124962789d2bfcd99e28941765bf11 tuning diff -r da75568e7f12 -r bf6861ee3b90 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Wed Dec 23 23:22:02 2009 +0100 +++ b/Quot/quotient_tacs.ML Wed Dec 23 23:53:03 2009 +0100 @@ -23,13 +23,13 @@ (* various helper fuctions *) -(* composition of two theorems, used in map *) +(* composition of two theorems, used in maps *) fun OF1 thm1 thm2 = thm2 RS thm1 (* makes sure a subgoal is solved *) fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) -(* prints warning, if goal is unsolved *) +(* prints warning, if the subgoal is unsolved *) fun WARN (tac, msg) i st = case Seq.pull ((SOLVES' tac) i st) of NONE => (warning msg; Seq.single st) @@ -426,6 +426,7 @@ fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) + fun mk_abs u i t = if incr_boundvars i u aconv t then Bound i else (case t of @@ -454,7 +455,7 @@ (* First instantiates the types and known subterms. *) (* Then solves the quotient assumptions to get Rep2 and Abs1 *) (* Finally instantiates the function f using make_inst *) -(* If Rep2 is identity then the pattern is simpler and *) +(* If Rep2 is an identity then the pattern is simpler and *) (* make_inst_id is used *) fun lambda_prs_simple_conv ctxt ctrm = case (term_of ctrm) of @@ -468,8 +469,10 @@ val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te - val make_inst = if ty_c = ty_d then make_inst_id else make_inst - val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) + val (insp, inst) = + if ty_c = ty_d + then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) + else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts in Conv.rewr_conv ti ctrm @@ -500,28 +503,28 @@ (* 5. test for refl *) fun clean_tac_aux lthy = - let - val thy = ProofContext.theory_of lthy; - val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) +let + val thy = ProofContext.theory_of lthy; + val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) - val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} - val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) - fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver - in - EVERY' [simp_tac (simps thms1), - fun_map_tac lthy, - lambda_prs_tac lthy, - simp_tac (simps thms2), - TRY o rtac refl] - end + val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} + val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) + fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver +in + EVERY' [simp_tac (simps thms1), + fun_map_tac lthy, + lambda_prs_tac lthy, + simp_tac (simps thms2), + TRY o rtac refl] +end fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) -(********************************************************) -(* Tactic for Genralisation of Free Variables in a Goal *) -(********************************************************) +(****************************************************) +(* Tactic for Generalising Free Variables in a Goal *) +(****************************************************) fun inst_spec ctrm = Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} @@ -603,10 +606,10 @@ fun procedure_tac ctxt rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (goal, i) => + THEN' SUBGOAL (fn (goal, i) => let val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) + val rule = procedure_inst ctxt (prop_of rthm') goal in (rtac rule THEN' rtac rthm') i end) diff -r da75568e7f12 -r bf6861ee3b90 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Wed Dec 23 23:22:02 2009 +0100 +++ b/Quot/quotient_term.ML Wed Dec 23 23:53:03 2009 +0100 @@ -145,7 +145,7 @@ if s = s' then let - val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") + val exc = LIFT_MATCH ("mk_resp_arg (no relation map function found for type " ^ s ^ ")") val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc val args = map (mk_resp_arg ctxt) (tys ~~ tys') in @@ -188,7 +188,7 @@ (* produces a regularized version of rtrm *) (* *) -(* - the result still contains dummyTs *) +(* - the result might contain dummyTs *) (* *) (* - for regularisation we do not need any *) (* special treatment of bound variables *) @@ -228,7 +228,7 @@ (rel, Const (@{const_name "op ="}, ty')) => let val exc = LIFT_MATCH "regularise (relation mismatch)" - val rel_ty = (fastype_of rel) handle TERM _ => raise exc + val rel_ty = fastype_of rel val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') in if rel' aconv rel then rtrm else raise exc @@ -258,7 +258,7 @@ val qtrm_str = Syntax.string_of_term ctxt qtrm val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") - val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 + val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1 in if Pattern.matches thy (rtrm', rtrm) then rtrm else raise exc2