--- a/src/Provers/clasimp.ML Fri Sep 01 00:30:25 2000 +0200
+++ b/src/Provers/clasimp.ML Fri Sep 01 00:31:08 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: Provers/clasimp.ML
+(* Title: Provers/clasimp.ML
ID: $Id$
Author: David von Oheimb, TU Muenchen
@@ -24,33 +24,33 @@
type claset
type simpset
type clasimpset
- val addSIs2 : clasimpset * thm list -> clasimpset
- val addSEs2 : clasimpset * thm list -> clasimpset
- val addSDs2 : clasimpset * thm list -> clasimpset
- val addIs2 : clasimpset * thm list -> clasimpset
- val addEs2 : clasimpset * thm list -> clasimpset
- val addDs2 : clasimpset * thm list -> clasimpset
- val addsimps2 : clasimpset * thm list -> clasimpset
- val delsimps2 : clasimpset * thm list -> clasimpset
- val addSss : claset * simpset -> claset
- val addss : claset * simpset -> claset
+ val addSIs2 : clasimpset * thm list -> clasimpset
+ val addSEs2 : clasimpset * thm list -> clasimpset
+ val addSDs2 : clasimpset * thm list -> clasimpset
+ val addIs2 : clasimpset * thm list -> clasimpset
+ val addEs2 : clasimpset * thm list -> clasimpset
+ val addDs2 : clasimpset * thm list -> clasimpset
+ val addsimps2 : clasimpset * thm list -> clasimpset
+ val delsimps2 : clasimpset * thm list -> clasimpset
+ val addSss : claset * simpset -> claset
+ val addss : claset * simpset -> claset
val CLASIMPSET :(clasimpset -> tactic) -> tactic
val CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
val clarsimp_tac: clasimpset -> int -> tactic
val Clarsimp_tac: int -> tactic
val mk_auto_tac : clasimpset -> int -> int -> tactic
- val auto_tac : clasimpset -> tactic
- val Auto_tac : tactic
- val auto : unit -> unit
- val force_tac : clasimpset -> int -> tactic
- val Force_tac : int -> tactic
- val force : int -> unit
+ val auto_tac : clasimpset -> tactic
+ val Auto_tac : tactic
+ val auto : unit -> unit
+ val force_tac : clasimpset -> int -> tactic
+ val Force_tac : int -> tactic
+ val force : int -> unit
val fast_simp_tac : clasimpset -> int -> tactic
val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
val get_local_clasimpset: Proof.context -> clasimpset
val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val setup : (theory -> theory) list
+ val setup : (theory -> theory) list
end;
functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
@@ -86,9 +86,9 @@
(*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.addSaltern (cs, ("safe_asm_full_simp_tac",
- CHANGED o safe_asm_full_simp_tac ss));
-fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
- CHANGED o Simplifier.asm_full_simp_tac ss));
+ CHANGED o safe_asm_full_simp_tac ss));
+fun cs addss ss = Classical.addbefore (cs, ("asm_full_simp_tac",
+ CHANGED o Simplifier.asm_full_simp_tac ss));
(* tacticals *)
@@ -100,26 +100,26 @@
fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW
- Classical.clarify_tac (cs addSss ss);
+ Classical.clarify_tac (cs addSss ss);
fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;
(* auto_tac *)
fun blast_depth_tac cs m i thm =
- Blast.depth_tac cs m i thm
+ Blast.depth_tac cs m i thm
handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
-
-(* a variant of depth_tac that avoids interference of the simplifier
+
+(* 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);
-in fun nodup_depth_tac cs m i state = 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))
+fun slow_step_tac' cs = Classical.appWrappers cs
+ (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
+in fun nodup_depth_tac cs m i state = 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 state;
end;
@@ -127,30 +127,31 @@
in some of the subgoals*)
fun mk_auto_tac (cs, ss) m n =
let val cs' = cs addss ss
- val maintac =
- blast_depth_tac cs m (* fast but can't use wrappers *)
+ val maintac =
+ blast_depth_tac cs m (* fast but can't use wrappers *)
ORELSE'
(CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
- TRY (Classical.safe_tac cs),
- REPEAT (FIRSTGOAL maintac),
+ TRY (Classical.safe_tac cs),
+ REPEAT (FIRSTGOAL maintac),
TRY (Classical.safe_tac (cs addSss ss)),
- prune_params_tac]
+ prune_params_tac]
end;
-fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
+fun auto_tac css = mk_auto_tac css 4 2;
fun Auto_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st;
fun auto () = by Auto_tac;
+
(* 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 SELECT_GOAL (EVERY [
- Classical.clarify_tac cs' 1,
- IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
- ALLGOALS (Classical.first_best_tac cs')]) end;
+ Classical.clarify_tac cs' 1,
+ IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
+ ALLGOALS (Classical.first_best_tac cs')]) end;
fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i;
fun force i = by (Force_tac i);
@@ -160,7 +161,7 @@
fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end;
-(* attributes *)
+(* change clasimpset *)
fun change_global_css f (thy, th) =
let
@@ -199,11 +200,20 @@
val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
+fun auto_args m =
+ Method.bang_sectioned_args' clasimp_modifiers (Scan.lift (Scan.option (Args.nat -- Args.nat))) m;
+
+fun auto_meth None = clasimp_meth (CHANGED o auto_tac)
+ | auto_meth (Some (m, n)) = clasimp_meth (CHANGED o (fn css => mk_auto_tac css m n));
+
+
+(* theory setup *)
+
val setup =
[Method.add_methods
[("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
("force", clasimp_method' force_tac, "force"),
- ("auto", clasimp_method (CHANGED o auto_tac), "auto"),
+ ("auto", auto_args auto_meth, "auto"),
("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];