src/Provers/simplifier.ML
author nipkow
Thu, 25 Nov 1993 13:41:08 +0100
changeset 146 dbee71d43339
parent 88 9df4dfedee01
child 217 c972c57e7762
permissions -rw-r--r--
asm_full_simp_tac now fails if there are no subgoals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
     1
(*  Title:      Provers/simplifier
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
*)
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
     9
infix addsimps addeqcongs delsimps
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
      setsolver setloop setmksimps setsubgoaler;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
signature SIMPLIFIER =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  type simpset
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
    15
  val addeqcongs: simpset * thm list -> simpset
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val addsimps: simpset * thm list -> simpset
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    17
  val delsimps: simpset * thm list -> simpset
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val asm_full_simp_tac: simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  val asm_simp_tac: simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val empty_ss: simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val merge_ss: simpset * simpset -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val prems_of_ss: simpset -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  val rep_ss: simpset -> {simps: thm list, congs: thm list}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val setsolver: simpset * (thm list -> int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val setloop: simpset * (int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  val setmksimps: simpset * (thm -> thm list) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val simp_tac: simpset -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
structure Simplifier:SIMPLIFIER =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
datatype simpset =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  SS of {mss: meta_simpset,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
         simps: thm list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
         congs: thm list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
         subgoal_tac: simpset -> int -> tactic,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
         finish_tac: thm list -> int -> tactic,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
         loop_tac: int -> tactic};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val empty_ss =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  SS{mss=empty_mss,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
     simps= [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
     congs= [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
     subgoal_tac= K(K no_tac),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
     finish_tac= K(K no_tac),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
     loop_tac= K no_tac};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  SS{mss=mss,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
     simps= simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
     congs= congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
     subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
     finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
     loop_tac=loop_tac};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  SS{mss=mss,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
     simps= simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
     congs= congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
     subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
     finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
     loop_tac=loop_tac};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  SS{mss=mss,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
     simps= simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
     congs= congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
     subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
     finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
     loop_tac=loop_tac};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  SS{mss=Thm.set_mk_rews(mss,mk_simps),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
     simps= simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
     congs= congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
     subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
     finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
     loop_tac=loop_tac};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    84
  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  SS{mss= Thm.add_simps(mss,rews'),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
     simps= rews' @ simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
     congs= congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
     subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
     finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
     loop_tac=loop_tac}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
88
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    93
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    94
  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    95
  SS{mss= Thm.del_simps(mss,rews'),
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    96
     simps= foldl (gen_rem eq_thm) (simps,rews'),
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    97
     congs= congs,
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    98
     subgoal_tac= subgoal_tac,
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
    99
     finish_tac=finish_tac,
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   100
     loop_tac=loop_tac}
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   101
  end;
9df4dfedee01 added infix delsimps
nipkow
parents: 17
diff changeset
   102
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   103
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
  SS{mss= Thm.add_congs(mss,newcongs),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
     simps= simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
     congs= newcongs @ congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
     subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
     finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
     loop_tac=loop_tac};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
             SS{simps=simps2,congs=congs2,...}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  let val simps' = gen_union eq_thm (simps,simps2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
      val congs' = gen_union eq_thm (congs,congs2)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
      val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
      val mss' = Thm.add_simps(mss',simps')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
      val mss' = Thm.add_congs(mss',congs')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
  in SS{mss=         mss',
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
        simps=       simps,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
        congs=       congs',
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
        subgoal_tac= subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
        finish_tac=  finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
        loop_tac=    loop_tac}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
  let val rews = flat(map (mk_rews_of_mss mss) prems)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
  in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
        subgoal_tac=subgoal_tac,finish_tac=finish_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
        loop_tac=loop_tac}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   137
fun NEWSUBGOALS tac tacf =
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   138
  STATE(fn state0 =>
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   139
    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
   140
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
  let fun solve_all_tac mss =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
        let val ss = SS{mss=mss,simps=simps,congs=congs,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
                        subgoal_tac=subgoal_tac,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
                        finish_tac=finish_tac, loop_tac=loop_tac}
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   146
            val solve1_tac =
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   147
              NEWSUBGOALS (subgoal_tac ss 1)
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   148
                          (fn n => if n<0 then all_tac else no_tac)
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   149
        in DEPTH_SOLVE(solve1_tac) end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
      fun simp_loop i thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
        tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   153
               (finish_tac (prems_of_mss mss) i  ORELSE  looper i),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
               thm)
1
c6a6e3db5353 changed addcongs to addeqcongs in simplifier.ML
nipkow
parents: 0
diff changeset
   155
      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
   156
      and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
      and simp_loop_tac i = Tactic(simp_loop i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
146
dbee71d43339 asm_full_simp_tac now fails if there are no subgoals
nipkow
parents: 88
diff changeset
   159
  in fn i => COND (has_fewer_prems 1) no_tac (simp_loop_tac i) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
fun asm_simp_tac ss =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
      METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
end;