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