--- 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'),