src/Provers/simplifier.ML
author paulson
Fri Feb 16 18:00:47 1996 +0100 (1996-02-16)
changeset 1512 ce37c64244c0
parent 1260 c76ac4a9dc2b
child 1676 db29ab9c1490
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 (*  Title:      Provers/simplifier.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1993  TU Munich
     5 
     6 Generic simplifier, suitable for most logics.
     7  
     8 *)
     9 
    10 infix 4 addsimps addeqcongs delsimps
    11         setsolver setloop setmksimps setsubgoaler;
    12 
    13 signature SIMPLIFIER =
    14 sig
    15   type simpset
    16   val addeqcongs: simpset * thm list -> simpset
    17   val addsimps: simpset * thm list -> simpset
    18   val delsimps: simpset * thm list -> simpset
    19   val asm_full_simp_tac: simpset -> int -> tactic
    20   val asm_simp_tac: simpset -> int -> tactic
    21   val empty_ss: simpset
    22   val merge_ss: simpset * simpset -> simpset
    23   val prems_of_ss: simpset -> thm list
    24   val rep_ss: simpset -> {simps: thm list, congs: thm list}
    25   val setsolver: simpset * (thm list -> int -> tactic) -> simpset
    26   val setloop: simpset * (int -> tactic) -> simpset
    27   val setmksimps: simpset * (thm -> thm list) -> simpset
    28   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
    29   val simp_tac: simpset -> int -> tactic
    30 
    31   val simpset: simpset ref
    32   val Addsimps: thm list -> unit
    33   val Delsimps: thm list -> unit
    34   val Simp_tac: int -> tactic
    35   val Asm_simp_tac: int -> tactic
    36   val Asm_full_simp_tac: int -> tactic
    37 end;
    38 
    39 structure Simplifier :SIMPLIFIER =
    40 struct
    41 
    42 datatype simpset =
    43   Simpset of {mss: meta_simpset,
    44               simps: thm list,
    45               congs: thm list,
    46               subgoal_tac: simpset -> int -> tactic,
    47               finish_tac: thm list -> int -> tactic,
    48               loop_tac: int -> tactic};
    49 
    50 val empty_ss =
    51   Simpset{mss=empty_mss,
    52           simps= [],
    53           congs= [],
    54           subgoal_tac= K(K no_tac),
    55           finish_tac= K(K no_tac),
    56           loop_tac= K no_tac};
    57 
    58 val simpset = ref empty_ss;
    59 
    60 fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
    61   Simpset{mss=mss,
    62           simps= simps,
    63           congs= congs,
    64           subgoal_tac= subgoal_tac,
    65           finish_tac=finish_tac,
    66           loop_tac= DETERM o loop_tac};
    67 
    68 fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
    69   Simpset{mss=mss,
    70           simps= simps,
    71           congs= congs,
    72           subgoal_tac= subgoal_tac,
    73           finish_tac=finish_tac,
    74           loop_tac=loop_tac};
    75 
    76 fun (Simpset{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler
    77     subgoal_tac =
    78   Simpset{mss=mss,
    79           simps= simps,
    80           congs= congs,
    81           subgoal_tac= subgoal_tac,
    82           finish_tac=finish_tac,
    83           loop_tac=loop_tac};
    84      
    85 fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps
    86     mk_simps =
    87   Simpset{mss=Thm.set_mk_rews(mss,mk_simps),
    88           simps= simps,
    89           congs= congs,
    90           subgoal_tac= subgoal_tac,
    91           finish_tac=finish_tac,
    92           loop_tac=loop_tac};
    93 
    94 fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
    95   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
    96   Simpset{mss= Thm.add_simps(mss,rews'),
    97           simps= rews' @ simps,
    98           congs= congs,
    99           subgoal_tac= subgoal_tac,
   100           finish_tac=finish_tac,
   101           loop_tac=loop_tac}
   102   end;
   103 
   104 fun Addsimps rews = (simpset := !simpset addsimps rews);
   105 
   106 fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
   107   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
   108   Simpset{mss= Thm.del_simps(mss,rews'),
   109           simps= foldl (gen_rem eq_thm) (simps,rews'),
   110           congs= congs,
   111           subgoal_tac= subgoal_tac,
   112           finish_tac=finish_tac,
   113           loop_tac=loop_tac}
   114   end;
   115 
   116 fun Delsimps rews = (simpset := !simpset delsimps rews);
   117 
   118 fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs
   119     newcongs =
   120   Simpset{mss= Thm.add_congs(mss,newcongs),
   121           simps= simps,
   122           congs= newcongs @ congs,
   123           subgoal_tac= subgoal_tac,
   124           finish_tac=finish_tac,
   125           loop_tac=loop_tac};
   126      
   127 fun merge_ss(Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
   128              Simpset{simps=simps2,congs=congs2,...}) =
   129   let val simps' = gen_union eq_thm (simps,simps2)
   130       val congs' = gen_union eq_thm (congs,congs2)
   131       val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
   132       val mss' = Thm.add_simps(mss',simps')
   133       val mss' = Thm.add_congs(mss',congs')
   134   in Simpset{mss=         mss',
   135              simps=       simps',
   136              congs=       congs',
   137              subgoal_tac= subgoal_tac,
   138              finish_tac=  finish_tac,
   139              loop_tac=    loop_tac}
   140   end;
   141 
   142 fun prems_of_ss(Simpset{mss,...}) = prems_of_mss mss;
   143 
   144 fun rep_ss(Simpset{simps,congs,...}) = {simps=simps,congs=congs};
   145 
   146 fun NEWSUBGOALS tac tacf =
   147   STATE(fn state0 =>
   148     tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0)));
   149 
   150 fun gen_simp_tac mode =
   151   fn (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =>
   152   let fun solve_all_tac mss =
   153         let val ss = Simpset{mss=mss,simps=simps,congs=congs,
   154                              subgoal_tac=subgoal_tac,
   155                              finish_tac=finish_tac, loop_tac=loop_tac}
   156             val solve1_tac =
   157               NEWSUBGOALS (subgoal_tac ss 1)
   158                           (fn n => if n<0 then all_tac else no_tac)
   159         in DEPTH_SOLVE(solve1_tac) end
   160 
   161       fun simp_loop_tac i thm =
   162 	  (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
   163 	   (finish_tac (prems_of_mss mss) i  ORELSE  looper i))  thm
   164       and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
   165       and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
   166   in simp_loop_tac end;
   167 
   168 val asm_full_simp_tac = gen_simp_tac (true,true);
   169 val asm_simp_tac = gen_simp_tac (false,true);
   170 val simp_tac = gen_simp_tac (false,false);
   171 
   172 fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i;
   173 fun Asm_simp_tac i = asm_simp_tac (!simpset) i;
   174 fun Simp_tac i = simp_tac (!simpset) i;
   175 
   176 end;