factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
authoroheimb
Wed Feb 25 20:25:27 1998 +0100 (1998-02-25 ago)
changeset 4652d24cca140eeb
parent 4651 70dd492a1698
child 4653 d60f76680bf4
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML
explicitly introducing combined type clasimpset
src/FOL/simpdata.ML
src/HOL/TLA/cladata.ML
src/HOL/simpdata.ML
src/Provers/clasimp.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Feb 25 15:51:24 1998 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Feb 25 20:25:27 1998 +0100
     1.3 @@ -309,6 +309,10 @@
     1.4  
     1.5  
     1.6  
     1.7 +
     1.8 +
     1.9 +
    1.10 +
    1.11  (*** Integration of simplifier with classical reasoner ***)
    1.12  
    1.13  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    1.14 @@ -324,64 +328,8 @@
    1.15  		if n>0 then rotate_tac n i else no_tac end)
    1.16  end;
    1.17  
    1.18 -
    1.19 -fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
    1.20 -				     safe_asm_full_simp_tac ss;
    1.21 -(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
    1.22 -  better: asm_really_full_simp_tac, a yet to be implemented version of
    1.23 -			asm_full_simp_tac that applies all equalities in the
    1.24 -			premises to all the premises *)
    1.25 -
    1.26 -(*Add a simpset to a classical set!*)
    1.27 -infix 4 addSss addss;
    1.28 -fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
    1.29 -				  CHANGED o (safe_asm_more_full_simp_tac ss));
    1.30 -fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
    1.31 -
    1.32 -fun Addss ss = (claset_ref() := claset() addss ss);
    1.33 -
    1.34 -(*Designed to be idempotent, except if best_tac instantiates variables
    1.35 -  in some of the subgoals*)
    1.36 -
    1.37 -type clasimpset = (claset * simpset);
    1.38 +use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    1.39 +open Clasimp;
    1.40  
    1.41  val FOL_css = (FOL_cs, FOL_ss);
    1.42  
    1.43 -fun pair_upd1 f ((a,b),x) = (f(a,x), b);
    1.44 -fun pair_upd2 f ((a,b),x) = (a, f(b,x));
    1.45 -
    1.46 -infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
    1.47 -	addsimps2 delsimps2 addcongs2 delcongs2;
    1.48 -fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
    1.49 -fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
    1.50 -fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
    1.51 -fun op addIs2    arg = pair_upd1 (op addIs ) arg;
    1.52 -fun op addEs2    arg = pair_upd1 (op addEs ) arg;
    1.53 -fun op addDs2    arg = pair_upd1 (op addDs ) arg;
    1.54 -fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
    1.55 -fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
    1.56 -fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    1.57 -fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    1.58 -
    1.59 -
    1.60 -fun mk_auto_tac (cs, ss) m n =
    1.61 -    let val cs' = cs addss ss 
    1.62 -	val bdt = Blast.depth_tac cs m;
    1.63 -	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
    1.64 -		(warning ("Blast_tac: " ^ s); Seq.empty);
    1.65 -        val maintac = 
    1.66 -          blast_depth_tac	   (*fast but can't use addss*)
    1.67 -          ORELSE'
    1.68 -          depth_tac cs' n;         (*slower but general*)
    1.69 -    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
    1.70 -	       TRY (safe_tac cs'),
    1.71 -	       REPEAT (FIRSTGOAL maintac),
    1.72 -               TRY (safe_tac (cs addSss ss)),
    1.73 -	       prune_params_tac] 
    1.74 -    end;
    1.75 -
    1.76 -fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
    1.77 -
    1.78 -fun Auto_tac st = auto_tac (claset(), simpset()) st;
    1.79 -
    1.80 -fun auto () = by Auto_tac;
     2.1 --- a/src/HOL/TLA/cladata.ML	Wed Feb 25 15:51:24 1998 +0100
     2.2 +++ b/src/HOL/TLA/cladata.ML	Wed Feb 25 20:25:27 1998 +0100
     2.3 @@ -51,7 +51,7 @@
     2.4  
     2.5  AddSIs [actionI,intI];
     2.6  AddDs  [actionD,intD];
     2.7 -Addss  (simpset());
     2.8 +claset_ref() := claset() addss (simpset());
     2.9  
    2.10  
    2.11  
     3.1 --- a/src/HOL/simpdata.ML	Wed Feb 25 15:51:24 1998 +0100
     3.2 +++ b/src/HOL/simpdata.ML	Wed Feb 25 20:25:27 1998 +0100
     3.3 @@ -424,6 +424,10 @@
     3.4  simpset_ref() := HOL_ss;
     3.5  
     3.6  
     3.7 +
     3.8 +
     3.9 +
    3.10 +
    3.11  (*** Integration of simplifier with classical reasoner ***)
    3.12  
    3.13  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    3.14 @@ -438,77 +442,7 @@
    3.15  		if n>0 then rotate_tac n i else no_tac end)
    3.16  end;
    3.17  
    3.18 -(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
    3.19 -  better: asm_really_full_simp_tac, a yet to be implemented version of
    3.20 -			asm_full_simp_tac that applies all equalities in the
    3.21 -			premises to all the premises *)
    3.22 -fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
    3.23 -				     safe_asm_full_simp_tac ss;
    3.24 -
    3.25 -(*Add a simpset to a classical set!*)
    3.26 -infix 4 addSss addss;
    3.27 -fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
    3.28 -				  CHANGED o (safe_asm_more_full_simp_tac ss));
    3.29 -fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
    3.30 -
    3.31 -fun Addss ss = (claset_ref() := claset() addss ss);
    3.32 -
    3.33 -(*Designed to be idempotent, except if best_tac instantiates variables
    3.34 -  in some of the subgoals*)
    3.35 -
    3.36 -type clasimpset = (claset * simpset);
    3.37 +use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    3.38 +open Clasimp;
    3.39  
    3.40  val HOL_css = (HOL_cs, HOL_ss);
    3.41 -
    3.42 -fun pair_upd1 f ((a,b),x) = (f(a,x), b);
    3.43 -fun pair_upd2 f ((a,b),x) = (a, f(b,x));
    3.44 -
    3.45 -infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
    3.46 -	addsimps2 delsimps2 addcongs2 delcongs2;
    3.47 -fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
    3.48 -fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
    3.49 -fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
    3.50 -fun op addIs2    arg = pair_upd1 (op addIs ) arg;
    3.51 -fun op addEs2    arg = pair_upd1 (op addEs ) arg;
    3.52 -fun op addDs2    arg = pair_upd1 (op addDs ) arg;
    3.53 -fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
    3.54 -fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
    3.55 -fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    3.56 -fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    3.57 -
    3.58 -fun mk_auto_tac (cs, ss) m n =
    3.59 -    let val cs' = cs addss ss 
    3.60 -	val bdt = Blast.depth_tac cs m;
    3.61 -	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
    3.62 -		(warning ("Blast_tac: " ^ s); Seq.empty);
    3.63 -
    3.64 -	(* a variant of depth_tac that avoids interference of the simplifier 
    3.65 -	   with dup_step_tac when they are combined by auto_tac *)
    3.66 -	fun nodup_depth_tac cs m i state = 
    3.67 -	  SELECT_GOAL 
    3.68 -	   (appWrappers cs
    3.69 -	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
    3.70 -				     (safe_step_tac cs i)) THEN_ELSE
    3.71 -	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
    3.72 -	      inst0_step_tac cs i  APPEND
    3.73 -	      COND (K(m=0)) no_tac
    3.74 -	        ((instp_step_tac cs i APPEND step_tac cs i)
    3.75 -		 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
    3.76 -	  i state;
    3.77 -
    3.78 -        val maintac = 
    3.79 -          blast_depth_tac	   (*fast but can't use addss*)
    3.80 -          ORELSE'
    3.81 -          nodup_depth_tac cs' n;   (*slower but more general*)
    3.82 -    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
    3.83 -	       TRY (safe_tac cs'),
    3.84 -	       REPEAT (FIRSTGOAL maintac),
    3.85 -               TRY (safe_tac (cs addSss ss)),
    3.86 -	       prune_params_tac] 
    3.87 -    end;
    3.88 -
    3.89 -fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
    3.90 -
    3.91 -fun Auto_tac st = auto_tac (claset(), simpset()) st;
    3.92 -
    3.93 -fun auto () = by Auto_tac;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Provers/clasimp.ML	Wed Feb 25 20:25:27 1998 +0100
     4.3 @@ -0,0 +1,110 @@
     4.4 +(*  Title: 	Provers/clasimp.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     David von Oheimb, TU Muenchen
     4.7 +
     4.8 +Combination of classical reasoner and simplifier
     4.9 +to be used after installing both of them
    4.10 +*)
    4.11 +
    4.12 +infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
    4.13 +	addsimps2 delsimps2 addcongs2 delcongs2;
    4.14 +infix 4 addSss addss;
    4.15 +
    4.16 +type clasimpset = claset * simpset;
    4.17 +
    4.18 +signature CLASIMP =
    4.19 +sig
    4.20 +  val addSIs2	: clasimpset * thm list -> clasimpset
    4.21 +  val addSEs2	: clasimpset * thm list -> clasimpset
    4.22 +  val addSDs2	: clasimpset * thm list -> clasimpset
    4.23 +  val addIs2	: clasimpset * thm list -> clasimpset
    4.24 +  val addEs2	: clasimpset * thm list -> clasimpset
    4.25 +  val addDs2	: clasimpset * thm list -> clasimpset
    4.26 +  val addsimps2	: clasimpset * thm list -> clasimpset
    4.27 +  val delsimps2	: clasimpset * thm list -> clasimpset
    4.28 +  val addSss	: claset * simpset -> claset
    4.29 +  val addss	: claset * simpset -> claset
    4.30 +  val mk_auto_tac:clasimpset -> int -> int -> tactic
    4.31 +  val auto_tac	: clasimpset -> tactic
    4.32 +  val Auto_tac	: tactic
    4.33 +  val auto	: unit -> unit
    4.34 +end;
    4.35 +
    4.36 +structure Clasimp: CLASIMP =
    4.37 +struct
    4.38 +
    4.39 +local 
    4.40 +  fun pair_upd1 f ((a,b),x) = (f(a,x), b);
    4.41 +  fun pair_upd2 f ((a,b),x) = (a, f(b,x));
    4.42 +in
    4.43 +  fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
    4.44 +  fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
    4.45 +  fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
    4.46 +  fun op addIs2    arg = pair_upd1 (op addIs ) arg;
    4.47 +  fun op addEs2    arg = pair_upd1 (op addEs ) arg;
    4.48 +  fun op addDs2    arg = pair_upd1 (op addDs ) arg;
    4.49 +  fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
    4.50 +  fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
    4.51 +  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    4.52 +  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    4.53 +end;
    4.54 +
    4.55 +(*an unsatisfactory fix for the incomplete safe_asm_full_simp_tac!
    4.56 +  better: asm_really_full_simp_tac, a yet to be implemented version of
    4.57 +			asm_full_simp_tac that applies all equalities in the
    4.58 +			premises to all the premises *)
    4.59 +fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
    4.60 +				     safe_asm_full_simp_tac ss;
    4.61 +
    4.62 +(*Add a simpset to a classical set!*)
    4.63 +(*Caution: only one simpset added can be added by each of addSss and addss*)
    4.64 +fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
    4.65 +			CHANGED o (safe_asm_more_full_simp_tac ss));
    4.66 +fun cs addss  ss = cs addbefore  (     "asm_full_simp_tac",
    4.67 +					asm_full_simp_tac ss);
    4.68 +
    4.69 +
    4.70 +local
    4.71 +
    4.72 +	fun blast_depth_tac cs m i thm = Blast.depth_tac cs m i thm 
    4.73 +		handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
    4.74 +
    4.75 +	(* a variant of depth_tac that avoids interference of the simplifier 
    4.76 +	   with dup_step_tac when they are combined by auto_tac *)
    4.77 +	fun nodup_depth_tac cs m i state = 
    4.78 +	  SELECT_GOAL 
    4.79 +	   (appWrappers cs
    4.80 +	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
    4.81 +	                             (safe_step_tac cs i)) THEN_ELSE
    4.82 +	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
    4.83 +	      inst0_step_tac cs i  APPEND
    4.84 +	      COND (K(m=0)) no_tac
    4.85 +	        ((instp_step_tac cs i APPEND step_tac cs i)
    4.86 +	         THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
    4.87 +	  i state;
    4.88 +
    4.89 +in
    4.90 +
    4.91 +(*Designed to be idempotent, except if best_tac instantiates variables
    4.92 +  in some of the subgoals*)
    4.93 +fun mk_auto_tac (cs, ss) m n =
    4.94 +    let val cs' = cs addss ss 
    4.95 +        val maintac = 
    4.96 +          blast_depth_tac cs m		(*fast but can't use addss*)
    4.97 +          ORELSE'
    4.98 +          nodup_depth_tac cs' n;	(*slower but more general*)
    4.99 +    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
   4.100 +	       TRY (safe_tac cs'),
   4.101 +	       REPEAT (FIRSTGOAL maintac),
   4.102 +               TRY (safe_tac (cs addSss ss)),
   4.103 +	       prune_params_tac] 
   4.104 +    end;
   4.105 +end;
   4.106 +
   4.107 +fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
   4.108 +
   4.109 +fun Auto_tac st = auto_tac (claset(), simpset()) st;
   4.110 +
   4.111 +fun auto () = by Auto_tac;
   4.112 +
   4.113 +end;