modernized Clasimp setup;
authorwenzelm
Tue Apr 26 21:49:39 2011 +0200 (2011-04-26)
changeset 424788a526c010c3b
parent 42477 52fa26b6c524
child 42479 b7c9f09d4d88
modernized Clasimp setup;
src/FOL/simpdata.ML
src/HOL/Tools/simpdata.ML
src/Provers/clasimp.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Apr 26 21:27:01 2011 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Apr 26 21:49:39 2011 +0200
     1.3 @@ -130,10 +130,16 @@
     1.4  
     1.5  (*** integration of simplifier with classical reasoner ***)
     1.6  
     1.7 -structure Clasimp = ClasimpFun
     1.8 - (structure Simplifier = Simplifier and Splitter = Splitter
     1.9 -  and Classical  = Cla and Blast = Blast
    1.10 -  val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
    1.11 +structure Clasimp = Clasimp
    1.12 +(
    1.13 +  structure Simplifier = Simplifier
    1.14 +    and Splitter = Splitter
    1.15 +    and Classical = Cla
    1.16 +    and Blast = Blast
    1.17 +  val iffD1 = @{thm iffD1}
    1.18 +  val iffD2 = @{thm iffD2}
    1.19 +  val notE = @{thm notE}
    1.20 +);
    1.21  open Clasimp;
    1.22  
    1.23  ML_Antiquote.value "clasimpset"
     2.1 --- a/src/HOL/Tools/simpdata.ML	Tue Apr 26 21:27:01 2011 +0200
     2.2 +++ b/src/HOL/Tools/simpdata.ML	Tue Apr 26 21:49:39 2011 +0200
     2.3 @@ -151,10 +151,16 @@
     2.4  
     2.5  (* integration of simplifier with classical reasoner *)
     2.6  
     2.7 -structure Clasimp = ClasimpFun
     2.8 - (structure Simplifier = Simplifier and Splitter = Splitter
     2.9 -  and Classical  = Classical and Blast = Blast
    2.10 -  val iffD1 = @{thm iffD1} val iffD2 = @{thm iffD2} val notE = @{thm notE});
    2.11 +structure Clasimp = Clasimp
    2.12 +(
    2.13 +  structure Simplifier = Simplifier
    2.14 +    and Splitter = Splitter
    2.15 +    and Classical  = Classical
    2.16 +    and Blast = Blast
    2.17 +  val iffD1 = @{thm iffD1}
    2.18 +  val iffD2 = @{thm iffD2}
    2.19 +  val notE = @{thm notE}
    2.20 +);
    2.21  open Clasimp;
    2.22  
    2.23  val _ = ML_Antiquote.value "clasimpset"
     3.1 --- a/src/Provers/clasimp.ML	Tue Apr 26 21:27:01 2011 +0200
     3.2 +++ b/src/Provers/clasimp.ML	Tue Apr 26 21:49:39 2011 +0200
     3.3 @@ -21,7 +21,6 @@
     3.4  
     3.5  signature CLASIMP =
     3.6  sig
     3.7 -  include CLASIMP_DATA
     3.8    type claset
     3.9    type clasimpset
    3.10    val get_css: Context.generic -> clasimpset
    3.11 @@ -56,10 +55,12 @@
    3.12    val clasimp_setup: theory -> theory
    3.13  end;
    3.14  
    3.15 -functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
    3.16 +functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
    3.17  struct
    3.18  
    3.19 -open Data;
    3.20 +structure Splitter = Data.Splitter;
    3.21 +structure Classical = Data.Classical;
    3.22 +structure Blast = Data.Blast;
    3.23  
    3.24  
    3.25  (* type clasimpset *)
    3.26 @@ -104,12 +105,14 @@
    3.27  
    3.28  (*Add a simpset to a classical set!*)
    3.29  (*Caution: only one simpset added can be added by each of addSss and addss*)
    3.30 -fun cs addSss ss = Classical.addSafter (cs, ("safe_asm_full_simp_tac",
    3.31 -                            CHANGED o safe_asm_full_simp_tac ss));
    3.32 -fun cs addss  ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
    3.33 -                            CHANGED o Simplifier.asm_full_simp_tac ss));
    3.34 -fun cs addss' ss = Classical.addbefore  (cs, ("asm_full_simp_tac",
    3.35 -                            CHANGED o Simplifier.asm_lr_simp_tac ss));
    3.36 +fun cs addSss ss =
    3.37 +  Classical.addSafter (cs, ("safe_asm_full_simp_tac", CHANGED o safe_asm_full_simp_tac ss));
    3.38 +
    3.39 +fun cs addss ss =
    3.40 +  Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss));
    3.41 +
    3.42 +fun cs addss' ss =
    3.43 +  Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss));
    3.44  
    3.45  (* iffs: addition of rules to simpsets and clasets simultaneously *)
    3.46  
    3.47 @@ -126,18 +129,18 @@
    3.48      val (elim, intro) = if n = 0 then decls1 else decls2;
    3.49      val zero_rotate = zero_var_indexes o rotate_prems n;
    3.50    in
    3.51 -    (elim (intro (cs, [zero_rotate (th RS iffD2)]),
    3.52 -           [Tactic.make_elim (zero_rotate (th RS iffD1))])
    3.53 -      handle THM _ => (elim (cs, [zero_rotate (th RS notE)])
    3.54 +    (elim (intro (cs, [zero_rotate (th RS Data.iffD2)]),
    3.55 +           [Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
    3.56 +      handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)])
    3.57          handle THM _ => intro (cs, [th])),
    3.58       simp (ss, [th]))
    3.59    end;
    3.60  
    3.61  fun delIff delcs delss ((cs, ss), th) =
    3.62    let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
    3.63 -    (delcs (cs, [zero_rotate (th RS iffD2),
    3.64 -        Tactic.make_elim (zero_rotate (th RS iffD1))])
    3.65 -      handle THM _ => (delcs (cs, [zero_rotate (th RS notE)])
    3.66 +    (delcs (cs, [zero_rotate (th RS Data.iffD2),
    3.67 +        Tactic.make_elim (zero_rotate (th RS Data.iffD1))])
    3.68 +      handle THM _ => (delcs (cs, [zero_rotate (th RS Data.notE)])
    3.69          handle THM _ => delcs (cs, [th])),
    3.70       delss (ss, [th]))
    3.71    end;
    3.72 @@ -167,7 +170,7 @@
    3.73  end;
    3.74  
    3.75  
    3.76 -(* tacticals *)
    3.77 +(* tactics *)
    3.78  
    3.79  fun clarsimp_tac (cs, ss) =
    3.80    safe_asm_full_simp_tac ss THEN_ALL_NEW
    3.81 @@ -177,36 +180,43 @@
    3.82  (* auto_tac *)
    3.83  
    3.84  fun blast_depth_tac cs m i thm =
    3.85 -    Blast.depth_tac cs m i thm
    3.86 -      handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
    3.87 +  Blast.depth_tac cs m i thm
    3.88 +    handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
    3.89  
    3.90  (* a variant of depth_tac that avoids interference of the simplifier
    3.91     with dup_step_tac when they are combined by auto_tac *)
    3.92  local
    3.93 -fun slow_step_tac' cs = Classical.appWrappers cs
    3.94 -        (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
    3.95 -in fun nodup_depth_tac cs m i state = SELECT_GOAL
    3.96 -   (Classical.safe_steps_tac cs 1 THEN_ELSE
    3.97 -        (DEPTH_SOLVE (nodup_depth_tac cs m 1),
    3.98 -         Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
    3.99 -             (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1))
   3.100 -        )) i state;
   3.101 +
   3.102 +fun slow_step_tac' cs =
   3.103 +  Classical.appWrappers cs
   3.104 +    (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
   3.105 +
   3.106 +in
   3.107 +
   3.108 +fun nodup_depth_tac cs m i state =
   3.109 +  SELECT_GOAL
   3.110 +    (Classical.safe_steps_tac cs 1 THEN_ELSE
   3.111 +      (DEPTH_SOLVE (nodup_depth_tac cs m 1),
   3.112 +        Classical.inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
   3.113 +          (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m - 1) 1)))) i state;
   3.114  end;
   3.115  
   3.116  (*Designed to be idempotent, except if blast_depth_tac instantiates variables
   3.117    in some of the subgoals*)
   3.118  fun mk_auto_tac (cs, ss) m n =
   3.119 -    let val cs' = cs addss ss
   3.120 -        val maintac =
   3.121 -          blast_depth_tac cs m               (* fast but can't use wrappers *)
   3.122 -          ORELSE'
   3.123 -          (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
   3.124 -    in  EVERY [PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)),
   3.125 -               TRY (Classical.safe_tac cs),
   3.126 -               REPEAT_DETERM (FIRSTGOAL maintac),
   3.127 -               TRY (Classical.safe_tac (cs addSss ss)),
   3.128 -               prune_params_tac]
   3.129 -    end;
   3.130 +  let
   3.131 +    val cs' = cs addss ss;
   3.132 +    val main_tac =
   3.133 +      blast_depth_tac cs m               (* fast but can't use wrappers *)
   3.134 +      ORELSE'
   3.135 +      (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
   3.136 +  in
   3.137 +    EVERY [PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)),
   3.138 +      TRY (Classical.safe_tac cs),
   3.139 +      REPEAT_DETERM (FIRSTGOAL main_tac),
   3.140 +      TRY (Classical.safe_tac (cs addSss ss)),
   3.141 +      prune_params_tac]
   3.142 +  end;
   3.143  
   3.144  fun auto_tac css = mk_auto_tac css 4 2;
   3.145  
   3.146 @@ -214,10 +224,13 @@
   3.147  (* force_tac *)
   3.148  
   3.149  (* aimed to solve the given subgoal totally, using whatever tools possible *)
   3.150 -fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
   3.151 -        Classical.clarify_tac cs' 1,
   3.152 -        IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
   3.153 -        ALLGOALS (Classical.first_best_tac cs')]) end;
   3.154 +fun force_tac (cs, ss) =
   3.155 +  let val cs' = cs addss ss in
   3.156 +    SELECT_GOAL (EVERY [
   3.157 +      Classical.clarify_tac cs' 1,
   3.158 +      IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
   3.159 +      ALLGOALS (Classical.first_best_tac cs')])
   3.160 +  end;
   3.161  
   3.162  
   3.163  (* basic combinations *)
   3.164 @@ -229,9 +242,8 @@
   3.165  val best_simp_tac = ADDSS Classical.best_tac;
   3.166  
   3.167  
   3.168 -(* access clasimpset *)
   3.169  
   3.170 -
   3.171 +(** access clasimpset **)
   3.172  
   3.173  (* attributes *)
   3.174