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