src/Provers/clasimp.ML
changeset 9772 c07777210a69
parent 9591 590d36e059d1
child 9805 10b617bdd028
--- 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")]];