--- a/Quot/quotient_tacs.ML Tue Jan 12 16:44:33 2010 +0100
+++ b/Quot/quotient_tacs.ML Tue Jan 12 17:46:35 2010 +0100
@@ -1,13 +1,13 @@
signature QUOTIENT_TACS =
sig
- val regularize_tac: Proof.context -> int -> tactic
- val injection_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 quotient_tac: Proof.context -> int -> tactic
- val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
+ val regularize_tac: Proof.context -> int -> tactic
+ val injection_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 quotient_tac: Proof.context -> int -> tactic
+ val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
end;
structure Quotient_Tacs: QUOTIENT_TACS =
@@ -70,7 +70,8 @@
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
+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
@@ -87,7 +88,7 @@
fun get_match_inst thy pat trm =
let
val univ = Unify.matchers thy [(pat, trm)]
- val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *)
+ val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *)
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
in
@@ -131,27 +132,22 @@
| _ => NONE
end
-(* 0. preliminary simplification step according to *)
-(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *)
-(* ball_reg_eqv_range bex_reg_eqv_range *)
-(* *)
-(* 1. eliminating simple Ball/Bex instances *)
-(* 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-equalities, which need to be *)
-(* instantiated with the followig theorem *)
-(* to avoid loops: *)
-(* thm eq_imp_rel *)
-(* *)
-(* 5. then simplification like 0 *)
-(* *)
-(* finally jump back to 1 *)
+(*
+0. preliminary simplification step according to
+ ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range
+
+1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left)
+
+2. monos
+3. commutation rules for ball and bex (ball_all_comm bex_ex_comm)
+
+4. then rel-equalities, which need to be instantiated with 'eq_imp_rel'
+ to avoid loops
+
+5. then simplification like 0
+
+finally jump back to 1 *)
fun regularize_tac ctxt =
let
val thy = ProofContext.theory_of ctxt
@@ -384,7 +380,7 @@
FIRST' [
injection_match_tac ctxt,
- (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *)
+ (* 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)],
@@ -392,13 +388,13 @@
(* merge with previous tactic *)
Cong_Tac.cong_tac @{thm cong} THEN'
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
-
+
(* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
-
+
(* resolving with R x y assumptions *)
atac,
-
+
(* reflexivity of the basic relations *)
(* R ... ... *)
resolve_tac rel_refl]
@@ -513,16 +509,16 @@
(* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
val prs = prs_rules_get lthy
val ids = id_simps_get lthy
-
+
fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
- val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
+ val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
in
EVERY' [simp_tac ss1,
fun_map_tac lthy,
lambda_prs_tac lthy,
simp_tac ss2,
- TRY o rtac refl]
+ TRY o rtac refl]
end
@@ -543,18 +539,18 @@
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
fun gen_frees_tac ctxt =
- SUBGOAL (fn (concl, i) =>
- let
- val thy = ProofContext.theory_of ctxt
- val vrs = Term.add_frees concl []
- val cvrs = map (cterm_of thy o Free) vrs
- val concl' = apply_under_Trueprop (all_list vrs) concl
- val goal = Logic.mk_implies (concl', concl)
- val rule = Goal.prove ctxt [] [] goal
- (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
- in
- rtac rule i
- end)
+ SUBGOAL (fn (concl, i) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val vrs = Term.add_frees concl []
+ val cvrs = map (cterm_of thy o Free) vrs
+ val concl' = apply_under_Trueprop (all_list vrs) concl
+ val goal = Logic.mk_implies (concl', concl)
+ val rule = Goal.prove ctxt [] [] goal
+ (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+ in
+ rtac rule i
+ end)
(** The General Shape of the Lifting Procedure **)
@@ -570,11 +566,11 @@
- 3rd prem is the cleaning part
the Quot_True premise in 2nd records the lifted theorem *)
-val lifting_procedure_thm =
- @{lemma "[|A;
- A --> B;
- Quot_True D ==> B = C;
- C = D|] ==> D"
+val lifting_procedure_thm =
+ @{lemma "[|A;
+ A --> B;
+ Quot_True D ==> B = C;
+ C = D|] ==> D"
by (simp add: Quot_True_def)}
fun lift_match_error ctxt str rtrm qtrm =