src/Pure/simplifier.ML
author wenzelm
Fri Apr 03 19:56:51 2015 +0200 (2015-04-03)
changeset 59917 9830c944670f
parent 59621 291934bac95e
child 61098 e1b4b24f2ebd
permissions -rw-r--r--
more uniform "verbose" option to print name space;
     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 simp_tac: Proof.context -> int -> tactic
    12   val asm_simp_tac: Proof.context -> int -> tactic
    13   val full_simp_tac: Proof.context -> int -> tactic
    14   val asm_lr_simp_tac: Proof.context -> int -> tactic
    15   val asm_full_simp_tac: Proof.context -> int -> tactic
    16   val safe_simp_tac: Proof.context -> int -> tactic
    17   val safe_asm_simp_tac: Proof.context -> int -> tactic
    18   val safe_full_simp_tac: Proof.context -> int -> tactic
    19   val safe_asm_lr_simp_tac: Proof.context -> int -> tactic
    20   val safe_asm_full_simp_tac: Proof.context -> int -> tactic
    21   val simplify: Proof.context -> thm -> thm
    22   val asm_simplify: Proof.context -> thm -> thm
    23   val full_simplify: Proof.context -> thm -> thm
    24   val asm_lr_simplify: Proof.context -> thm -> thm
    25   val asm_full_simplify: Proof.context -> thm -> thm
    26 end;
    27 
    28 signature SIMPLIFIER =
    29 sig
    30   include BASIC_SIMPLIFIER
    31   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
    32   val attrib: (thm -> Proof.context -> Proof.context) -> attribute
    33   val simp_add: attribute
    34   val simp_del: attribute
    35   val cong_add: attribute
    36   val cong_del: attribute
    37   val check_simproc: Proof.context -> xstring * Position.T -> string
    38   val the_simproc: Proof.context -> string -> simproc
    39   val def_simproc: {name: binding, lhss: term list,
    40     proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    41     local_theory -> local_theory
    42   val def_simproc_cmd: {name: binding, lhss: string list,
    43     proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    44     local_theory -> local_theory
    45   val pretty_simpset: bool -> Proof.context -> Pretty.T
    46   val default_mk_sym: Proof.context -> thm -> thm option
    47   val prems_of: Proof.context -> thm list
    48   val add_simp: thm -> Proof.context -> Proof.context
    49   val del_simp: thm -> Proof.context -> Proof.context
    50   val add_eqcong: thm -> Proof.context -> Proof.context
    51   val del_eqcong: thm -> Proof.context -> Proof.context
    52   val add_cong: thm -> Proof.context -> Proof.context
    53   val del_cong: thm -> Proof.context -> Proof.context
    54   val add_prems: thm list -> Proof.context -> Proof.context
    55   val mksimps: Proof.context -> thm -> thm list
    56   val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context
    57   val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
    58   val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
    59   val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
    60   val set_termless: (term * term -> bool) -> Proof.context -> Proof.context
    61   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
    62   type trace_ops
    63   val set_trace_ops: trace_ops -> theory -> theory
    64   val simproc_global_i: theory -> string -> term list ->
    65     (Proof.context -> term -> thm option) -> simproc
    66   val simproc_global: theory -> string -> string list ->
    67     (Proof.context -> term -> thm option) -> simproc
    68   val rewrite: Proof.context -> conv
    69   val asm_rewrite: Proof.context -> conv
    70   val full_rewrite: Proof.context -> conv
    71   val asm_lr_rewrite: Proof.context -> conv
    72   val asm_full_rewrite: Proof.context -> conv
    73   val cong_modifiers: Method.modifier parser list
    74   val simp_modifiers': Method.modifier parser list
    75   val simp_modifiers: Method.modifier parser list
    76   val method_setup: Method.modifier parser list -> theory -> theory
    77   val easy_setup: thm -> thm list -> theory -> theory
    78 end;
    79 
    80 structure Simplifier: SIMPLIFIER =
    81 struct
    82 
    83 open Raw_Simplifier;
    84 
    85 
    86 (** declarations **)
    87 
    88 (* attributes *)
    89 
    90 fun attrib f = Thm.declaration_attribute (map_ss o f);
    91 
    92 val simp_add = attrib add_simp;
    93 val simp_del = attrib del_simp;
    94 val cong_add = attrib add_cong;
    95 val cong_del = attrib del_cong;
    96 
    97 
    98 (** named simprocs **)
    99 
   100 structure Simprocs = Generic_Data
   101 (
   102   type T = simproc Name_Space.table;
   103   val empty : T = Name_Space.empty_table "simproc";
   104   val extend = I;
   105   fun merge data : T = Name_Space.merge_tables data;
   106 );
   107 
   108 
   109 (* get simprocs *)
   110 
   111 val get_simprocs = Simprocs.get o Context.Proof;
   112 
   113 fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
   114 val the_simproc = Name_Space.get o get_simprocs;
   115 
   116 val _ = Theory.setup
   117   (ML_Antiquotation.value @{binding simproc}
   118     (Args.context -- Scan.lift (Parse.position Args.name)
   119       >> (fn (ctxt, name) =>
   120         "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
   121 
   122 
   123 (* define simprocs *)
   124 
   125 local
   126 
   127 fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
   128   let
   129     val simproc = make_simproc
   130       {name = Local_Theory.full_name lthy b,
   131        lhss =
   132         let
   133           val lhss' = prep lthy lhss;
   134           val ctxt' = fold Variable.auto_fixes lhss' lthy;
   135         in Variable.export_terms ctxt' lthy lhss' end |> map (Thm.cterm_of lthy),
   136        proc = proc,
   137        identifier = identifier};
   138   in
   139     lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
   140       let
   141         val b' = Morphism.binding phi b;
   142         val simproc' = transform_simproc phi simproc;
   143       in
   144         context
   145         |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
   146         |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
   147       end)
   148   end;
   149 
   150 in
   151 
   152 val def_simproc = gen_simproc Syntax.check_terms;
   153 val def_simproc_cmd = gen_simproc Syntax.read_terms;
   154 
   155 end;
   156 
   157 
   158 
   159 (** pretty_simpset **)
   160 
   161 fun pretty_simpset verbose ctxt =
   162   let
   163     val pretty_term = Syntax.pretty_term ctxt;
   164     val pretty_thm = Display.pretty_thm ctxt;
   165     val pretty_thm_item = Display.pretty_thm_item ctxt;
   166 
   167     fun pretty_simproc (name, lhss) =
   168       Pretty.block
   169         (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
   170           Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss));
   171 
   172     fun pretty_cong_name (const, name) =
   173       pretty_term ((if const then Const else Free) (name, dummyT));
   174     fun pretty_cong (name, thm) =
   175       Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
   176 
   177     val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
   178       dest_ss (simpset_of ctxt);
   179     val simprocs =
   180       Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
   181   in
   182     [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
   183       Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
   184       Pretty.big_list "congruences:" (map pretty_cong congs),
   185       Pretty.strs ("loopers:" :: map quote loopers),
   186       Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
   187       Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
   188     |> Pretty.chunks
   189   end;
   190 
   191 
   192 
   193 (** simplification tactics and rules **)
   194 
   195 fun solve_all_tac solvers ctxt =
   196   let
   197     val {subgoal_tac, ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
   198     val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt) THEN_ALL_NEW (K no_tac);
   199   in DEPTH_SOLVE (solve_tac 1) end;
   200 
   201 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   202 fun generic_simp_tac safe mode ctxt =
   203   let
   204     val {loop_tacs, solvers = (unsafe_solvers, solvers), ...} =
   205       Raw_Simplifier.internal_ss (simpset_of ctxt);
   206     val loop_tac = FIRST' (map (fn (_, tac) => tac ctxt) (rev loop_tacs));
   207     val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
   208       (rev (if safe then solvers else unsafe_solvers)));
   209 
   210     fun simp_loop_tac i =
   211       Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
   212       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   213   in PREFER_GOAL (simp_loop_tac 1) end;
   214 
   215 local
   216 
   217 fun simp rew mode ctxt thm =
   218   let
   219     val {solvers = (unsafe_solvers, _), ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
   220     val tacf = solve_all_tac (rev unsafe_solvers);
   221     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   222   in rew mode prover ctxt thm end;
   223 
   224 in
   225 
   226 val simp_thm = simp Raw_Simplifier.rewrite_thm;
   227 val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
   228 
   229 end;
   230 
   231 
   232 (* tactics *)
   233 
   234 val simp_tac = generic_simp_tac false (false, false, false);
   235 val asm_simp_tac = generic_simp_tac false (false, true, false);
   236 val full_simp_tac = generic_simp_tac false (true, false, false);
   237 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
   238 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   239 
   240 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   241 val safe_simp_tac = generic_simp_tac true (false, false, false);
   242 val safe_asm_simp_tac = generic_simp_tac true (false, true, false);
   243 val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   244 val safe_asm_lr_simp_tac = generic_simp_tac true (true, true, false);
   245 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   246 
   247 
   248 (* conversions *)
   249 
   250 val          simplify = simp_thm (false, false, false);
   251 val      asm_simplify = simp_thm (false, true, false);
   252 val     full_simplify = simp_thm (true, false, false);
   253 val   asm_lr_simplify = simp_thm (true, true, false);
   254 val asm_full_simplify = simp_thm (true, true, true);
   255 
   256 val          rewrite = simp_cterm (false, false, false);
   257 val      asm_rewrite = simp_cterm (false, true, false);
   258 val     full_rewrite = simp_cterm (true, false, false);
   259 val   asm_lr_rewrite = simp_cterm (true, true, false);
   260 val asm_full_rewrite = simp_cterm (true, true, true);
   261 
   262 
   263 
   264 (** concrete syntax of attributes **)
   265 
   266 (* add / del *)
   267 
   268 val simpN = "simp";
   269 val congN = "cong";
   270 val onlyN = "only";
   271 val no_asmN = "no_asm";
   272 val no_asm_useN = "no_asm_use";
   273 val no_asm_simpN = "no_asm_simp";
   274 val asm_lrN = "asm_lr";
   275 
   276 
   277 (* simprocs *)
   278 
   279 local
   280 
   281 val add_del =
   282   (Args.del -- Args.colon >> K (op delsimprocs) ||
   283     Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   284   >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
   285       (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))));
   286 
   287 in
   288 
   289 val simproc_att =
   290   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
   291     Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
   292   >> (fn atts => Thm.declaration_attribute (fn th =>
   293         fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));
   294 
   295 end;
   296 
   297 
   298 (* conversions *)
   299 
   300 local
   301 
   302 fun conv_mode x =
   303   ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
   304     Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
   305     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   306     Scan.succeed asm_full_simplify) |> Scan.lift) x;
   307 
   308 in
   309 
   310 val simplified = conv_mode -- Attrib.thms >>
   311   (fn (f, ths) => Thm.rule_attribute (fn context =>
   312     f ((if null ths then I else Raw_Simplifier.clear_simpset)
   313         (Context.proof_of context) addsimps ths)));
   314 
   315 end;
   316 
   317 
   318 (* setup attributes *)
   319 
   320 val _ = Theory.setup
   321  (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
   322     "declaration of Simplifier rewrite rule" #>
   323   Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
   324     "declaration of Simplifier congruence rule" #>
   325   Attrib.setup @{binding simproc} simproc_att
   326     "declaration of simplification procedures" #>
   327   Attrib.setup @{binding simplified} simplified "simplified rule");
   328 
   329 
   330 
   331 (** method syntax **)
   332 
   333 val cong_modifiers =
   334  [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add @{here}),
   335   Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
   336   Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here})];
   337 
   338 val simp_modifiers =
   339  [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
   340   Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
   341   Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
   342   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
   343     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
   344    @ cong_modifiers;
   345 
   346 val simp_modifiers' =
   347  [Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
   348   Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
   349   Args.$$$ onlyN -- Args.colon >>
   350     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
   351    @ cong_modifiers;
   352 
   353 val simp_options =
   354  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   355   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   356   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   357   Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   358   Scan.succeed asm_full_simp_tac);
   359 
   360 fun simp_method more_mods meth =
   361   Scan.lift simp_options --|
   362     Method.sections (more_mods @ simp_modifiers') >>
   363     (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts));
   364 
   365 
   366 
   367 (** setup **)
   368 
   369 fun method_setup more_mods =
   370   Method.setup @{binding simp}
   371     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   372       HEADGOAL (Method.insert_tac facts THEN'
   373         (CHANGED_PROP oo tac) ctxt)))
   374     "simplification" #>
   375   Method.setup @{binding simp_all}
   376     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   377       ALLGOALS (Method.insert_tac facts) THEN
   378         (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
   379     "simplification (all goals)";
   380 
   381 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn ctxt0 =>
   382   let
   383     val trivialities = Drule.reflexive_thm :: trivs;
   384 
   385     fun unsafe_solver_tac ctxt =
   386       FIRST' [resolve_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
   387     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   388 
   389     (*no premature instantiation of variables during simplification*)
   390     fun safe_solver_tac ctxt =
   391       FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
   392     val safe_solver = mk_solver "easy safe" safe_solver_tac;
   393 
   394     fun mk_eq thm =
   395       if can Logic.dest_equals (Thm.concl_of thm) then [thm]
   396       else [thm RS reflect] handle THM _ => [];
   397 
   398     fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
   399   in
   400     empty_simpset ctxt0
   401     setSSolver safe_solver
   402     setSolver unsafe_solver
   403     |> set_subgoaler asm_simp_tac
   404     |> set_mksimps (K mksimps)
   405   end));
   406 
   407 end;
   408 
   409 structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
   410 open Basic_Simplifier;