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