corrected problem with auto_tac: now uses a variant of depth_tac that avoids
authoroheimb
Wed Feb 18 18:42:54 1998 +0100 (1998-02-18)
changeset 4633d4a074973715
parent 4632 0a365c3e4b27
child 4634 83d364462ce1
corrected problem with auto_tac: now uses a variant of depth_tac that avoids
interference of the simplifier with dup_step_tac
src/HOL/Auth/Shared.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Wed Feb 18 17:32:18 1998 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Wed Feb 18 18:42:54 1998 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4  by (etac exE 1);
     1.5  by (cut_inst_tac [("evs","evs'")] 
     1.6      (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
     1.7 -by Auto_tac;
     1.8 +by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
     1.9  qed "Key_supply2";
    1.10  
    1.11  goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
     2.1 --- a/src/HOL/simpdata.ML	Wed Feb 18 17:32:18 1998 +0100
     2.2 +++ b/src/HOL/simpdata.ML	Wed Feb 18 18:42:54 1998 +0100
     2.3 @@ -476,10 +476,25 @@
     2.4  	val bdt = Blast.depth_tac cs m;
     2.5  	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
     2.6  		(warning ("Blast_tac: " ^ s); Seq.empty);
     2.7 +
     2.8 +	(* a variant of depth_tac that avoids interference of the simplifier 
     2.9 +	   with dup_step_tac when they are combined by auto_tac *)
    2.10 +	fun nodup_depth_tac cs m i state = 
    2.11 +	  SELECT_GOAL 
    2.12 +	   (getWrapper cs
    2.13 +	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
    2.14 +				     (safe_step_tac cs i)) THEN_ELSE
    2.15 +	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
    2.16 +	      inst0_step_tac cs i  APPEND
    2.17 +	      COND (K(m=0)) no_tac
    2.18 +	        ((instp_step_tac cs i APPEND step_tac cs i)
    2.19 +		 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
    2.20 +	  i state;
    2.21 +
    2.22          val maintac = 
    2.23            blast_depth_tac	   (*fast but can't use addss*)
    2.24            ORELSE'
    2.25 -          depth_tac cs' n;         (*slower but general*)
    2.26 +          nodup_depth_tac cs' n;   (*slower but more general*)
    2.27      in  EVERY [ALLGOALS (asm_full_simp_tac ss),
    2.28  	       TRY (safe_tac cs'),
    2.29  	       REPEAT (FIRSTGOAL maintac),