--- a/NEWS Sun Nov 09 14:08:00 2014 +0100
+++ b/NEWS Sun Nov 09 17:04:14 2014 +0100
@@ -190,7 +190,7 @@
*** ML ***
-* Proper context for various elementary tactics: compose_tac,
+* Proper context for various elementary tactics: match_tac, compose_tac,
Splitter.split_tac etc. Minor INCOMPATIBILITY.
* Tactical PARALLEL_ALLGOALS is the most common way to refer to
--- a/src/CCL/Wfd.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/CCL/Wfd.thy Sun Nov 09 17:04:14 2014 +0100
@@ -453,10 +453,11 @@
in IHinst tac @{thms rcallTs} i end
THEN eresolve_tac @{thms rcall_lemmas} i
-fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
- rcall_tac ctxt i ORELSE
- ematch_tac [@{thm SubtypeE}] i ORELSE
- match_tac [@{thm SubtypeI}] i
+fun raw_step_tac ctxt prems i =
+ ares_tac (prems@type_rls) i ORELSE
+ rcall_tac ctxt i ORELSE
+ ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
+ match_tac ctxt [@{thm SubtypeI}] i
fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
--- a/src/Doc/Implementation/Tactic.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Doc/Implementation/Tactic.thy Sun Nov 09 17:04:14 2014 +0100
@@ -284,10 +284,10 @@
@{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
@{index_ML assume_tac: "int -> tactic"} \\
@{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
- @{index_ML match_tac: "thm list -> int -> tactic"} \\
- @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
- @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
- @{index_ML bimatch_tac: "(bool * thm) list -> int -> tactic"} \\
+ @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
+ @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+ @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+ @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
\end{mldecls}
\begin{description}
--- a/src/FOL/FOL.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/FOL.thy Sun Nov 09 17:04:14 2014 +0100
@@ -420,7 +420,7 @@
val rulify_fallback = @{thms induct_rulify_fallback}
val equal_def = @{thm induct_equal_def}
fun dest_def _ = NONE
- fun trivial_tac _ = no_tac
+ fun trivial_tac _ _ = no_tac
);
*}
--- a/src/FOL/intprover.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/intprover.ML Sun Nov 09 17:04:14 2014 +0100
@@ -66,9 +66,9 @@
FIRST' [
eq_assume_tac,
eq_mp_tac,
- bimatch_tac safe0_brls,
+ bimatch_tac ctxt safe0_brls,
hyp_subst_tac ctxt,
- bimatch_tac safep_brls];
+ bimatch_tac ctxt safep_brls];
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
--- a/src/FOL/simpdata.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/simpdata.ML Sun Nov 09 17:04:14 2014 +0100
@@ -113,7 +113,8 @@
(*No premature instantiation of variables during simplification*)
fun safe_solver ctxt =
- FIRST' [match_tac (triv_rls @ Simplifier.prems_of ctxt), eq_assume_tac, ematch_tac @{thms FalseE}];
+ FIRST' [match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
+ eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss =
--- a/src/FOLP/FOLP.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/FOLP.thy Sun Nov 09 17:04:14 2014 +0100
@@ -134,7 +134,7 @@
"?p2 : ~P | P"
"?p3 : ~ ~ P <-> P"
"?p4 : (~P --> P) <-> P"
- apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
+ apply (tactic {* ALLGOALS (Cla.fast_tac @{context} FOLP_cs) *})
done
ML_file "simpdata.ML"
--- a/src/FOLP/classical.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/classical.ML Sun Nov 09 17:04:14 2014 +0100
@@ -44,19 +44,19 @@
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list,
safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
haz_brls: (bool*thm)list}
- val best_tac : claset -> int -> tactic
+ val best_tac : Proof.context -> claset -> int -> tactic
val contr_tac : int -> tactic
- val fast_tac : claset -> int -> tactic
+ val fast_tac : Proof.context -> claset -> int -> tactic
val inst_step_tac : int -> tactic
val joinrules : thm list * thm list -> (bool * thm) list
val mp_tac: int -> tactic
- val safe_tac : claset -> tactic
- val safe_step_tac : claset -> int -> tactic
- val slow_step_tac : claset -> int -> tactic
- val step_tac : claset -> int -> tactic
+ val safe_tac : Proof.context -> claset -> tactic
+ val safe_step_tac : Proof.context -> claset -> int -> tactic
+ val slow_step_tac : Proof.context -> claset -> int -> tactic
+ val step_tac : Proof.context -> claset -> int -> tactic
val swapify : thm list -> thm list
val swap_res_tac : thm list -> int -> tactic
- val uniq_mp_tac: int -> tactic
+ val uniq_mp_tac: Proof.context -> int -> tactic
end;
@@ -76,7 +76,7 @@
fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i;
(*Like mp_tac but instantiates no variables*)
-fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i THEN uniq_assume_tac i;
+fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i THEN uniq_assume_tac i;
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [swap]);
@@ -148,38 +148,38 @@
(*** Simple tactics for theorem proving ***)
(*Attack subgoals using safe inferences*)
-fun safe_step_tac (CS{safe0_brls,safep_brls,...}) =
+fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) =
FIRST' [uniq_assume_tac,
- uniq_mp_tac,
+ uniq_mp_tac ctxt,
biresolve_tac safe0_brls,
FIRST' hyp_subst_tacs,
biresolve_tac safep_brls] ;
(*Repeatedly attack subgoals using safe inferences*)
-fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
+fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
(*These steps could instantiate variables and are therefore unsafe.*)
val inst_step_tac = assume_tac APPEND' contr_tac;
(*Single step for the prover. FAILS unless it makes progress. *)
-fun step_tac (cs as (CS{haz_brls,...})) i =
- FIRST [safe_tac cs,
+fun step_tac ctxt (cs as (CS{haz_brls,...})) i =
+ FIRST [safe_tac ctxt cs,
inst_step_tac i,
biresolve_tac haz_brls i];
(*** The following tactics all fail unless they solve one goal ***)
(*Dumb but fast*)
-fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1));
(*Slower but smarter than fast_tac*)
-fun best_tac cs =
- SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
+fun best_tac ctxt cs =
+ SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
(*Using a "safe" rule to instantiate variables is unsafe. This tactic
allows backtracking from "safe" rules to "unsafe" rules here.*)
-fun slow_step_tac (cs as (CS{haz_brls,...})) i =
- safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
+fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i =
+ safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
end;
end;
--- a/src/FOLP/ex/Classical.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Classical.thy Sun Nov 09 17:04:14 2014 +0100
@@ -10,14 +10,14 @@
begin
schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*If and only if*)
schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
schematic_lemma "?p : ~ (P <-> ~P)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*Sample problems from
@@ -33,134 +33,134 @@
text "Pelletier's examples"
(*1*)
schematic_lemma "?p : (P-->Q) <-> (~Q --> ~P)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*2*)
schematic_lemma "?p : ~ ~ P <-> P"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*3*)
schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*4*)
schematic_lemma "?p : (~P-->Q) <-> (~Q --> P)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*5*)
schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*6*)
schematic_lemma "?p : P | ~ P"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*7*)
schematic_lemma "?p : P | ~ ~ ~ P"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*8. Peirce's law*)
schematic_lemma "?p : ((P-->Q) --> P) --> P"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*9*)
schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*10*)
schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
schematic_lemma "?p : P<->P"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*12. "Dijkstra's law"*)
schematic_lemma "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*13. Distributive law*)
schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*14*)
schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*15*)
schematic_lemma "?p : (P --> Q) <-> (~P | Q)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*16*)
schematic_lemma "?p : (P-->Q) | (Q-->P)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
(*17*)
schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Classical Logic: examples with quantifiers"
schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
schematic_lemma "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
schematic_lemma "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
schematic_lemma "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problems requiring quantifier duplication"
(*Needs multiple instantiation of ALL.*)
schematic_lemma "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
(*Needs double instantiation of the quantifier*)
schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Hard examples with quantifiers"
text "Problem 18"
schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 19"
schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 20"
schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
--> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 21"
schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 22"
schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 23"
schematic_lemma "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 24"
schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
(~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
--> (EX x. P(x)&R(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 25"
schematic_lemma "?p : (EX x. P(x)) &
@@ -174,7 +174,7 @@
schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &
(ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
--> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 27"
schematic_lemma "?p : (EX x. P(x) & ~Q(x)) &
@@ -182,49 +182,49 @@
(ALL x. M(x) & L(x) --> P(x)) &
((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
--> (ALL x. M(x) --> ~L(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 28. AMENDED"
schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &
((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
((EX x. S(x)) --> (ALL x. L(x) --> M(x)))
--> (ALL x. P(x) & L(x) --> M(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 29. Essentially the same as Principia Mathematica *11.71"
schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))
--> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
(ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 30"
schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &
(ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
--> (ALL x. S(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 31"
schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &
(EX x. L(x) & P(x)) &
(ALL x. ~ R(x) --> M(x))
--> (EX x. L(x) & M(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 32"
schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
(ALL x. S(x) & R(x) --> L(x)) &
(ALL x. M(x) --> R(x))
--> (ALL x. P(x) & M(x) --> L(x))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 33"
schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <->
(ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 35"
schematic_lemma "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 36"
schematic_lemma
@@ -232,7 +232,7 @@
(ALL x. EX y. G(x,y)) &
(ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
--> (ALL x. EX y. H(x,y))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 37"
schematic_lemma "?p : (ALL z. EX w. ALL x. EX y.
@@ -240,63 +240,63 @@
(ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &
((EX x y. Q(x,y)) --> (ALL x. R(x,x)))
--> (ALL x. EX y. R(x,y))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 39"
schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 40. AMENDED"
schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->
~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 41"
schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))
--> ~ (EX z. ALL x. f(x,z))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 44"
schematic_lemma "?p : (ALL x. f(x) -->
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
(EX x. j(x) & (ALL y. g(y) --> h(x,y)))
--> (EX x. j(x) & ~f(x))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problems (mainly) involving equality or functions"
text "Problem 48"
schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 50"
(*What has this to do with equality?*)
schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 56"
schematic_lemma
"?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 57"
schematic_lemma
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
(ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
text "Problem 58 NOT PROVED AUTOMATICALLY"
schematic_lemma
notes f_cong = subst_context [where t = f]
shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
- by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
+ by (tactic {* fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
text "Problem 59"
schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
- by (tactic "best_tac FOLP_dup_cs 1")
+ by (tactic "best_tac @{context} FOLP_dup_cs 1")
text "Problem 60"
schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
- by (tactic "fast_tac FOLP_cs 1")
+ by (tactic "fast_tac @{context} FOLP_cs 1")
end
--- a/src/FOLP/ex/If.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/If.thy Sun Nov 09 17:04:14 2014 +0100
@@ -9,7 +9,7 @@
assumes "!!x. x : P ==> f(x) : Q" "!!x. x : ~P ==> g(x) : R"
shows "?p : if(P,Q,R)"
apply (unfold if_def)
-apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
+apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *})
done
schematic_lemma ifE:
@@ -19,7 +19,7 @@
shows "?p : S"
apply (insert 1)
apply (unfold if_def)
-apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
+apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
done
schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
@@ -33,11 +33,11 @@
ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
-apply (tactic {* fast_tac if_cs 1 *})
+apply (tactic {* fast_tac @{context} if_cs 1 *})
done
schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-apply (tactic {* fast_tac if_cs 1 *})
+apply (tactic {* fast_tac @{context} if_cs 1 *})
done
end
--- a/src/FOLP/ex/Intro.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Intro.thy Sun Nov 09 17:04:14 2014 +0100
@@ -45,13 +45,13 @@
schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
--> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
-apply (tactic {* fast_tac FOLP_cs 1 *})
+apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
done
schematic_lemma "?p : ALL x. P(x,f(x)) <->
(EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-apply (tactic {* fast_tac FOLP_cs 1 *})
+apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
done
--- a/src/FOLP/ex/Propositional_Cla.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Propositional_Cla.thy Sun Nov 09 17:04:14 2014 +0100
@@ -12,106 +12,106 @@
text "commutative laws of & and | "
schematic_lemma "?p : P & Q --> Q & P"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : P | Q --> Q | P"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "associative laws of & and | "
schematic_lemma "?p : (P & Q) & R --> P & (Q & R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P | Q) | R --> P | (Q | R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "distributive laws of & and | "
schematic_lemma "?p : (P & Q) | R --> (P | R) & (Q | R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "Laws involving implication"
schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "Propositions-as-types"
(*The combinator K*)
schematic_lemma "?p : P --> (Q --> P)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*The combinator S*)
schematic_lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*Converse is classical*)
schematic_lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "Schwichtenberg's examples (via T. Nipkow)"
schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
--> ((P --> Q) --> P) --> P"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)
--> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)
--> (((P8 --> P2) --> P9) --> P3 --> P10)
--> (P1 --> P8) --> P6 --> P7
--> (((P3 --> P2) --> P9) --> P4)
--> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)
--> (((P3 --> P2) --> P9) --> P4)
--> (((P6 --> P1) --> P2) --> P9)
--> (((P7 --> P1) --> P10) --> P4 --> P5)
--> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
end
--- a/src/FOLP/ex/Quantifiers_Cla.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Quantifiers_Cla.thy Sun Nov 09 17:04:14 2014 +0100
@@ -11,91 +11,91 @@
begin
schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*Converse is false*)
schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "Some harder ones"
schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*Converse is false*)
schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "Basic test of quantifier reasoning"
(*TRUE*)
schematic_lemma "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "The following should fail, as they are false!"
schematic_lemma "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
- apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+ apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
oops
schematic_lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))"
- apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+ apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
oops
schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
- apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+ apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
oops
schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
- apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+ apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
oops
text "Back to things that are provable..."
schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*An example of why exI should be delayed as long as possible*)
schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
text "Some slow ones"
(*Principia Mathematica *11.53 *)
schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*Principia Mathematica *11.55 *)
schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
(*Principia Mathematica *11.61 *)
schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
- by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+ by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
end
--- a/src/HOL/HOL.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOL.thy Sun Nov 09 17:04:14 2014 +0100
@@ -1463,7 +1463,7 @@
val equal_def = @{thm induct_equal_def}
fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
| dest_def _ = NONE
- val trivial_tac = match_tac @{thms induct_trueI}
+ fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
)
*}
--- a/src/HOL/HOLCF/Cfun.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Sun Nov 09 17:04:14 2014 +0100
@@ -148,7 +148,7 @@
val tr = instantiate' [SOME T, SOME U] [SOME f]
(mk_meta_eq @{thm Abs_cfun_inverse2});
val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
- val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
+ val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
in SOME (perhaps (SINGLE (tac 1)) tr) end
*}
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Sun Nov 09 17:04:14 2014 +0100
@@ -391,7 +391,6 @@
subsection "input_enabledness and par"
-
(* ugly case distinctions. Heart of proof:
1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
@@ -400,7 +399,7 @@
==> input_enabled (A||B)"
apply (unfold input_enabled_def)
apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac @{theory_context Fun}")
+apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
apply (simp add: inp_is_act)
prefer 2
apply (simp add: inp_is_act)
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Sun Nov 09 17:04:14 2014 +0100
@@ -297,7 +297,8 @@
fun mkex_induct_tac ctxt sch exA exB =
EVERY'[Seq_induct_tac ctxt sch defs,
asm_full_simp_tac ctxt,
- SELECT_GOAL (safe_tac @{theory_context Fun}),
+ SELECT_GOAL
+ (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
Seq_case_simp_tac ctxt exA,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ctxt,
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Nov 09 17:04:14 2014 +0100
@@ -151,9 +151,9 @@
let
val prop = mk_trp (mk_cont functional)
val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
- val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
+ fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1
in
- Goal.prove_global thy [] [] prop (K tac)
+ Goal.prove_global thy [] [] prop (tac o #context)
end
val tuple_unfold_thm =
--- a/src/HOL/HOLCF/Tools/fixrec.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Sun Nov 09 17:04:14 2014 +0100
@@ -131,7 +131,7 @@
"The error occurred for the goal statement:\n" ^
Syntax.string_of_term lthy prop)
val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
- val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)))
+ val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac lthy (rev rules)))
val slow_tac = SOLVED' (simp_tac lthy)
val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
in
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Sun Nov 09 17:04:14 2014 +0100
@@ -80,7 +80,7 @@
fun prove_rhs ctxt def lhs =
Old_Z3_Proof_Tools.by_tac ctxt (
CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
- THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
+ THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sun Nov 09 17:04:14 2014 +0100
@@ -412,17 +412,17 @@
@{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
@{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
- fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
+ fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
rtac thm ORELSE'
- (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
- (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
+ (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
+ (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
- fun nnf_quant_tac_varified vars eq =
- nnf_quant_tac (Old_Z3_Proof_Tools.varify vars eq)
+ fun nnf_quant_tac_varified ctxt vars eq =
+ nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq)
fun nnf_quant ctxt vars qs p ct =
Old_Z3_Proof_Tools.as_meta_eq ct
- |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
+ |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs)
fun prove_nnf ctxt = try_apply ctxt [] [
named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq,
@@ -555,7 +555,7 @@
val thm = meta_eq_of p
val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules
val cu = Old_Z3_Proof_Tools.as_meta_eq ct
- val tac = REPEAT_ALL_NEW (match_tac rules')
+ val tac = REPEAT_ALL_NEW (match_tac ctxt rules')
in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end
end
@@ -577,15 +577,15 @@
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
- fun elim_unused_tac i st = (
- match_tac [@{thm refl}]
- ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+ fun elim_unused_tac ctxt i st = (
+ match_tac ctxt [@{thm refl}]
+ ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
ORELSE' (
- match_tac [@{thm iff_allI}, @{thm iff_exI}]
- THEN' elim_unused_tac)) i st
+ match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
+ THEN' elim_unused_tac ctxt)) i st
in
-fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt elim_unused_tac
+fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt)
end
@@ -601,7 +601,7 @@
val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
in
fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
- REPEAT_ALL_NEW (match_tac [rule])
+ REPEAT_ALL_NEW (match_tac ctxt [rule])
THEN' rtac @{thm excluded_middle})
end
--- a/src/HOL/NSA/transfer.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/NSA/transfer.ML Sun Nov 09 17:04:14 2014 +0100
@@ -62,10 +62,10 @@
val tac =
rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
- match_tac [transitive_thm] 1 THEN
+ match_tac ctxt [transitive_thm] 1 THEN
resolve_tac [@{thm transfer_start}] 1 THEN
REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
- match_tac [reflexive_thm] 1
+ match_tac ctxt [reflexive_thm] 1
in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
fun transfer_tac ctxt ths =
--- a/src/HOL/Nominal/nominal_induct.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Nov 09 17:04:14 2014 +0100
@@ -127,7 +127,7 @@
(rtac (rename_params_rule false [] rule') i THEN
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
THEN_ALL_NEW_CASES
- ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
+ ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
else K all_tac)
THEN_ALL_NEW Induct.rulify_tac ctxt)
end;
--- a/src/HOL/Tools/Meson/meson.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Sun Nov 09 17:04:14 2014 +0100
@@ -40,8 +40,8 @@
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
val safe_best_meson_tac: Proof.context -> int -> tactic
val depth_meson_tac: Proof.context -> int -> tactic
- val prolog_step_tac': thm list -> int -> tactic
- val iter_deepen_prolog_tac: thm list -> tactic
+ val prolog_step_tac': Proof.context -> thm list -> int -> tactic
+ val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
val make_meta_clause: thm -> thm
val make_meta_clauses: thm list -> thm list
@@ -741,17 +741,17 @@
(*This version does only one inference per call;
having only one eq_assume_tac speeds it up!*)
-fun prolog_step_tac' horns =
+fun prolog_step_tac' ctxt horns =
let val (horn0s, _) = (*0 subgoals vs 1 or more*)
take_prefix Thm.no_prems horns
val nrtac = net_resolve_tac horns
in fn i => eq_assume_tac i ORELSE
- match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*)
+ match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*)
((assume_tac i APPEND nrtac i) THEN check_tac)
end;
-fun iter_deepen_prolog_tac horns =
- ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
+fun iter_deepen_prolog_tac ctxt horns =
+ ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);
fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
(fn cls =>
@@ -766,7 +766,7 @@
["clauses:"] @ map (Display.string_of_thm ctxt) horns))
in
THEN_ITER_DEEPEN iter_deepen_limit
- (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
+ (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
end));
fun meson_tac ctxt ths =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 09 17:04:14 2014 +0100
@@ -742,7 +742,7 @@
THEN rename_tac outer_param_names 1
THEN copy_prems_tac (map snd ax_counts) [] 1)
THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
- THEN match_tac [prems_imp_false] 1
+ THEN match_tac ctxt' [prems_imp_false] 1
THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
THEN rotate_tac (rotation_of_subgoal i) i
THEN PRIMITIVE (unify_first_prem_with_concl thy i)
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Nov 09 17:04:14 2014 +0100
@@ -471,14 +471,14 @@
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
-fun elim_unused_tac i st = (
- match_tac [@{thm refl}]
- ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+fun elim_unused_tac ctxt i st = (
+ match_tac ctxt [@{thm refl}]
+ ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
ORELSE' (
- match_tac [@{thm iff_allI}, @{thm iff_exI}]
- THEN' elim_unused_tac)) i st
+ match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
+ THEN' elim_unused_tac ctxt)) i st
-fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
+fun elim_unused ctxt _ t = prove ctxt t elim_unused_tac
(* destructive equality resolution *)
--- a/src/HOL/Tools/simpdata.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML Sun Nov 09 17:04:14 2014 +0100
@@ -120,9 +120,9 @@
reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
fun sol_tac i =
FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
- (match_tac intros THEN_ALL_NEW sol_tac) i
+ (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
in
- (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
+ (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
end;
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
@@ -130,9 +130,9 @@
(*No premature instantiation of variables during simplification*)
fun safe_solver_tac ctxt =
- (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
- FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
- eq_assume_tac, ematch_tac @{thms FalseE}];
+ (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN'
+ FIRST' [match_tac ctxt (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
+ eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
val safe_solver = mk_solver "HOL safe" safe_solver_tac;
--- a/src/Provers/blast.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/blast.ML Sun Nov 09 17:04:14 2014 +0100
@@ -488,8 +488,8 @@
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
-fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
-fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
+fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac ctxt [rl]);
+fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac ctxt [rl]);
(*Tableau rule from elimination rule.
Flag "upd" says that the inference updated the branch.
@@ -781,8 +781,8 @@
exception PROVE;
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
-val contr_tac = ematch_tac [Data.notE] THEN'
- (eq_assume_tac ORELSE' assume_tac);
+fun contr_tac ctxt =
+ ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac);
(*Try to unify complementary literals and return the corresponding tactic. *)
fun tryClose state (G, L) =
@@ -795,8 +795,8 @@
in
if isGoal G then close (arg G) L eAssume_tac
else if isGoal L then close G (arg L) eAssume_tac
- else if isNot G then close (arg G) L eContr_tac
- else if isNot L then close G (arg L) eContr_tac
+ else if isNot G then close (arg G) L (eContr_tac ctxt)
+ else if isNot L then close G (arg L) (eContr_tac ctxt)
else NONE
end;
--- a/src/Provers/classical.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/classical.ML Sun Nov 09 17:04:14 2014 +0100
@@ -75,7 +75,7 @@
val dup_elim: thm -> thm
val dup_intr: thm -> thm
val dup_step_tac: Proof.context -> int -> tactic
- val eq_mp_tac: int -> tactic
+ val eq_mp_tac: Proof.context -> int -> tactic
val haz_step_tac: Proof.context -> int -> tactic
val joinrules: thm list * thm list -> (bool * thm) list
val mp_tac: int -> tactic
@@ -187,7 +187,7 @@
fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
(*Like mp_tac but instantiates no variables*)
-fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
+fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [Data.swap]);
@@ -689,10 +689,14 @@
fun ctxt addafter (name, tac2) =
ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
-fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
-fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
-fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
-fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
+fun ctxt addD2 (name, thm) =
+ ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
+fun ctxt addE2 (name, thm) =
+ ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
+fun ctxt addSD2 (name, thm) =
+ ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
+fun ctxt addSE2 (name, thm) =
+ ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac);
@@ -704,7 +708,7 @@
appSWrappers ctxt
(FIRST'
[eq_assume_tac,
- eq_mp_tac,
+ eq_mp_tac ctxt,
bimatch_from_nets_tac safe0_netpair,
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
bimatch_from_nets_tac safep_netpair])
@@ -727,24 +731,24 @@
fun n_bimatch_from_nets_tac n =
biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
-fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
-val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
+fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
+fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
(*Two-way branching is allowed only if one of the branches immediately closes*)
-fun bimatch2_tac netpair i =
+fun bimatch2_tac ctxt netpair i =
n_bimatch_from_nets_tac 2 netpair i THEN
- (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
+ (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
(*Attack subgoals using safe inferences -- matching, not resolution*)
fun clarify_step_tac ctxt =
let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
appSWrappers ctxt
(FIRST'
- [eq_assume_contr_tac,
+ [eq_assume_contr_tac ctxt,
bimatch_from_nets_tac safe0_netpair,
FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
n_bimatch_from_nets_tac 1 safep_netpair,
- bimatch2_tac safep_netpair])
+ bimatch2_tac ctxt safep_netpair])
end;
fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
--- a/src/Provers/hypsubst.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/hypsubst.ML Sun Nov 09 17:04:14 2014 +0100
@@ -223,7 +223,7 @@
discarding equalities on Bound variables
and on Free variables if thin=true*)
fun hyp_subst_tac_thin thin ctxt =
- REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
+ REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl],
gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
if thin then thin_free_eq_tac else K no_tac];
--- a/src/Pure/Isar/class_declaration.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML Sun Nov 09 17:04:14 2014 +0100
@@ -94,11 +94,11 @@
val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
val axclass_intro = #intro (Axclass.get_info thy class);
val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
- val tac =
+ fun tac ctxt =
REPEAT (SOMEGOAL
- (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
+ (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
ORELSE' assume_tac));
- val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
+ val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
--- a/src/Pure/Isar/method.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/Isar/method.ML Sun Nov 09 17:04:14 2014 +0100
@@ -18,8 +18,8 @@
val SIMPLE_METHOD': (int -> tactic) -> method
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
val cheating: Proof.context -> bool -> method
- val intro: thm list -> method
- val elim: thm list -> method
+ val intro: Proof.context -> thm list -> method
+ val elim: Proof.context -> thm list -> method
val unfold: thm list -> Proof.context -> method
val fold: thm list -> Proof.context -> method
val atomize: bool -> Proof.context -> method
@@ -127,8 +127,8 @@
(* unfold intro/elim rules *)
-fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
-fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
+fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths));
+fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths));
(* unfold/fold definitions *)
@@ -590,9 +590,9 @@
"do nothing (insert current facts only)" #>
setup @{binding insert} (Attrib.thms >> (K o insert))
"insert theorems, ignoring facts (improper)" #>
- setup @{binding intro} (Attrib.thms >> (K o intro))
+ setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
"repeatedly apply introduction rules" #>
- setup @{binding elim} (Attrib.thms >> (K o elim))
+ setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
"repeatedly apply elimination rules" #>
setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
--- a/src/Pure/simplifier.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/simplifier.ML Sun Nov 09 17:04:14 2014 +0100
@@ -389,7 +389,7 @@
(*no premature instantiation of variables during simplification*)
fun safe_solver_tac ctxt =
- FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+ FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
val safe_solver = mk_solver "easy safe" safe_solver_tac;
fun mk_eq thm =
--- a/src/Pure/tactic.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/tactic.ML Sun Nov 09 17:04:14 2014 +0100
@@ -24,10 +24,10 @@
val ftac: thm -> int -> tactic
val ares_tac: thm list -> int -> tactic
val solve_tac: thm list -> int -> tactic
- val bimatch_tac: (bool * thm) list -> int -> tactic
- val match_tac: thm list -> int -> tactic
- val ematch_tac: thm list -> int -> tactic
- val dmatch_tac: thm list -> int -> tactic
+ val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
+ val match_tac: Proof.context -> thm list -> int -> tactic
+ val ematch_tac: Proof.context -> thm list -> int -> tactic
+ val dmatch_tac: Proof.context -> thm list -> int -> tactic
val flexflex_tac: Proof.context -> tactic
val distinct_subgoal_tac: int -> tactic
val distinct_subgoals_tac: tactic
@@ -146,10 +146,10 @@
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
(*Matching tactics -- as above, but forbid updating of state*)
-fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution NONE true brules i);
-fun match_tac rules = bimatch_tac (map (pair false) rules);
-fun ematch_tac rules = bimatch_tac (map (pair true) rules);
-fun dmatch_tac rls = ematch_tac (map make_elim rls);
+fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i);
+fun match_tac ctxt rules = bimatch_tac ctxt (map (pair false) rules);
+fun ematch_tac ctxt rules = bimatch_tac ctxt (map (pair true) rules);
+fun dmatch_tac ctxt rls = ematch_tac ctxt (map make_elim rls);
(*Smash all flex-flex disagreement pairs in the proof state.*)
fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));
--- a/src/Sequents/simpdata.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Sequents/simpdata.ML Sun Nov 09 17:04:14 2014 +0100
@@ -62,7 +62,8 @@
(*No premature instantiation of variables during simplification*)
fun safe_solver ctxt =
- FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ctxt) i), eq_assume_tac];
+ FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i),
+ eq_assume_tac];
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
--- a/src/Tools/induct.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Tools/induct.ML Sun Nov 09 17:04:14 2014 +0100
@@ -12,7 +12,7 @@
val rulify_fallback: thm list
val equal_def: thm
val dest_def: term -> (term * term) option
- val trivial_tac: int -> tactic
+ val trivial_tac: Proof.context -> int -> tactic
end;
signature INDUCT =
@@ -67,7 +67,7 @@
val rulify_tac: Proof.context -> int -> tactic
val simplified_rule: Proof.context -> thm -> thm
val simplify_tac: Proof.context -> int -> tactic
- val trivial_tac: int -> tactic
+ val trivial_tac: Proof.context -> int -> tactic
val rotate_tac: int -> int -> int -> tactic
val internalize: Proof.context -> int -> thm -> thm
val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
@@ -513,7 +513,7 @@
CASES (Rule_Cases.make_common (thy,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
- (if simp then TRY o trivial_tac else K all_tac)) i) st
+ (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
end)
end;
@@ -810,7 +810,7 @@
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
end)
THEN_ALL_NEW_CASES
- ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
+ ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
THEN_ALL_NEW rulify_tac ctxt);
val induct_tac = gen_induct_tac (K I);
--- a/src/Tools/intuitionistic.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Tools/intuitionistic.ML Sun Nov 09 17:04:14 2014 +0100
@@ -17,13 +17,13 @@
local
-val remdups_tac = SUBGOAL (fn (g, i) =>
+fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
let val prems = Logic.strip_assums_hyp g in
REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
- (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+ (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
end);
-fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
+fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
@@ -39,8 +39,8 @@
bires_tac false (Context_Rules.netpair ctxt));
fun step_tac ctxt i =
- REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
- REMDUPS (unsafe_step_tac ctxt) i;
+ REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
+ REMDUPS unsafe_step_tac ctxt i;
fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
if d > lim then no_tac