author wenzelm
Sun, 06 Nov 2011 21:51:46 +0100
changeset 45375 7fe19930dfc9
parent 44890 22f665a2e91c
child 47967 c422128d3889
permissions -rw-r--r--
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;

(*  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 =
  structure Splitter: SPLITTER
  structure Classical: CLASSICAL
  structure Blast: BLAST
  val notE: thm
  val iffD1: thm
  val iffD2: thm

signature CLASIMP =
  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': attribute
  val iff_del: attribute
  val iff_modifiers: Method.modifier parser list
  val clasimp_modifiers: Method.modifier parser list
  val clasimp_setup: theory -> theory

functor Clasimp(Data: CLASIMP_DATA): CLASIMP =

structure Splitter = Data.Splitter;
structure Classical = Data.Classical;
structure Blast = Data.Blast;

(* simp as classical wrapper *)

(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);

fun clasimp f name tac ctxt =
  Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;

(*Add a simpset to the claset!*)
(*Caution: only one simpset added can be added by each of addSss and addss*)
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;

(* iffs: addition of rules to simpsets and clasets simultaneously *)


(*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 add_iff safe unsafe =
  Thm.declaration_attribute (fn th =>
      val n = nprems_of th;
      val (elim, intro) = if n = 0 then safe else unsafe;
      val zero_rotate = zero_var_indexes o rotate_prems n;
      Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #>
      Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
      handle THM _ =>
        (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE))
          handle THM _ => Thm.attribute_declaration intro th)

fun del_iff del = Thm.declaration_attribute (fn th =>
  let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
    Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #>
    Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
    handle THM _ =>
      (Thm.attribute_declaration del (zero_rotate (th RS Data.notE))
        handle THM _ => Thm.attribute_declaration del th)


val iff_add =
  Thm.declaration_attribute (fn th =>
    Thm.attribute_declaration (add_iff
      (Classical.safe_elim NONE, Classical.safe_intro NONE)
      (Classical.haz_elim NONE, Classical.haz_intro NONE)) th
    #> Thm.attribute_declaration Simplifier.simp_add th);

val iff_add' =
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);

val iff_del =
  Thm.declaration_attribute (fn th =>
    Thm.attribute_declaration (del_iff Classical.rule_del) th #>
    Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
    Thm.attribute_declaration Simplifier.simp_del th);


(* tactics *)

fun clarsimp_tac ctxt =
  safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
  Classical.clarify_tac (addSss ctxt);

(* auto_tac *)

(* a variant of depth_tac that avoids interference of the simplifier
   with dup_step_tac when they are combined by auto_tac *)

fun slow_step_tac' ctxt =
  Classical.appWrappers ctxt
    (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);


fun nodup_depth_tac ctxt m i st =
    (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;


(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
  in some of the subgoals*)
fun mk_auto_tac ctxt m n =
    val main_tac =
      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
      (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
    PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
    TRY (Classical.safe_tac ctxt) THEN
    TRY (Classical.safe_tac (addSss ctxt)) THEN

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 =
  let val ctxt' = addss ctxt in
     (Classical.clarify_tac ctxt' 1 THEN
      IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
      ALLGOALS (Classical.first_best_tac ctxt'))

(* basic combinations *)

fun fast_simp_tac ctxt i =
  let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead"
  in Classical.fast_tac (addss ctxt) i end;

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 *)

fun iff_att x = (Scan.lift
 (Args.del >> K iff_del ||
  Scan.option Args.add -- Args.query >> K iff_add' ||
  Scan.option Args.add >> K iff_add)) x;

(* method modifiers *)

val iffN = "iff";

val iff_modifiers =
 [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];

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 >>
    | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));

(* theory setup *)

val clasimp_setup =
  Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
  Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #>
  Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
  Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
  Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
  Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
  Method.setup @{binding auto} auto_method "auto" #>
  Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
    "clarify simplified goal";