src/Provers/simplifier.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16 ago)
changeset 0 a5a9c433f639
child 1 c6a6e3db5353
permissions -rw-r--r--
Initial revision
clasohm@0
     1
infix addsimps addcongs
clasohm@0
     2
      setsolver setloop setmksimps setsubgoaler;
clasohm@0
     3
clasohm@0
     4
signature SIMPLIFIER =
clasohm@0
     5
sig
clasohm@0
     6
  type simpset
clasohm@0
     7
  val addcongs: simpset * thm list -> simpset
clasohm@0
     8
  val addsimps: simpset * thm list -> simpset
clasohm@0
     9
  val asm_full_simp_tac: simpset -> int -> tactic
clasohm@0
    10
  val asm_simp_tac: simpset -> int -> tactic
clasohm@0
    11
  val empty_ss: simpset
clasohm@0
    12
  val merge_ss: simpset * simpset -> simpset
clasohm@0
    13
  val prems_of_ss: simpset -> thm list
clasohm@0
    14
  val rep_ss: simpset -> {simps: thm list, congs: thm list}
clasohm@0
    15
  val setsolver: simpset * (thm list -> int -> tactic) -> simpset
clasohm@0
    16
  val setloop: simpset * (int -> tactic) -> simpset
clasohm@0
    17
  val setmksimps: simpset * (thm -> thm list) -> simpset
clasohm@0
    18
  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
clasohm@0
    19
  val simp_tac: simpset -> int -> tactic
clasohm@0
    20
end;
clasohm@0
    21
clasohm@0
    22
structure Simplifier:SIMPLIFIER =
clasohm@0
    23
struct
clasohm@0
    24
clasohm@0
    25
datatype simpset =
clasohm@0
    26
  SS of {mss: meta_simpset,
clasohm@0
    27
         simps: thm list,
clasohm@0
    28
         congs: thm list,
clasohm@0
    29
         subgoal_tac: simpset -> int -> tactic,
clasohm@0
    30
         finish_tac: thm list -> int -> tactic,
clasohm@0
    31
         loop_tac: int -> tactic};
clasohm@0
    32
clasohm@0
    33
val empty_ss =
clasohm@0
    34
  SS{mss=empty_mss,
clasohm@0
    35
     simps= [],
clasohm@0
    36
     congs= [],
clasohm@0
    37
     subgoal_tac= K(K no_tac),
clasohm@0
    38
     finish_tac= K(K no_tac),
clasohm@0
    39
     loop_tac= K no_tac};
clasohm@0
    40
clasohm@0
    41
clasohm@0
    42
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
clasohm@0
    43
  SS{mss=mss,
clasohm@0
    44
     simps= simps,
clasohm@0
    45
     congs= congs,
clasohm@0
    46
     subgoal_tac= subgoal_tac,
clasohm@0
    47
     finish_tac=finish_tac,
clasohm@0
    48
     loop_tac=loop_tac};
clasohm@0
    49
clasohm@0
    50
fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
clasohm@0
    51
  SS{mss=mss,
clasohm@0
    52
     simps= simps,
clasohm@0
    53
     congs= congs,
clasohm@0
    54
     subgoal_tac= subgoal_tac,
clasohm@0
    55
     finish_tac=finish_tac,
clasohm@0
    56
     loop_tac=loop_tac};
clasohm@0
    57
clasohm@0
    58
fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac =
clasohm@0
    59
  SS{mss=mss,
clasohm@0
    60
     simps= simps,
clasohm@0
    61
     congs= congs,
clasohm@0
    62
     subgoal_tac= subgoal_tac,
clasohm@0
    63
     finish_tac=finish_tac,
clasohm@0
    64
     loop_tac=loop_tac};
clasohm@0
    65
clasohm@0
    66
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =
clasohm@0
    67
  SS{mss=Thm.set_mk_rews(mss,mk_simps),
clasohm@0
    68
     simps= simps,
clasohm@0
    69
     congs= congs,
clasohm@0
    70
     subgoal_tac= subgoal_tac,
clasohm@0
    71
     finish_tac=finish_tac,
clasohm@0
    72
     loop_tac=loop_tac};
clasohm@0
    73
clasohm@0
    74
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
clasohm@0
    75
  let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)
clasohm@0
    76
  in
