added erule;
authorwenzelm
Fri, 30 Jul 1999 13:41:43 +0200
changeset 7130 a17f7b5ac40f
parent 7129 7e0ec1b293c3
child 7131 0b2fe9ec709c
added erule; renamed same to -;
src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Jul 30 13:34:27 1999 +0200
+++ b/src/Pure/Isar/method.ML	Fri Jul 30 13:41:43 1999 +0200
@@ -26,7 +26,9 @@
   val assumption: Proof.method
   val forward_chain: thm list -> thm list -> thm Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
+  val erule_tac: thm list -> thm list -> int -> tactic
   val rule: thm list -> Proof.method
+  val erule: thm list -> Proof.method
   exception METHOD_FAIL of (string * Position.T) * exn
   val method: theory -> Args.src -> Proof.context -> Proof.method
   val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
@@ -137,14 +139,18 @@
 
 fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
 
-fun rule_tac rules [] = resolve_tac rules
-  | rule_tac erules facts =
+fun gen_rule_tac tac rules [] = tac rules
+  | gen_rule_tac tac erules facts =
       let
         val rules = forward_chain facts erules;
-        fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules);
-      in tac end;
+        fun tactic i state = Seq.flat (Seq.map (fn rule => tac [rule] i state) rules);
+      in tactic end;
+
+val rule_tac = gen_rule_tac Tactic.resolve_tac;
+val erule_tac = gen_rule_tac Tactic.eresolve_tac;
 
 fun rule rules = METHOD (FIRSTGOAL o rule_tac rules);
+fun erule rules = METHOD (FIRSTGOAL o erule_tac rules);
 
 
 
@@ -350,12 +356,13 @@
 val pure_methods =
  [("fail", no_args fail, "force failure"),
   ("succeed", no_args succeed, "succeed"),
-  ("same", no_args same, "insert facts, nothing else"),
+  ("-", no_args same, "insert facts, nothing else"),
   ("assumption", no_args assumption, "proof by assumption"),
   ("finish", no_args asm_finish, "finish proof by assumption"),
   ("fold", thms_args fold, "fold definitions"),
   ("unfold", thms_args unfold, "unfold definitions"),
-  ("rule", thms_args rule, "apply some rule")];
+  ("rule", thms_args rule, "apply some rule"),
+  ("erule", thms_args erule, "apply some erule (improper!)")];
 
 
 (* setup *)