src/Provers/simplifier.ML
author nipkow
Wed, 29 May 1996 12:03:32 +0200
changeset 1770 608050b43bee
parent 1676 db29ab9c1490
child 2503 7590fd5ce3c7
permissions -rw-r--r--
Added addsolver
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
     1
(*  Title:      Provers/simplifier.ML
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     2
    ID:         $Id$
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     3
    Author:     Tobias Nipkow
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     4
    Copyright   1993  TU Munich
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     5
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     6
Generic simplifier, suitable for most logics.
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     7
 
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     8
*)
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
     9
1770
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    10
infix 4 addsimps addeqcongs addsolver delsimps
983
6f80fed73e29 Precedence of infixes is now 4 (just above that of :=)
lcp
parents: 433
diff changeset
    11
        setsolver setloop setmksimps setsubgoaler;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
signature SIMPLIFIER =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  type simpset
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
    16
  val addeqcongs: simpset * thm list -> simpset
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val addsimps: simpset * thm list -> simpset
1770
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    18
  val addsolver: simpset * (thm list -> int -> tactic) -> simpset
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    19
  val delsimps: simpset * thm list -> simpset
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val asm_full_simp_tac: simpset -> int -> tactic
1676
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
    21
  val     full_simp_tac: simpset -> int -> tactic
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
    22
  val      asm_simp_tac: simpset -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val empty_ss: simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val merge_ss: simpset * simpset -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val prems_of_ss: simpset -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val rep_ss: simpset -> {simps: thm list, congs: thm list}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val setsolver: simpset * (thm list -> int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val setloop: simpset * (int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val setmksimps: simpset * (thm -> thm list) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val simp_tac: simpset -> int -> tactic
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    32
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    33
  val simpset: simpset ref
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    34
  val Addsimps: thm list -> unit
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    35
  val Delsimps: thm list -> unit
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    36
  val Simp_tac: int -> tactic
1676
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
    37
  val      Asm_simp_tac: int -> tactic
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
    38
  val     Full_simp_tac: int -> tactic
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    39
  val Asm_full_simp_tac: int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1260
diff changeset
    42
structure Simplifier :SIMPLIFIER =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
datatype simpset =
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    46
  Simpset of {mss: meta_simpset,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    47
              simps: thm list,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    48
              congs: thm list,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    49
              subgoal_tac: simpset -> int -> tactic,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    50
              finish_tac: thm list -> int -> tactic,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    51
              loop_tac: int -> tactic};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val empty_ss =
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    54
  Simpset{mss=empty_mss,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    55
          simps= [],
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    56
          congs= [],
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    57
          subgoal_tac= K(K no_tac),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    58
          finish_tac= K(K no_tac),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    59
          loop_tac= K no_tac};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
    61
val simpset = ref empty_ss;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    63
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    64
  Simpset{mss=mss,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    65
          simps= simps,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    66
          congs= congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    67
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    68
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    69
          loop_tac= DETERM o loop_tac};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    71
fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    72
  Simpset{mss=mss,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    73
          simps= simps,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    74
          congs= congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    75
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    76
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    77
          loop_tac=loop_tac};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
1770
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    79
fun (Simpset{mss,simps,congs,subgoal_tac,loop_tac,finish_tac}) addsolver tac =
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    80
  Simpset{mss=mss,
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    81
          simps= simps,
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    82
          congs= congs,
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    83
          subgoal_tac= subgoal_tac,
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    84
          finish_tac=fn hyps => finish_tac hyps ORELSE' tac hyps,
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    85
          loop_tac=loop_tac};
608050b43bee Added addsolver
nipkow
parents: 1676
diff changeset
    86
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    87
fun (Simpset{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    88
    subgoal_tac =
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    89
  Simpset{mss=mss,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    90
          simps= simps,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    91
          congs= congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    92
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    93
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    94
          loop_tac=loop_tac};
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    95
     
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    96
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    97
    mk_simps =
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    98
  Simpset{mss=Thm.set_mk_rews(mss,mk_simps),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
    99
          simps= simps,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   100
          congs= congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   101
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   102
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   103
          loop_tac=loop_tac};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   105
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   106
  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   107
  Simpset{mss= Thm.add_simps(mss,rews'),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   108
          simps= rews' @ simps,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   109
          congs= congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   110
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   111
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   112
          loop_tac=loop_tac}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
   115
fun Addsimps rews = (simpset := !simpset addsimps rews);
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
   116
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   117
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   118
  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   119
  Simpset{mss= Thm.del_simps(mss,rews'),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   120
          simps= foldl (gen_rem eq_thm) (simps,rews'),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   121
          congs= congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   122
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   123
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   124
          loop_tac=loop_tac}
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   125
  end;
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   126
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
   127
fun Delsimps rews = (simpset := !simpset delsimps rews);
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
   128
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   129
fun (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   130
    newcongs =
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   131
  Simpset{mss= Thm.add_congs(mss,newcongs),
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   132
          simps= simps,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   133
          congs= newcongs @ congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   134
          subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   135
          finish_tac=finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   136
          loop_tac=loop_tac};
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   137
     
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   138
fun merge_ss(Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   139
             Simpset{simps=simps2,congs=congs2,...}) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
  let val simps' = gen_union eq_thm (simps,simps2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
      val congs' = gen_union eq_thm (congs,congs2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
      val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
      val mss' = Thm.add_simps(mss',simps')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
      val mss' = Thm.add_congs(mss',congs')
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   145
  in Simpset{mss=         mss',
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   146
             simps=       simps',
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   147
             congs=       congs',
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   148
             subgoal_tac= subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   149
             finish_tac=  finish_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   150
             loop_tac=    loop_tac}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   153
fun prems_of_ss(Simpset{mss,...}) = prems_of_mss mss;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   155
fun rep_ss(Simpset{simps,congs,...}) = {simps=simps,congs=congs};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   157
fun NEWSUBGOALS tac tacf =
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   158
  STATE(fn state0 =>
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   159
    tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0)));
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   160
217
c972c57e7762 got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents: 146
diff changeset
   161
fun gen_simp_tac mode =
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   162
  fn (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
  let fun solve_all_tac mss =
1260
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   164
        let val ss = Simpset{mss=mss,simps=simps,congs=congs,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   165
                             subgoal_tac=subgoal_tac,
c76ac4a9dc2b renamed SS to Simpset; fixed bug in merge_ss
clasohm
parents: 1243
diff changeset
   166
                             finish_tac=finish_tac, loop_tac=loop_tac}
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   167
            val solve1_tac =
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   168
              NEWSUBGOALS (subgoal_tac ss 1)
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   169
                          (fn n => if n<0 then all_tac else no_tac)
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   170
        in DEPTH_SOLVE(solve1_tac) end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
1512
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1260
diff changeset
   172
      fun simp_loop_tac i thm =
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1260
diff changeset
   173
	  (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
ce37c64244c0 Elimination of fully-functorial style.
paulson
parents: 1260
diff changeset
   174
	   (finish_tac (prems_of_mss mss) i  ORELSE  looper i))  thm
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   175
      and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   176
      and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
217
c972c57e7762 got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents: 146
diff changeset
   177
  in simp_loop_tac end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
1676
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   179
val asm_full_simp_tac = gen_simp_tac (true ,true );
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   180
val     full_simp_tac = gen_simp_tac (true ,false);
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   181
val      asm_simp_tac = gen_simp_tac (false,true );
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   182
val          simp_tac = gen_simp_tac (false,false);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
   184
fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i;
1676
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   185
fun     Full_simp_tac i =     full_simp_tac (!simpset) i;
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   186
fun      Asm_simp_tac i =      asm_simp_tac (!simpset) i;
db29ab9c1490 *** empty log message ***
oheimb
parents: 1512
diff changeset
   187
fun          Simp_tac i =          simp_tac (!simpset) i;
406
4d4e0442b106 simpset is hidden in a functor now.
nipkow
parents: 217
diff changeset
   188
1243
fa09705a5890 added global simpset
clasohm
parents: 983
diff changeset
   189
end;