--- 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