# HG changeset patch # User Cezary Kaliszyk # Date 1263308631 -3600 # Node ID 0eb018699f468747e1bb3490a2d4b53f87e290b9 # Parent b89707cd030f7aa9bbe348ebb0c9dba85c514f76 Cleaning comments, indentation etc in quotient_tacs. diff -r b89707cd030f -r 0eb018699f46 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Tue Jan 12 15:48:46 2010 +0100 +++ b/Quot/quotient_tacs.ML Tue Jan 12 16:03:51 2010 +0100 @@ -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,7 +64,7 @@ (* 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)])) @@ -173,12 +174,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 +232,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 +243,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 @@ -413,16 +414,14 @@ 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 @@ -493,23 +492,19 @@ 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 + 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 *) @@ -531,9 +526,9 @@ end -(****************************************************) -(* 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} @@ -561,21 +556,20 @@ 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 + - 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; @@ -588,20 +582,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'),