1.1 --- a/src/Provers/simp.ML	Thu Sep 16 12:20:38 1993 +0200
     1.2 +++ b/src/Provers/simp.ML	Thu Sep 16 14:21:44 1993 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Provers/simp
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow
     1.7      Copyright   1993  University of Cambridge
     1.8  

     2.1 --- a/src/Provers/simplifier.ML	Thu Sep 16 12:20:38 1993 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Thu Sep 16 14:21:44 1993 +0200
     2.3 @@ -1,10 +1,18 @@
     2.4 -infix addsimps addcongs
     2.5 +(*  Title:      Provers/simplifier
     2.6 +    ID:         $Id$
     2.7 +    Author:     Tobias Nipkow
     2.8 +    Copyright   1993  TU Munich
     2.9 +
    2.10 +Generic simplifier, suitable for most logics.
    2.11 + 
    2.12 +*)
    2.13 +infix addsimps addeqcongs
    2.14        setsolver setloop setmksimps setsubgoaler;
    2.15  
    2.16  signature SIMPLIFIER =
    2.17  sig
    2.18    type simpset
    2.19 -  val addcongs: simpset * thm list -> simpset
    2.20 +  val addeqcongs: simpset * thm list -> simpset
    2.21    val addsimps: simpset * thm list -> simpset
    2.22    val asm_full_simp_tac: simpset -> int -> tactic
    2.23    val asm_simp_tac: simpset -> int -> tactic
    2.24 @@ -82,7 +90,7 @@
    2.25       loop_tac=loop_tac}
    2.26    end;
    2.27  
    2.28 -fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =
    2.29 +fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
    2.30    SS{mss= Thm.add_congs(mss,newcongs),
    2.31       simps= simps,
    2.32       congs= newcongs @ congs,
    2.33 @@ -116,29 +124,26 @@
    2.34          loop_tac=loop_tac}
    2.35    end;
    2.36  
    2.37 +fun NEWSUBGOALS tac tacf =
    2.38 +  STATE(fn state0 =>
    2.39 +    tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0)));
    2.40 +
    2.41  fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
    2.42    let fun solve_all_tac mss =
    2.43          let val ss = SS{mss=mss,simps=simps,congs=congs,
    2.44                          subgoal_tac=subgoal_tac,
    2.45                          finish_tac=finish_tac, loop_tac=loop_tac}
    2.46 -            fun solve1 thm = tapply(
    2.47 -                  STATE(fn state => let val n = nprems_of state
    2.48 -                    in if n=0 then all_tac
    2.49 -                       else subgoal_tac ss 1 THEN
    2.50 -                            COND (has_fewer_prems n) (Tactic solve1) no_tac
    2.51 -                    end),
    2.52 -                  thm)
    2.53 -        in DEPTH_SOLVE(Tactic solve1) end
    2.54 +            val solve1_tac =
    2.55 +              NEWSUBGOALS (subgoal_tac ss 1)
    2.56 +                          (fn n => if n<0 then all_tac else no_tac)
    2.57 +        in DEPTH_SOLVE(solve1_tac) end
    2.58  
    2.59        fun simp_loop i thm =
    2.60          tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
    2.61 -               (finish_tac (prems_of_mss mss) i  ORELSE  STATE(looper i)),
    2.62 +               (finish_tac (prems_of_mss mss) i  ORELSE  looper i),
    2.63                 thm)
    2.64 -      and allsimp i m state =
    2.65 -        let val n = nprems_of state
    2.66 -        in EVERY(map (fn j => simp_loop_tac (i+j)) ((n-m) downto 0)) end
    2.67 -      and looper i state =
    2.68 -        TRY(loop_tac i THEN STATE(allsimp i (nprems_of state)))
    2.69 +      and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
    2.70 +      and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
    2.71        and simp_loop_tac i = Tactic(simp_loop i)
    2.72  
    2.73    in simp_loop_tac end;