src/Pure/simplifier.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 32786 f1ac4b515af9
child 33092 c859019d3ac5
permissions -rw-r--r--
map_range (and map_index) combinator
     1 (*  Title:      Pure/simplifier.ML
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 
     4 Generic simplifier, suitable for most logics (see also
     5 meta_simplifier.ML for the actual meta-level rewriting engine).
     6 *)
     7 
     8 signature BASIC_SIMPLIFIER =
     9 sig
    10   include BASIC_META_SIMPLIFIER
    11   val change_simpset: (simpset -> simpset) -> unit
    12   val global_simpset_of: theory -> simpset
    13   val Addsimprocs: simproc list -> unit
    14   val Delsimprocs: simproc list -> unit
    15   val simpset_of: Proof.context -> simpset
    16   val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    17   val safe_asm_full_simp_tac: simpset -> int -> tactic
    18   val               simp_tac: simpset -> int -> tactic
    19   val           asm_simp_tac: simpset -> int -> tactic
    20   val          full_simp_tac: simpset -> int -> tactic
    21   val        asm_lr_simp_tac: simpset -> int -> tactic
    22   val      asm_full_simp_tac: simpset -> int -> tactic
    23   val          simplify: simpset -> thm -> thm
    24   val      asm_simplify: simpset -> thm -> thm
    25   val     full_simplify: simpset -> thm -> thm
    26   val   asm_lr_simplify: simpset -> thm -> thm
    27   val asm_full_simplify: simpset -> thm -> thm
    28 end;
    29 
    30 signature SIMPLIFIER =
    31 sig
    32   include BASIC_SIMPLIFIER
    33   val pretty_ss: Proof.context -> simpset -> Pretty.T
    34   val clear_ss: simpset -> simpset
    35   val debug_bounds: bool Unsynchronized.ref
    36   val inherit_context: simpset -> simpset -> simpset
    37   val the_context: simpset -> Proof.context
    38   val context: Proof.context -> simpset -> simpset
    39   val theory_context: theory  -> simpset -> simpset
    40   val simproc_i: theory -> string -> term list
    41     -> (theory -> simpset -> term -> thm option) -> simproc
    42   val simproc: theory -> string -> string list
    43     -> (theory -> simpset -> term -> thm option) -> simproc
    44   val          rewrite: simpset -> conv
    45   val      asm_rewrite: simpset -> conv
    46   val     full_rewrite: simpset -> conv
    47   val   asm_lr_rewrite: simpset -> conv
    48   val asm_full_rewrite: simpset -> conv
    49   val get_ss: Context.generic -> simpset
    50   val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
    51   val attrib: (simpset * thm list -> simpset) -> attribute
    52   val simp_add: attribute
    53   val simp_del: attribute
    54   val cong_add: attribute
    55   val cong_del: attribute
    56   val map_simpset: (simpset -> simpset) -> theory -> theory
    57   val get_simproc: Context.generic -> xstring -> simproc
    58   val def_simproc: {name: string, lhss: string list,
    59     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    60     local_theory -> local_theory
    61   val def_simproc_i: {name: string, lhss: term list,
    62     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    63     local_theory -> local_theory
    64   val cong_modifiers: Method.modifier parser list
    65   val simp_modifiers': Method.modifier parser list
    66   val simp_modifiers: Method.modifier parser list
    67   val method_setup: Method.modifier parser list -> theory -> theory
    68   val easy_setup: thm -> thm list -> theory -> theory
    69 end;
    70 
    71 structure Simplifier: SIMPLIFIER =
    72 struct
    73 
    74 open MetaSimplifier;
    75 
    76 
    77 (** pretty printing **)
    78 
    79 fun pretty_ss ctxt ss =
    80   let
    81     val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
    82     val pretty_thm = Display.pretty_thm ctxt;
    83     fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
    84     fun pretty_cong (name, thm) =
    85       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
    86 
    87     val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
    88   in
    89     [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
    90       Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
    91       Pretty.big_list "congruences:" (map pretty_cong congs),
    92       Pretty.strs ("loopers:" :: map quote loopers),
    93       Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
    94       Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
    95     |> Pretty.chunks
    96   end;
    97 
    98 
    99 
   100 (** simpset data **)
   101 
   102 structure SimpsetData = GenericDataFun
   103 (
   104   type T = simpset;
   105   val empty = empty_ss;
   106   fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
   107   fun merge _ = merge_ss;
   108 );
   109 
   110 val get_ss = SimpsetData.get;
   111 val map_ss = SimpsetData.map;
   112 
   113 
   114 (* attributes *)
   115 
   116 fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
   117 
   118 val simp_add = attrib (op addsimps);
   119 val simp_del = attrib (op delsimps);
   120 val cong_add = attrib (op addcongs);
   121 val cong_del = attrib (op delcongs);
   122 
   123 
   124 (* global simpset *)
   125 
   126 fun map_simpset f = Context.theory_map (map_ss f);
   127 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
   128 fun global_simpset_of thy =
   129   MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
   130 
   131 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   132 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   133 
   134 
   135 (* local simpset *)
   136 
   137 fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
   138 
   139 val _ = ML_Antiquote.value "simpset"
   140   (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
   141 
   142 
   143 
   144 (** named simprocs **)
   145 
   146 fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
   147 
   148 
   149 (* data *)
   150 
   151 structure Simprocs = GenericDataFun
   152 (
   153   type T = simproc NameSpace.table;
   154   val empty = NameSpace.empty_table;
   155   val extend = I;
   156   fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
   157     handle Symtab.DUP dup => err_dup_simproc dup;
   158 );
   159 
   160 
   161 (* get simprocs *)
   162 
   163 fun get_simproc context xname =
   164   let
   165     val (space, tab) = Simprocs.get context;
   166     val name = NameSpace.intern space xname;
   167   in
   168     (case Symtab.lookup tab name of
   169       SOME proc => proc
   170     | NONE => error ("Undefined simplification procedure: " ^ quote name))
   171   end;
   172 
   173 val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
   174   "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
   175 
   176 
   177 (* define simprocs *)
   178 
   179 local
   180 
   181 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
   182   let
   183     val b = Binding.name name;
   184     val naming = LocalTheory.full_naming lthy;
   185     val simproc = make_simproc
   186       {name = LocalTheory.full_name lthy b,
   187        lhss =
   188         let
   189           val lhss' = prep lthy lhss;
   190           val ctxt' = lthy
   191             |> fold Variable.declare_term lhss'
   192             |> fold Variable.auto_fixes lhss';
   193         in Variable.export_terms ctxt' lthy lhss' end
   194         |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
   195        proc = proc,
   196        identifier = identifier}
   197       |> morph_simproc (LocalTheory.target_morphism lthy);
   198   in
   199     lthy |> LocalTheory.declaration (fn phi =>
   200       let
   201         val b' = Morphism.binding phi b;
   202         val simproc' = morph_simproc phi simproc;
   203       in
   204         Simprocs.map (fn simprocs =>
   205           NameSpace.define naming (b', simproc') simprocs |> snd
   206             handle Symtab.DUP dup => err_dup_simproc dup)
   207         #> map_ss (fn ss => ss addsimprocs [simproc'])
   208       end)
   209   end;
   210 
   211 in
   212 
   213 val def_simproc = gen_simproc Syntax.read_terms;
   214 val def_simproc_i = gen_simproc Syntax.check_terms;
   215 
   216 end;
   217 
   218 
   219 
   220 (** simplification tactics and rules **)
   221 
   222 fun solve_all_tac solvers ss =
   223   let
   224     val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
   225     val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   226   in DEPTH_SOLVE (solve_tac 1) end;
   227 
   228 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   229 fun generic_simp_tac safe mode ss =
   230   let
   231     val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
   232     val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
   233     val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
   234       (rev (if safe then solvers else unsafe_solvers)));
   235 
   236     fun simp_loop_tac i =
   237       asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
   238       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   239   in simp_loop_tac end;
   240 
   241 local
   242 
   243 fun simp rew mode ss thm =
   244   let
   245     val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
   246     val tacf = solve_all_tac (rev unsafe_solvers);
   247     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   248   in rew mode prover ss thm end;
   249 
   250 in
   251 
   252 val simp_thm = simp MetaSimplifier.rewrite_thm;
   253 val simp_cterm = simp MetaSimplifier.rewrite_cterm;
   254 
   255 end;
   256 
   257 
   258 (* tactics *)
   259 
   260 val simp_tac = generic_simp_tac false (false, false, false);
   261 val asm_simp_tac = generic_simp_tac false (false, true, false);
   262 val full_simp_tac = generic_simp_tac false (true, false, false);
   263 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
   264 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   265 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   266 
   267 
   268 (* conversions *)
   269 
   270 val          simplify = simp_thm (false, false, false);
   271 val      asm_simplify = simp_thm (false, true, false);
   272 val     full_simplify = simp_thm (true, false, false);
   273 val   asm_lr_simplify = simp_thm (true, true, false);
   274 val asm_full_simplify = simp_thm (true, true, true);
   275 
   276 val          rewrite = simp_cterm (false, false, false);
   277 val      asm_rewrite = simp_cterm (false, true, false);
   278 val     full_rewrite = simp_cterm (true, false, false);
   279 val   asm_lr_rewrite = simp_cterm (true, true, false);
   280 val asm_full_rewrite = simp_cterm (true, true, true);
   281 
   282 
   283 
   284 (** concrete syntax of attributes **)
   285 
   286 (* add / del *)
   287 
   288 val simpN = "simp";
   289 val congN = "cong";
   290 val onlyN = "only";
   291 val no_asmN = "no_asm";
   292 val no_asm_useN = "no_asm_use";
   293 val no_asm_simpN = "no_asm_simp";
   294 val asm_lrN = "asm_lr";
   295 
   296 
   297 (* simprocs *)
   298 
   299 local
   300 
   301 val add_del =
   302   (Args.del -- Args.colon >> K (op delsimprocs) ||
   303     Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   304   >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
   305       (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
   306 
   307 in
   308 
   309 val simproc_att =
   310   Scan.peek (fn context =>
   311     add_del :|-- (fn decl =>
   312       Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
   313       >> (Library.apply o map Morphism.form)));
   314 
   315 end;
   316 
   317 
   318 (* conversions *)
   319 
   320 local
   321 
   322 fun conv_mode x =
   323   ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
   324     Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
   325     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   326     Scan.succeed asm_full_simplify) |> Scan.lift) x;
   327 
   328 in
   329 
   330 val simplified = conv_mode -- Attrib.thms >>
   331   (fn (f, ths) => Thm.rule_attribute (fn context =>
   332     f ((if null ths then I else MetaSimplifier.clear_ss)
   333         (simpset_of (Context.proof_of context)) addsimps ths)));
   334 
   335 end;
   336 
   337 
   338 (* setup attributes *)
   339 
   340 val _ = Context.>> (Context.map_theory
   341  (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
   342     "declaration of Simplifier rewrite rule" #>
   343   Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
   344     "declaration of Simplifier congruence rule" #>
   345   Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
   346   Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
   347 
   348 
   349 
   350 (** method syntax **)
   351 
   352 val cong_modifiers =
   353  [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
   354   Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
   355   Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
   356 
   357 val simp_modifiers =
   358  [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
   359   Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
   360   Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
   361   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
   362     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   363    @ cong_modifiers;
   364 
   365 val simp_modifiers' =
   366  [Args.add -- Args.colon >> K (I, simp_add),
   367   Args.del -- Args.colon >> K (I, simp_del),
   368   Args.$$$ onlyN -- Args.colon
   369     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   370    @ cong_modifiers;
   371 
   372 val simp_options =
   373  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   374   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   375   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   376   Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   377   Scan.succeed asm_full_simp_tac);
   378 
   379 fun simp_method more_mods meth =
   380   Args.bang_facts -- Scan.lift simp_options --|
   381     Method.sections (more_mods @ simp_modifiers') >>
   382     (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
   383 
   384 
   385 
   386 (** setup **)
   387 
   388 fun method_setup more_mods =
   389   Method.setup (Binding.name simpN)
   390     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   391       HEADGOAL (Method.insert_tac facts THEN'
   392         (CHANGED_PROP oo tac) (simpset_of ctxt))))
   393     "simplification" #>
   394   Method.setup (Binding.name "simp_all")
   395     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   396       ALLGOALS (Method.insert_tac facts) THEN
   397         (CHANGED_PROP o ALLGOALS o tac) (simpset_of ctxt)))
   398     "simplification (all goals)";
   399 
   400 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
   401   let
   402     val trivialities = Drule.reflexive_thm :: trivs;
   403 
   404     fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
   405     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   406 
   407     (*no premature instantiation of variables during simplification*)
   408     fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
   409     val safe_solver = mk_solver "easy safe" safe_solver_tac;
   410 
   411     fun mk_eq thm =
   412       if can Logic.dest_equals (Thm.concl_of thm) then [thm]
   413       else [thm RS reflect] handle THM _ => [];
   414 
   415     fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   416   in
   417     empty_ss setsubgoaler asm_simp_tac
   418     setSSolver safe_solver
   419     setSolver unsafe_solver
   420     setmksimps mksimps
   421   end));
   422 
   423 end;
   424 
   425 structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
   426 open Basic_Simplifier;