diff -r a95f6bb081cf -r d6acae26d027 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Tue Dec 22 07:42:16 2009 +0100 +++ b/Quot/quotient_tacs.ML Tue Dec 22 20:51:37 2009 +0100 @@ -1,10 +1,10 @@ signature QUOTIENT_TACS = sig val regularize_tac: Proof.context -> int -> tactic - val all_inj_repabs_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 lift_tac: Proof.context -> thm -> int -> tactic val quotient_tac: Proof.context -> int -> tactic end; @@ -48,14 +48,32 @@ end +(*********************) (* Regularize Tactic *) +(*********************) +(* solvers for equivp and quotient assumptions *) fun equiv_tac ctxt = REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac +(* test whether DETERM makes any difference *) +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 + +fun solve_quotient_assm ctxt thm = + case Seq.pull (quotient_tac ctxt 1 thm) of + SOME (t, _) => t + | _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing" + + fun prep_trm thy (x, (T, t)) = (cterm_of thy (Var (x, T)), cterm_of thy t) @@ -74,7 +92,7 @@ (* calculates the instantiations for te lemmas *) (* ball_reg_eqv_range and bex_reg_eqv_range *) -fun calculate_instance ctxt ball_bex_thm redex R1 R2 = +fun calculate_inst ctxt ball_bex_thm redex R1 R2 = let fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) val thy = ProofContext.theory_of ctxt @@ -93,7 +111,6 @@ (* FIXME/TODO: Can one not find out from the types of R1 or R2, *) (* FIXME/TODO: or from their form, when NONE should be returned? *) - fun ball_bex_range_simproc ss redex = let val ctxt = Simplifier.the_context ss @@ -101,29 +118,15 @@ case redex of (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 + | _ => NONE end -(* test whether DETERM makes any difference *) -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 - -fun solve_quotient_assm ctxt thm = - case Seq.pull (quotient_tac ctxt 1 thm) of - SOME (t, _) => t - | _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing" - - (* 0. preliminary simplification step according to *) (* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) (* ball_reg_eqv_range bex_reg_eqv_range *) @@ -132,11 +135,13 @@ (* 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-equality (which need to be *) -(* instantiated to avoid loops) *) +(* 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 *) @@ -156,25 +161,26 @@ val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) in simp_tac simpset THEN' - REPEAT_ALL_NEW (CHANGED o FIRST' [ - resolve_tac @{thms ball_reg_right bex_reg_left}, - resolve_tac (Inductive.get_monos ctxt), - resolve_tac @{thms ball_all_comm bex_ex_comm}, - resolve_tac eq_eqvs, - simp_tac simpset]) + REPEAT_ALL_NEW (CHANGED o FIRST' + [resolve_tac @{thms ball_reg_right bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + resolve_tac @{thms ball_all_comm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) end - +(********************) (* 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 = case trm of - (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true + (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true | _ => false in case find_first find_fun asms of @@ -184,7 +190,7 @@ fun quot_true_simple_conv ctxt fnctn ctrm = case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ x) => + (Const (@{const_name Quot_True}, _) $ x) => let val fx = fnctn x; val thy = ProofContext.theory_of ctxt; @@ -192,14 +198,14 @@ val cfx = cterm_of thy fx; val cxt = ctyp_of thy (fastype_of x); val cfxt = ctyp_of thy (fastype_of fx); - val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} + val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp} in Conv.rewr_conv thm ctrm end fun quot_true_conv ctxt fnctn ctrm = case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ _) => + (Const (@{const_name Quot_True}, _) $ _) => quot_true_simple_conv ctxt fnctn ctrm | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm @@ -225,8 +231,8 @@ val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl -(* we apply apply_rsp only in case if the type needs lifting, *) -(* which is the case if the type of the data in the QUOT_TRUE *) +(* 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,...} => @@ -262,7 +268,7 @@ in rtac thm THEN' quotient_tac ctxt end -(* raised by instantiate' *) +(* Are they raised by instantiate'? *) handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac @@ -309,7 +315,7 @@ *) -fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => +fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) => (case (bare_concl goal) of (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) @@ -365,11 +371,11 @@ | _ => K no_tac ) i) -fun inj_repabs_step_tac ctxt rel_refl = +fun injection_step_tac ctxt rel_refl = FIRST' [ - inj_repabs_tac_match ctxt, - (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) - + injection_match_tac ctxt, + + (* 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)], @@ -388,20 +394,21 @@ (* R ... ... *) resolve_tac rel_refl] -fun inj_repabs_tac ctxt = +fun injection_tac ctxt = 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' inj_repabs_step_tac ctxt rel_refl + THEN' injection_step_tac ctxt rel_refl end -fun all_inj_repabs_tac ctxt = - REPEAT_ALL_NEW (inj_repabs_tac ctxt) +fun all_injection_tac ctxt = + REPEAT_ALL_NEW (injection_tac ctxt) +(***************************) (* Cleaning of the Theorem *) - +(***************************) (* expands all fun_maps, except in front of bound variables *) fun fun_map_simple_conv xs ctrm = @@ -472,9 +479,8 @@ handle _ => Conv.all_conv ctrm) | _ => Conv.all_conv ctrm -val lambda_prs_conv = - More_Conv.top_conv lambda_prs_simple_conv +fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) @@ -484,7 +490,7 @@ (* *) (* 2. unfolding of ---> in front of everything, except *) (* bound variables (this prevents lambda_prs from *) -(* becoming stuck *) +(* becoming stuck) *) (* thm fun_map.simps *) (* *) (* 3. simplification with *) @@ -493,7 +499,7 @@ (* 4. simplification with *) (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) (* *) -(* 5. Test for refl *) +(* 5. test for refl *) fun clean_tac_aux lthy = let @@ -514,7 +520,10 @@ fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) + +(********************************************************) (* Tactic for Genralisation of Free Variables in a Goal *) +(********************************************************) fun inst_spec ctrm = Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} @@ -542,8 +551,9 @@ rtac rule i end) - +(**********************************************) (* The General Shape of the Lifting Procedure *) +(**********************************************) (* - A is the original raw theorem *) (* - B is the regularized theorem *) @@ -554,20 +564,20 @@ (* - 2nd prem is the rep/abs injection step *) (* - 3rd prem is the cleaning part *) (* *) -(* the QUOT_TRUE premise in 2 records the lifted theorem *) +(* the Quot_True premise in 2 records the lifted theorem *) val lifting_procedure = @{lemma "[|A; A --> B; - QUOT_TRUE D ==> B = C; + Quot_True D ==> B = C; C = D|] ==> D" - by (simp add: QUOT_TRUE_def)} + by (simp add: Quot_True_def)} -fun lift_match_error ctxt fun_str rtrm qtrm = +fun lift_match_error ctxt str rtrm qtrm = let val rtrm_str = Syntax.string_of_term ctxt rtrm val qtrm_str = Syntax.string_of_term ctxt qtrm - val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, + val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, "", "does not match with original theorem", rtrm_str] in error msg @@ -580,10 +590,10 @@ val qtrm' = HOLogic.dest_Trueprop qtrm val reg_goal = Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') - handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm + handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm 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 + handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm in Drule.instantiate' [] [SOME (cterm_of thy rtrm'), @@ -619,7 +629,7 @@ procedure_tac ctxt rthm THEN' RANGE_WARN [(regularize_tac ctxt, msg1), - (all_inj_repabs_tac ctxt, msg2), + (all_injection_tac ctxt, msg2), (clean_tac ctxt, msg3)] end; (* structure *) \ No newline at end of file