corrected auto_tac (applications of unsafe wrappers)
authoroheimb
Fri Oct 23 20:35:56 1998 +0200 (1998-10-23)
changeset 57568ef5288c24b0
parent 5755 22081de41254
child 5757 0ad476dabbc6
corrected auto_tac (applications of unsafe wrappers)
by correcting (and simplifying) nodup_depth_tac
src/Provers/clasimp.ML
     1.1 --- a/src/Provers/clasimp.ML	Fri Oct 23 20:35:19 1998 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Fri Oct 23 20:35:56 1998 +0200
     1.3 @@ -99,27 +99,28 @@
     1.4  fun blast_depth_tac cs m i thm =
     1.5      Blast.depth_tac cs m i thm 
     1.6        handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
     1.7 -
     1.8 + 
     1.9  (* a variant of depth_tac that avoids interference of the simplifier 
    1.10     with dup_step_tac when they are combined by auto_tac *)
    1.11 -fun nodup_depth_tac cs m i state = CHANGED (SELECT_GOAL 
    1.12 -   (REPEAT_DETERM1 (COND (has_fewer_prems 1) no_tac
    1.13 -                                             (Classical.safe_step_tac cs 1))
    1.14 -    THEN_ELSE (DEPTH_SOLVE (nodup_depth_tac cs m 1),
    1.15 -	Classical.appWrappers cs (fn i => Classical.inst0_step_tac cs i APPEND
    1.16 -        COND (K(m=0)) no_tac
    1.17 -            ((Classical.instp_step_tac cs i APPEND Classical.step_tac cs i)
    1.18 -            THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i))) 1))
    1.19 -  i) state;
    1.20 +local
    1.21 +fun slow_step_tac' cs = Classical.appWrappers cs 
    1.22 +	(Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs);
    1.23 +in fun nodup_depth_tac cs m i state = SELECT_GOAL 
    1.24 +   (Classical.safe_steps_tac cs 1 THEN_ELSE 
    1.25 +	(DEPTH_SOLVE (nodup_depth_tac cs m 1),
    1.26 +	 Classical.inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
    1.27 +	     (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) 1))
    1.28 +        )) i state;
    1.29 +end;
    1.30  
    1.31  (*Designed to be idempotent, except if best_tac instantiates variables
    1.32    in some of the subgoals*)
    1.33  fun mk_auto_tac (cs, ss) m n =
    1.34      let val cs' = cs addss ss
    1.35          val maintac = 
    1.36 -          blast_depth_tac cs m		(* fast but can't use addss *)
    1.37 +          blast_depth_tac cs m		     (* fast but can't use wrappers *)
    1.38            ORELSE'
    1.39 -          nodup_depth_tac cs' n;	(* slower but more general *)
    1.40 +          (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
    1.41      in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
    1.42  	       TRY (Classical.safe_tac cs),
    1.43  	       REPEAT (FIRSTGOAL maintac),