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