(* Title: Provers/clasimp.ML Author: David von Oheimb, TU Muenchen
Combination of classical reasoner and simplifier (depends on splitter.ML, classical.ML, blast.ML).
*)
signature CLASIMP_DATA = sig structure Splitter: SPLITTER structure Classical: CLASSICAL structure Blast: BLAST val notE: thm val iffD1: thm val iffD2: thm end;
signature CLASIMP = sig val addSss: Proof.context -> Proof.context val addss: Proof.context -> Proof.context val clarsimp_tac: Proof.context -> int -> tactic val mk_auto_tac: Proof.context -> int -> int -> tactic val auto_tac: Proof.context -> tactic val force_tac: Proof.context -> int -> tactic val fast_force_tac: Proof.context -> int -> tactic val slow_simp_tac: Proof.context -> int -> tactic val best_simp_tac: Proof.context -> int -> tactic val iff_add: attribute val iff_add_pure: attribute val iff_del: attribute val iff_modifiers: Method.modifier parser list val clasimp_modifiers: Method.modifier parser list end;
(*Caution: only one simpset added can be added by each of addSss and addss*)
local fun add_wrapper f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt)); in val addSss =
add_wrapper Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac; val addss =
add_wrapper Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac; end;
(* iffs: addition of rules to simpsets and clasets simultaneously *)
local
val safe_atts =
{intro = Classical.safe_intro NONE,
elim = Classical.safe_elim NONE,
dest = Classical.safe_dest NONE};
val unsafe_atts =
{intro = Classical.unsafe_intro NONE,
elim = Classical.unsafe_elim NONE,
dest = Classical.unsafe_dest NONE};
val pure_atts =
{intro = Context_Rules.intro_query NONE,
elim = Context_Rules.elim_query NONE,
dest = Context_Rules.dest_query NONE};
val del_atts =
{intro = Classical.rule_del,
elim = Classical.rule_del,
dest = Classical.rule_del};
(*Takes (possibly conditional) theorems of the form A<->B to the Safe Intr rule B==>A and the Safe Destruct rule A==>B. Also ~A goes to the Safe Elim rule A ==> ?R
Failing other cases, A is added as a Safe Intr rule*)
fun iff_decl safe unsafe =
Thm.declaration_attribute (fn th => fn context => let val n = Thm.nprems_of th; val {intro, elim, dest} = if n = 0 then safe else unsafe; val zero_rotate = zero_var_indexes o rotate_prems n; val decls =
[(intro, zero_rotate (th RS Data.iffD2)),
(dest, zero_rotate (th RS Data.iffD1))] handle THM _ => [(elim, zero_rotate (th RS Data.notE))] handle THM _ => [(intro, th)]; in fold (uncurry Thm.attribute_declaration) decls context end);
fun nodup_depth_tac ctxt m i st =
SELECT_GOAL
(Classical.safe_steps_tac ctxt 1 THEN_ELSE
(DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
(slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
end;
(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
in some of the subgoals*) fun mk_auto_tac ctxt m n = let val main_tac =
Blast.depth_tac ctxt m (* fast but can't use wrappers *)
ORELSE'
(CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) in
PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN TRY (Classical.safe_tac ctxt) THEN
REPEAT_DETERM (FIRSTGOAL main_tac) THEN TRY (Classical.safe_tac (addSss ctxt)) THEN
prune_params_tac ctxt end;
fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
(* force_tac *)
(* aimed to solve the given subgoal totally, using whatever tools possible *) fun force_tac ctxt = letval ctxt' = addss ctxt in
SELECT_GOAL
(Classical.clarify_tac ctxt' 1 THEN
IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN
ALLGOALS (Classical.first_best_tac ctxt')) end;
(* basic combinations *)
val fast_force_tac = Classical.fast_tac o addss; val slow_simp_tac = Classical.slow_tac o addss; val best_simp_tac = Classical.best_tac o addss;
(** concrete syntax **)
(* attributes *)
val _ =
Theory.setup
(Attrib.setup \<^binding>\<open>iff\<close>
(Scan.lift
(Args.del >> K iff_del ||
Scan.option Args.add -- Args.query >> K iff_add_pure ||
Scan.option Args.add >> K iff_add)) "declaration of Simplifier / Classical rules");
(* method modifiers *)
val iff_token = Args.$$$ "iff";
val iff_modifiers =
[iff_token -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
iff_token -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add_pure \<^here>),
iff_token -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @
Classical.cla_modifiers @ iff_modifiers;
(* methods *)
fun clasimp_method' tac =
Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
val auto_method =
Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
Method.sections clasimp_modifiers >>
(fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
| SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
val _ =
Theory.setup
(Method.setup \<^binding>\<open>fastforce\<close> (clasimp_method' fast_force_tac) "combined fast and simp" #>
Method.setup \<^binding>\<open>slowsimp\<close> (clasimp_method' slow_simp_tac) "combined slow and simp" #>
Method.setup \<^binding>\<open>bestsimp\<close> (clasimp_method' best_simp_tac) "combined best and simp" #>
Method.setup \<^binding>\<open>force\<close> (clasimp_method' force_tac) "force" #>
Method.setup \<^binding>\<open>auto\<close> auto_method "auto" #>
Method.setup \<^binding>\<open>clarsimp\<close> (clasimp_method' (CHANGED_PROP oo clarsimp_tac)) "clarify simplified goal");
end;
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
