src/Provers/simplifier.ML
changeset 1243 fa09705a5890
parent 983 6f80fed73e29
child 1260 c76ac4a9dc2b
equal deleted inserted replaced
1242:b3f68a644380 1243:fa09705a5890
     1 (*  Title:      Provers/simplifier
     1 (*  Title:      Provers/simplifier.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1993  TU Munich
     4     Copyright   1993  TU Munich
     5 
     5 
     6 Generic simplifier, suitable for most logics.
     6 Generic simplifier, suitable for most logics.
    24   val setsolver: simpset * (thm list -> int -> tactic) -> simpset
    24   val setsolver: simpset * (thm list -> int -> tactic) -> simpset
    25   val setloop: simpset * (int -> tactic) -> simpset
    25   val setloop: simpset * (int -> tactic) -> simpset
    26   val setmksimps: simpset * (thm -> thm list) -> simpset
    26   val setmksimps: simpset * (thm -> thm list) -> simpset
    27   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
    27   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
    28   val simp_tac: simpset -> int -> tactic
    28   val simp_tac: simpset -> int -> tactic
       
    29 
       
    30   val simpset: simpset ref
       
    31   val Addsimps: thm list -> unit
       
    32   val Delsimps: thm list -> unit
       
    33   val Simp_tac: int -> tactic
       
    34   val Asm_simp_tac: int -> tactic
       
    35   val Asm_full_simp_tac: int -> tactic
    29 end;
    36 end;
    30 
    37 
    31 functor SimplifierFUN():SIMPLIFIER =
    38 functor SimplifierFUN():SIMPLIFIER =
    32 struct
    39 struct
    33 
    40 
    45      congs= [],
    52      congs= [],
    46      subgoal_tac= K(K no_tac),
    53      subgoal_tac= K(K no_tac),
    47      finish_tac= K(K no_tac),
    54      finish_tac= K(K no_tac),
    48      loop_tac= K no_tac};
    55      loop_tac= K no_tac};
    49 
    56 
       
    57 val simpset = ref empty_ss;
    50 
    58 
    51 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
    59 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
    52   SS{mss=mss,
    60   SS{mss=mss,
    53      simps= simps,
    61      simps= simps,
    54      congs= congs,
    62      congs= congs,
    88      subgoal_tac= subgoal_tac,
    96      subgoal_tac= subgoal_tac,
    89      finish_tac=finish_tac,
    97      finish_tac=finish_tac,
    90      loop_tac=loop_tac}
    98      loop_tac=loop_tac}
    91   end;
    99   end;
    92 
   100 
       
   101 fun Addsimps rews = (simpset := !simpset addsimps rews);
       
   102 
    93 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
   103 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
    94   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
   104   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
    95   SS{mss= Thm.del_simps(mss,rews'),
   105   SS{mss= Thm.del_simps(mss,rews'),
    96      simps= foldl (gen_rem eq_thm) (simps,rews'),
   106      simps= foldl (gen_rem eq_thm) (simps,rews'),
    97      congs= congs,
   107      congs= congs,
    98      subgoal_tac= subgoal_tac,
   108      subgoal_tac= subgoal_tac,
    99      finish_tac=finish_tac,
   109      finish_tac=finish_tac,
   100      loop_tac=loop_tac}
   110      loop_tac=loop_tac}
   101   end;
   111   end;
       
   112 
       
   113 fun Delsimps rews = (simpset := !simpset delsimps rews);
   102 
   114 
   103 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
   115 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
   104   SS{mss= Thm.add_congs(mss,newcongs),
   116   SS{mss= Thm.add_congs(mss,newcongs),
   105      simps= simps,
   117      simps= simps,
   106      congs= newcongs @ congs,
   118      congs= newcongs @ congs,
   154 
   166 
   155 val asm_full_simp_tac = gen_simp_tac (true,true);
   167 val asm_full_simp_tac = gen_simp_tac (true,true);
   156 val asm_simp_tac = gen_simp_tac (false,true);
   168 val asm_simp_tac = gen_simp_tac (false,true);
   157 val simp_tac = gen_simp_tac (false,false);
   169 val simp_tac = gen_simp_tac (false,false);
   158 
   170 
       
   171 fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i;
       
   172 fun Asm_simp_tac i = asm_simp_tac (!simpset) i;
       
   173 fun Simp_tac i = simp_tac (!simpset) i;
       
   174 
   159 end;
   175 end;
   160 
       
   161 structure Simplifier = SimplifierFUN();