clasohm@0
    77
  SS{mss= Thm.add_simps(mss,rews'),
clasohm@0
    78
     simps= rews' @ simps,
clasohm@0
    79
     congs= congs,
clasohm@0
    80
     subgoal_tac= subgoal_tac,
clasohm@0
    81
     finish_tac=finish_tac,
clasohm@0
    82
     loop_tac=loop_tac}
clasohm@0
    83
  end;
clasohm@0
    84
clasohm@0
    85
fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =
clasohm@0
    86
  SS{mss= Thm.add_congs(mss,newcongs),
clasohm@0
    87
     simps= simps,
clasohm@0
    88
     congs= newcongs @ congs,
clasohm@0
    89
     subgoal_tac= subgoal_tac,
clasohm@0
    90
     finish_tac=finish_tac,
clasohm@0
    91
     loop_tac=loop_tac};
clasohm@0
    92
clasohm@0
    93
fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
clasohm@0
    94
             SS{simps=simps2,congs=congs2,...}) =
clasohm@0
    95
  let val simps' = gen_union eq_thm (simps,simps2)
clasohm@0
    96
      val congs' = gen_union eq_thm (congs,congs2)
clasohm@0
    97
      val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
clasohm@0
    98
      val mss' = Thm.add_simps(mss',simps')
clasohm@0
    99
      val mss' = Thm.add_congs(mss',congs')
clasohm@0
   100
  in SS{mss=         mss',
clasohm@0
   101
        simps=       simps,
clasohm@0
   102
        congs=       congs',
clasohm@0
   103
        subgoal_tac= subgoal_tac,
clasohm@0
   104
        finish_tac=  finish_tac,
clasohm@0
   105
        loop_tac=    loop_tac}
clasohm@0
   106
  end;
clasohm@0
   107
clasohm@0
   108
fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;
clasohm@0
   109
clasohm@0
   110
fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
clasohm@0
   111
clasohm@0
   112
fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =
clasohm@0
   113
  let val rews = flat(map (mk_rews_of_mss mss) prems)
clasohm@0
   114
  in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
clasohm@0
   115
        subgoal_tac=subgoal_tac,finish_tac=finish_tac,
clasohm@0
   116
        loop_tac=loop_tac}
clasohm@0
   117
  end;
clasohm@0
   118
clasohm@0
   119
fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
clasohm@0
   120
  let fun solve_all_tac mss =
clasohm@0
   121
        let val ss = SS{mss=mss,simps=simps,congs=congs,
clasohm@0
   122
                        subgoal_tac=subgoal_tac,
clasohm@0
   123
                        finish_tac=finish_tac, loop_tac=loop_tac}
clasohm@0
   124
            fun solve1 thm = tapply(
clasohm@0
   125
                  STATE(fn state => let val n = nprems_of state
clasohm@0
   126
                    in if n=0 then all_tac
clasohm@0
   127
                       else subgoal_tac ss 1 THEN
clasohm@0
   128
                            COND (has_fewer_prems n) (Tactic solve1) no_tac
clasohm@0
   129
                    end),
clasohm@0
   130
                  thm)
clasohm@0
   131
        in DEPTH_SOLVE(Tactic solve1) end
clasohm@0
   132
clasohm@0
   133
      fun simp_loop i thm =
clasohm@0
   134
        tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
clasohm@0
   135
               (finish_tac (prems_of_mss mss) i  ORELSE  STATE(looper i)),
clasohm@0
   136
               thm)
clasohm@0
   137
      and allsimp i m state =
clasohm@0
   138
        let val n = nprems_of state
clasohm@0
   139
        in EVERY(map (fn j => simp_loop_tac (i+j)) ((n-m) downto 0)) end
clasohm@0
   140
      and looper i state =
clasohm@0
   141
        TRY(loop_tac i THEN STATE(allsimp i (nprems_of state)))
clasohm@0
   142
      and simp_loop_tac i = Tactic(simp_loop i)
clasohm@0
   143
clasohm@0
   144
  in simp_loop_tac end;
clasohm@0
   145
clasohm@0
   146
fun asm_simp_tac ss =
clasohm@0
   147
      METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
clasohm@0
   148
clasohm@0
   149
fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
clasohm@0
   150
clasohm@0
   151
end;