# HG changeset patch
# User wenzelm
# Date 1303847379 -7200
# Node ID 8a526c010c3bafc50441c58690a25b0f03b9027c
# Parent  52fa26b6c524c1a399a7c7058b1565224548a208
modernized Clasimp setup;

diff -r 52fa26b6c524 -r 8a526c010c3b src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Apr 26 21:27:01 2011 +0200
+++ b/src/FOL/simpdata.ML	Tue Apr 26 21:49:39 2011 +0200
@@ -130,10 +130,16 @@
 
 (*** integration of simplifier with classical reasoner ***)
 
-structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier and Splitter = Splitter
-  and Classical  = Cla and Blast = Blast
-  val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
+structure Clasimp = Clasimp
+(
+  structure Simplifier = Simplifier
+    and Splitter = Splitter
+    and Classical = Cla
+    and Blast = Blast
+  val iffD1 = @{thm iffD1}
+  val iffD2 = @{thm iffD2}
+  val notE = @{thm notE}
+);
 open Clasimp;
 
 ML_Antiquote.value "clasimpset"
diff -r 52fa26b6c524 -r 8a526c010c3b src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Tue Apr 26 21:27:01 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML	Tue Apr 26 21:49:39 2011 +0200
@@ -151,10 +151,16 @@
 
 (* integration of simplifier with classical reasoner *)
 
-structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier and Splitter = Splitter
-  and Classical  = Classical and Blast = Blast
-  val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
+structure Clasimp = Clasimp
+(
+  structure Simplifier = Simplifier
+    and Splitter = Splitter
+    and Classical  = Classical
+    and Blast = Blast
+  val iffD1 = @{thm iffD1}
+  val iffD2 = @{thm iffD2}
+  val notE = @{thm notE}
+);
 open Clasimp;
 
 val _ = ML_Antiquote.value "clasimpset"
diff -r 52fa26b6c524 -r 8a526c010c3b src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Apr 26 21:27:01 2011 +0200
+++ b/src/Provers/clasimp.ML	Tue Apr 26 21:49:39 2011 +0200
@@ -21,7 +21,6 @@
 
 signature CLASIMP =
 sig
-  include CLASIMP_DATA
   type claset
   type clasimpset
   val get_css: Context.generic -> clasimpset
@@ -56,10 +55,12 @@
   val clasimp_setup: theory -> theory
 end;
 
-functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
+functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
 struct
 
-open Data;
+structure Splitter = Data.Splitter;
+structure Classical = Data.Classical;
+structure Blast = Data.Blast;
 
 
 (* type clasimpset *)
@@ -104,12 +105,14 @@
 
 (*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 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));
+fun cs addSss ss =
+  Classical.addSafter (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));
+
+fun cs addss' ss =
+  Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss));
 
 (* iffs: addition of rules to simpsets and clasets simultaneously *)
 
@@ -126,18 +129,18 @@
     val (elim, intro) = if n = 0 then decls1 else decls2;
     val zero_rotate = zero_var_indexes o rotate_prems n;
   in
-    (elim (intro (cs, [zero_rotate (th RS iffD2)]),
-           [Tactic.make_elim (zero_rotate (th RS iffD1))])
-      handle THM _ => (elim (cs, [zero_rotate (th RS notE)])
+    (elim (intro (cs, [zero_rotate (th RS Data.iffD2)]),
+           [Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
+      handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)])
         handle THM _ => intro (cs, [th])),
      simp (ss, [th]))
   end;
 
 fun delIff delcs delss ((cs, ss), th) =
   let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
-    (delcs (cs, [zero_rotate (th RS iffD2),
-        Tactic.make_elim (zero_rotate (th RS iffD1))])
-      handle THM _ => (delcs (cs, [zero_rotate (th RS notE)])
+    (delcs (cs, [zero_rotate (th RS Data.iffD2),
+        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
+      handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
         handle THM _ => delcs (cs, [th])),
      delss (ss, [th]))
   end;
@@ -167,7 +170,7 @@
 end;
 
 
-(* tacticals *)
+(* tactics *)
 
 fun clarsimp_tac (cs, ss) =
   safe_asm_full_simp_tac ss THEN_ALL_NEW
@@ -177,36 +180,43 @@
 (* auto_tac *)
 
 fun blast_depth_tac cs m i thm =
-    Blast.depth_tac cs m i thm
-      handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
+  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
    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))
-        )) i state;
+
+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;
 
 (*Designed to be idempotent, except if blast_depth_tac instantiates variables
   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 *)
-          ORELSE'
-          (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
-    in  EVERY [PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)),
-               TRY (Classical.safe_tac cs),
-               REPEAT_DETERM (FIRSTGOAL maintac),
-               TRY (Classical.safe_tac (cs addSss ss)),
-               prune_params_tac]
-    end;
+  let
+    val cs' = cs addss ss;
+    val main_tac =
+      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 [PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)),
+      TRY (Classical.safe_tac cs),
+      REPEAT_DETERM (FIRSTGOAL main_tac),
+      TRY (Classical.safe_tac (cs addSss ss)),
+      prune_params_tac]
+  end;
 
 fun auto_tac css = mk_auto_tac css 4 2;
 
@@ -214,10 +224,13 @@
 (* 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;
+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;
 
 
 (* basic combinations *)
@@ -229,9 +242,8 @@
 val best_simp_tac = ADDSS Classical.best_tac;
 
 
-(* access clasimpset *)
 
-
+(** access clasimpset **)
 
 (* attributes *)