diff -r 017cb46b27bb -r 433f7c17255f Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Wed Jan 13 00:46:31 2010 +0100 +++ b/Quot/quotient_tacs.ML Wed Jan 13 09:19:20 2010 +0100 @@ -1,13 +1,13 @@ signature QUOTIENT_TACS = sig - val regularize_tac: Proof.context -> int -> tactic - val injection_tac: Proof.context -> int -> tactic - val all_injection_tac: Proof.context -> int -> tactic - val clean_tac: Proof.context -> int -> tactic - val procedure_tac: Proof.context -> thm -> int -> tactic - val lift_tac: Proof.context -> thm -> int -> tactic - val quotient_tac: Proof.context -> int -> tactic - val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic + val regularize_tac: Proof.context -> int -> tactic + val injection_tac: Proof.context -> int -> tactic + val all_injection_tac: Proof.context -> int -> tactic + val clean_tac: Proof.context -> int -> tactic + val procedure_tac: Proof.context -> thm -> int -> tactic + val lift_tac: Proof.context -> thm -> int -> tactic + val quotient_tac: Proof.context -> int -> tactic + val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic end; structure Quotient_Tacs: QUOTIENT_TACS = @@ -16,7 +16,8 @@ open Quotient_Info; open Quotient_Term; -(* various helper fuctions *) + +(** various helper fuctions **) (* Since HOL_basic_ss is too "big" for us, we *) (* need to set up our own minimal simpset. *) @@ -48,14 +49,14 @@ end -(*********************) -(* Regularize Tactic *) -(*********************) + +(*** Regularize Tactic ***) -(* solvers for equivp and quotient assumptions *) +(** solvers for equivp and quotient assumptions **) + (* FIXME / TODO: should this SOLVES' the goal, like with quotient_tac? *) (* FIXME / TODO: none of te examples break if added *) -fun equiv_tac ctxt = +fun equiv_tac ctxt = REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) @@ -63,13 +64,14 @@ (* FIXME / TODO: test whether DETERM makes any runtime-difference *) (* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *) -fun quotient_tac ctxt = SOLVES' +fun quotient_tac ctxt = SOLVES' (REPEAT_ALL_NEW (FIRST' [rtac @{thm identity_quotient}, resolve_tac (quotient_rules_get ctxt)])) fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) -val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac +val quotient_solver = + Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac fun solve_quotient_assm ctxt thm = case Seq.pull (quotient_tac ctxt 1 thm) of @@ -86,7 +88,7 @@ fun get_match_inst thy pat trm = let val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) + val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) val tenv = Vartab.dest (Envir.term_env env) val tyenv = Vartab.dest (Envir.type_env env) in @@ -130,27 +132,22 @@ | _ => NONE end -(* 0. preliminary simplification step according to *) -(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) -(* ball_reg_eqv_range bex_reg_eqv_range *) -(* *) -(* 1. eliminating simple Ball/Bex instances *) -(* thm ball_reg_right bex_reg_left *) -(* *) -(* 2. monos *) -(* *) -(* 3. commutation rules for ball and bex *) -(* thm ball_all_comm bex_ex_comm *) -(* *) -(* 4. then rel-equalities, which need to be *) -(* instantiated with the followig theorem *) -(* to avoid loops: *) -(* thm eq_imp_rel *) -(* *) -(* 5. then simplification like 0 *) -(* *) -(* finally jump back to 1 *) +(* +0. preliminary simplification step according to + ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range + +1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) + +2. monos +3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) + +4. then rel-equalities, which need to be instantiated with 'eq_imp_rel' + to avoid loops + +5. then simplification like 0 + +finally jump back to 1 *) fun regularize_tac ctxt = let val thy = ProofContext.theory_of ctxt @@ -158,7 +155,7 @@ val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) val simpset = (mk_minimal_ss ctxt) - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get ctxt) + addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) @@ -173,12 +170,11 @@ end -(********************) -(* Injection Tactic *) -(********************) + +(*** Injection Tactic ***) -(* Looks for Quot_True assumtions, and in case its parameter *) -(* is an application, it returns the function and the argument. *) +(* Looks for Quot_True assumtions, and in case its parameter + is an application, it returns the function and the argument. *) fun find_qt_asm asms = let fun find_fun trm = @@ -232,9 +228,9 @@ val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl -(* We apply apply_rsp only in case if the type needs lifting. *) -(* This is the case if the type of the data in the Quot_True *) -(* assumption is different from the corresponding type in the goal. *) +(* We apply apply_rsp only in case if the type needs lifting. + This is the case if the type of the data in the Quot_True + assumption is different from the corresponding type in the goal. *) val apply_rsp_tac = Subgoal.FOCUS (fn {concl, asms, context,...} => let @@ -243,17 +239,18 @@ in case (bare_concl, qt_asm) of (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => - if (fastype_of qt_fun) = (fastype_of f) - then no_tac - else + if (fastype_of qt_fun) = (fastype_of f) + then no_tac + else let val ty_x = fastype_of x val ty_b = fastype_of qt_arg - val ty_f = range_type (fastype_of f) + val ty_f = range_type (fastype_of f) val thy = ProofContext.theory_of context val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; - val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} + val inst_thm = Drule.instantiate' ty_inst + ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} in (rtac inst_thm THEN' quotient_tac context) 1 end @@ -281,44 +278,45 @@ (* TODO: Again, can one specify more concretely *) (* TODO: in terms of R when no_tac should be returned? *) -fun rep_abs_rsp_tac ctxt = +fun rep_abs_rsp_tac ctxt = SUBGOAL (fn (goal, i) => - case (bare_concl goal) of - (rel $ _ $ (rep $ (abs $ _))) => - (let - val thy = ProofContext.theory_of ctxt; - val (ty_a, ty_b) = dest_fun_type (fastype_of abs); - val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; - val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; - val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} - in - (rtac inst_thm THEN' quotient_tac ctxt) i - end - handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *) + case (try bare_concl goal) of + SOME (rel $ _ $ (rep $ (abs $ _))) => + let + val thy = ProofContext.theory_of ctxt; + val (ty_a, ty_b) = dest_fun_type (fastype_of abs); + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; + in + case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of + SOME t_inst => + (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of + SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i + | NONE => no_tac) + | NONE => no_tac + end | _ => no_tac) -(* FIXME / TODO needs to be adapted *) (* -To prove that the regularised theorem implies the abs/rep injected, +To prove that the regularised theorem implies the abs/rep injected, we try: - 1) theorems 'trans2' from the appropriate Quot_Type - 2) remove lambdas from both sides: lambda_rsp_tac - 3) remove Ball/Bex from the right hand side - 4) use user-supplied RSP theorems - 5) remove rep_abs from the right side - 6) reflexivity of equality - 7) split applications of lifted type (apply_rsp) - 8) split applications of non-lifted type (cong_tac) - 9) apply extentionality - A) reflexivity of the relation - B) assumption + The deterministic part: + -) remove lambdas from both sides + -) prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp + -) prove Ball/Bex relations unfolding fun_rel_id + -) reflexivity of equality + -) prove equality of relations using equals_rsp + -) use user-supplied RSP theorems + -) solve 'relation of relations' goals using quot_rel_rsp + -) remove rep_abs from the right side (Lambdas under respects may have left us some assumptions) - C) proving obvious higher order equalities by simplifying fun_rel - (not sure if it is still needed?) - D) unfolding lambda on one side - E) simplifying (= ===> =) for simpler respectfulness + Then in order: + -) split applications of lifted type (apply_rsp) + -) split applications of non-lifted type (cong_tac) + -) apply extentionality + -) assumption + -) reflexivity of the relation *) @@ -382,7 +380,7 @@ FIRST' [ injection_match_tac ctxt, - (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) + (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) apply_rsp_tac ctxt THEN' RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], @@ -390,13 +388,13 @@ (* merge with previous tactic *) Cong_Tac.cong_tac @{thm cong} THEN' RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], - + (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) rtac @{thm ext} THEN' quot_true_tac ctxt unlam, - + (* resolving with R x y assumptions *) atac, - + (* reflexivity of the basic relations *) (* R ... ... *) resolve_tac rel_refl] @@ -405,24 +403,21 @@ let val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) in - simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) - THEN' injection_step_tac ctxt rel_refl + injection_step_tac ctxt rel_refl end fun all_injection_tac ctxt = REPEAT_ALL_NEW (injection_tac ctxt) -(***************************) -(* Cleaning of the Theorem *) -(***************************) -(* expands all fun_maps, except in front of the bound *) -(* variables listed in xs *) +(** Cleaning of the Theorem **) + +(* expands all fun_maps, except in front of the bound variables listed in xs *) fun fun_map_simple_conv xs ctrm = case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => - if (member (op=) xs h) + if (member (op=) xs h) then Conv.all_conv ctrm else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm | _ => Conv.all_conv ctrm @@ -461,58 +456,52 @@ (f, Abs ("x", T, mk_abs u 0 g)) end -(* Simplifies a redex using the 'lambda_prs' theorem. *) -(* 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 an identity then the pattern is simpler and *) -(* make_inst_id is used *) +(* Simplifies a redex using the 'lambda_prs' theorem. + 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 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 - (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[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 (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 - end - handle _ => Conv.all_conv ctrm) (* TODO: another catch all - can this be improved? *) + (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[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 (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 + end | _ => Conv.all_conv ctrm - fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) -(* 1. folding of definitions and preservation lemmas; *) -(* and simplification with *) -(* thm babs_prs all_prs ex_prs *) -(* *) -(* 2. unfolding of ---> in front of everything, except *) -(* bound variables (this prevents lambda_prs from *) -(* becoming stuck) *) -(* thm fun_map.simps *) -(* *) -(* 3. simplification with *) -(* thm lambda_prs *) -(* *) -(* 4. simplification with *) -(* thm Quotient_abs_rep Quotient_rel_rep id_simps *) -(* *) -(* 5. test for refl *) +(* Cleaning consists of: + 1. folding of definitions and preservation lemmas; + and simplification with babs_prs all_prs ex_prs -fun clean_tac_aux lthy = + 2. unfolding of ---> in front of everything, except + bound variables + (this prevents lambda_prs from becoming stuck) + + 3. simplification with lambda_prs + + 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps + + 5. test for refl *) +fun clean_tac lthy = let (* FIXME/TODO produce defs with lthy, like prs and ids *) val thy = ProofContext.theory_of lthy; @@ -520,24 +509,22 @@ (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) val prs = prs_rules_get lthy val ids = id_simps_get lthy - + fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs}) - val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) + val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) in EVERY' [simp_tac ss1, fun_map_tac lthy, lambda_prs_tac lthy, simp_tac ss2, - TRY o rtac refl] + TRY o rtac refl] end -fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) -(****************************************************) -(* Tactic for Generalising 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} @@ -552,39 +539,38 @@ HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop fun gen_frees_tac ctxt = - SUBGOAL (fn (concl, i) => - let - val thy = ProofContext.theory_of ctxt - val vrs = Term.add_frees concl [] - val cvrs = map (cterm_of thy o Free) vrs - val concl' = apply_under_Trueprop (all_list vrs) concl - val goal = Logic.mk_implies (concl', concl) - val rule = Goal.prove ctxt [] [] goal - (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) - in - rtac rule i - end) + SUBGOAL (fn (concl, i) => + let + val thy = ProofContext.theory_of ctxt + val vrs = Term.add_frees concl [] + val cvrs = map (cterm_of thy o Free) vrs + val concl' = apply_under_Trueprop (all_list vrs) concl + val goal = Logic.mk_implies (concl', concl) + val rule = Goal.prove ctxt [] [] goal + (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + in + rtac rule i + end) -(**********************************************) -(* The General Shape of the Lifting Procedure *) -(**********************************************) + +(** The General Shape of the Lifting Procedure **) -(* - A is the original raw theorem *) -(* - B is the regularized theorem *) -(* - C is the rep/abs injected version of B *) -(* - D is the lifted theorem *) -(* *) -(* - 1st prem is the regularization step *) -(* - 2nd prem is the rep/abs injection step *) -(* - 3rd prem is the cleaning part *) -(* *) -(* the Quot_True premise in 2nd records the lifted theorem *) + +(* - A is the original raw theorem + - B is the regularized theorem + - C is the rep/abs injected version of B + - D is the lifted theorem -val lifting_procedure_thm = - @{lemma "[|A; - A --> B; - Quot_True D ==> B = C; - C = D|] ==> D" + - 1st prem is the regularization step + - 2nd prem is the rep/abs injection step + - 3rd prem is the cleaning part + + the Quot_True premise in 2nd records the lifted theorem *) +val lifting_procedure_thm = + @{lemma "[|A; + A --> B; + Quot_True D ==> B = C; + C = D|] ==> D" by (simp add: Quot_True_def)} fun lift_match_error ctxt str rtrm qtrm = @@ -592,20 +578,20 @@ val rtrm_str = Syntax.string_of_term ctxt rtrm val qtrm_str = Syntax.string_of_term ctxt qtrm val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, - "", "does not match with original theorem", rtrm_str] + "", "does not match with original theorem", rtrm_str] in error msg end - + fun procedure_inst ctxt rtrm qtrm = let val thy = ProofContext.theory_of ctxt val rtrm' = HOLogic.dest_Trueprop rtrm val qtrm' = HOLogic.dest_Trueprop qtrm val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') - handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm + handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') - handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm + handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm in Drule.instantiate' [] [SOME (cterm_of thy rtrm'),