src/Pure/Isar/method.ML

--- a/src/Pure/Isar/method.ML	Wed Dec 05 03:16:43 2001 +0100
+++ b/src/Pure/Isar/method.ML	Wed Dec 05 03:17:34 2001 +0100
@@ -176,10 +176,16 @@
 end;
 
 
-(* unfold / fold definitions *)
+(* unfold/fold definitions *)
+
+fun unfold ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths));
+fun fold ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
 
-fun unfold thms = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac thms));
-fun fold thms = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac thms));
+
+(* unfold intro/elim rules *)
+
+fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
+fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
 
 
 (* multi_resolve *)
@@ -255,15 +261,6 @@
 
 local
 
-fun may_unify t nets =
-  flat (map (ContextRules.orderlist_no_weight o (fn net => Net.unify_term net t)) nets);
-
-fun find_erules [] = K []
-  | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact)));
-
-fun find_rules goal = may_unify (Logic.strip_assums_concl goal);
-
-
 fun gen_rule_tac tac rules [] i st = tac rules i st
   | gen_rule_tac tac rules facts i st =
       Seq.flat (Seq.map (fn rule => (tac o single) rule i st) (multi_resolves facts rules));
@@ -273,10 +270,9 @@
 
 fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) =>
   let
-    val netpairs = ContextRules.netpairs ctxt;
     val rules =
       if not (null arg_rules) then arg_rules
-      else map #2 (find_erules facts (map #2 netpairs) @ find_rules goal (map #1 netpairs));
+      else flat (ContextRules.find_rules ctxt facts goal)
   in trace ctxt rules; tac rules facts i end);
 
 fun meth tac x = METHOD (HEADGOAL o tac x);
@@ -504,13 +500,10 @@
     >> (pair (I: Proof.context -> Proof.context) o att);
 
 val rules_modifiers =
- [modifier destN Args.query_colon Args.query ContextRules.dest_query_local,
-  modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local,
+ [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local,
   modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local,
-  modifier elimN Args.query_colon Args.query ContextRules.elim_query_local,
   modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local,
   modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local,
-  modifier introN Args.query_colon Args.query ContextRules.intro_query_local,
   modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local,
   modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local,
   Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)];
@@ -644,11 +637,13 @@
   ("-", no_args insert_facts, "do nothing (insert current facts only)"),
   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   ("unfold", thms_args unfold, "unfold definitions"),
+  ("intro", thms_args intro, "repeatedly apply introduction rules"),
+  ("elim", thms_args elim, "repeatedly apply elimination rules"),
   ("fold", thms_args fold, "fold definitions"),
   ("atomize", no_args (SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)),
     "present local premises as object-level statements"),
   ("rules", rules_args rules_meth, "apply many rules, including proof search"),
-  ("rule", thms_ctxt_args some_rule, "apply some rule"),
+  ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
   ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
   ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
   ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),