src/Provers/simplifier.ML
author wenzelm
Fri Jul 25 13:18:09 1997 +0200 (1997-07-25)
changeset 3577 9715b6e3ec5f
parent 3557 9546f8185c43
child 3728 f92594f65af6
permissions -rw-r--r--
added prems argument to simplification procedures;
     1 (*  Title:      Provers/simplifier.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Generic simplifier, suitable for most logics.  See also Pure/thm.ML
     6 for the actual meta level rewriting engine.
     7 *)
     8 
     9 infix 4
    10   setsubgoaler setloop addloop setSSolver addSSolver setSolver
    11   addSolver setmksimps addsimps delsimps addeqcongs deleqcongs
    12   settermless addsimprocs delsimprocs;
    13 
    14 
    15 signature SIMPLIFIER =
    16 sig
    17   type simproc
    18   val mk_simproc: string -> cterm list
    19     -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    20   val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
    21     -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm
    22   type simpset
    23   val empty_ss: simpset
    24   val rep_ss: simpset ->
    25    {mss: meta_simpset,
    26     subgoal_tac:        simpset -> int -> tactic,
    27     loop_tac:                      int -> tactic,
    28            finish_tac: thm list -> int -> tactic,
    29     unsafe_finish_tac: thm list -> int -> tactic};
    30   val print_ss: simpset -> unit
    31   val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    32   val setloop:      simpset *             (int -> tactic) -> simpset
    33   val addloop:      simpset *             (int -> tactic) -> simpset
    34   val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    35   val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    36   val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
    37   val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
    38   val setmksimps:   simpset * (thm -> thm list) -> simpset
    39   val settermless:  simpset * (term * term -> bool) -> simpset
    40   val addsimps:     simpset * thm list -> simpset
    41   val delsimps:     simpset * thm list -> simpset
    42   val addeqcongs:   simpset * thm list -> simpset
    43   val deleqcongs:   simpset * thm list -> simpset
    44   val addsimprocs:  simpset * simproc list -> simpset
    45   val delsimprocs:  simpset * simproc list -> simpset
    46   val merge_ss:     simpset * simpset -> simpset
    47   val prems_of_ss:  simpset -> thm list
    48   val simpset:      simpset ref
    49   val Addsimps: thm list -> unit
    50   val Delsimps: thm list -> unit
    51   val Addsimprocs: simproc list -> unit
    52   val Delsimprocs: simproc list -> unit
    53   val               simp_tac: simpset -> int -> tactic
    54   val           asm_simp_tac: simpset -> int -> tactic
    55   val          full_simp_tac: simpset -> int -> tactic
    56   val      asm_full_simp_tac: simpset -> int -> tactic
    57   val safe_asm_full_simp_tac: simpset -> int -> tactic
    58   val               Simp_tac:            int -> tactic
    59   val           Asm_simp_tac:            int -> tactic
    60   val          Full_simp_tac:            int -> tactic
    61   val      Asm_full_simp_tac:            int -> tactic
    62   val          simplify: simpset -> thm -> thm
    63   val      asm_simplify: simpset -> thm -> thm
    64   val     full_simplify: simpset -> thm -> thm
    65   val asm_full_simplify: simpset -> thm -> thm
    66 end;
    67 
    68 
    69 structure Simplifier: SIMPLIFIER =
    70 struct
    71 
    72 
    73 (** simplification procedures **)
    74 
    75 (* datatype simproc *)
    76 
    77 datatype simproc =
    78   Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
    79 
    80 fun mk_simproc name lhss proc =
    81   Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
    82 
    83 fun rep_simproc (Simproc args) = args;
    84 
    85 
    86 (* generic conversion prover *)		(* FIXME move?, rename? *)
    87 
    88 fun conv_prover mk_eqv eqv_refl mk_meta_eq expand_tac norm_tac sg t u =
    89   let
    90     val X = Free (gensym "X.", fastype_of t);
    91     val goal = Logic.mk_implies (mk_eqv (X, t), mk_eqv (X, u));
    92     val pre_result =
    93       prove_goalw_cterm [] (cterm_of sg goal)   (*goal: X=t ==> X=u*)
    94         (fn prems => [
    95           expand_tac,				(*expand u*)
    96           ALLGOALS (cut_facts_tac prems),
    97           ALLGOALS norm_tac]);			(*normalize both t and u*)
    98   in
    99     mk_meta_eq (eqv_refl RS pre_result)         (*final result: t==u*)
   100   end
   101   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   102     (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
   103 
   104 
   105 
   106 (** simplification sets **)
   107 
   108 (* type simpset *)
   109 
   110 datatype simpset =
   111   Simpset of {
   112     mss: meta_simpset,
   113     subgoal_tac:        simpset -> int -> tactic,
   114     loop_tac:                      int -> tactic,
   115            finish_tac: thm list -> int -> tactic,
   116     unsafe_finish_tac: thm list -> int -> tactic};
   117 
   118 fun make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) =
   119   Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tac = loop_tac,
   120     finish_tac = finish_tac, unsafe_finish_tac = unsafe_finish_tac};
   121 
   122 val empty_ss =
   123   make_ss (Thm.empty_mss, K (K no_tac), K no_tac, K (K no_tac), K (K no_tac));
   124 
   125 fun rep_ss (Simpset args) = args;
   126 fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
   127 
   128 
   129 (* print simpsets *)
   130 
   131 fun print_ss ss =
   132   let
   133     val Simpset {mss, ...} = ss;
   134     val {simps, procs, congs} = Thm.dest_mss mss;
   135 
   136     val pretty_thms = map Display.pretty_thm;
   137     fun pretty_proc (name, lhss) =
   138       Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   139   in
   140     Pretty.writeln (Pretty.big_list "simplification rules:" (pretty_thms simps));
   141     Pretty.writeln (Pretty.big_list "simplification procedures:" (map pretty_proc procs));
   142     Pretty.writeln (Pretty.big_list "congruences:" (pretty_thms congs))
   143   end;
   144 
   145 
   146 (* extend simpsets *)
   147 
   148 fun (Simpset {mss, subgoal_tac = _, loop_tac, finish_tac, unsafe_finish_tac})
   149     setsubgoaler subgoal_tac =
   150   make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   151 
   152 fun (Simpset {mss, subgoal_tac, loop_tac = _, finish_tac, unsafe_finish_tac})
   153     setloop loop_tac =
   154   make_ss (mss, subgoal_tac, DETERM o loop_tac, finish_tac, unsafe_finish_tac);
   155 
   156 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   157     addloop tac =
   158   make_ss (mss, subgoal_tac, loop_tac ORELSE' (DETERM o tac), finish_tac, unsafe_finish_tac);
   159 
   160 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac = _, unsafe_finish_tac})
   161     setSSolver finish_tac =
   162   make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   163 
   164 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   165     addSSolver tac =
   166   make_ss (mss, subgoal_tac, loop_tac, fn hyps => finish_tac hyps ORELSE' tac hyps,
   167     unsafe_finish_tac);
   168 
   169 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac = _})
   170     setSolver unsafe_finish_tac =
   171   make_ss (mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   172 
   173 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   174     addSolver tac =
   175   make_ss (mss, subgoal_tac, loop_tac, finish_tac,
   176     fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
   177 
   178 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   179     setmksimps mk_simps =
   180   make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
   181     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   182 
   183 fun (Simpset {mss, subgoal_tac, loop_tac,  finish_tac, unsafe_finish_tac})
   184     settermless termless =
   185   make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tac,
   186     finish_tac, unsafe_finish_tac);
   187 
   188 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   189     addsimps rews =
   190   let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
   191     make_ss (Thm.add_simps (mss, rews'), subgoal_tac, loop_tac,
   192       finish_tac, unsafe_finish_tac)
   193   end;
   194 
   195 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   196     delsimps rews =
   197   let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
   198     make_ss (Thm.del_simps (mss, rews'), subgoal_tac, loop_tac,
   199       finish_tac, unsafe_finish_tac)
   200   end;
   201 
   202 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   203     addeqcongs newcongs =
   204   make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tac,
   205     finish_tac, unsafe_finish_tac);
   206 
   207 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   208     deleqcongs oldcongs =
   209   make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tac,
   210     finish_tac, unsafe_finish_tac);
   211 
   212 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   213     addsimprocs simprocs =
   214   make_ss
   215     (Thm.add_simprocs (mss, map rep_simproc simprocs),
   216       subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   217 
   218 fun (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac})
   219     delsimprocs simprocs =
   220   make_ss
   221     (Thm.del_simprocs (mss, map rep_simproc simprocs),
   222       subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   223 
   224 
   225 (* merge simpsets *)	(*NOTE: ignores tactics of 2nd simpset*)
   226 
   227 fun merge_ss
   228    (Simpset {mss = mss1, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac},
   229     Simpset {mss = mss2, ...}) =
   230   make_ss (Thm.merge_mss (mss1, mss2),
   231     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   232 
   233 
   234 
   235 (** the current simpset **)
   236 
   237 val simpset = ref empty_ss;
   238 
   239 fun Addsimps rews = (simpset := ! simpset addsimps rews);
   240 fun Delsimps rews = (simpset := ! simpset delsimps rews);
   241 
   242 fun Addsimprocs procs = (simpset := ! simpset addsimprocs procs);
   243 fun Delsimprocs procs = (simpset := ! simpset delsimprocs procs);
   244 
   245 
   246 
   247 (** simplification tactics **)
   248 
   249 fun NEWSUBGOALS tac tacf st0 =
   250   st0 |> (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
   251 
   252 fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss =
   253   let
   254     val ss =
   255       make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
   256     val solve1_tac =
   257       NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n < 0 then all_tac else no_tac);
   258   in DEPTH_SOLVE solve1_tac end;
   259 
   260 
   261 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   262 fun basic_gen_simp_tac mode =
   263   fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
   264     let
   265       fun simp_loop_tac i thm =
   266         (asm_rewrite_goal_tac mode
   267           (solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac)) mss i
   268         THEN (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm
   269       and allsimp i n = EVERY (map (fn j => simp_loop_tac (i + j)) (n downto 0))
   270       and looper i = TRY (NEWSUBGOALS (loop_tac i) (allsimp i));
   271   in simp_loop_tac end;
   272 
   273 fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) =
   274   basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac);
   275 
   276 
   277 val          simp_tac = gen_simp_tac (false, false);
   278 val      asm_simp_tac = gen_simp_tac (false, true);
   279 val     full_simp_tac = gen_simp_tac (true,  false);
   280 val asm_full_simp_tac = gen_simp_tac (true,  true);
   281 
   282 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   283 val safe_asm_full_simp_tac = basic_gen_simp_tac (true, true);
   284 
   285 fun          Simp_tac i =          simp_tac (! simpset) i;
   286 fun      Asm_simp_tac i =      asm_simp_tac (! simpset) i;
   287 fun     Full_simp_tac i =     full_simp_tac (! simpset) i;
   288 fun Asm_full_simp_tac i = asm_full_simp_tac (! simpset) i;
   289 
   290 
   291 
   292 (** simplification meta rules **)
   293 
   294 fun simp mode (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) thm =
   295   let
   296     val tacf = solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   297     fun prover m th = apsome fst (Sequence.pull (tacf m th));
   298   in
   299     Drule.rewrite_thm mode prover mss thm
   300   end;
   301 
   302 val          simplify = simp (false, false);
   303 val      asm_simplify = simp (false, true);
   304 val     full_simplify = simp (true, false);
   305 val asm_full_simplify = simp (true, true);
   306 
   307 
   308 end;