# HG changeset patch # User wenzelm # Date 1415549054 -3600 # Node ID c9e744ea8a3815a4d7a6aa3ab6a0ed14b0c0b09d # Parent a816aa3ff391152e714a2774729ee29b99ab8f62 proper context for match_tac etc.; diff -r a816aa3ff391 -r c9e744ea8a38 NEWS --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/CCL/Wfd.thy --- 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) diff -r a816aa3ff391 -r c9e744ea8a38 src/Doc/Implementation/Tactic.thy --- 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} diff -r a816aa3ff391 -r c9e744ea8a38 src/FOL/FOL.thy --- 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 ); *} diff -r a816aa3ff391 -r c9e744ea8a38 src/FOL/intprover.ML --- 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); diff -r a816aa3ff391 -r c9e744ea8a38 src/FOL/simpdata.ML --- 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 = diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/FOLP.thy --- 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" diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/classical.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; diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Classical.thy --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/If.thy --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Intro.thy --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Propositional_Cla.thy --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Quantifiers_Cla.thy --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOL.thy --- 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} ) *} diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/Cfun.thy --- 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 *} diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- 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) diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- 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, diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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 = diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/Tools/fixrec.ML --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML --- 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])) diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- 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 diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/NSA/transfer.ML --- 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 = diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Nominal/nominal_induct.ML --- 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; diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/Meson/meson.ML --- 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 = diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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) diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/SMT/z3_replay_methods.ML --- 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 *) diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/simpdata.ML --- 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; diff -r a816aa3ff391 -r c9e744ea8a38 src/Provers/blast.ML --- 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; diff -r a816aa3ff391 -r c9e744ea8a38 src/Provers/classical.ML --- 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)); diff -r a816aa3ff391 -r c9e744ea8a38 src/Provers/hypsubst.ML --- 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]; diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/Isar/class_declaration.ML --- 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; diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/Isar/method.ML --- 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" #> diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/simplifier.ML --- 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 = diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/tactic.ML --- 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)); diff -r a816aa3ff391 -r c9e744ea8a38 src/Sequents/simpdata.ML --- 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 = diff -r a816aa3ff391 -r c9e744ea8a38 src/Tools/induct.ML --- 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); diff -r a816aa3ff391 -r c9e744ea8a38 src/Tools/intuitionistic.ML --- 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