diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Thu Feb 11 09:23:59 2010 +0100 +++ b/Quot/quotient_tacs.ML Thu Feb 11 10:06:02 2010 +0100 @@ -102,7 +102,7 @@ Since the left-hand-side contains a non-pattern '?P (f ?x)' we rely on unification/instantiation to check whether the - theorem applies and return NONE if it doesn't. + theorem applies and return NONE if it doesn't. *) fun calculate_inst ctxt ball_bex_thm redex R1 R2 = let @@ -122,14 +122,14 @@ fun ball_bex_range_simproc ss redex = let val ctxt = Simplifier.the_context ss -in +in case redex of - (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ (Const (@{const_name "fun_rel"}, _) $ 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)) $ _) => + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 | _ => NONE @@ -151,7 +151,7 @@ 5. then simplification like 0 - finally jump back to 1 + finally jump back to 1 *) fun regularize_tac ctxt = let @@ -159,18 +159,18 @@ val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} 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) + val simpset = (mk_minimal_ss ctxt) addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [simproc] + addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) in simp_tac simpset THEN' - REPEAT_ALL_NEW (CHANGED o FIRST' + REPEAT_ALL_NEW (CHANGED o FIRST' [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, resolve_tac (Inductive.get_monos ctxt), resolve_tac @{thms ball_all_comm bex_ex_comm}, - resolve_tac eq_eqvs, + resolve_tac eq_eqvs, simp_tac simpset]) end @@ -179,7 +179,7 @@ (*** Injection Tactic ***) (* Looks for Quot_True assumptions, and in case its parameter - is an application, it returns the function and the argument. + is an application, it returns the function and the argument. *) fun find_qt_asm asms = let @@ -216,13 +216,13 @@ | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm | _ => Conv.all_conv ctrm -fun quot_true_tac ctxt fnctn = +fun quot_true_tac ctxt fnctn = CONVERSION ((Conv.params_conv ~1 (fn ctxt => (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) -fun dest_comb (f $ a) = (f, a) -fun dest_bcomb ((_ $ l) $ r) = (l, r) +fun dest_comb (f $ a) = (f, a) +fun dest_bcomb ((_ $ l) $ r) = (l, r) fun unlam t = case t of @@ -236,7 +236,7 @@ (* 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. + assumption is different from the corresponding type in the goal. *) val apply_rsp_tac = Subgoal.FOCUS (fn {concl, asms, context,...} => @@ -265,7 +265,7 @@ end) (* Instantiates and applies 'equals_rsp'. Since the theorem is - complex we rely on instantiation to tell us if it applies + complex we rely on instantiation to tell us if it applies *) fun equals_rsp_tac R ctxt = let @@ -304,7 +304,7 @@ -(* Injection means to prove that the regularised theorem implies +(* Injection means to prove that the regularised theorem implies the abs/rep injected one. The deterministic part: @@ -317,7 +317,7 @@ - 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) - + Then in order: - split applications of lifted type (apply_rsp) - split applications of non-lifted type (cong_tac) @@ -364,7 +364,7 @@ (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] -| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => +| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE' (equals_rsp_tac R ctxt THEN' RANGE [ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) @@ -379,7 +379,7 @@ (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) (* observe fun_map *) | _ $ _ $ _ - => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) + => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt | _ => K no_tac @@ -428,7 +428,7 @@ ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => if member (op=) xs h then Conv.all_conv ctrm - else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm + else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm | _ => Conv.all_conv ctrm fun fun_map_conv xs ctxt ctrm = @@ -470,7 +470,7 @@ 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 + make_inst_id is used *) fun lambda_prs_simple_conv ctxt ctrm = case (term_of ctrm) of @@ -501,20 +501,20 @@ (* Cleaning consists of: 1. unfolding of ---> in front of everything, except - bound variables (this prevents lambda_prs from + bound variables (this prevents lambda_prs from becoming stuck) 2. simplification with lambda_prs - 3. simplification with: + 3. simplification with: - - Quotient_abs_rep Quotient_rel_rep + - Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs - - id_simps and preservation lemmas and + - id_simps and preservation lemmas and - - symmetric versions of the definitions - (that is definitions of quotient constants + - symmetric versions of the definitions + (that is definitions of quotient constants are folded) 4. test for refl @@ -545,10 +545,10 @@ fun inst_spec_tac ctrms = EVERY' (map (dtac o inst_spec) ctrms) -fun all_list xs trm = +fun all_list xs trm = fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm -fun apply_under_Trueprop f = +fun apply_under_Trueprop f = HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop fun gen_frees_tac ctxt = @@ -577,7 +577,7 @@ - 2nd prem is the rep/abs injection step - 3rd prem is the cleaning part - the Quot_True premise in 2nd records the lifted theorem + the Quot_True premise in 2nd records the lifted theorem *) val lifting_procedure_thm = @{lemma "[|A; @@ -590,7 +590,7 @@ let val rtrm_str = Syntax.string_of_term ctxt rtrm val qtrm_str = Syntax.string_of_term ctxt qtrm - val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, + val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, "", "does not match with original theorem", rtrm_str] in error msg @@ -629,22 +629,22 @@ (* Automatic Proofs *) val msg1 = "The regularize proof failed." -val msg2 = cat_lines ["The injection proof failed.", +val msg2 = cat_lines ["The injection proof failed.", "This is probably due to missing respects lemmas.", - "Try invoking the injection method manually to see", + "Try invoking the injection method manually to see", "which lemmas are missing."] val msg3 = "The cleaning proof failed." fun lift_tac ctxt rthms = let - fun mk_tac rthm = + fun mk_tac rthm = procedure_tac ctxt rthm - THEN' RANGE_WARN + THEN' RANGE_WARN [(regularize_tac ctxt, msg1), (all_injection_tac ctxt, msg2), (clean_tac ctxt, msg3)] in - simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) + simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) THEN' RANGE (map mk_tac rthms) end