functorized Clasimp module;
authorwenzelm
Thu Jul 30 19:02:52 1998 +0200 (1998-07-30 ago)
changeset 5219924359415f09
parent 5218 1a49756a2e68
child 5220 07f80f447b27
functorized Clasimp module;
src/FOL/ROOT.ML
src/FOL/simpdata.ML
src/HOL/ROOT.ML
src/HOL/simpdata.ML
src/Provers/clasimp.ML
     1.1 --- a/src/FOL/ROOT.ML	Thu Jul 30 17:59:57 1998 +0200
     1.2 +++ b/src/FOL/ROOT.ML	Thu Jul 30 19:02:52 1998 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
     1.5  use "$ISABELLE_HOME/src/Provers/classical.ML";
     1.6  use "$ISABELLE_HOME/src/Provers/blast.ML";
     1.7 +use "$ISABELLE_HOME/src/Provers/clasimp.ML";
     1.8  use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
     1.9  
    1.10  use_thy "IFOL";
     2.1 --- a/src/FOL/simpdata.ML	Thu Jul 30 17:59:57 1998 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
     2.3 @@ -334,11 +334,7 @@
     2.4  
     2.5  
     2.6  
     2.7 -
     2.8 -
     2.9 -
    2.10 -
    2.11 -(*** Integration of simplifier with classical reasoner ***)
    2.12 +(*** integration of simplifier with classical reasoner ***)
    2.13  
    2.14  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    2.15     fails if there is no equaliy or if an equality is already at the front *)
    2.16 @@ -353,8 +349,12 @@
    2.17  		if n>0 then rotate_tac n i else no_tac end)
    2.18  end;
    2.19  
    2.20 -use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    2.21 +
    2.22 +structure Clasimp = ClasimpFun
    2.23 + (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
    2.24 +  val addcongs = op addcongs and delcongs = op delcongs
    2.25 +  and addSaltern = op addSaltern and addbefore = op addbefore);
    2.26 +
    2.27  open Clasimp;
    2.28  
    2.29  val FOL_css = (FOL_cs, FOL_ss);
    2.30 -
     3.1 --- a/src/HOL/ROOT.ML	Thu Jul 30 17:59:57 1998 +0200
     3.2 +++ b/src/HOL/ROOT.ML	Thu Jul 30 19:02:52 1998 +0200
     3.3 @@ -21,6 +21,7 @@
     3.4  use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
     3.5  use "$ISABELLE_HOME/src/Provers/classical.ML";
     3.6  use "$ISABELLE_HOME/src/Provers/blast.ML";
     3.7 +use "$ISABELLE_HOME/src/Provers/clasimp.ML";
     3.8  use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
     3.9  use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
    3.10  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
     4.1 --- a/src/HOL/simpdata.ML	Thu Jul 30 17:59:57 1998 +0200
     4.2 +++ b/src/HOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
     4.3 @@ -457,7 +457,7 @@
     4.4  
     4.5  
     4.6  
     4.7 -(*** Integration of simplifier with classical reasoner ***)
     4.8 +(*** integration of simplifier with classical reasoner ***)
     4.9  
    4.10  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    4.11     fails if there is no equaliy or if an equality is already at the front *)
    4.12 @@ -471,7 +471,12 @@
    4.13  		if n>0 then rotate_tac n i else no_tac end)
    4.14  end;
    4.15  
    4.16 -use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    4.17 +
    4.18 +structure Clasimp = ClasimpFun
    4.19 + (structure Simplifier = Simplifier and Classical = Classical and Blast = Blast
    4.20 +  val addcongs = op addcongs and delcongs = op delcongs
    4.21 +  and addSaltern = op addSaltern and addbefore = op addbefore);
    4.22 +
    4.23  open Clasimp;
    4.24  
    4.25  val HOL_css = (HOL_cs, HOL_ss);
     5.1 --- a/src/Provers/clasimp.ML	Thu Jul 30 17:59:57 1998 +0200
     5.2 +++ b/src/Provers/clasimp.ML	Thu Jul 30 19:02:52 1998 +0200
     5.3 @@ -2,18 +2,32 @@
     5.4      ID:         $Id$
     5.5      Author:     David von Oheimb, TU Muenchen
     5.6  
     5.7 -Combination of classical reasoner and simplifier
     5.8 -to be used after installing both of them
     5.9 +Combination of classical reasoner and simplifier (depends on
    5.10 +simplifier.ML, classical.ML, blast.ML).
    5.11  *)
    5.12  
    5.13 -type clasimpset = claset * simpset;
    5.14 -
    5.15  infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
    5.16  	addsimps2 delsimps2 addcongs2 delcongs2;
    5.17  infix 4 addSss addss;
    5.18  
    5.19 +signature CLASIMP_DATA =
    5.20 +sig
    5.21 +  structure Simplifier: SIMPLIFIER
    5.22 +  structure Classical: CLASSICAL
    5.23 +  structure Blast: BLAST
    5.24 +  sharing type Classical.claset = Blast.claset
    5.25 +  val addcongs: Simplifier.simpset * thm list -> Simplifier.simpset
    5.26 +  val delcongs: Simplifier.simpset * thm list -> Simplifier.simpset
    5.27 +  val addSaltern: Classical.claset * (string * (int -> tactic)) -> Classical.claset
    5.28 +  val addbefore: Classical.claset * (string * (int -> tactic)) -> Classical.claset
    5.29 +end
    5.30 +
    5.31  signature CLASIMP =
    5.32  sig
    5.33 +  include CLASIMP_DATA
    5.34 +  type claset
    5.35 +  type simpset
    5.36 +  type clasimpset
    5.37    val addSIs2	: clasimpset * thm list -> clasimpset
    5.38    val addSEs2	: clasimpset * thm list -> clasimpset
    5.39    val addSDs2	: clasimpset * thm list -> clasimpset
    5.40 @@ -35,89 +49,101 @@
    5.41    val force	: int -> unit
    5.42  end;
    5.43  
    5.44 -structure Clasimp: CLASIMP =
    5.45 +functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
    5.46  struct
    5.47  
    5.48 -(* this interface for updating a clasimpset is rudimentary and just for 
    5.49 -   convenience for the most common cases. 
    5.50 -   In other cases a clasimpset may be dealt with componentwise. *)
    5.51 -local 
    5.52 -  fun pair_upd1 f ((a,b),x) = (f(a,x), b);
    5.53 -  fun pair_upd2 f ((a,b),x) = (a, f(b,x));
    5.54 -in
    5.55 -  fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
    5.56 -  fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
    5.57 -  fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
    5.58 -  fun op addIs2    arg = pair_upd1 (op addIs ) arg;
    5.59 -  fun op addEs2    arg = pair_upd1 (op addEs ) arg;
    5.60 -  fun op addDs2    arg = pair_upd1 (op addDs ) arg;
    5.61 -  fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
    5.62 -  fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
    5.63 -  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    5.64 -  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    5.65 -end;
    5.66 +open Data;
    5.67 +
    5.68 +type claset = Classical.claset;
    5.69 +type simpset = Simplifier.simpset;
    5.70 +type clasimpset = claset * simpset;
    5.71 +
    5.72 +
    5.73 +(* clasimpset operations *)
    5.74 +
    5.75 +(*this interface for updating a clasimpset is rudimentary and just for
    5.76 +  convenience for the most common cases*)
    5.77 +
    5.78 +fun pair_upd1 f ((a,b),x) = (f(a,x), b);
    5.79 +fun pair_upd2 f ((a,b),x) = (a, f(b,x));
    5.80 +
    5.81 +fun op addSIs2   arg = pair_upd1 Classical.addSIs arg;
    5.82 +fun op addSEs2   arg = pair_upd1 Classical.addSEs arg;
    5.83 +fun op addSDs2   arg = pair_upd1 Classical.addSDs arg;
    5.84 +fun op addIs2    arg = pair_upd1 Classical.addIs arg;
    5.85 +fun op addEs2    arg = pair_upd1 Classical.addEs arg;
    5.86 +fun op addDs2    arg = pair_upd1 Classical.addDs arg;
    5.87 +fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg;
    5.88 +fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg;
    5.89 +fun op addcongs2 arg = pair_upd2 Data.addcongs arg;
    5.90 +fun op delcongs2 arg = pair_upd2 Data.delcongs arg;
    5.91  
    5.92  (*Add a simpset to a classical set!*)
    5.93  (*Caution: only one simpset added can be added by each of addSss and addss*)
    5.94  fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
    5.95 -			CHANGED o (safe_asm_full_simp_tac ss));
    5.96 -fun cs addss  ss = cs addbefore  (     "asm_full_simp_tac",
    5.97 -					asm_full_simp_tac ss);
    5.98 +			CHANGED o Simplifier.safe_asm_full_simp_tac ss);
    5.99 +fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", Simplifier.asm_full_simp_tac ss);
   5.100  
   5.101  
   5.102 -fun CLASIMPSET tacf state = CLASET (fn cs => SIMPSET (fn ss => tacf (cs, ss))) state;
   5.103 -fun CLASIMPSET' tacf i state = CLASET (fn cs => SIMPSET (fn ss => tacf (cs, ss) i)) state;
   5.104 +(* tacticals *)
   5.105 +
   5.106 +fun CLASIMPSET tacf state =
   5.107 +  Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
   5.108 +
   5.109 +fun CLASIMPSET' tacf i state =
   5.110 +  Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
   5.111  
   5.112  
   5.113 -local
   5.114 +(* auto_tac *)
   5.115  
   5.116 -	fun blast_depth_tac cs m i thm = Blast.depth_tac cs m i thm 
   5.117 -		handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
   5.118 +fun blast_depth_tac cs m i thm =
   5.119 +  Blast.depth_tac cs m i thm handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
   5.120  
   5.121 -	(* a variant of depth_tac that avoids interference of the simplifier 
   5.122 -	   with dup_step_tac when they are combined by auto_tac *)
   5.123 -	fun nodup_depth_tac cs m i state = 
   5.124 -	  SELECT_GOAL 
   5.125 -	   (appWrappers cs
   5.126 -	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
   5.127 -	                             (safe_step_tac cs i)) THEN_ELSE
   5.128 -	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
   5.129 -	      inst0_step_tac cs i  APPEND
   5.130 -	      COND (K(m=0)) no_tac
   5.131 -	        ((instp_step_tac cs i APPEND step_tac cs i)
   5.132 -	         THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
   5.133 -	  i state;
   5.134 -
   5.135 -in
   5.136 +(* a variant of depth_tac that avoids interference of the simplifier 
   5.137 +   with dup_step_tac when they are combined by auto_tac *)
   5.138 +fun nodup_depth_tac cs m i state = 
   5.139 +  SELECT_GOAL 
   5.140 +   (Classical.appWrappers cs
   5.141 +    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
   5.142 +                             (Classical.safe_step_tac cs i)) THEN_ELSE
   5.143 +     (DEPTH_SOLVE (nodup_depth_tac cs m i),
   5.144 +      Classical.inst0_step_tac cs i  APPEND
   5.145 +      COND (K(m=0)) no_tac
   5.146 +        ((Classical.instp_step_tac cs i APPEND Classical.step_tac cs i)
   5.147 +         THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
   5.148 +  i state;
   5.149  
   5.150  (*Designed to be idempotent, except if best_tac instantiates variables
   5.151    in some of the subgoals*)
   5.152  fun mk_auto_tac (cs, ss) m n =
   5.153 -    let val cs' = cs addss ss 
   5.154 +    let val cs' = cs addss ss
   5.155          val maintac = 
   5.156            blast_depth_tac cs m		(*fast but can't use addss*)
   5.157            ORELSE'
   5.158            nodup_depth_tac cs' n;	(*slower but more general*)
   5.159 -    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
   5.160 -	       TRY (safe_tac cs'),
   5.161 +    in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
   5.162 +	       TRY (Classical.safe_tac cs'),
   5.163  	       REPEAT (FIRSTGOAL maintac),
   5.164 -               TRY (safe_tac (cs addSss ss)),
   5.165 +               TRY (Classical.safe_tac (cs addSss ss)),
   5.166  	       prune_params_tac] 
   5.167      end;
   5.168 -end;
   5.169  
   5.170  fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
   5.171  
   5.172 -fun Auto_tac st = auto_tac (claset(), simpset()) st;
   5.173 +fun Auto_tac st = auto_tac (Classical.claset(), Simplifier.simpset()) st;
   5.174  
   5.175  fun auto () = by Auto_tac;
   5.176  
   5.177 +
   5.178 +(* force_tac *)
   5.179 +
   5.180  (* aimed to solve the given subgoal totally, using whatever tools possible *)
   5.181  fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
   5.182 -	clarify_tac cs' 1,
   5.183 -	IF_UNSOLVED (asm_full_simp_tac ss 1),
   5.184 -	ALLGOALS (best_tac cs')]) end;
   5.185 -fun Force_tac i = force_tac (claset(), simpset()) i;
   5.186 +	Classical.clarify_tac cs' 1,
   5.187 +	IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
   5.188 +	ALLGOALS (Classical.best_tac cs')]) end;
   5.189 +fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i;
   5.190  fun force i = by (Force_tac i);
   5.191  
   5.192 +
   5.193  end;