src/Pure/Isar/method.ML

--- a/src/Pure/Isar/method.ML	Fri Jan 28 12:06:52 2000 +0100
+++ b/src/Pure/Isar/method.ML	Fri Jan 28 12:10:47 2000 +0100
@@ -14,6 +14,16 @@
 signature METHOD =
 sig
   include BASIC_METHOD
+  val print_global_rules: theory -> unit
+  val print_local_rules: Proof.context -> unit
+  val dest_global: theory attribute
+  val elim_global: theory attribute
+  val intro_global: theory attribute
+  val delrule_global: theory attribute
+  val dest_local: Proof.context attribute
+  val elim_local: Proof.context attribute
+  val intro_local: Proof.context attribute
+  val delrule_local: Proof.context attribute
   val METHOD: (thm list -> tactic) -> Proof.method
   val METHOD0: tactic -> Proof.method
   val fail: Proof.method
@@ -84,6 +94,93 @@
 struct
 
 
+(** global and local rule data **)
+
+fun prt_rules kind ths =
+  Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:") (map Display.pretty_thm ths));
+
+fun print_rules (intro, elim) =
+  (prt_rules "introduction" intro; prt_rules "elimination" elim);
+
+fun merge_rules (ths1, ths2) = Library.generic_merge Thm.eq_thm I I ths1 ths2;
+
+
+(* theory data kind 'Isar/rules' *)
+
+structure GlobalRulesArgs =
+struct
+  val name = "Isar/rules";
+  type T = thm list * thm list;
+
+  val empty = ([], []);
+  val copy = I;
+  val prep_ext = I;
+  fun merge ((intro1, elim1), (intro2, elim2)) =
+    (merge_rules (intro1, intro2), merge_rules (elim1, elim2));
+  fun print _ = print_rules;
+end;
+
+structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
+val print_global_rules = GlobalRules.print;
+
+
+(* proof data kind 'Isar/rules' *)
+
+structure LocalRulesArgs =
+struct
+  val name = "Isar/rules";
+  type T = thm list * thm list;
+
+  val init = GlobalRules.get;
+  fun print _ = print_rules;
+end;
+
+structure LocalRules = ProofDataFun(LocalRulesArgs);
+val print_local_rules = LocalRules.print;
+
+
+
+(** attributes **)
+
+(* add rules *)
+
+local
+
+fun add_rule thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
+fun del_rule thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
+
+fun add_dest thm (intro, elim) = (intro, add_rule (Tactic.make_elim thm) elim);
+fun add_elim thm (intro, elim) = (intro, add_rule thm elim);
+fun add_intro thm (intro, elim) = (add_rule thm intro, elim);
+fun delrule thm (intro, elim) = (del_rule thm intro, del_rule thm elim);
+
+fun mk_att f g (x, thm) = (f (g thm) x, thm);
+
+in
+
+val dest_global = mk_att GlobalRules.map add_dest;
+val elim_global = mk_att GlobalRules.map add_elim;
+val intro_global = mk_att GlobalRules.map add_intro;
+val delrule_global = mk_att GlobalRules.map delrule;
+
+val dest_local = mk_att LocalRules.map add_dest;
+val elim_local = mk_att LocalRules.map add_elim;
+val intro_local = mk_att LocalRules.map add_intro;
+val delrule_local = mk_att LocalRules.map delrule;
+
+end;
+
+
+(* concrete syntax *)
+
+val rule_atts =
+ [("dest", (Attrib.no_args dest_global, Attrib.no_args dest_local), "destruction rule"),
+  ("elim", (Attrib.no_args elim_global, Attrib.no_args elim_local), "elimination rule"),
+  ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "introduction rule"),
+  ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), "delete rule")];
+
+
+
 (** proof methods **)
 
 (* method from tactic *)
@@ -154,13 +251,24 @@
         fun tactic i state = Seq.flat (Seq.map (fn rule => tac [rule] i state) rules);
       in tactic end;
 
+fun gen_rule tac rules = METHOD (FINDGOAL o tac rules);
+
+fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
+  let val rules =
+    if not (null arg_rules) then arg_rules
+    else if null facts then #1 (LocalRules.get ctxt)
+    else op @ (LocalRules.get ctxt);
+  in FINDGOAL (tac rules facts) end);
+
 in
 
 val rule_tac = gen_rule_tac Tactic.resolve_tac;
-val erule_tac = gen_rule_tac Tactic.eresolve_tac;
+val rule = gen_rule rule_tac;
+val some_rule = gen_rule' rule_tac;
 
-fun rule rules = METHOD (FIRSTGOAL o rule_tac rules);
-fun erule rules = METHOD (FIRSTGOAL o erule_tac rules);
+val erule_tac = gen_rule_tac Tactic.eresolve_tac;
+val erule = gen_rule erule_tac;
+val some_erule = gen_rule' erule_tac;
 
 end;
 
@@ -174,8 +282,8 @@
   | assumption_tac _ [fact] = resolve_tac [fact]
   | assumption_tac _ _ = K no_tac;
 
-fun assumption ctxt = METHOD (FIRSTGOAL o assumption_tac ctxt);
-fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt))));
+fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
+fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
 
 
 
@@ -390,14 +498,17 @@
   ("insert", thms_args insert, "insert theorems, ignoring facts (improper!)"),
   ("unfold", thms_args unfold, "unfold definitions"),
   ("fold", thms_args fold, "fold definitions"),
-  ("rule", thms_args rule, "apply some rule"),
-  ("erule", thms_args erule, "apply some erule (improper!)"),
+  ("default", thms_ctxt_args some_rule, "apply some rule"),
+  ("rule", thms_ctxt_args some_rule, "apply some rule"),
+  ("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"),
   ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];
 
 
 (* setup *)
 
-val setup = [MethodsData.init, add_methods pure_methods];
+val setup =
+ [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts,
+  MethodsData.init, add_methods pure_methods];
 
 
 end;