# HG changeset patch
# User wenzelm
# Date 1423648493 -3600
# Node ID d881f5288d5a13a8013dc9f7d78b0692951a3f14
# Parent  9937bc07202b7b85c8b966d2a2e93c079f7bdf5d
proper context and method setup;

diff -r 9937bc07202b -r d881f5288d5a src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Tue Feb 10 23:02:39 2015 +0100
+++ b/src/FOL/IFOL.thy	Wed Feb 11 10:54:53 2015 +0100
@@ -208,8 +208,8 @@
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
 ML {*
-  fun mp_tac i = eresolve0_tac [@{thm notE}, @{thm impE}] i  THEN  atac i
-  fun eq_mp_tac i = eresolve0_tac [@{thm notE}, @{thm impE}] i  THEN  eq_assume_tac i
+  fun mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i
+  fun eq_mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i
 *}
 
 
@@ -304,18 +304,20 @@
 
 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
 ML {*
-  fun iff_tac prems i =
-    resolve0_tac (prems RL @{thms iffE}) i THEN
-    REPEAT1 (eresolve0_tac [@{thm asm_rl}, @{thm mp}] i)
+  fun iff_tac ctxt prems i =
+    resolve_tac ctxt (prems RL @{thms iffE}) i THEN
+    REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i)
 *}
 
+method_setup iff =
+  \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+
 lemma conj_cong:
   assumes "P <-> P'"
     and "P' ==> Q <-> Q'"
   shows "(P&Q) <-> (P'&Q')"
   apply (insert assms)
-  apply (assumption | rule iffI conjI | erule iffE conjE mp |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 (*Reversed congruence rule!   Used in ZF/Order*)
@@ -324,8 +326,7 @@
     and "P' ==> Q <-> Q'"
   shows "(Q&P) <-> (Q'&P')"
   apply (insert assms)
-  apply (assumption | rule iffI conjI | erule iffE conjE mp |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 lemma disj_cong:
@@ -340,8 +341,7 @@
     and "P' ==> Q <-> Q'"
   shows "(P-->Q) <-> (P'-->Q')"
   apply (insert assms)
-  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
   done
 
 lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
@@ -355,22 +355,19 @@
 lemma all_cong:
   assumes "!!x. P(x) <-> Q(x)"
   shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
-  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
   done
 
 lemma ex_cong:
   assumes "!!x. P(x) <-> Q(x)"
   shows "(EX x. P(x)) <-> (EX x. Q(x))"
-  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
   done
 
 lemma ex1_cong:
   assumes "!!x. P(x) <-> Q(x)"
   shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
-  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
   done
 
 (*** Equality rules ***)
diff -r 9937bc07202b -r d881f5288d5a src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Tue Feb 10 23:02:39 2015 +0100
+++ b/src/FOL/intprover.ML	Wed Feb 11 10:54:53 2015 +0100
@@ -6,7 +6,7 @@
 
 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
 
-Completeness (for propositional logic) is proved in 
+Completeness (for propositional logic) is proved in
 
 Roy Dyckhoff.
 Contraction-Free Sequent Calculi for Intuitionistic Logic.
@@ -15,7 +15,7 @@
 The approach was developed independently by Roy Dyckhoff and L C Paulson.
 *)
 
-signature INT_PROVER = 
+signature INT_PROVER =
 sig
   val best_tac: Proof.context -> int -> tactic
   val best_dup_tac: Proof.context -> int -> tactic
@@ -31,7 +31,7 @@
 end;
 
 
-structure IntPr : INT_PROVER   = 
+structure IntPr : INT_PROVER   =
 struct
 
 (*Negation is treated as a primitive symbol, with rules notI (introduction),
@@ -44,11 +44,11 @@
       (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
       (true, @{thm conjE}), (true, @{thm exE}),
       (false, @{thm conjI}), (true, @{thm conj_impE}),
-      (true, @{thm disj_impE}), (true, @{thm disjE}), 
+      (true, @{thm disj_impE}), (true, @{thm disjE}),
       (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
 
 val haz_brls =
-    [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), 
+    [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
       (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
       (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
 
@@ -65,7 +65,7 @@
 fun safe_step_tac ctxt =
   FIRST' [
     eq_assume_tac,
-    eq_mp_tac,
+    eq_mp_tac ctxt,
     bimatch_tac ctxt safe0_brls,
     hyp_subst_tac ctxt,
     bimatch_tac ctxt safep_brls];
@@ -75,7 +75,7 @@
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 fun inst_step_tac ctxt =
-  assume_tac ctxt APPEND' mp_tac APPEND' 
+  assume_tac ctxt APPEND' mp_tac ctxt APPEND'
   biresolve_tac ctxt (safe0_brls @ safep_brls);
 
 (*One safe or unsafe step. *)
diff -r 9937bc07202b -r d881f5288d5a src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Tue Feb 10 23:02:39 2015 +0100
+++ b/src/FOLP/IFOLP.thy	Wed Feb 11 10:54:53 2015 +0100
@@ -275,6 +275,7 @@
   fun mp_tac ctxt i =
     eresolve_tac ctxt [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac ctxt i
 *}
+method_setup mp = \<open>Scan.succeed (SIMPLE_METHOD' o mp_tac)\<close>
 
 (*Like mp_tac but instantiates no variables*)
 ML {*
@@ -360,23 +361,25 @@
 
 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
 ML {*
-fun iff_tac prems i =
-    resolve0_tac (prems RL [@{thm iffE}]) i THEN
-    REPEAT1 (eresolve0_tac [asm_rl, @{thm mp}] i)
+fun iff_tac ctxt prems i =
+    resolve_tac ctxt (prems RL [@{thm iffE}]) i THEN
+    REPEAT1 (eresolve_tac ctxt [asm_rl, @{thm mp}] i)
 *}
 
+method_setup iff =
+  \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+
 schematic_lemma conj_cong:
   assumes "p:P <-> P'"
     and "!!x. x:P' ==> q(x):Q <-> Q'"
   shows "?p:(P&Q) <-> (P'&Q')"
   apply (insert assms(1))
-  apply (assumption | rule iffI conjI |
-    erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
   done
 
 schematic_lemma disj_cong:
   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
-  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
+  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | mp)+
   done
 
 schematic_lemma imp_cong:
@@ -384,32 +387,29 @@
     and "!!x. x:P' ==> q(x):Q <-> Q'"
   shows "?p:(P-->Q) <-> (P'-->Q')"
   apply (insert assms(1))
-  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac @{context} 1 *} |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI impI | erule iffE | mp | iff assms)+
   done
 
 schematic_lemma iff_cong:
   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
-  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
+  apply (erule iffE | assumption | rule iffI | mp)+
   done
 
 schematic_lemma not_cong:
   "p:P <-> P' ==> ?p:~P <-> ~P'"
-  apply (assumption | rule iffI notI | tactic {* mp_tac @{context} 1 *} | erule iffE notE)+
+  apply (assumption | rule iffI notI | mp | erule iffE notE)+
   done
 
 schematic_lemma all_cong:
   assumes "!!x. f(x):P(x) <-> Q(x)"
   shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
-  apply (assumption | rule iffI allI | tactic {* mp_tac @{context} 1 *} | erule allE |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (assumption | rule iffI allI | mp | erule allE | iff assms)+
   done
 
 schematic_lemma ex_cong:
   assumes "!!x. f(x):P(x) <-> Q(x)"
   shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
-  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac @{context} 1 *} |
-    tactic {* iff_tac @{thms assms} 1 *})+
+  apply (erule exE | assumption | rule iffI exI | mp | iff assms)+
   done
 
 (*NOT PROVED