src/Provers/simplifier.ML
changeset 1243 fa09705a5890
parent 983 6f80fed73e29
child 1260 c76ac4a9dc2b
     1.1 --- a/src/Provers/simplifier.ML	Fri Sep 01 13:28:54 1995 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Fri Sep 01 13:32:13 1995 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Provers/simplifier
     1.5 +(*  Title:      Provers/simplifier.ML
     1.6      ID:         $Id$
     1.7      Author:     Tobias Nipkow
     1.8      Copyright   1993  TU Munich
     1.9 @@ -26,6 +26,13 @@
    1.10    val setmksimps: simpset * (thm -> thm list) -> simpset
    1.11    val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
    1.12    val simp_tac: simpset -> int -> tactic
    1.13 +
    1.14 +  val simpset: simpset ref
    1.15 +  val Addsimps: thm list -> unit
    1.16 +  val Delsimps: thm list -> unit
    1.17 +  val Simp_tac: int -> tactic
    1.18 +  val Asm_simp_tac: int -> tactic
    1.19 +  val Asm_full_simp_tac: int -> tactic
    1.20  end;
    1.21  
    1.22  functor SimplifierFUN():SIMPLIFIER =
    1.23 @@ -47,6 +54,7 @@
    1.24       finish_tac= K(K no_tac),
    1.25       loop_tac= K no_tac};
    1.26  
    1.27 +val simpset = ref empty_ss;
    1.28  
    1.29  fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
    1.30    SS{mss=mss,
    1.31 @@ -90,6 +98,8 @@
    1.32       loop_tac=loop_tac}
    1.33    end;
    1.34  
    1.35 +fun Addsimps rews = (simpset := !simpset addsimps rews);
    1.36 +
    1.37  fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
    1.38    let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
    1.39    SS{mss= Thm.del_simps(mss,rews'),
    1.40 @@ -100,6 +110,8 @@
    1.41       loop_tac=loop_tac}
    1.42    end;
    1.43  
    1.44 +fun Delsimps rews = (simpset := !simpset delsimps rews);
    1.45 +
    1.46  fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
    1.47    SS{mss= Thm.add_congs(mss,newcongs),
    1.48       simps= simps,
    1.49 @@ -156,6 +168,8 @@
    1.50  val asm_simp_tac = gen_simp_tac (false,true);
    1.51  val simp_tac = gen_simp_tac (false,false);
    1.52  
    1.53 -end;
    1.54 +fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i;
    1.55 +fun Asm_simp_tac i = asm_simp_tac (!simpset) i;
    1.56 +fun Simp_tac i = simp_tac (!simpset) i;
    1.57  
    1.58 -structure Simplifier = SimplifierFUN();
    1.59 +end;