# HG changeset patch
# User clasohm
# Date 812807615 -3600
# Node ID c76ac4a9dc2b1077ee47fe38d2e700804ae7591c
# Parent  6f5d2d76e19b9dee762cae00b71e0643cf2043d6
renamed SS to Simpset; fixed bug in merge_ss

diff -r 6f5d2d76e19b -r c76ac4a9dc2b src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Sep 26 11:49:55 1995 +0100
+++ b/src/Provers/simplifier.ML	Wed Oct 04 12:53:35 1995 +0100
@@ -6,6 +6,7 @@
 Generic simplifier, suitable for most logics.
  
 *)
+
 infix 4 addsimps addeqcongs delsimps
         setsolver setloop setmksimps setsubgoaler;
 
@@ -35,120 +36,123 @@
   val Asm_full_simp_tac: int -> tactic
 end;
 
-functor SimplifierFUN():SIMPLIFIER =
+functor SimplifierFun():SIMPLIFIER =
 struct
 
 datatype simpset =
-  SS of {mss: meta_simpset,
-         simps: thm list,
-         congs: thm list,
-         subgoal_tac: simpset -> int -> tactic,
-         finish_tac: thm list -> int -> tactic,
-         loop_tac: int -> tactic};
+  Simpset of {mss: meta_simpset,
+              simps: thm list,
+              congs: thm list,
+              subgoal_tac: simpset -> int -> tactic,
+              finish_tac: thm list -> int -> tactic,
+              loop_tac: int -> tactic};
 
 val empty_ss =
-  SS{mss=empty_mss,
-     simps= [],
-     congs= [],
-     subgoal_tac= K(K no_tac),
-     finish_tac= K(K no_tac),
-     loop_tac= K no_tac};
+  Simpset{mss=empty_mss,
+          simps= [],
+          congs= [],
+          subgoal_tac= K(K no_tac),
+          finish_tac= K(K no_tac),
+          loop_tac= K no_tac};
 
 val simpset = ref empty_ss;
 
-fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
-  SS{mss=mss,
-     simps= simps,
-     congs= congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac= DETERM o loop_tac};
+fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
+  Simpset{mss=mss,
+          simps= simps,
+          congs= congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac= DETERM o loop_tac};
 
-fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
-  SS{mss=mss,
-     simps= simps,
-     congs= congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac=loop_tac};
+fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
+  Simpset{mss=mss,
+          simps= simps,
+          congs= congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac=loop_tac};
 
-fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac =
-  SS{mss=mss,
-     simps= simps,
-     congs= congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac=loop_tac};
+fun (Simpset{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler
+    subgoal_tac =
+  Simpset{mss=mss,
+          simps= simps,
+          congs= congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac=loop_tac};
+     
+fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps
+    mk_simps =
+  Simpset{mss=Thm.set_mk_rews(mss,mk_simps),
+          simps= simps,
+          congs= congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac=loop_tac};
 
-fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =
-  SS{mss=Thm.set_mk_rews(mss,mk_simps),
-     simps= simps,
-     congs= congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac=loop_tac};
-
-fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
+fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
-  SS{mss= Thm.add_simps(mss,rews'),
-     simps= rews' @ simps,
-     congs= congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac=loop_tac}
+  Simpset{mss= Thm.add_simps(mss,rews'),
+          simps= rews' @ simps,
+          congs= congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac=loop_tac}
   end;
 
 fun Addsimps rews = (simpset := !simpset addsimps rews);
 
-fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
+fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
-  SS{mss= Thm.del_simps(mss,rews'),
-     simps= foldl (gen_rem eq_thm) (simps,rews'),
-     congs= congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac=loop_tac}
+  Simpset{mss= Thm.del_simps(mss,rews'),
+          simps= foldl (gen_rem eq_thm) (simps,rews'),
+          congs= congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac=loop_tac}
   end;
 
 fun Delsimps rews = (simpset := !simpset delsimps rews);
 
-fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
-  SS{mss= Thm.add_congs(mss,newcongs),
-     simps= simps,
-     congs= newcongs @ congs,
-     subgoal_tac= subgoal_tac,
-     finish_tac=finish_tac,
-     loop_tac=loop_tac};
-
-fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
-             SS{simps=simps2,congs=congs2,...}) =
+fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs
+    newcongs =
+  Simpset{mss= Thm.add_congs(mss,newcongs),
+          simps= simps,
+          congs= newcongs @ congs,
+          subgoal_tac= subgoal_tac,
+          finish_tac=finish_tac,
+          loop_tac=loop_tac};
+     
+fun merge_ss(Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
+             Simpset{simps=simps2,congs=congs2,...}) =
   let val simps' = gen_union eq_thm (simps,simps2)
       val congs' = gen_union eq_thm (congs,congs2)
       val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
       val mss' = Thm.add_simps(mss',simps')
       val mss' = Thm.add_congs(mss',congs')
-  in SS{mss=         mss',
-        simps=       simps,
-        congs=       congs',
-        subgoal_tac= subgoal_tac,
-        finish_tac=  finish_tac,
-        loop_tac=    loop_tac}
+  in Simpset{mss=         mss',
+             simps=       simps',
+             congs=       congs',
+             subgoal_tac= subgoal_tac,
+             finish_tac=  finish_tac,
+             loop_tac=    loop_tac}
   end;
 
-fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;
+fun prems_of_ss(Simpset{mss,...}) = prems_of_mss mss;
 
-fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
+fun rep_ss(Simpset{simps,congs,...}) = {simps=simps,congs=congs};
 
 fun NEWSUBGOALS tac tacf =
   STATE(fn state0 =>
     tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0)));
 
 fun gen_simp_tac mode =
-  fn (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =>
+  fn (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =>
   let fun solve_all_tac mss =
-        let val ss = SS{mss=mss,simps=simps,congs=congs,
-                        subgoal_tac=subgoal_tac,
-                        finish_tac=finish_tac, loop_tac=loop_tac}
+        let val ss = Simpset{mss=mss,simps=simps,congs=congs,
+                             subgoal_tac=subgoal_tac,
+                             finish_tac=finish_tac, loop_tac=loop_tac}
             val solve1_tac =
               NEWSUBGOALS (subgoal_tac ss 1)
                           (fn n => if n<0 then all_tac else no_tac)