src/Pure/simplifier.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70308 7f568724d67e
child 70586 57df8a85317a
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     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 simp_flip: attribute
    36   val cong_add: attribute
    37   val cong_del: attribute
    38   val check_simproc: Proof.context -> xstring * Position.T -> string
    39   val the_simproc: Proof.context -> string -> simproc
    40   type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
    41   val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
    42   val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
    43   val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
    44   val pretty_simpset: bool -> Proof.context -> Pretty.T
    45   val default_mk_sym: Proof.context -> thm -> thm option
    46   val prems_of: Proof.context -> thm list
    47   val add_simp: thm -> Proof.context -> Proof.context
    48   val del_simp: thm -> Proof.context -> Proof.context
    49   val init_simpset: thm list -> 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_term_ord: (term * term -> order) -> 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 rewrite: Proof.context -> conv
    65   val asm_rewrite: Proof.context -> conv
    66   val full_rewrite: Proof.context -> conv
    67   val asm_lr_rewrite: Proof.context -> conv
    68   val asm_full_rewrite: Proof.context -> conv
    69   val cong_modifiers: Method.modifier parser list
    70   val simp_modifiers': Method.modifier parser list
    71   val simp_modifiers: Method.modifier parser list
    72   val method_setup: Method.modifier parser list -> theory -> theory
    73   val unsafe_solver_tac: Proof.context -> int -> tactic
    74   val unsafe_solver: solver
    75   val safe_solver_tac: Proof.context -> int -> tactic
    76   val safe_solver: solver
    77 end;
    78 
    79 structure Simplifier: SIMPLIFIER =
    80 struct
    81 
    82 open Raw_Simplifier;
    83 
    84 
    85 (** declarations **)
    86 
    87 (* attributes *)
    88 
    89 fun attrib f = Thm.declaration_attribute (map_ss o f);
    90 
    91 val simp_add = attrib add_simp;
    92 val simp_del = attrib del_simp;
    93 val simp_flip = attrib flip_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_embedded \<^binding>\<open>simproc\<close>
   118     (Args.context -- Scan.lift Args.embedded_position
   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 type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option};
   126 
   127 fun make_simproc ctxt name {lhss, proc} =
   128   let
   129     val ctxt' = fold Proof_Context.augment lhss ctxt;
   130     val lhss' = Variable.export_terms ctxt' ctxt lhss;
   131   in
   132     cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
   133   end;
   134 
   135 local
   136 
   137 fun def_simproc prep b {lhss, proc} lthy =
   138   let
   139     val simproc =
   140       make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
   141   in
   142     lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
   143       let
   144         val b' = Morphism.binding phi b;
   145         val simproc' = transform_simproc phi simproc;
   146       in
   147         context
   148         |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
   149         |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
   150       end)
   151   end;
   152 
   153 in
   154 
   155 val define_simproc = def_simproc Syntax.check_terms;
   156 val define_simproc_cmd = def_simproc Syntax.read_terms;
   157 
   158 end;
   159 
   160 
   161 
   162 (** pretty_simpset **)
   163 
   164 fun pretty_simpset verbose ctxt =
   165   let
   166     val pretty_term = Syntax.pretty_term ctxt;
   167     val pretty_thm = Thm.pretty_thm ctxt;
   168     val pretty_thm_item = Thm.pretty_thm_item ctxt;
   169 
   170     fun pretty_simproc (name, lhss) =
   171       Pretty.block
   172         (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
   173           Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss));
   174 
   175     fun pretty_cong_name (const, name) =
   176       pretty_term ((if const then Const else Free) (name, dummyT));
   177     fun pretty_cong (name, thm) =
   178       Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
   179 
   180     val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
   181       dest_ss (simpset_of ctxt);
   182     val simprocs =
   183       Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
   184   in
   185     [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
   186       Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
   187       Pretty.big_list "congruences:" (map pretty_cong congs),
   188       Pretty.strs ("loopers:" :: map quote loopers),
   189       Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
   190       Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
   191     |> Pretty.chunks
   192   end;
   193 
   194 
   195 
   196 (** simplification tactics and rules **)
   197 
   198 fun solve_all_tac solvers ctxt =
   199   let
   200     val {subgoal_tac, ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
   201     val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt) THEN_ALL_NEW (K no_tac);
   202   in DEPTH_SOLVE (solve_tac 1) end;
   203 
   204 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   205 fun generic_simp_tac safe mode ctxt =
   206   let
   207     val {loop_tacs, solvers = (unsafe_solvers, solvers), ...} =
   208       Raw_Simplifier.internal_ss (simpset_of ctxt);
   209     val loop_tac = FIRST' (map (fn (_, tac) => tac ctxt) (rev loop_tacs));
   210     val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
   211       (rev (if safe then solvers else unsafe_solvers)));
   212 
   213     fun simp_loop_tac i =
   214       Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
   215       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   216   in PREFER_GOAL (simp_loop_tac 1) end;
   217 
   218 local
   219 
   220 fun simp rew mode ctxt thm =
   221   let
   222     val {solvers = (unsafe_solvers, _), ...} = Raw_Simplifier.internal_ss (simpset_of ctxt);
   223     val tacf = solve_all_tac (rev unsafe_solvers);
   224     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   225   in rew mode prover ctxt thm end;
   226 
   227 in
   228 
   229 val simp_thm = simp Raw_Simplifier.rewrite_thm;
   230 val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
   231 
   232 end;
   233 
   234 
   235 (* tactics *)
   236 
   237 val simp_tac = generic_simp_tac false (false, false, false);
   238 val asm_simp_tac = generic_simp_tac false (false, true, false);
   239 val full_simp_tac = generic_simp_tac false (true, false, false);
   240 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
   241 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   242 
   243 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   244 val safe_simp_tac = generic_simp_tac true (false, false, false);
   245 val safe_asm_simp_tac = generic_simp_tac true (false, true, false);
   246 val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   247 val safe_asm_lr_simp_tac = generic_simp_tac true (true, true, false);
   248 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   249 
   250 
   251 (* conversions *)
   252 
   253 val          simplify = simp_thm (false, false, false);
   254 val      asm_simplify = simp_thm (false, true, false);
   255 val     full_simplify = simp_thm (true, false, false);
   256 val   asm_lr_simplify = simp_thm (true, true, false);
   257 val asm_full_simplify = simp_thm (true, true, true);
   258 
   259 val          rewrite = simp_cterm (false, false, false);
   260 val      asm_rewrite = simp_cterm (false, true, false);
   261 val     full_rewrite = simp_cterm (true, false, false);
   262 val   asm_lr_rewrite = simp_cterm (true, true, false);
   263 val asm_full_rewrite = simp_cterm (true, true, true);
   264 
   265 
   266 
   267 (** concrete syntax of attributes **)
   268 
   269 (* add / del *)
   270 
   271 val simpN = "simp";
   272 val flipN = "flip"
   273 val congN = "cong";
   274 val onlyN = "only";
   275 val no_asmN = "no_asm";
   276 val no_asm_useN = "no_asm_use";
   277 val no_asm_simpN = "no_asm_simp";
   278 val asm_lrN = "asm_lr";
   279 
   280 
   281 (* simprocs *)
   282 
   283 local
   284 
   285 val add_del =
   286   (Args.del -- Args.colon >> K (op delsimprocs) ||
   287     Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   288   >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
   289       (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))));
   290 
   291 in
   292 
   293 val simproc_att =
   294   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
   295     Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
   296   >> (fn atts => Thm.declaration_attribute (fn th =>
   297         fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));
   298 
   299 end;
   300 
   301 
   302 (* conversions *)
   303 
   304 local
   305 
   306 fun conv_mode x =
   307   ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
   308     Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
   309     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   310     Scan.succeed asm_full_simplify) |> Scan.lift) x;
   311 
   312 in
   313 
   314 val simplified = conv_mode -- Attrib.thms >>
   315   (fn (f, ths) => Thm.rule_attribute ths (fn context =>
   316     f ((if null ths then I else Raw_Simplifier.clear_simpset)
   317         (Context.proof_of context) addsimps ths)));
   318 
   319 end;
   320 
   321 
   322 (* setup attributes *)
   323 
   324 val _ = Theory.setup
   325  (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
   326     "declaration of Simplifier rewrite rule" #>
   327   Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del)
   328     "declaration of Simplifier congruence rule" #>
   329   Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
   330     "declaration of simplification procedures" #>
   331   Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
   332 
   333 
   334 
   335 (** method syntax **)
   336 
   337 val cong_modifiers =
   338  [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add \<^here>),
   339   Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>),
   340   Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>)];
   341 
   342 val simp_modifiers =
   343  [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
   344   Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   345   Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
   346   Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   347   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
   348     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
   349    @ cong_modifiers;
   350 
   351 val simp_modifiers' =
   352  [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   353   Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
   354   Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   355   Args.$$$ onlyN -- Args.colon >>
   356     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
   357    @ cong_modifiers;
   358 
   359 val simp_options =
   360  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   361   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   362   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   363   Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   364   Scan.succeed asm_full_simp_tac);
   365 
   366 fun simp_method more_mods meth =
   367   Scan.lift simp_options --|
   368     Method.sections (more_mods @ simp_modifiers') >>
   369     (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts));
   370 
   371 
   372 
   373 (** setup **)
   374 
   375 fun method_setup more_mods =
   376   Method.setup \<^binding>\<open>simp\<close>
   377     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   378       HEADGOAL (Method.insert_tac ctxt facts THEN'
   379         (CHANGED_PROP oo tac) ctxt)))
   380     "simplification" #>
   381   Method.setup \<^binding>\<open>simp_all\<close>
   382     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
   383       ALLGOALS (Method.insert_tac ctxt facts) THEN
   384         (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
   385     "simplification (all goals)";
   386 
   387 fun unsafe_solver_tac ctxt =
   388   FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
   389 val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
   390 
   391 (*no premature instantiation of variables during simplification*)
   392 fun safe_solver_tac ctxt =
   393   FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
   394 val safe_solver = mk_solver "Pure safe" safe_solver_tac;
   395 
   396 val _ =
   397   Theory.setup
   398     (method_setup [] #> Context.theory_map (map_ss (fn ctxt =>
   399       empty_simpset ctxt
   400       setSSolver safe_solver
   401       setSolver unsafe_solver
   402       |> set_subgoaler asm_simp_tac)));
   403 
   404 end;
   405 
   406 structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
   407 open Basic_Simplifier;