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