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