--- a/src/Provers/clasimp.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/Provers/clasimp.ML Fri May 13 22:55:00 2011 +0200
@@ -5,14 +5,11 @@
splitter.ML, classical.ML, blast.ML).
*)
-infix 4 addSss addss addss';
-
signature CLASIMP_DATA =
sig
structure Splitter: SPLITTER
structure Classical: CLASSICAL
structure Blast: BLAST
- sharing type Classical.claset = Blast.claset
val notE: thm
val iffD1: thm
val iffD2: thm
@@ -20,19 +17,16 @@
signature CLASIMP =
sig
- type claset
- type clasimpset
- val clasimpset_of: Proof.context -> clasimpset
- val addSss: claset * simpset -> claset
- val addss: claset * simpset -> claset
- val addss': claset * simpset -> claset
- val clarsimp_tac: clasimpset -> int -> tactic
- val mk_auto_tac: clasimpset -> int -> int -> tactic
- val auto_tac: clasimpset -> tactic
- val force_tac: clasimpset -> int -> tactic
- val fast_simp_tac: clasimpset -> int -> tactic
- val slow_simp_tac: clasimpset -> int -> tactic
- val best_simp_tac: clasimpset -> int -> tactic
+ val addSss: Proof.context -> Proof.context
+ val addss: Proof.context -> Proof.context
+ val addss': Proof.context -> Proof.context
+ val clarsimp_tac: Proof.context -> int -> tactic
+ val mk_auto_tac: Proof.context -> int -> int -> tactic
+ val auto_tac: Proof.context -> tactic
+ val force_tac: Proof.context -> int -> tactic
+ val fast_simp_tac: Proof.context -> int -> tactic
+ val slow_simp_tac: Proof.context -> int -> tactic
+ val best_simp_tac: Proof.context -> int -> tactic
val iff_add: attribute
val iff_add': attribute
val iff_del: attribute
@@ -49,29 +43,20 @@
structure Blast = Data.Blast;
-(* type clasimpset *)
-
-type claset = Classical.claset;
-type clasimpset = claset * simpset;
-
-fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
-
-
(* simp as classical wrapper *)
(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
-(*Add a simpset to a classical set!*)
-(*Caution: only one simpset added can be added by each of addSss and addss*)
-fun cs addSss ss =
- Classical.addSafter (cs, ("safe_asm_full_simp_tac", CHANGED o safe_asm_full_simp_tac ss));
+fun clasimp f name tac ctxt =
+ Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
-fun cs addss ss =
- Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss));
-
-fun cs addss' ss =
- Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss));
+(*Add a simpset to the claset!*)
+(*Caution: only one simpset added can be added by each of addSss and addss*)
+val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
+val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
+(* FIXME "asm_lr_simp_tac" !? *)
+val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac;
(* iffs: addition of rules to simpsets and clasets simultaneously *)
@@ -128,75 +113,72 @@
(* tactics *)
-fun clarsimp_tac (cs, ss) =
- safe_asm_full_simp_tac ss THEN_ALL_NEW
- Classical.clarify_tac (cs addSss ss);
+fun clarsimp_tac ctxt =
+ safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
+ Classical.clarify_tac (addSss ctxt);
(* auto_tac *)
-fun blast_depth_tac cs m i thm =
- Blast.depth_tac cs m i thm
+fun blast_depth_tac ctxt m i thm =
+ Blast.depth_tac ctxt m i thm
handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
(* a variant of depth_tac that avoids interference of the simplifier
with dup_step_tac when they are combined by auto_tac *)
local
-fun slow_step_tac' cs =
- Classical.appWrappers cs
- (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
+fun slow_step_tac' ctxt =
+ Classical.appWrappers ctxt
+ (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);
in
-fun nodup_depth_tac cs m i st =
+fun nodup_depth_tac ctxt m i st =
SELECT_GOAL
- (Classical.safe_steps_tac cs 1 THEN_ELSE
- (DEPTH_SOLVE (nodup_depth_tac cs m 1),
- Classical.inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
- (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m - 1) 1)))) i st;
+ (Classical.safe_steps_tac ctxt 1 THEN_ELSE
+ (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
+ Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
+ (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
end;
(*Designed to be idempotent, except if blast_depth_tac instantiates variables
in some of the subgoals*)
-fun mk_auto_tac (cs, ss) m n =
+fun mk_auto_tac ctxt m n =
let
- val cs' = cs addss ss;
val main_tac =
- blast_depth_tac cs m (* fast but can't use wrappers *)
+ blast_depth_tac ctxt m (* fast but can't use wrappers *)
ORELSE'
- (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
+ (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *)
in
- PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)) THEN
- TRY (Classical.safe_tac cs) THEN
+ PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
+ TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN
- TRY (Classical.safe_tac (cs addSss ss)) THEN
+ TRY (Classical.safe_tac (addSss ctxt)) THEN
prune_params_tac
end;
-fun auto_tac css = mk_auto_tac css 4 2;
+fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
(* force_tac *)
(* aimed to solve the given subgoal totally, using whatever tools possible *)
-fun force_tac (cs, ss) =
- let val cs' = cs addss ss in
+fun force_tac ctxt =
+ let val ctxt' = addss ctxt in
SELECT_GOAL
- (Classical.clarify_tac cs' 1 THEN
- IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1) THEN
- ALLGOALS (Classical.first_best_tac cs'))
+ (Classical.clarify_tac ctxt' 1 THEN
+ IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
+ ALLGOALS (Classical.first_best_tac ctxt'))
end;
(* basic combinations *)
-fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end;
-
-val fast_simp_tac = ADDSS Classical.fast_tac;
-val slow_simp_tac = ADDSS Classical.slow_tac;
-val best_simp_tac = ADDSS Classical.best_tac;
+val fast_simp_tac = Classical.fast_tac o addss;
+val slow_simp_tac = Classical.slow_tac o addss;
+val best_simp_tac = Classical.best_tac o addss;
@@ -226,21 +208,14 @@
(* methods *)
-fun clasimp_meth tac ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
-
-fun clasimp_meth' tac ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
-
-
fun clasimp_method' tac =
- Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
+ Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
val auto_method =
Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
Method.sections clasimp_modifiers >>
- (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
- | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
+ (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
+ | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
(* theory setup *)