# HG changeset patch # User wenzelm # Date 1415652588 -3600 # Node ID 26bf09b95dda6ae5935309154a99fe135dd442d5 # Parent 4bee6d8c15004624578a572a2201c35f2bef3c1e proper context for assume_tac (atac remains as fall-back without context); diff -r 4bee6d8c1500 -r 26bf09b95dda NEWS --- a/NEWS Sun Nov 09 20:49:28 2014 +0100 +++ b/NEWS Mon Nov 10 21:49:48 2014 +0100 @@ -190,8 +190,9 @@ *** ML *** -* Proper context for various elementary tactics: match_tac, compose_tac, -Splitter.split_tac etc. Minor INCOMPATIBILITY. +* Proper context for various elementary tactics: assume_tac, +match_tac, compose_tac, Splitter.split_tac etc. Minor +INCOMPATIBILITY. * Tactical PARALLEL_ALLGOALS is the most common way to refer to PARALLEL_GOALS. diff -r 4bee6d8c1500 -r 26bf09b95dda src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CCL/Wfd.thy Mon Nov 10 21:49:48 2014 +0100 @@ -48,7 +48,7 @@ ML {* fun wfd_strengthen_tac ctxt s i = - res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) + res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1) *} lemma wf_anti_sym: "[| Wfd(r); :r; :r |] ==> P" diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/Arith.thy --- a/src/CTT/Arith.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/Arith.thy Mon Nov 10 21:49:48 2014 +0100 @@ -54,12 +54,12 @@ lemma add_typing: "[| a:N; b:N |] ==> a #+ b : N" apply (unfold arith_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done lemma add_typingL: "[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N" apply (unfold arith_defs) -apply (tactic "equal_tac []") +apply (tactic "equal_tac @{context} []") done @@ -67,12 +67,12 @@ lemma addC0: "b:N ==> 0 #+ b = b : N" apply (unfold arith_defs) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done lemma addC_succ: "[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N" apply (unfold arith_defs) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done @@ -82,24 +82,24 @@ lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N" apply (unfold arith_defs) -apply (tactic {* typechk_tac [@{thm add_typing}] *}) +apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *}) done lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N" apply (unfold arith_defs) -apply (tactic {* equal_tac [@{thm add_typingL}] *}) +apply (tactic {* equal_tac @{context} [@{thm add_typingL}] *}) done (*computation for mult: 0 and successor cases*) lemma multC0: "b:N ==> 0 #* b = 0 : N" apply (unfold arith_defs) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done lemma multC_succ: "[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N" apply (unfold arith_defs) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done @@ -109,12 +109,12 @@ lemma diff_typing: "[| a:N; b:N |] ==> a - b : N" apply (unfold arith_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done lemma diff_typingL: "[| a=c:N; b=d:N |] ==> a - b = c - d : N" apply (unfold arith_defs) -apply (tactic "equal_tac []") +apply (tactic "equal_tac @{context} []") done @@ -122,7 +122,7 @@ lemma diffC0: "a:N ==> a - 0 = a : N" apply (unfold arith_defs) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done (*Note: rec(a, 0, %z w.z) is pred(a). *) @@ -130,7 +130,7 @@ lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N" apply (unfold arith_defs) apply (tactic {* NE_tac @{context} "b" 1 *}) -apply (tactic "hyp_rew_tac []") +apply (tactic "hyp_rew_tac @{context} []") done @@ -138,9 +138,9 @@ succ(a) - succ(b) rewrites to pred(succ(a) - b) *) lemma diff_succ_succ: "[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N" apply (unfold arith_defs) -apply (tactic "hyp_rew_tac []") +apply (tactic "hyp_rew_tac @{context} []") apply (tactic {* NE_tac @{context} "b" 1 *}) -apply (tactic "hyp_rew_tac []") +apply (tactic "hyp_rew_tac @{context} []") done @@ -173,11 +173,11 @@ local val congr_rls = @{thms congr_rls} in -fun arith_rew_tac prems = make_rew_tac - (Arith_simp.norm_tac(congr_rls, prems)) +fun arith_rew_tac ctxt prems = make_rew_tac ctxt + (Arith_simp.norm_tac ctxt (congr_rls, prems)) -fun hyp_arith_rew_tac prems = make_rew_tac - (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems)) +fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt + (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems)) end *} @@ -188,7 +188,7 @@ (*Associative law for addition*) lemma add_assoc: "[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") done @@ -196,11 +196,11 @@ Must simplify after first induction! Orientation of rewrites is delicate*) lemma add_commute: "[| a:N; b:N |] ==> a #+ b = b #+ a : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") apply (tactic {* NE_tac @{context} "b" 2 *}) apply (rule sym_elem) apply (tactic {* NE_tac @{context} "b" 1 *}) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") done @@ -209,32 +209,32 @@ (*right annihilation in product*) lemma mult_0_right: "a:N ==> a #* 0 = 0 : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") done (*right successor law for multiplication*) lemma mult_succ_right: "[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *}) +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *}) apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ done (*Commutative law for multiplication*) lemma mult_commute: "[| a:N; b:N |] ==> a #* b = b #* a : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *}) +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm mult_0_right}, @{thm mult_succ_right}] *}) done (*addition distributes over multiplication*) lemma add_mult_distrib: "[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *}) +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *}) done (*Associative law for multiplication*) lemma mult_assoc: "[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *}) +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_mult_distrib}] *}) done @@ -246,7 +246,7 @@ lemma diff_self_eq_0: "a:N ==> a - a = 0 : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") done @@ -263,15 +263,15 @@ apply (rule_tac [3] intr_rls) (*case analysis on x in (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *) -apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4") +apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac @{context} 4") (*Prepare for simplification of types -- the antecedent succ(u)<=x *) apply (rule_tac [5] replace_type) apply (rule_tac [4] replace_type) -apply (tactic "arith_rew_tac []") +apply (tactic "arith_rew_tac @{context} []") (*Solves first 0 goal, simplifies others. Two sugbgoals remain. Both follow by rewriting, (2) using quantified induction hyp*) -apply (tactic "intr_tac []") (*strips remaining PRODs*) -apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *}) +apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*) +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *}) apply assumption done @@ -293,46 +293,46 @@ lemma absdiff_typing: "[| a:N; b:N |] ==> a |-| b : N" apply (unfold arith_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done lemma absdiff_typingL: "[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N" apply (unfold arith_defs) -apply (tactic "equal_tac []") +apply (tactic "equal_tac @{context} []") done lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N" apply (unfold absdiff_def) -apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *}) +apply (tactic {* arith_rew_tac @{context} [@{thm diff_self_eq_0}] *}) done lemma absdiffC0: "a:N ==> 0 |-| a = a : N" apply (unfold absdiff_def) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") done lemma absdiff_succ_succ: "[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N" apply (unfold absdiff_def) -apply (tactic "hyp_arith_rew_tac []") +apply (tactic "hyp_arith_rew_tac @{context} []") done (*Note how easy using commutative laws can be? ...not always... *) lemma absdiff_commute: "[| a:N; b:N |] ==> a |-| b = b |-| a : N" apply (unfold absdiff_def) apply (rule add_commute) -apply (tactic {* typechk_tac [@{thm diff_typing}] *}) +apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *}) done (*If a+b=0 then a=0. Surprisingly tedious*) schematic_lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" apply (tactic {* NE_tac @{context} "a" 1 *}) apply (rule_tac [3] replace_type) -apply (tactic "arith_rew_tac []") -apply (tactic "intr_tac []") (*strips remaining PRODs*) +apply (tactic "arith_rew_tac @{context} []") +apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*) apply (rule_tac [2] zero_ne_succ [THEN FE]) apply (erule_tac [3] EqE [THEN sym_elem]) -apply (tactic {* typechk_tac [@{thm add_typing}] *}) +apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *}) done (*Version of above with the premise a+b=0. @@ -341,7 +341,7 @@ apply (rule EqE) apply (rule add_eq0_lemma [THEN ProdE]) apply (rule_tac [3] EqI) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *) @@ -349,12 +349,12 @@ "[| a:N; b:N; a |-| b = 0 : N |] ==> ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)" apply (unfold absdiff_def) -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (rule_tac [2] add_eq0) apply (rule add_eq0) apply (rule_tac [6] add_commute [THEN trans_elem]) -apply (tactic {* typechk_tac [@{thm diff_typing}] *}) +apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *}) done (*if a |-| b = 0 then a = b @@ -362,11 +362,11 @@ lemma absdiff_eq0: "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N" apply (rule EqE) apply (rule absdiff_eq0_lem [THEN SumE]) -apply (tactic "TRYALL assume_tac") -apply (tactic eqintr_tac) +apply (tactic "TRYALL (assume_tac @{context})") +apply (tactic "eqintr_tac @{context}") apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) -apply (rule_tac [3] EqE, tactic "assume_tac 3") -apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *}) +apply (rule_tac [3] EqE, tactic "assume_tac @{context} 3") +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *}) done @@ -376,12 +376,12 @@ lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N" apply (unfold mod_def) -apply (tactic {* typechk_tac [@{thm absdiff_typing}] *}) +apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}] *}) done lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N" apply (unfold mod_def) -apply (tactic {* equal_tac [@{thm absdiff_typingL}] *}) +apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}] *}) done @@ -389,13 +389,13 @@ lemma modC0: "b:N ==> 0 mod b = 0 : N" apply (unfold mod_def) -apply (tactic {* rew_tac [@{thm absdiff_typing}] *}) +apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *}) done lemma modC_succ: "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N" apply (unfold mod_def) -apply (tactic {* rew_tac [@{thm absdiff_typing}] *}) +apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *}) done @@ -403,12 +403,12 @@ lemma div_typing: "[| a:N; b:N |] ==> a div b : N" apply (unfold div_def) -apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *}) +apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}, @{thm mod_typing}] *}) done lemma div_typingL: "[| a=c:N; b=d:N |] ==> a div b = c div d : N" apply (unfold div_def) -apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *}) +apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}, @{thm mod_typingL}] *}) done lemmas div_typing_rls = mod_typing div_typing absdiff_typing @@ -418,14 +418,14 @@ lemma divC0: "b:N ==> 0 div b = 0 : N" apply (unfold div_def) -apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *}) +apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm absdiff_typing}] *}) done lemma divC_succ: "[| a:N; b:N |] ==> succ(a) div b = rec(succ(a) mod b, succ(a div b), %x y. a div b) : N" apply (unfold div_def) -apply (tactic {* rew_tac [@{thm mod_typing}] *}) +apply (tactic {* rew_tac @{context} [@{thm mod_typing}] *}) done @@ -433,9 +433,9 @@ lemma divC_succ2: "[| a:N; b:N |] ==> succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N" apply (rule divC_succ [THEN trans_elem]) -apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *}) +apply (tactic {* rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC_succ}]) *}) apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *}) -apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *}) +apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *}) done (*for case analysis on whether a number is 0 or a successor*) @@ -444,26 +444,26 @@ apply (tactic {* NE_tac @{context} "a" 1 *}) apply (rule_tac [3] PlusI_inr) apply (rule_tac [2] PlusI_inl) -apply (tactic eqintr_tac) -apply (tactic "equal_tac []") +apply (tactic "eqintr_tac @{context}") +apply (tactic "equal_tac @{context} []") done (*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @ +apply (tactic {* arith_rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) apply (rule EqE) (*case analysis on succ(u mod b)|-|b *) apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) apply (erule_tac [3] SumE) -apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @ +apply (tactic {* hyp_arith_rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) (*Replace one occurrence of b by succ(u mod b). Clumsy!*) apply (rule add_typingL [THEN trans_elem]) apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) apply (rule_tac [3] refl_elem) -apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *}) +apply (tactic {* hyp_arith_rew_tac @{context} @{thms div_typing_rls} *}) done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/Bool.thy --- a/src/CTT/Bool.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/Bool.thy Mon Nov 10 21:49:48 2014 +0100 @@ -33,7 +33,7 @@ (*formation rule*) lemma boolF: "Bool type" apply (unfold bool_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done @@ -41,21 +41,21 @@ lemma boolI_true: "true : Bool" apply (unfold bool_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done lemma boolI_false: "false : Bool" apply (unfold bool_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done (*elimination rule: typing of cond*) lemma boolE: "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)" apply (unfold bool_defs) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") apply (erule_tac [!] TE) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done lemma boolEL: @@ -72,18 +72,18 @@ "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)" apply (unfold bool_defs) apply (rule comp_rls) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") apply (erule_tac [!] TE) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done lemma boolC_false: "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)" apply (unfold bool_defs) apply (rule comp_rls) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") apply (erule_tac [!] TE) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/CTT.thy --- a/src/CTT/CTT.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/CTT.thy Mon Nov 10 21:49:48 2014 +0100 @@ -336,11 +336,11 @@ in (*Try solving a:A or a=b:A by assumption provided a is rigid!*) -val test_assume_tac = SUBGOAL(fn (prem,i) => +fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) => if is_rigid_elem (Logic.strip_assums_concl prem) - then assume_tac i else no_tac) + then assume_tac ctxt i else no_tac) -fun ASSUME tf i = test_assume_tac i ORELSE tf i +fun ASSUME ctxt tf i = test_assume_tac ctxt i ORELSE tf i end; @@ -356,26 +356,26 @@ @{thms elimL_rls} @ @{thms refl_elem} in -fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4); +fun routine_tac rls ctxt prems = ASSUME ctxt (filt_resolve_tac (prems @ rls) 4); (*Solve all subgoals "A type" using formation rules. *) -val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac @{thms form_rls} 1)); +fun form_tac ctxt = REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac @{thms form_rls} 1)); (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *) -fun typechk_tac thms = +fun typechk_tac ctxt thms = let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3 - in REPEAT_FIRST (ASSUME tac) end + in REPEAT_FIRST (ASSUME ctxt tac) end (*Solve a:A (a flexible, A rigid) by introduction rules. Cannot use stringtrees (filt_resolve_tac) since goals like ?a:SUM(A,B) have a trivial head-string *) -fun intr_tac thms = +fun intr_tac ctxt thms = let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1 - in REPEAT_FIRST (ASSUME tac) end + in REPEAT_FIRST (ASSUME ctxt tac) end (*Equality proving: solve a=b:A (where a is rigid) by long rules. *) -fun equal_tac thms = - REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3)) +fun equal_tac ctxt thms = + REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3)) end @@ -408,7 +408,8 @@ ML {* (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification. Uses other intro rules to avoid changing flexible goals.*) -val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1)) +fun eqintr_tac ctxt = + REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1)) (** Tactics that instantiate CTT-rules. Vars in the given terms will be incremented! @@ -426,11 +427,11 @@ (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *) -fun add_mp_tac i = - rtac @{thm subst_prodE} i THEN assume_tac i THEN assume_tac i +fun add_mp_tac ctxt i = + rtac @{thm subst_prodE} i THEN assume_tac ctxt i THEN assume_tac ctxt i (*Finds P-->Q and P in the assumptions, replaces implication by Q *) -fun mp_tac i = etac @{thm subst_prodE} i THEN assume_tac i +fun mp_tac ctxt i = etac @{thm subst_prodE} i THEN assume_tac ctxt i (*"safe" when regarded as predicate calculus rules*) val safe_brls = sort (make_ord lessb) @@ -445,18 +446,18 @@ val (safe0_brls, safep_brls) = List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls -fun safestep_tac thms i = - form_tac ORELSE +fun safestep_tac ctxt thms i = + form_tac ctxt ORELSE resolve_tac thms i ORELSE - biresolve_tac safe0_brls i ORELSE mp_tac i ORELSE + biresolve_tac safe0_brls i ORELSE mp_tac ctxt i ORELSE DETERM (biresolve_tac safep_brls i) -fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i) +fun safe_tac ctxt thms i = DEPTH_SOLVE_1 (safestep_tac ctxt thms i) -fun step_tac thms = safestep_tac thms ORELSE' biresolve_tac unsafe_brls +fun step_tac ctxt thms = safestep_tac ctxt thms ORELSE' biresolve_tac unsafe_brls (*Fails unless it solves the goal!*) -fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms) +fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms) *} ML_file "rew.ML" @@ -479,7 +480,7 @@ apply (unfold basic_defs) apply (rule major [THEN SumE]) apply (rule SumC [THEN subst_eqtyparg, THEN replace_type]) - apply (tactic {* typechk_tac @{thms assms} *}) + apply (tactic {* typechk_tac @{context} @{thms assms} *}) done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/ex/Elimination.thy --- a/src/CTT/ex/Elimination.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/ex/Elimination.thy Mon Nov 10 21:49:48 2014 +0100 @@ -15,36 +15,36 @@ text "This finds the functions fst and snd!" schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" -apply (tactic {* pc_tac [] 1 *}) +apply (tactic {* pc_tac @{context} [] 1 *}) done schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A" -apply (tactic {* pc_tac [] 1 *}) +apply (tactic {* pc_tac @{context} [] 1 *}) back done text "Double negation of the Excluded Middle" schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F" -apply (tactic "intr_tac []") +apply (tactic "intr_tac @{context} []") apply (rule ProdE) apply assumption -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done schematic_lemma "[| A type; B type |] ==> ?a : (A*B) --> (B*A)" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done (*The sequent version (ITT) could produce an interesting alternative by backtracking. No longer.*) text "Binary sums and products" schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done (*A distributive law*) schematic_lemma "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done (*more general version, same proof*) @@ -53,12 +53,12 @@ and "!!x. x:A ==> B(x) type" and "!!x. x:A ==> C(x) type" shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))" -apply (tactic {* pc_tac @{thms assms} 1 *}) +apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) done text "Construction of the currying functional" schematic_lemma "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done (*more general goal with same proof*) @@ -68,12 +68,12 @@ and "!!z. z: (SUM x:A. B(x)) ==> C(z) type" shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). (PROD x:A . PROD y:B(x) . C())" -apply (tactic {* pc_tac @{thms assms} 1 *}) +apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) done text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)" schematic_lemma "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done (*more general goal with same proof*) @@ -83,12 +83,12 @@ and "!!z. z: (SUM x:A . B(x)) ==> C(z) type" shows "?a : (PROD x:A . PROD y:B(x) . C()) --> (PROD z : (SUM x:A . B(x)) . C(z))" -apply (tactic {* pc_tac @{thms assms} 1 *}) +apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) done text "Function application" schematic_lemma "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done text "Basic test of quantifier reasoning" @@ -99,7 +99,7 @@ shows "?a : (SUM y:B . PROD x:A . C(x,y)) --> (PROD x:A . SUM y:B . C(x,y))" -apply (tactic {* pc_tac @{thms assms} 1 *}) +apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) done text "Martin-Lof (1984) pages 36-7: the combinator S" @@ -109,7 +109,7 @@ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" shows "?a : (PROD x:A. PROD y:B(x). C(x,y)) --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* pc_tac @{thms assms} 1 *}) +apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) done text "Martin-Lof (1984) page 58: the axiom of disjunction elimination" @@ -119,13 +119,13 @@ and "!!z. z: A+B ==> C(z) type" shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) --> (PROD z: A+B. C(z))" -apply (tactic {* pc_tac @{thms assms} 1 *}) +apply (tactic {* pc_tac @{context} @{thms assms} 1 *}) done (*towards AXIOM OF CHOICE*) schematic_lemma [folded basic_defs]: "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)" -apply (tactic "pc_tac [] 1") +apply (tactic "pc_tac @{context} [] 1") done @@ -137,15 +137,15 @@ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* intr_tac @{thms assms} *}) -apply (tactic "add_mp_tac 2") -apply (tactic "add_mp_tac 1") +apply (tactic {* intr_tac @{context} @{thms assms} *}) +apply (tactic "add_mp_tac @{context} 2") +apply (tactic "add_mp_tac @{context} 1") apply (erule SumE_fst) apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) apply (rule_tac [4] SumE_snd) -apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms assms}) *}) +apply (tactic {* typechk_tac @{context} (@{thm SumE_fst} :: @{thms assms}) *}) done text "Axiom of choice. Proof without fst, snd. Harder still!" @@ -155,19 +155,19 @@ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* intr_tac @{thms assms} *}) +apply (tactic {* intr_tac @{context} @{thms assms} *}) (*Must not use add_mp_tac as subst_prodE hides the construction.*) apply (rule ProdE [THEN SumE], assumption) -apply (tactic "TRYALL assume_tac") +apply (tactic "TRYALL (assume_tac @{context})") apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) apply (erule_tac [4] ProdE [THEN SumE]) -apply (tactic {* typechk_tac @{thms assms} *}) +apply (tactic {* typechk_tac @{context} @{thms assms} *}) apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) -apply (tactic {* typechk_tac @{thms assms} *}) +apply (tactic {* typechk_tac @{context} @{thms assms} *}) apply assumption done @@ -183,11 +183,11 @@ apply (tactic {* biresolve_tac safe_brls 2 *}) (*Now must convert assumption C(z) into antecedent C() *) apply (rule_tac [2] a = "y" in ProdE) -apply (tactic {* typechk_tac @{thms assms} *}) +apply (tactic {* typechk_tac @{context} @{thms assms} *}) apply (rule SumE, assumption) -apply (tactic "intr_tac []") -apply (tactic "TRYALL assume_tac") -apply (tactic {* typechk_tac @{thms assms} *}) +apply (tactic "intr_tac @{context} []") +apply (tactic "TRYALL (assume_tac @{context})") +apply (tactic {* typechk_tac @{context} @{thms assms} *}) done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/ex/Equality.thy --- a/src/CTT/ex/Equality.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/ex/Equality.thy Mon Nov 10 21:49:48 2014 +0100 @@ -12,27 +12,27 @@ lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done lemma when_eq: "[| A type; B type; p : A+B |] ==> when(p,inl,inr) = p : A + B" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done (*in the "rec" formulation of addition, 0+n=n *) lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done (*the harder version, n+0=n: recursive, uses induction hypothesis*) lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic "hyp_rew_tac []") +apply (tactic "hyp_rew_tac @{context} []") done (*Associativity of addition*) @@ -40,19 +40,19 @@ ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic "hyp_rew_tac []") +apply (tactic "hyp_rew_tac @{context} []") done (*Martin-Lof (1984) page 62: pairing is surjective*) lemma "p : Sum(A,B) ==> = p : Sum(A,B)" apply (rule EqE) apply (rule elim_rls, assumption) -apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*) +apply (tactic {* DEPTH_SOLVE_1 (rew_tac @{context} []) *}) (*!!!!!!!*) done lemma "[| a : A; b : B |] ==> (lam u. split(u, %v w.)) ` = : SUM x:B. A" -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done (*a contrived, complicated simplication, requires sum-elimination also*) @@ -61,9 +61,9 @@ apply (rule reduction_rls) apply (rule_tac [3] intrL_rls) apply (rule_tac [4] EqE) -apply (rule_tac [4] SumE, tactic "assume_tac 4") +apply (rule_tac [4] SumE, tactic "assume_tac @{context} 4") (*order of unifiers is essential here*) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/ex/Synthesis.thy --- a/src/CTT/ex/Synthesis.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/ex/Synthesis.thy Mon Nov 10 21:49:48 2014 +0100 @@ -12,21 +12,21 @@ text "discovery of predecessor function" schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0) * (PROD n:N. Eq(N, pred ` succ(n), n))" -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (rule_tac [3] reduction_rls) apply (rule_tac [5] comp_rls) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done text "the function fst as an element of a function type" schematic_lemma [folded basic_defs]: "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` , i)" -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (rule_tac [2] reduction_rls) apply (rule_tac [4] comp_rls) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") txt "now put in A everywhere" apply assumption+ done @@ -36,10 +36,10 @@ See following example.*) schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) * Eq(?A, ?b(inr(i)), )" -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (rule comp_rls) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done (*Here we allow the type to depend on i. @@ -55,13 +55,13 @@ schematic_lemma [folded basic_defs]: "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl()), i) * Eq(?A, ?b(inr()), j)" -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (rule PlusC_inl [THEN trans_elem]) apply (rule_tac [4] comp_rls) apply (rule_tac [7] reduction_rls) apply (rule_tac [10] comp_rls) -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done (*similar but allows the type to depend on i and j*) @@ -79,10 +79,10 @@ schematic_lemma [folded arith_defs]: "?c : PROD n:N. Eq(N, ?f(0,n), n) * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))" -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (rule comp_rls) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done text "The addition function -- using explicit lambdas" @@ -90,15 +90,15 @@ "?c : SUM plus : ?A . PROD x:N. Eq(N, plus`0`x, x) * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))" -apply (tactic "intr_tac []") -apply (tactic eqintr_tac) +apply (tactic "intr_tac @{context} []") +apply (tactic "eqintr_tac @{context}") apply (tactic "resolve_tac [TSimp.split_eqn] 3") -apply (tactic "SELECT_GOAL (rew_tac []) 4") +apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4") apply (tactic "resolve_tac [TSimp.split_eqn] 3") -apply (tactic "SELECT_GOAL (rew_tac []) 4") +apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4") apply (rule_tac [3] p = "y" in NC_succ) (** by (resolve_tac comp_rls 3); caused excessive branching **) -apply (tactic "rew_tac []") +apply (tactic "rew_tac @{context} []") done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/ex/Typechecking.thy --- a/src/CTT/ex/Typechecking.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/ex/Typechecking.thy Mon Nov 10 21:49:48 2014 +0100 @@ -34,34 +34,34 @@ subsection {* Multi-step proofs: Type inference *} lemma "PROD w:N. N + N type" -apply (tactic form_tac) +apply (tactic "form_tac @{context}") done schematic_lemma "<0, succ(0)> : ?A" -apply (tactic "intr_tac []") +apply (tactic "intr_tac @{context} []") done schematic_lemma "PROD w:N . Eq(?A,w,w) type" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done text "typechecking an application of fst" schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done text "typechecking the predecessor function" schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done text "typechecking the addition function" schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") done (*Proofs involving arbitrary types. @@ -69,18 +69,18 @@ ML {* val N_tac = TRYALL (rtac @{thm NF}) *} schematic_lemma "lam w. : ?A" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") apply (tactic N_tac) done schematic_lemma "lam x. lam y. x : ?A" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") apply (tactic N_tac) done text "typechecking fst (as a function object)" schematic_lemma "lam i. split(i, %j k. j) : ?A" -apply (tactic "typechk_tac []") +apply (tactic "typechk_tac @{context} []") apply (tactic N_tac) done diff -r 4bee6d8c1500 -r 26bf09b95dda src/CTT/rew.ML --- a/src/CTT/rew.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/CTT/rew.ML Mon Nov 10 21:49:48 2014 +0100 @@ -23,7 +23,7 @@ val trans_red = @{thm trans_red} val red_if_equal = @{thm red_if_equal} val default_rls = @{thms comp_rls} - val routine_tac = routine_tac (@{thms routine_rls}) + val routine_tac = routine_tac @{thms routine_rls} end; structure TSimp = TSimpFun (TSimp_data); @@ -31,12 +31,12 @@ val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls}; (*Make a rewriting tactic from a normalization tactic*) -fun make_rew_tac ntac = - TRY eqintr_tac THEN TRYALL (resolve_tac [TSimp.split_eqn]) THEN +fun make_rew_tac ctxt ntac = + TRY (eqintr_tac ctxt) THEN TRYALL (resolve_tac [TSimp.split_eqn]) THEN ntac; -fun rew_tac thms = make_rew_tac - (TSimp.norm_tac(standard_congr_rls, thms)); +fun rew_tac ctxt thms = make_rew_tac ctxt + (TSimp.norm_tac ctxt (standard_congr_rls, thms)); -fun hyp_rew_tac thms = make_rew_tac - (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms)); +fun hyp_rew_tac ctxt thms = make_rew_tac ctxt + (TSimp.cond_norm_tac ctxt (prove_cond_tac, standard_congr_rls, thms)); diff -r 4bee6d8c1500 -r 26bf09b95dda src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Doc/Implementation/Tactic.thy Mon Nov 10 21:49:48 2014 +0100 @@ -282,7 +282,7 @@ @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\ @{index_ML forward_tac: "thm list -> int -> tactic"} \\ @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex] - @{index_ML assume_tac: "int -> tactic"} \\ + @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\ @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex] @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\ @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\ @@ -324,7 +324,7 @@ elimination rules, which is useful to organize the search process systematically in proof tools. - \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i} + \item @{ML assume_tac}~@{text "ctxt i"} attempts to solve subgoal @{text i} by assumption (modulo higher-order unification). \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks diff -r 4bee6d8c1500 -r 26bf09b95dda src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Doc/Isar_Ref/Generic.thy Mon Nov 10 21:49:48 2014 +0100 @@ -1053,7 +1053,7 @@ ML \ fun subgoaler_tac ctxt = - assume_tac ORELSE' + assume_tac ctxt ORELSE' resolve_tac (Simplifier.prems_of ctxt) ORELSE' asm_simp_tac ctxt \ diff -r 4bee6d8c1500 -r 26bf09b95dda src/Doc/Tutorial/Protocol/Event.thy --- a/src/Doc/Tutorial/Protocol/Event.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Doc/Tutorial/Protocol/Event.thy Mon Nov 10 21:49:48 2014 +0100 @@ -260,10 +260,10 @@ ML {* -val analz_mono_contra_tac = +fun analz_mono_contra_tac ctxt = rtac @{thm analz_impI} THEN' REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) - THEN' mp_tac + THEN' mp_tac ctxt *} lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" @@ -285,7 +285,7 @@ intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) method_setup analz_mono_contra = {* - Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *} + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} @@ -330,7 +330,7 @@ val knows_Spy_subset_knows_Spy_Gets = @{thm knows_Spy_subset_knows_Spy_Gets}; -val synth_analz_mono_contra_tac = +fun synth_analz_mono_contra_tac ctxt = rtac @{thm syan_impI} THEN' REPEAT1 o (dresolve_tac @@ -338,11 +338,11 @@ @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) THEN' - mp_tac + mp_tac ctxt *} method_setup synth_analz_mono_contra = {* - Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *} + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *} "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" (*>*) diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOL/IFOL.thy Mon Nov 10 21:49:48 2014 +0100 @@ -208,7 +208,7 @@ (*Finds P-->Q and P in the assumptions, replaces implication by Q *) ML {* - fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN assume_tac i + fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN atac i fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i *} diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOL/intprover.ML --- a/src/FOL/intprover.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOL/intprover.ML Mon Nov 10 21:49:48 2014 +0100 @@ -20,7 +20,7 @@ val best_tac: Proof.context -> int -> tactic val best_dup_tac: Proof.context -> int -> tactic val fast_tac: Proof.context -> int -> tactic - val inst_step_tac: int -> tactic + val inst_step_tac: Proof.context -> int -> tactic val safe_step_tac: Proof.context -> int -> tactic val safe_brls: (bool * thm) list val safe_tac: Proof.context -> tactic @@ -74,14 +74,14 @@ fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); (*These steps could instantiate variables and are therefore unsafe.*) -val inst_step_tac = - assume_tac APPEND' mp_tac APPEND' +fun inst_step_tac ctxt = + assume_tac ctxt APPEND' mp_tac APPEND' biresolve_tac (safe0_brls @ safep_brls); (*One safe or unsafe step. *) -fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i]; +fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i]; -fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i]; +fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_dup_brls i]; (*Dumb but fast*) fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOL/simpdata.ML Mon Nov 10 21:49:48 2014 +0100 @@ -108,7 +108,7 @@ fun unsafe_solver ctxt = FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), - assume_tac, + assume_tac ctxt, eresolve_tac @{thms FalseE}]; (*No premature instantiation of variables during simplification*) diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/IFOLP.thy Mon Nov 10 21:49:48 2014 +0100 @@ -252,7 +252,7 @@ local fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P; in -val uniq_assume_tac = +fun uniq_assume_tac ctxt = SUBGOAL (fn (prem,i) => let val hyps = map discard_proof (Logic.strip_assums_hyp prem) @@ -260,7 +260,7 @@ in if exists (fn hyp => hyp aconv concl) hyps then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of - [_] => assume_tac i + [_] => assume_tac ctxt i | _ => no_tac else no_tac end); @@ -272,12 +272,14 @@ (*Finds P-->Q and P in the assumptions, replaces implication by Q *) ML {* - fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac i + fun mp_tac ctxt i = + eresolve_tac [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac ctxt i *} (*Like mp_tac but instantiates no variables*) ML {* - fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac i + fun int_uniq_mp_tac ctxt i = + eresolve_tac [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac ctxt i *} @@ -374,7 +376,7 @@ schematic_lemma disj_cong: "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" - apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+ + apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+ done schematic_lemma imp_cong: @@ -382,31 +384,31 @@ and "!!x. x:P' ==> q(x):Q <-> Q'" shows "?p:(P-->Q) <-> (P'-->Q')" apply (insert assms(1)) - apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} | + apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac @{context} 1 *} | tactic {* iff_tac @{thms assms} 1 *})+ done schematic_lemma iff_cong: "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" - apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+ + apply (erule iffE | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+ done schematic_lemma not_cong: "p:P <-> P' ==> ?p:~P <-> ~P'" - apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+ + apply (assumption | rule iffI notI | tactic {* mp_tac @{context} 1 *} | erule iffE notE)+ done schematic_lemma all_cong: assumes "!!x. f(x):P(x) <-> Q(x)" shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))" - apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE | + apply (assumption | rule iffI allI | tactic {* mp_tac @{context} 1 *} | erule allE | tactic {* iff_tac @{thms assms} 1 *})+ done schematic_lemma ex_cong: assumes "!!x. f(x):P(x) <-> Q(x)" shows "?p:(EX x. P(x)) <-> (EX x. Q(x))" - apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} | + apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac @{context} 1 *} | tactic {* iff_tac @{thms assms} 1 *})+ done @@ -636,7 +638,7 @@ "?p6 : P & ~P <-> False" "?p7 : ~P & P <-> False" "?p8 : (P & Q) & R <-> P & (Q & R)" - apply (tactic {* fn st => IntPr.fast_tac 1 st *})+ + apply (tactic {* fn st => IntPr.fast_tac @{context} 1 st *})+ done schematic_lemma disj_rews: @@ -646,13 +648,13 @@ "?p4 : False | P <-> P" "?p5 : P | P <-> P" "?p6 : (P | Q) | R <-> P | (Q | R)" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done schematic_lemma not_rews: "?p1 : ~ False <-> True" "?p2 : ~ True <-> False" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done schematic_lemma imp_rews: @@ -662,7 +664,7 @@ "?p4 : (True --> P) <-> P" "?p5 : (P --> P) <-> True" "?p6 : (P --> ~P) <-> ~P" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done schematic_lemma iff_rews: @@ -671,13 +673,13 @@ "?p3 : (P <-> P) <-> True" "?p4 : (False <-> P) <-> ~P" "?p5 : (P <-> False) <-> ~P" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done schematic_lemma quant_rews: "?p1 : (ALL x. P) <-> P" "?p2 : (EX x. P) <-> P" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done (*These are NOT supplied by default!*) @@ -686,7 +688,7 @@ "?p2 : P & (Q | R) <-> P&Q | P&R" "?p3 : (Q | R) & P <-> Q&P | R&P" "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done schematic_lemma distrib_rews2: @@ -694,17 +696,17 @@ "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)" "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))" "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))" - apply (tactic {* IntPr.fast_tac 1 *})+ + apply (tactic {* IntPr.fast_tac @{context} 1 *})+ done lemmas distrib_rews = distrib_rews1 distrib_rews2 schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)" - apply (tactic {* IntPr.fast_tac 1 *}) + apply (tactic {* IntPr.fast_tac @{context} 1 *}) done schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)" - apply (tactic {* IntPr.fast_tac 1 *}) + apply (tactic {* IntPr.fast_tac @{context} 1 *}) done end diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/classical.ML --- a/src/FOLP/classical.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/classical.ML Mon Nov 10 21:49:48 2014 +0100 @@ -45,17 +45,17 @@ safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list, haz_brls: (bool*thm)list} val best_tac : Proof.context -> claset -> int -> tactic - val contr_tac : int -> tactic + val contr_tac : Proof.context -> int -> tactic val fast_tac : Proof.context -> claset -> int -> tactic - val inst_step_tac : int -> tactic + val inst_step_tac : Proof.context -> int -> tactic val joinrules : thm list * thm list -> (bool * thm) list - val mp_tac: int -> tactic + val mp_tac: Proof.context -> 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 swap_res_tac : Proof.context -> thm list -> int -> tactic val uniq_mp_tac: Proof.context -> int -> tactic end; @@ -70,22 +70,22 @@ val imp_elim = make_elim mp; (*Solve goal that assumes both P and ~P. *) -val contr_tac = etac not_elim THEN' assume_tac; +fun contr_tac ctxt = etac not_elim THEN' assume_tac ctxt; (*Finds P-->Q and P in the assumptions, replaces implication by Q *) -fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac i; +fun mp_tac ctxt i = eresolve_tac ([not_elim,imp_elim]) i THEN assume_tac ctxt i; (*Like mp_tac but instantiates no variables*) -fun uniq_mp_tac ctxt i = ematch_tac ctxt ([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 ctxt i; (*Creates rules to eliminate ~A, from rules to introduce A*) fun swapify intrs = intrs RLN (2, [swap]); (*Uses introduction rules in the normal way, or on negated assumptions, trying rules in order. *) -fun swap_res_tac rls = +fun swap_res_tac ctxt rls = let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap)) - in assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls) + in assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls) end; @@ -149,7 +149,7 @@ (*Attack subgoals using safe inferences*) fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = - FIRST' [uniq_assume_tac, + FIRST' [uniq_assume_tac ctxt, uniq_mp_tac ctxt, biresolve_tac safe0_brls, FIRST' hyp_subst_tacs, @@ -159,12 +159,12 @@ 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; +fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt; (*Single step for the prover. FAILS unless it makes progress. *) fun step_tac ctxt (cs as (CS{haz_brls,...})) i = FIRST [safe_tac ctxt cs, - inst_step_tac i, + inst_step_tac ctxt i, biresolve_tac haz_brls i]; (*** The following tactics all fail unless they solve one goal ***) @@ -179,7 +179,7 @@ (*Using a "safe" rule to instantiate variables is unsafe. This tactic allows backtracking from "safe" rules to "unsafe" rules here.*) 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); + safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac haz_brls i); end; end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/ex/Intuitionistic.thy --- a/src/FOLP/ex/Intuitionistic.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/ex/Intuitionistic.thy Mon Nov 10 21:49:48 2014 +0100 @@ -31,39 +31,39 @@ begin schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ~~~P <-> ~P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P<->Q) <-> (Q<->P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) subsection {* Lemmas for the propositional double-negation translation *} schematic_lemma "?p : P --> ~~P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ~~(~~P --> P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) subsection {* The following are classically but not constructively valid *} (*The attempt to prove them terminates quickly!*) schematic_lemma "?p : ((P-->Q) --> P) --> P" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops @@ -71,74 +71,74 @@ text "Problem ~~1" schematic_lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~2" schematic_lemma "?p : ~~(~~P <-> P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem 3" schematic_lemma "?p : ~(P-->Q) --> (Q-->P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~4" schematic_lemma "?p : ~~((~P-->Q) <-> (~Q --> P))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~5" schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~6" schematic_lemma "?p : ~~(P | ~P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~7" schematic_lemma "?p : ~~(P | ~~~P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~8. Peirce's law" schematic_lemma "?p : ~~(((P-->Q) --> P) --> P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem 9" schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem 10" schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "11. Proved in each direction (incorrectly, says Pelletier!!) " schematic_lemma "?p : P<->P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~12. Dijkstra's law " schematic_lemma "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem 13. Distributive law" schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~14" schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~15" schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~16" schematic_lemma "?p : ~~((P-->Q) | (Q-->P))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~17" schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))" - by (tactic {* IntPr.fast_tac 1 *}) -- slow + by (tactic {* IntPr.fast_tac @{context} 1 *}) -- slow subsection {* Examples with quantifiers *} @@ -146,43 +146,43 @@ text "The converse is classical in the following implications..." schematic_lemma "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "The following are not constructively valid!" text "The attempt to prove them terminates quickly!" schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops @@ -204,7 +204,7 @@ 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem 21" schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops @@ -212,21 +212,21 @@ text "Problem 22" schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Problem ~~23" schematic_lemma "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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))" (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) - apply (tactic "IntPr.safe_tac") + apply (tactic "IntPr.safe_tac @{context}") apply (erule impE) - apply (tactic "IntPr.fast_tac 1") - apply (tactic "IntPr.fast_tac 1") + apply (tactic "IntPr.fast_tac @{context} 1") + apply (tactic "IntPr.fast_tac @{context} 1") done text "Problem 25" @@ -235,72 +235,72 @@ (ALL x. P(x) --> (M(x) & L(x))) & ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) --> (EX x. Q(x)&P(x))" - by (tactic "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 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 "IntPr.fast_tac 1") + by (tactic "IntPr.fast_tac @{context} 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 "IntPr.fast_tac 1") + by (tactic "IntPr.fast_tac @{context} 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 "IntPr.fast_tac 1") + by (tactic "IntPr.fast_tac @{context} 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 "IntPr.best_tac 1") -- slow + by (tactic "IntPr.best_tac @{context} 1") -- slow text "Problem 39" schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" - by (tactic "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 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 "IntPr.best_tac 1") -- slow + by (tactic "IntPr.best_tac @{context} 1") -- slow 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 "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 1") text "Problem 48" schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" - by (tactic "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 1") text "Problem 51" schematic_lemma "?p : (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)" - by (tactic "IntPr.best_tac 1") -- {*60 seconds*} + by (tactic "IntPr.best_tac @{context} 1") -- {*60 seconds*} 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 "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 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 "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 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 "IntPr.best_tac 1") + by (tactic "IntPr.best_tac @{context} 1") end diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/ex/Propositional_Int.thy --- a/src/FOLP/ex/Propositional_Int.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/ex/Propositional_Int.thy Mon Nov 10 21:49:48 2014 +0100 @@ -12,106 +12,106 @@ text "commutative laws of & and | " schematic_lemma "?p : P & Q --> Q & P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : P | Q --> Q | P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "associative laws of & and | " schematic_lemma "?p : (P & Q) & R --> P & (Q & R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P | Q) | R --> P | (Q | R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "distributive laws of & and | " schematic_lemma "?p : (P & Q) | R --> (P | R) & (Q | R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P | R) & (Q | R) --> (P & Q) | R" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P | Q) & R --> (P & R) | (Q & R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P & R) | (Q & R) --> (P | Q) & R" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Laws involving implication" schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Propositions-as-types" (*The combinator K*) schematic_lemma "?p : P --> (Q --> P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) (*The combinator S*) schematic_lemma "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) (*Converse is classical*) schematic_lemma "?p : (P-->Q) | (P-->R) --> (P --> Q | R)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (P-->Q) --> (~Q --> ~P)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) --> ((P --> Q) --> P) --> P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q) --> (((P --> Q) --> R) --> P --> Q) --> P --> Q" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) end diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/ex/Quantifiers_Int.thy --- a/src/FOLP/ex/Quantifiers_Int.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/ex/Quantifiers_Int.thy Mon Nov 10 21:49:48 2014 +0100 @@ -11,91 +11,91 @@ begin schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) (*Converse is false*) schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) text "Some harder ones" schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) (*Converse is false*) schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : (EX x. Q(x)) --> (ALL x. Q(x))" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : P(?a) --> (ALL x. P(x))" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 1 *})? oops schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))" - apply (tactic {* IntPr.fast_tac 1 *})? + apply (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) schematic_lemma "?p : (ALL x. Q(x)) --> (EX x. Q(x))" - by (tactic {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 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 {* IntPr.fast_tac 1 *}) + by (tactic {* IntPr.fast_tac @{context} 1 *}) end diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/intprover.ML --- a/src/FOLP/intprover.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/intprover.ML Mon Nov 10 21:49:48 2014 +0100 @@ -15,13 +15,13 @@ signature INT_PROVER = sig - val best_tac: int -> tactic - val fast_tac: int -> tactic - val inst_step_tac: int -> tactic - val safe_step_tac: int -> tactic + val best_tac: Proof.context -> int -> tactic + val fast_tac: Proof.context -> int -> tactic + val inst_step_tac: Proof.context -> int -> tactic + val safe_step_tac: Proof.context -> int -> tactic val safe_brls: (bool * thm) list - val safe_tac: tactic - val step_tac: int -> tactic + val safe_tac: Proof.context -> tactic + val step_tac: Proof.context -> int -> tactic val haz_brls: (bool * thm) list end; @@ -52,26 +52,26 @@ List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; (*Attack subgoals using safe inferences*) -val safe_step_tac = FIRST' [uniq_assume_tac, - int_uniq_mp_tac, +fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, + int_uniq_mp_tac ctxt, biresolve_tac safe0_brls, hyp_subst_tac, biresolve_tac safep_brls] ; (*Repeatedly attack subgoals using safe inferences*) -val safe_tac = DETERM (REPEAT_FIRST safe_step_tac); +fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt)); (*These steps could instantiate variables and are therefore unsafe.*) -val inst_step_tac = assume_tac APPEND' mp_tac; +fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt; (*One safe or unsafe step. *) -fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; +fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i]; (*Dumb but fast*) -val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); +fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); (*Slower but smarter than fast_tac*) -val best_tac = - SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1)); +fun best_tac ctxt = + SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/FOLP/simp.ML --- a/src/FOLP/simp.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/FOLP/simp.ML Mon Nov 10 21:49:48 2014 +0100 @@ -451,7 +451,7 @@ thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) end | NONE => if more - then rew((lhs_net_tac anet i THEN assume_tac i) thm, + then rew((lhs_net_tac anet i THEN atac i) thm, thm,ss,anet,ats,cs,false) else (ss,thm,anet,ats,cs); diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Auth/Event.thy Mon Nov 10 21:49:48 2014 +0100 @@ -270,14 +270,14 @@ ML {* -val analz_mono_contra_tac = +fun analz_mono_contra_tac ctxt = rtac @{thm analz_impI} THEN' REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) - THEN' mp_tac + THEN' (mp_tac ctxt) *} method_setup analz_mono_contra = {* - Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *} + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} @@ -286,7 +286,7 @@ ML {* -val synth_analz_mono_contra_tac = +fun synth_analz_mono_contra_tac ctxt = rtac @{thm syan_impI} THEN' REPEAT1 o (dresolve_tac @@ -294,11 +294,11 @@ @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) THEN' - mp_tac + mp_tac ctxt *} method_setup synth_analz_mono_contra = {* - Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *} + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *} "for proving theorems of the form X \ synth (analz (knows Spy evs)) --> P" end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Auth/Recur.thy Mon Nov 10 21:49:48 2014 +0100 @@ -163,7 +163,7 @@ [THEN respond.Cons, THEN respond.Cons]], THEN recur.RA4, THEN recur.RA4]) apply basic_possibility -apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)") +apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [refl, conjI, disjCI] 1)") done diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Bali/AxSem.thy Mon Nov 10 21:49:48 2014 +0100 @@ -661,13 +661,14 @@ lemma ax_thin [rule_format (no_asm)]: "G,(A'::'a triple set)|\(ts::'a triple set) \ \A. A' \ A \ G,A|\ts" apply (erule ax_derivs.induct) -apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])") +apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1])") apply (rule ax_derivs.empty) apply (erule (1) ax_derivs.insert) apply (fast intro: ax_derivs.asm) (*apply (fast intro: ax_derivs.cut) *) apply (fast intro: ax_derivs.weaken) -apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) +apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac @{context} 3 1",clarify, + tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI) (* 37 subgoals *) prefer 18 (* Methd *) apply (rule ax_derivs.Methd, drule spec, erule mp, fast) @@ -700,7 +701,7 @@ apply (fast intro: ax_derivs.asm) (*apply (blast intro: ax_derivs.cut) *) apply (fast intro: ax_derivs.weaken) -apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *)) +apply (rule ax_derivs.conseq, clarify, tactic "smp_tac @{context} 3 1", blast(* unused *)) (*37 subgoals*) apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) THEN_ALL_NEW fast_tac @{context}) *}) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Bali/AxSound.thy --- a/src/HOL/Bali/AxSound.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Bali/AxSound.thy Mon Nov 10 21:49:48 2014 +0100 @@ -50,13 +50,13 @@ apply (rule iffI) apply fast apply clarify -apply (tactic "smp_tac 3 1") +apply (tactic "smp_tac @{context} 3 1") apply (case_tac "normal s") apply clarsimp apply (elim conjE impE) apply blast -apply (tactic "smp_tac 2 1") +apply (tactic "smp_tac @{context} 2 1") apply (drule evaln_eval) apply (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+) apply simp @@ -84,7 +84,7 @@ "\G\n\{Normal P} body G C sig-\{Q}\ \ G\Suc n\{Normal P} Methd C sig-\ {Q}" apply (simp (no_asm_use) add: triple_valid2_def2) -apply (intro strip, tactic "smp_tac 3 1", clarify) +apply (intro strip, tactic "smp_tac @{context} 3 1", clarify) apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases) apply (unfold body_def Let_def) apply (clarsimp simp add: inj_term_simps) @@ -400,14 +400,14 @@ from valid_A conf wt da eval P con have "Q v s1 Z" apply (simp add: ax_valids2_def triple_valid2_def2) - apply (tactic "smp_tac 3 1") + apply (tactic "smp_tac @{context} 3 1") apply clarify - apply (tactic "smp_tac 1 1") + apply (tactic "smp_tac @{context} 1 1") apply (erule allE,erule allE, erule mp) apply (intro strip) - apply (tactic "smp_tac 3 1") - apply (tactic "smp_tac 2 1") - apply (tactic "smp_tac 1 1") + apply (tactic "smp_tac @{context} 3 1") + apply (tactic "smp_tac @{context} 2 1") + apply (tactic "smp_tac @{context} 1 1") by blast moreover have "s1\\(G, L)" proof (cases "normal s0") @@ -2065,7 +2065,7 @@ (abupd (absorb (Cont l')) s2') \ s3'" apply (simp only: True if_True eqs) apply (elim conjE) - apply (tactic "smp_tac 3 1") + apply (tactic "smp_tac @{context} 3 1") apply fast done from eval_e diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Bali/Evaln.thy Mon Nov 10 21:49:48 2014 +0100 @@ -449,7 +449,7 @@ "G\s \t\\n\ (w, s') \ \m. n\m \ G\s \t\\m\ (w, s')" apply (erule evaln.induct) apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma}, - REPEAT o smp_tac 1, + REPEAT o smp_tac @{context} 1, resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *}) (* 3 subgoals *) apply (auto split del: split_if) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Bali/Table.thy Mon Nov 10 21:49:48 2014 +0100 @@ -396,7 +396,7 @@ apply (rename_tac "ba") apply (drule_tac x = "ba" in spec) apply clarify -apply (tactic "smp_tac 2 1") +apply (tactic "smp_tac @{context} 2 1") apply (erule (1) notE impE) apply (case_tac "aa = b") apply fast+ diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Mon Nov 10 21:49:48 2014 +0100 @@ -80,7 +80,7 @@ TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)] (Thm.trivial ct)) - fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) + fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) (* The result of the quantifier elimination *) val (th, tac) = (case (prop_of pre_thm) of diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Mon Nov 10 21:49:48 2014 +0100 @@ -61,7 +61,7 @@ [simp_tac simpset0 1, TRY (simp_tac (put_simpset ferrack_ss ctxt) 1)] (Thm.trivial ct)) - fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) + fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) (* The result of the quantifier elimination *) val (th, tac) = case prop_of pre_thm of Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Mon Nov 10 21:49:48 2014 +0100 @@ -108,7 +108,7 @@ TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac (put_simpset mir_ss ctxt) 1)] (Thm.trivial ct)) - fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) + fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) (* The result of the quantifier elimination *) val (th, tac) = case (prop_of pre_thm) of Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/HOL.thy Mon Nov 10 21:49:48 2014 +0100 @@ -1982,7 +1982,7 @@ val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of); in fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]); - fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac]; + fun smp_tac ctxt j = EVERY'[dresolve_tac (smp j), assume_tac ctxt]; end; local diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/HOLCF/FOCUS/Buffer_adm.thy --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy Mon Nov 10 21:49:48 2014 +0100 @@ -199,7 +199,7 @@ apply (drule spec, erule impE) apply (erule BufAC_Asm_antiton [THEN antitonPD]) apply (erule is_ub_thelub) -apply (tactic "smp_tac 3 1") +apply (tactic "smp_tac @{context} 3 1") apply (drule is_ub_thelub) apply (drule (1) mp) apply (drule (1) mp) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Hoare_Parallel/Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Mon Nov 10 21:49:48 2014 +0100 @@ -777,7 +777,7 @@ apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) apply(tactic {* TRYALL (etac disjE) *}) apply simp_all -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *}) +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *}) apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *}) apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *}) done diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Nov 10 21:49:48 2014 +0100 @@ -1187,7 +1187,7 @@ --{* 72 subgoals left *} apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) --{* 35 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *}) +apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *}) --{* 28 subgoals left *} apply(tactic {* TRYALL (etac conjE) *}) apply(tactic {* TRYALL (etac disjE) *}) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/IMPP/Hoare.thy Mon Nov 10 21:49:48 2014 +0100 @@ -209,13 +209,13 @@ *) lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts" apply (erule hoare_derivs.induct) -apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1]) *}) +apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) apply (rule hoare_derivs.empty) apply (erule (1) hoare_derivs.insert) apply (fast intro: hoare_derivs.asm) apply (fast intro: hoare_derivs.cut) apply (fast intro: hoare_derivs.weaken) -apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) +apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac @{context} 2 1", clarify, tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI) prefer 7 apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast) apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *}) @@ -287,9 +287,9 @@ apply (blast) (* weaken *) apply (tactic {* ALLGOALS (EVERY' [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y", - simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac 1]) *}) + simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) apply (simp_all (no_asm_use) add: triple_valid_def2) -apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *) +apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *) apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *) prefer 3 apply (force) (* Call *) apply (erule_tac [2] evaln_elim_cases) (* If *) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/IMPP/Misc.thy --- a/src/HOL/IMPP/Misc.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/IMPP/Misc.thy Mon Nov 10 21:49:48 2014 +0100 @@ -71,12 +71,12 @@ apply (simp (no_asm_use) add: triple_valid_def2) apply clarsimp apply (drule_tac x = "s" in spec) -apply (tactic "smp_tac 1 1") +apply (tactic "smp_tac @{context} 1 1") apply (drule spec) apply (drule_tac x = "s[Loc Y::=a s]" in spec) apply (simp (no_asm_use)) apply (erule (1) notE impE) -apply (tactic "smp_tac 1 1") +apply (tactic "smp_tac @{context} 1 1") apply simp done diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/IMPP/Natural.thy --- a/src/HOL/IMPP/Natural.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/IMPP/Natural.thy Mon Nov 10 21:49:48 2014 +0100 @@ -139,7 +139,8 @@ lemma evalc_evaln: " -c-> t ==> ? n. -n-> t" apply (erule evalc.induct) apply (tactic {* ALLGOALS (REPEAT o etac exE) *}) -apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *}) +apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac @{context}, + REPEAT o eresolve_tac [exE, conjE]]) *}) apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *}) done diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon Nov 10 21:49:48 2014 +0100 @@ -138,7 +138,7 @@ apply( drule (3) Call_lemma) apply( clarsimp simp add: wf_java_mdecl_def) apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) -apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2") +apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac @{context} 2") apply( rule conformsI) apply( erule conforms_heapD) apply( rule lconf_ext) @@ -156,10 +156,10 @@ apply( fast intro: hext_trans) apply( rule conjI) apply( rule_tac [2] impI) -apply( erule_tac [2] notE impE, tactic "assume_tac 2") +apply( erule_tac [2] notE impE, tactic "assume_tac @{context} 2") apply( frule_tac [2] conf_widen) -apply( tactic "assume_tac 4") -apply( tactic "assume_tac 2") +apply( tactic "assume_tac @{context} 4") +apply( tactic "assume_tac @{context} 2") prefer 2 apply( fast elim!: widen_trans) apply (rule conforms_xcpt_change) @@ -177,8 +177,9 @@ declare wf_prog_ws_prog [simp] ML{* -val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac, - (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) +fun forward_hyp_tac ctxt = + ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac ctxt, + (mp_tac ctxt ORELSE' (dtac spec THEN' mp_tac ctxt)), REPEAT o (etac conjE)])) *} @@ -226,8 +227,8 @@ apply( erule conf_litval) -- "13 BinOp" -apply (tactic "forward_hyp_tac") -apply (tactic "forward_hyp_tac") +apply (tactic "forward_hyp_tac @{context}") +apply (tactic "forward_hyp_tac @{context}") apply( rule conjI, erule (1) hext_trans) apply( erule conjI) apply( clarsimp) @@ -246,7 +247,7 @@ apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW (asm_full_simp_tac @{context})) 7*}) -apply (tactic "forward_hyp_tac") +apply (tactic "forward_hyp_tac @{context}") -- "11+1 if" prefer 7 @@ -294,7 +295,7 @@ apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) apply(force elim: hext_trans) -apply (tactic "forward_hyp_tac") +apply (tactic "forward_hyp_tac @{context}") -- "4 Cond" prefer 4 @@ -317,7 +318,7 @@ apply( case_tac "x2") -- "x2 = None" apply (simp) - apply (tactic forward_hyp_tac, clarify) + apply (tactic "forward_hyp_tac @{context}", clarify) apply( drule eval_no_xcpt) apply( erule FAss_type_sound, rule HOL.refl, assumption+) -- "x2 = Some a" diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/NanoJava/AxSem.thy --- a/src/HOL/NanoJava/AxSem.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/NanoJava/AxSem.thy Mon Nov 10 21:49:48 2014 +0100 @@ -152,7 +152,7 @@ "(A' |\ C \ (\A. A' \ A \ A |\ C )) \ (A' \\<^sub>e {P} e {Q} \ (\A. A' \ A \ A \\<^sub>e {P} e {Q}))" apply (rule hoare_ehoare.induct) -apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])") +apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1])") apply (blast intro: hoare_ehoare.Skip) apply (blast intro: hoare_ehoare.Comp) apply (blast intro: hoare_ehoare.Cond) @@ -164,7 +164,7 @@ apply (blast intro: hoare_ehoare.NewC) apply (blast intro: hoare_ehoare.Cast) apply (erule hoare_ehoare.Call) -apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption) +apply (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption) apply blast apply (blast intro!: hoare_ehoare.Meth) apply (blast intro!: hoare_ehoare.Impl) @@ -172,9 +172,9 @@ apply (blast intro: hoare_ehoare.ConjI) apply (blast intro: hoare_ehoare.ConjE) apply (rule hoare_ehoare.Conseq) -apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) +apply (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+) apply (rule hoare_ehoare.eConseq) -apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) +apply (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+) done lemma cThin: "\A' |\ C; A' \ A\ \ A |\ C" diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/NanoJava/Equivalence.thy Mon Nov 10 21:49:48 2014 +0100 @@ -111,7 +111,7 @@ apply fast apply fast apply fast - apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) + apply (clarify,tactic "smp_tac @{context} 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) apply fast apply fast apply fast diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/NanoJava/Example.thy --- a/src/HOL/NanoJava/Example.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/NanoJava/Example.thy Mon Nov 10 21:49:48 2014 +0100 @@ -131,7 +131,7 @@ apply auto apply (case_tac "aa=a") apply auto -apply (tactic "smp_tac 1 1") +apply (tactic "smp_tac @{context} 1 1") apply (case_tac "aa=a") apply auto done diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Nov 10 21:49:48 2014 +0100 @@ -438,11 +438,11 @@ in fold (fn (s, tvs) => fn thy => Axclass.prove_arity (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name]) - (fn _ => EVERY + (fn ctxt => EVERY [Class.intro_classes_tac [], resolve_tac perm_empty_thms 1, resolve_tac perm_append_thms 1, - resolve_tac perm_eq_thms 1, assume_tac 1]) thy) + resolve_tac perm_eq_thms 1, assume_tac ctxt 1]) thy) (full_new_type_names' ~~ tyvars) thy end) atoms |> Global_Theory.add_thmss @@ -562,7 +562,7 @@ [Old_Datatype_Aux.ind_tac rep_induct [] 1, ALLGOALS (simp_tac (ctxt addsimps (Thm.symmetric perm_fun_def :: abs_perm))), - ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])), + ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac ctxt)])), length new_type_names)); val perm_closed_thmss = map mk_perm_closed atoms; @@ -1721,9 +1721,9 @@ (S $ Free x $ Free y, P $ (Free y))) (rec_unique_frees'' ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))) - (fn _ => + (fn {context = ctxt, ...} => rtac rec_induct 1 THEN - REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1)))); + REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac ctxt) 1)))); val rec_fin_supp_thms' = map (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths)) (rec_fin_supp_thms ~~ finite_thss); diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/SET_Protocol/Cardholder_Registration.thy --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Mon Nov 10 21:49:48 2014 +0100 @@ -539,7 +539,7 @@ Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant (fn i => EVERY [ftac @{thm Gets_certificate_valid} i, - assume_tac i, + assume_tac ctxt i, etac conjE i, REPEAT (hyp_subst_tac ctxt i)])) *} diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/SET_Protocol/Event_SET.thy --- a/src/HOL/SET_Protocol/Event_SET.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/SET_Protocol/Event_SET.thy Mon Nov 10 21:49:48 2014 +0100 @@ -182,14 +182,14 @@ ML {* -val analz_mono_contra_tac = +fun analz_mono_contra_tac ctxt = rtac @{thm analz_impI} THEN' REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) - THEN' mp_tac + THEN' mp_tac ctxt *} method_setup analz_mono_contra = {* - Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *} + Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/SET_Protocol/Purchase.thy --- a/src/HOL/SET_Protocol/Purchase.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/SET_Protocol/Purchase.thy Mon Nov 10 21:49:48 2014 +0100 @@ -483,7 +483,7 @@ Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant (fn i => EVERY [ftac @{thm Gets_certificate_valid} i, - assume_tac i, REPEAT (hyp_subst_tac ctxt i)])) + assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)])) *} diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Set.thy --- a/src/HOL/Set.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Set.thy Mon Nov 10 21:49:48 2014 +0100 @@ -383,7 +383,7 @@ setup {* map_theory_claset (fn ctxt => - ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac)) + ctxt addbefore ("bspec", fn ctxt' => dresolve_tac @{thms bspec} THEN' assume_tac ctxt')) *} ML {* diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Nov 10 21:49:48 2014 +0100 @@ -227,7 +227,7 @@ val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); val fast_solver = mk_solver "fast_solver" (fn ctxt => if Config.get ctxt config_fast_solver - then assume_tac ORELSE' (etac notE) + then assume_tac ctxt ORELSE' (etac notE) else K no_tac); *} diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Nov 10 21:49:48 2014 +0100 @@ -2471,7 +2471,7 @@ fun distinct_prems ctxt thm = Goal.prove (*no sorry*) ctxt [] [] (thm |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies) - (fn _ => HEADGOAL (cut_tac thm THEN' atac) THEN ALLGOALS eq_assume_tac); + (fn _ => HEADGOAL (cut_tac thm THEN' assume_tac ctxt) THEN ALLGOALS eq_assume_tac); fun eq_ifIN _ [thm] = thm | eq_ifIN ctxt (thm :: thms) = diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Mon Nov 10 21:49:48 2014 +0100 @@ -44,7 +44,7 @@ (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN' REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos, SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac @{thm order_refl}, - atac, resolve_tac co_inducts, + assume_tac ctxt, resolve_tac co_inducts, resolve_tac C_IH_monos THEN' REPEAT_ALL_NEW (eresolve_tac nesting_rel_monos)]))) co_inducts) end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Nov 10 21:49:48 2014 +0100 @@ -452,7 +452,7 @@ val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (K ((hyp_subst_tac lthy THEN' atac) 1)) + (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1)) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -550,7 +550,7 @@ val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1) + (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Nov 10 21:49:48 2014 +0100 @@ -394,7 +394,7 @@ val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (K ((hyp_subst_tac lthy THEN' atac) 1)) + (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1)) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Nov 10 21:49:48 2014 +0100 @@ -906,7 +906,7 @@ val thms = @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => - mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac) + mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL (assume_tac ctxt)) |> Thm.close_derivation |> not triv ? perhaps (try (fn thm => refl RS thm))) ms discD_thms sel_thmss trivs goals; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Mon Nov 10 21:49:48 2014 +0100 @@ -683,7 +683,7 @@ subset_induct_rule |> Thm.forall_intr (cterm_of thy D) |> Thm.forall_elim (cterm_of thy acc_R) - |> assume_tac 1 |> Seq.hd + |> atac 1 |> Seq.hd |> (curry op COMP) (acc_downward |> (instantiate' [SOME (ctyp_of thy domT)] (map (SOME o cterm_of thy) [R, x, z])) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Function/function_elims.ML --- a/src/HOL/Tools/Function/function_elims.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Function/function_elims.ML Mon Nov 10 21:49:48 2014 +0100 @@ -125,7 +125,7 @@ REPEAT (eresolve_tac @{thms Pair_inject} i) THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i THEN propagate_tac ctxt i - THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i) + THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i) THEN bool_subst_tac ctxt i; val elim_stripped = diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 10 21:49:48 2014 +0100 @@ -396,6 +396,6 @@ fun induction_schema_tac ctxt = - mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; + mk_ind_tac (K all_tac) (assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Mon Nov 10 21:49:48 2014 +0100 @@ -32,8 +32,8 @@ in EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]), REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]), - rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt - [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac, + rtac rel_mono THEN_ALL_NEW assume_tac ctxt, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt + [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW assume_tac ctxt, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]), hyp_subst_tac ctxt, rtac refl] i end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Mon Nov 10 21:49:48 2014 +0100 @@ -30,8 +30,8 @@ val make_clauses_unsorted: Proof.context -> thm list -> thm list val make_clauses: Proof.context -> thm list -> thm list val make_horns: thm list -> thm list - val best_prolog_tac: (thm -> int) -> thm list -> tactic - val depth_prolog_tac: thm list -> tactic + val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic + val depth_prolog_tac: Proof.context -> thm list -> tactic val gocls: thm list -> thm list val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic val MESON: @@ -503,8 +503,8 @@ (* net_resolve_tac actually made it slower... *) -fun prolog_step_tac horns i = - (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN +fun prolog_step_tac ctxt horns i = + (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN TRYALL_eq_assume_tac; (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) @@ -690,11 +690,11 @@ (*Could simply use nprems_of, which would count remaining subgoals -- no discrimination as to their size! With BEST_FIRST, fails for problem 41.*) -fun best_prolog_tac sizef horns = - BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); +fun best_prolog_tac ctxt sizef horns = + BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1); -fun depth_prolog_tac horns = - DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); +fun depth_prolog_tac ctxt horns = + DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1); (*Return all negative clauses, as possible goal clauses*) fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); @@ -723,7 +723,7 @@ (fn cls => THEN_BEST_FIRST (resolve_tac (gocls cls) 1) (has_fewer_prems 1, sizef) - (prolog_step_tac (make_horns cls) 1)) + (prolog_step_tac ctxt (make_horns cls) 1)) ctxt (*First, breaks the goal into independent units*) @@ -734,7 +734,7 @@ fun depth_meson_tac ctxt = MESON all_tac (make_clauses ctxt) - (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]) + (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)]) ctxt (** Iterative deepening version **) @@ -747,7 +747,7 @@ val nrtac = net_resolve_tac horns in fn i => eq_assume_tac i ORELSE match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*) - ((assume_tac i APPEND nrtac i) THEN check_tac) + ((assume_tac ctxt i APPEND nrtac i) THEN check_tac) end; fun iter_deepen_prolog_tac ctxt horns = diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Nov 10 21:49:48 2014 +0100 @@ -439,7 +439,10 @@ val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped val goal = Logic.list_implies (prems, concl) val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt - val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS assume_tac + val tac = + cut_tac th 1 THEN + rewrite_goals_tac ctxt' meta_not_not THEN + ALLGOALS (assume_tac ctxt') in if length prems = length prems0 then raise METIS_RECONSTRUCT ("resynchronize", "Out of sync") @@ -746,7 +749,7 @@ 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) - THEN assume_tac i + THEN assume_tac ctxt' i THEN flexflex_tac ctxt'))) handle ERROR msg => cat_error msg diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Nov 10 21:49:48 2014 +0100 @@ -382,8 +382,8 @@ (map (pair "x") Ts, S $ Old_Datatype_Aux.app_bnds f i)), HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts (r $ (a $ Old_Datatype_Aux.app_bnds f i)), f)))) - (fn _ => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1), - REPEAT (etac allE 1), rtac thm 1, atac 1]) + (fn {context = ctxt, ...} => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1), + REPEAT (etac allE 1), rtac thm 1, assume_tac ctxt 1]) end in map (fn r => r RS subst) (thm :: map mk_thm arities) end; @@ -431,12 +431,12 @@ [REPEAT (eresolve_tac (Scons_inject :: map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1), REPEAT (cong_tac ctxt 1), rtac refl 1, - REPEAT (atac 1 ORELSE (EVERY + REPEAT (assume_tac ctxt 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1), REPEAT (eresolve_tac (mp :: allE :: map make_elim (Suml_inject :: Sumr_inject :: Lim_inject :: inj_thms') @ fun_congs) 1), - atac 1]))])])])]); + assume_tac ctxt 1]))])])])]); val inj_thms'' = map (fn r => r RS datatype_injI) (Old_Datatype_Aux.split_conj_thm inj_thm); @@ -565,7 +565,7 @@ REPEAT (eresolve_tac inj_thms 1), REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1), REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1), - atac 1]))]) + assume_tac ctxt 1]))]) end; val constr_inject = diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Old_Datatype/old_rep_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Nov 10 21:49:48 2014 +0100 @@ -183,7 +183,7 @@ REPEAT_DETERM_N j distinct_tac, TRY (dresolve_tac inject 1), REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1, - REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]), + REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac ctxt 1]), TRY (hyp_subst_tac ctxt 1), resolve_tac [refl] 1, REPEAT_DETERM_N (n - j - 1) distinct_tac], diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Nov 10 21:49:48 2014 +0100 @@ -171,8 +171,8 @@ THEN EVERY1 (select_disj (length disjuncts) (index + 1)) THEN (EVERY (map (fn y => rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps)) - THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1) - THEN TRY (atac 1) + THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1) + THEN TRY (assume_tac ctxt' 1) in Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac) end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Nov 10 21:49:48 2014 +0100 @@ -78,7 +78,7 @@ THEN trace_tac ctxt options "prove_param" THEN f_tac THEN trace_tac ctxt options "after prove_param" - THEN (REPEAT_DETERM (atac 1)) + THEN (REPEAT_DETERM (assume_tac ctxt 1)) THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) THEN REPEAT_DETERM (rtac @{thm refl} 1) end @@ -97,11 +97,11 @@ THEN trace_tac ctxt options "after intro rule" (* for the right assumption in first position *) THEN rotate_tac premposition 1 - THEN atac 1 + THEN assume_tac ctxt 1 THEN trace_tac ctxt options "parameter goal" (* work with parameter arguments *) THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) - THEN (REPEAT_DETERM (atac 1)) + THEN (REPEAT_DETERM (assume_tac ctxt 1)) end | (Free _, _) => trace_tac ctxt options "proving parameter call.." @@ -242,7 +242,7 @@ THEN rtac (nth prems premposition) 1) ctxt 1 THEN trace_tac ctxt options "after applying not introduction rule" THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations)) - THEN (REPEAT_DETERM (atac 1)) + THEN (REPEAT_DETERM (assume_tac ctxt 1)) else rtac @{thm not_predI'} 1 (* test: *) @@ -410,8 +410,10 @@ THEN (rtac pred_intro_rule (* How to handle equality correctly? *) THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching") - THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac))) - THEN' (K (trace_tac ctxt options "state after pre-simplification:")) + THEN' (assume_tac ctxt ORELSE' + ((CHANGED o asm_full_simp_tac split_simpset) THEN' + (TRY o assume_tac ctxt))) THEN' + (K (trace_tac ctxt options "state after pre-simplification:")) THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1)) | prove_prems2 out_ts ((p, deriv) :: ps) = let diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Nov 10 21:49:48 2014 +0100 @@ -396,7 +396,7 @@ RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], (* resolving with R x y assumptions *) - atac, + assume_tac ctxt, (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) rtac @{thm ext} THEN' quot_true_tac ctxt unlam, @@ -560,7 +560,7 @@ val concl' = apply_under_Trueprop (all_list vrs) concl val goal = Logic.mk_implies (concl', concl) val rule = Goal.prove ctxt [] [] goal - (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt])) in rtac rule i end) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Mon Nov 10 21:49:48 2014 +0100 @@ -51,7 +51,7 @@ (* tactic to prove the quot_type theorem for the new type *) -fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) = +fun typedef_quot_type_tac ctxt equiv_thm ((_, typedef_info): Typedef.info) = let val rep_thm = #Rep typedef_info RS mem_def1 val rep_inv = #Rep_inverse typedef_info @@ -62,7 +62,7 @@ rtac equiv_thm, rtac rep_thm, rtac rep_inv, - rtac abs_inv THEN' rtac mem_def2 THEN' atac, + rtac abs_inv THEN' rtac mem_def2 THEN' assume_tac ctxt, rtac rep_inj]) 1 end @@ -74,7 +74,7 @@ val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) in Goal.prove lthy [] [] goal - (K (typedef_quot_type_tac equiv_thm typedef_info)) + (fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info) end open Lifting_Util diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Nov 10 21:49:48 2014 +0100 @@ -78,12 +78,13 @@ rel_OO_of_bnf bnf] in (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf) - THEN_ALL_NEW atac) i + THEN_ALL_NEW assume_tac ctxt) i end fun bi_constraint_tac constr_iff sided_constr_intros ctxt i = (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN' - CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i + CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW + (REPEAT_DETERM o etac conjE THEN' assume_tac ctxt)) sided_constr_intros) i fun generate_relation_constraint_goal ctxt bnf constraint_def = let @@ -199,7 +200,8 @@ in_rel_of_bnf bnf, pred_def]), rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt, CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp), - etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}], + etac imageE, dtac set_rev_mp, assume_tac ctxt, + REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}], hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]}, etac @{thm DomainPI}]) set_map's, REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI], @@ -209,7 +211,8 @@ rtac @{thm fst_conv}]), rtac CollectI, CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}), REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}], - dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's + dtac (rotate_prems 1 bspec), assume_tac ctxt, + etac @{thm DomainpE}, etac @{thm someI}]) set_map's ] i end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/cnf.ML --- a/src/HOL/Tools/cnf.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/cnf.ML Mon Nov 10 21:49:48 2014 +0100 @@ -42,7 +42,7 @@ val clause2raw_thm: thm -> thm val make_nnf_thm: theory -> term -> thm - val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) + val weakening_tac: Proof.context -> int -> tactic (* removes the first hypothesis of a subgoal *) val make_cnf_thm: Proof.context -> term -> thm val make_cnfx_thm: Proof.context -> term -> thm @@ -528,8 +528,8 @@ (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal *) (* ------------------------------------------------------------------------- *) -fun weakening_tac i = - dresolve_tac [weakening_thm] i THEN assume_tac (i+1); +fun weakening_tac ctxt i = + dresolve_tac [weakening_thm] i THEN assume_tac ctxt (i+1); (* ------------------------------------------------------------------------- *) (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *) @@ -551,7 +551,7 @@ let val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) in - PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm + PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm end) i; (* ------------------------------------------------------------------------- *) @@ -573,7 +573,7 @@ let val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) in - PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm + PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm end) i; end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Mon Nov 10 21:49:48 2014 +0100 @@ -118,7 +118,7 @@ ALLGOALS (Object_Logic.atomize_prems_tac ctxt), rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites), REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => - REPEAT (etac allE i) THEN atac i)) 1)]) + REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)]) |> Drule.export_without_context; val ind_name = Thm.derivation_name induct; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/inductive.ML Mon Nov 10 21:49:48 2014 +0100 @@ -381,7 +381,7 @@ (fn _ => EVERY [resolve_tac @{thms monoI} 1, REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1), REPEAT (FIRST - [assume_tac 1, + [assume_tac ctxt 1, resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1, eresolve_tac @{thms le_funE} 1, dresolve_tac @{thms le_boolD} 1])])); @@ -406,7 +406,7 @@ EVERY1 (select_disj (length intr_ts) (i + 1)), (*Not ares_tac, since refl must be tried before any equality assumptions; backtracking may occur if the premises have extra variables!*) - DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) + DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac ctxt 1)]) |> singleton (Proof_Context.export ctxt ctxt')) intr_ts in (intrs, unfold) end; @@ -544,7 +544,7 @@ (*delete needless equality assumptions*) val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"} - (fn _ => assume_tac 1); + (fn {context = ctxt, ...} => assume_tac ctxt 1); val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; val elim_tac = REPEAT o eresolve_tac elim_rls; @@ -741,7 +741,7 @@ some premise involves disjunction.*) REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)), REPEAT (FIRSTGOAL - (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))), + (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac ctxt3))), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, conjI, refl] 1)) prems)]); @@ -752,9 +752,9 @@ REPEAT (EVERY [REPEAT (resolve_tac [conjI, impI] 1), REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1), - assume_tac 1, + assume_tac ctxt3 1, rewrite_goals_tac ctxt3 simp_thms1, - assume_tac 1])]); + assume_tac ctxt3 1])]); in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Mon Nov 10 21:49:48 2014 +0100 @@ -397,7 +397,7 @@ rewrite_goals_tac ctxt rews, REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt, - DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); + DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]); val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) @@ -460,7 +460,7 @@ ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)), rewrite_goals_tac ctxt rews, REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN' - DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); + DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]); val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_" (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy in diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/record.ML Mon Nov 10 21:49:48 2014 +0100 @@ -1625,9 +1625,9 @@ (fn {context = ctxt, ...} => EVERY1 [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt, - etac @{thm meta_allE}, atac, + etac @{thm meta_allE}, assume_tac ctxt, rtac (@{thm prop_subst} OF [surject]), - REPEAT o etac @{thm meta_allE}, atac])); + REPEAT o etac @{thm meta_allE}, assume_tac ctxt])); val induct = timeit_msg ctxt "record extension induct proof:" (fn () => let val (assm, concl) = induct_prop in @@ -2160,9 +2160,9 @@ (fn {context = ctxt', ...} => EVERY1 [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt', - etac @{thm meta_allE}, atac, + etac @{thm meta_allE}, assume_tac ctxt', rtac (@{thm prop_subst} OF [surjective]), - REPEAT o etac @{thm meta_allE}, atac])); + REPEAT o etac @{thm meta_allE}, assume_tac ctxt'])); val split_object = timeit_msg ctxt "record split_object proof:" (fn () => Goal.prove_sorry_global defs_thy [] [] split_object_prop diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Mon Nov 10 21:49:48 2014 +0100 @@ -344,7 +344,7 @@ THEN' resolve_tac @{thms UnI2} THEN' tac1_of_formula ctxt fm2 | tac1_of_formula ctxt (Atom _) = - REPEAT_DETERM1 o (assume_tac + REPEAT_DETERM1 o (assume_tac ctxt ORELSE' resolve_tac @{thms SigmaI} ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN' TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])) @@ -356,7 +356,7 @@ ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]}))) ORELSE' resolve_tac @{thms UNIV_I} ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]} - ORELSE' assume_tac) + ORELSE' assume_tac ctxt) fun tac2_of_formula ctxt (Int (fm1, fm2)) = TRY o eresolve_tac @{thms IntE} @@ -370,7 +370,7 @@ THEN' tac2_of_formula ctxt fm2 | tac2_of_formula ctxt (Atom _) = REPEAT_DETERM o - (assume_tac + (assume_tac ctxt ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]} ORELSE' eresolve_tac @{thms conjE} ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN' @@ -434,14 +434,14 @@ THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms) THEN' resolve_tac @{thms iffI} THEN' REPEAT_DETERM o resolve_tac @{thms exI} - THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac + THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac ctxt THEN' REPEAT_DETERM o eresolve_tac @{thms exE} THEN' eresolve_tac @{thms conjE} THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject} THEN' Subgoal.FOCUS (fn {prems, ...} => (* FIXME inner context!? *) simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt - THEN' TRY o assume_tac + THEN' TRY o assume_tac ctxt in case try mk_term (term_of ct) of NONE => Thm.reflexive ct diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/simpdata.ML Mon Nov 10 21:49:48 2014 +0100 @@ -119,7 +119,7 @@ val sol_thms = 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 + FIRST [resolve_tac sol_thms i, assume_tac ctxt i , eresolve_tac @{thms FalseE} i] ORELSE (match_tac ctxt intros THEN_ALL_NEW sol_tac) i in (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Nov 10 21:49:48 2014 +0100 @@ -713,7 +713,7 @@ EVERY [ simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1, rtac @{thm guarantees_PLam_I} 1, - assume_tac 2, + assume_tac ctxt 2, (*preserves: routine reasoning*) asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2, (*the guarantee for "lift i (rename client_map Client)" *) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Nov 10 21:49:48 2014 +0100 @@ -110,7 +110,7 @@ full_simp_tac ctxt 1, REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])), - REPEAT (FIRSTGOAL analz_mono_contra_tac), + REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)), ALLGOALS (asm_simp_tac ctxt)]) i; (*Tactic for proving secrecy theorems*) diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Nov 10 21:49:48 2014 +0100 @@ -6,7 +6,8 @@ *) (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) -val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin} +fun Always_Int_tac ctxt = + dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin} (*Combines a list of invariance THEOREMS into one.*) val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}) @@ -16,7 +17,7 @@ fun constrains_tac ctxt i = SELECT_GOAL (EVERY - [REPEAT (Always_Int_tac 1), + [REPEAT (Always_Int_tac ctxt 1), (*reduce the fancy safety properties to "constrains"*) REPEAT (etac @{thm Always_ConstrainsI} 1 ORELSE @@ -35,7 +36,7 @@ fun ensures_tac ctxt sact = SELECT_GOAL (EVERY - [REPEAT (Always_Int_tac 1), + [REPEAT (Always_Int_tac ctxt 1), etac @{thm Always_LeadsTo_Basis} 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Word/Word.thy Mon Nov 10 21:49:48 2014 +0100 @@ -1565,8 +1565,8 @@ ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN REPEAT (etac conjE n) THEN REPEAT (dtac @{thm word_of_int_inverse} n - THEN atac n - THEN atac n)), + THEN assume_tac ctxt n + THEN assume_tac ctxt n)), TRYALL arith_tac' ] end diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/ex/Meson_Test.thy Mon Nov 10 21:49:48 2014 +0100 @@ -40,7 +40,7 @@ val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => rtac go25 1 THEN - Meson.depth_prolog_tac horns25); + Meson.depth_prolog_tac ctxt' horns25); *} oops @@ -66,7 +66,7 @@ val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => rtac go26 1 THEN - Meson.depth_prolog_tac horns26); (*7 ms*) + Meson.depth_prolog_tac ctxt' horns26); (*7 ms*) (*Proof is of length 107!!*) *} oops @@ -93,7 +93,7 @@ val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => rtac go43 1 THEN - Meson.best_prolog_tac Meson.size_of_subgoals horns43); (*7ms*) + Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43); (*7ms*) *} oops diff -r 4bee6d8c1500 -r 26bf09b95dda src/Provers/blast.ML --- a/src/Provers/blast.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Provers/blast.ML Mon Nov 10 21:49:48 2014 +0100 @@ -782,14 +782,14 @@ (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) fun contr_tac ctxt = - ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac); + ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); (*Try to unify complementary literals and return the corresponding tactic. *) fun tryClose state (G, L) = let val State {ctxt, ...} = state; val eContr_tac = TRACE ctxt Data.notE contr_tac; - val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac); + val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac ctxt); fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; fun arg (_ $ t) = t; in diff -r 4bee6d8c1500 -r 26bf09b95dda src/Provers/classical.ML --- a/src/Provers/classical.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Provers/classical.ML Mon Nov 10 21:49:48 2014 +0100 @@ -71,14 +71,14 @@ val depth_tac: Proof.context -> int -> int -> tactic val deepen_tac: Proof.context -> int -> int -> tactic - val contr_tac: int -> tactic + val contr_tac: Proof.context -> int -> tactic val dup_elim: Context.generic option -> thm -> thm val dup_intr: thm -> thm val dup_step_tac: Proof.context -> 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 + val mp_tac: Proof.context -> int -> tactic val safe_tac: Proof.context -> tactic val safe_steps_tac: Proof.context -> int -> tactic val safe_step_tac: Proof.context -> int -> tactic @@ -87,7 +87,7 @@ val step_tac: Proof.context -> int -> tactic val slow_step_tac: Proof.context -> int -> tactic val swapify: thm list -> thm list - val swap_res_tac: thm list -> int -> tactic + val swap_res_tac: Proof.context -> thm list -> int -> tactic val inst_step_tac: Proof.context -> int -> tactic val inst0_step_tac: Proof.context -> int -> tactic val instp_step_tac: Proof.context -> int -> tactic @@ -179,12 +179,12 @@ (*Prove goal that assumes both P and ~P. No backtracking if it finds an equal assumption. Perhaps should call ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) -val contr_tac = - eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac); +fun contr_tac ctxt = + eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt); (*Finds P-->Q and P in the assumptions, replaces implication by Q. Could do the same thing for P<->Q and P... *) -fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i; +fun mp_tac ctxt i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i; (*Like mp_tac but instantiates no variables*) fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i; @@ -195,10 +195,10 @@ (*Uses introduction rules in the normal way, or on negated assumptions, trying rules in order. *) -fun swap_res_tac rls = +fun swap_res_tac ctxt rls = let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in - assume_tac ORELSE' - contr_tac ORELSE' + assume_tac ctxt ORELSE' + contr_tac ctxt ORELSE' biresolve_tac (fold_rev addrl rls []) end; @@ -693,9 +693,9 @@ 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); + ctxt addafter (name, fn ctxt' => dresolve_tac [thm] THEN' assume_tac ctxt'); fun ctxt addE2 (name, thm) = - ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac); + ctxt addafter (name, fn ctxt' => eresolve_tac [thm] THEN' assume_tac ctxt'); fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac); fun ctxt addSE2 (name, thm) = @@ -762,8 +762,8 @@ (*Backtracking is allowed among the various these unsafe ways of proving a subgoal. *) fun inst0_step_tac ctxt = - assume_tac APPEND' - contr_tac APPEND' + assume_tac ctxt APPEND' + contr_tac ctxt APPEND' biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt)); (*These unsafe steps could generate more subgoals.*) diff -r 4bee6d8c1500 -r 26bf09b95dda src/Provers/typedsimp.ML --- a/src/Provers/typedsimp.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Provers/typedsimp.ML Mon Nov 10 21:49:48 2014 +0100 @@ -18,19 +18,19 @@ (*Built-in rewrite rules*) val default_rls: thm list (*Type checking or similar -- solution of routine conditions*) - val routine_tac: thm list -> int -> tactic + val routine_tac: Proof.context -> thm list -> int -> tactic end; signature TSIMP = sig - val asm_res_tac: thm list -> int -> tactic - val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic - val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic - val norm_tac: (thm list * thm list) -> tactic + val asm_res_tac: Proof.context -> thm list -> int -> tactic + val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic + val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic + val norm_tac: Proof.context -> (thm list * thm list) -> tactic val process_rules: thm list -> thm list * thm list val rewrite_res_tac: int -> tactic val split_eqn: thm - val step_tac: (thm list * thm list) -> int -> tactic + val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic val subconv_res_tac: thm list -> int -> tactic end; @@ -95,29 +95,29 @@ ORELSE' filt_resolve_tac [refl,refl_red] 1; (*Resolve with asms, whether rewrites or not*) -fun asm_res_tac asms = +fun asm_res_tac ctxt asms = let val (xsimp_rls,xother_rls) = process_rules asms - in routine_tac xother_rls ORELSE' + in routine_tac ctxt xother_rls ORELSE' filt_resolve_tac xsimp_rls 2 end; (*Single step for simple rewriting*) -fun step_tac (congr_rls,asms) = - asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' +fun step_tac ctxt (congr_rls,asms) = + asm_res_tac ctxt asms ORELSE' rewrite_res_tac ORELSE' subconv_res_tac congr_rls; (*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*) -fun cond_step_tac (prove_cond_tac, congr_rls, asms) = - asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' +fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) = + asm_res_tac ctxt asms ORELSE' rewrite_res_tac ORELSE' (resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE' subconv_res_tac congr_rls; (*Unconditional normalization tactic*) -fun norm_tac arg = REPEAT_FIRST (step_tac arg) THEN +fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg) THEN TRYALL (resolve_tac [red_if_equal]); (*Conditional normalization tactic*) -fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg) THEN +fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg) THEN TRYALL (resolve_tac [red_if_equal]); end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Pure/Isar/class_declaration.ML Mon Nov 10 21:49:48 2014 +0100 @@ -97,7 +97,7 @@ fun tac ctxt = REPEAT (SOMEGOAL (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs) - ORELSE' assume_tac)); + ORELSE' assume_tac ctxt)); 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 4bee6d8c1500 -r 26bf09b95dda src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Pure/Isar/method.ML Mon Nov 10 21:49:48 2014 +0100 @@ -167,7 +167,7 @@ in fun assm_tac ctxt = - assume_tac APPEND' + assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt APPEND' cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND' cond_rtac (can Logic.dest_term) Drule.termI; @@ -211,7 +211,7 @@ THEN_ALL_NEW Goal.norm_hhf_tac ctxt; fun gen_arule_tac tac ctxt j rules facts = - EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac); + EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt)); fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => let diff -r 4bee6d8c1500 -r 26bf09b95dda src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Pure/Tools/rule_insts.ML Mon Nov 10 21:49:48 2014 +0100 @@ -301,7 +301,7 @@ fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule); (*forward tactic applies a rule to an assumption without deleting it*) -fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac; +fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac ctxt; (*dresolve tactic applies a rule to replace an assumption*) fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule); diff -r 4bee6d8c1500 -r 26bf09b95dda src/Pure/goal.ML --- a/src/Pure/goal.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Pure/goal.ML Mon Nov 10 21:49:48 2014 +0100 @@ -336,7 +336,7 @@ val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val tacs = Rs |> map (fn R => - eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac); + eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt); in fold_rev (curry op APPEND') tacs (K no_tac) i end); end; diff -r 4bee6d8c1500 -r 26bf09b95dda src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Pure/simplifier.ML Mon Nov 10 21:49:48 2014 +0100 @@ -384,7 +384,7 @@ val trivialities = Drule.reflexive_thm :: trivs; fun unsafe_solver_tac ctxt = - FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac]; + FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt]; val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; (*no premature instantiation of variables during simplification*) diff -r 4bee6d8c1500 -r 26bf09b95dda src/Pure/tactic.ML --- a/src/Pure/tactic.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Pure/tactic.ML Mon Nov 10 21:49:48 2014 +0100 @@ -8,7 +8,7 @@ sig val trace_goalno_tac: (int -> tactic) -> int -> tactic val rule_by_tactic: Proof.context -> tactic -> thm -> thm - val assume_tac: int -> tactic + val assume_tac: Proof.context -> int -> tactic val eq_assume_tac: int -> tactic val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic val make_elim: thm -> thm @@ -101,7 +101,8 @@ thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) (*Solve subgoal i by assumption*) -fun assume_tac i = PRIMSEQ (Thm.assumption NONE i); +fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i); +fun atac i = PRIMSEQ (Thm.assumption NONE i); (*Solve subgoal i by assumption, using no unification*) fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i); @@ -128,22 +129,21 @@ fun eresolve_tac rules = biresolve_tac (map (pair true) rules); (*Forward reasoning using destruction rules.*) -fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; +fun forward_tac rls = resolve_tac (map make_elim rls) THEN' atac; (*Like forward_tac, but deletes the assumption after use.*) fun dresolve_tac rls = eresolve_tac (map make_elim rls); (*Shorthand versions: for resolution with a single theorem*) -val atac = assume_tac; fun rtac rl = resolve_tac [rl]; fun dtac rl = dresolve_tac [rl]; fun etac rl = eresolve_tac [rl]; fun ftac rl = forward_tac [rl]; (*Use an assumption or some rules ... A popular combination!*) -fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; +fun ares_tac rules = atac ORELSE' resolve_tac rules; -fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; +fun solve_tac rules = resolve_tac rules THEN_ALL_NEW atac; (*Matching tactics -- as above, but forbid updating of state*) fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i); diff -r 4bee6d8c1500 -r 26bf09b95dda src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Sequents/simpdata.ML Mon Nov 10 21:49:48 2014 +0100 @@ -58,7 +58,7 @@ @{thm iff_refl}, reflexive_thm]; fun unsafe_solver ctxt = - FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac]; + FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt]; (*No premature instantiation of variables during simplification*) fun safe_solver ctxt = diff -r 4bee6d8c1500 -r 26bf09b95dda src/Tools/intuitionistic.ML --- a/src/Tools/intuitionistic.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Tools/intuitionistic.ML Mon Nov 10 21:49:48 2014 +0100 @@ -34,7 +34,7 @@ fun unsafe_step_tac ctxt = Context_Rules.wrap ctxt - (assume_tac APPEND' + (assume_tac ctxt APPEND' bires_tac false (Context_Rules.netpair_bang ctxt) APPEND' bires_tac false (Context_Rules.netpair ctxt)); diff -r 4bee6d8c1500 -r 26bf09b95dda src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/ZF/Tools/inductive_package.ML Mon Nov 10 21:49:48 2014 +0100 @@ -220,7 +220,7 @@ resolve_tac [disjIn] 2, (*Not ares_tac, since refl must be tried before equality assumptions; backtracking may occur if the premises have extra variables!*) - DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2), + DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac ctxt 2), (*Now solve the equations like Tcons(a,f) = Inl(?b4)*) rewrite_goals_tac ctxt con_defs, REPEAT (resolve_tac @{thms refl} 2), @@ -233,7 +233,7 @@ ORELSE' hyp_subst_tac ctxt1)), if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:" else all_tac, - DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)]; + DEPTH_SOLVE (swap_res_tac ctxt (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)]; (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*) val mk_disj_rls = Balanced_Tree.accesses @@ -330,7 +330,7 @@ |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))) setSolver (mk_solver "minimal" (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt) - ORELSE' assume_tac + ORELSE' assume_tac ctxt ORELSE' eresolve_tac @{thms FalseE})); val quant_induct = diff -r 4bee6d8c1500 -r 26bf09b95dda src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/ZF/Tools/typechk.ML Mon Nov 10 21:49:48 2014 +0100 @@ -81,16 +81,17 @@ | is_rigid_elem _ = false; (*Try solving a:A by assumption provided a is rigid!*) -val test_assume_tac = SUBGOAL(fn (prem,i) => +fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) => if is_rigid_elem (Logic.strip_assums_concl prem) - then assume_tac i else eq_assume_tac i); + then assume_tac ctxt i else eq_assume_tac i); (*Type checking solves a:?A (a rigid, ?A maybe flexible). match_tac is too strict; would refuse to instantiate ?A*) -fun typecheck_step_tac (TC{net,...}) = - FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net); +fun typecheck_step_tac ctxt = + let val TC {net, ...} = tcset_of ctxt + in FIRSTGOAL (test_assume_tac ctxt ORELSE' net_res_tac 3 net) end; -fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt)); +fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt); (*Compiles a term-net for speed*) val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @@ -102,7 +103,7 @@ (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1 ORELSE basic_res_tac 1 ORELSE (ares_tac hyps 1 - APPEND typecheck_step_tac (tcset_of ctxt)))); + APPEND typecheck_step_tac ctxt))); val type_solver = Simplifier.mk_solver "ZF typecheck" (fn ctxt => diff -r 4bee6d8c1500 -r 26bf09b95dda src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/ZF/UNITY/Constrains.thy Mon Nov 10 21:49:48 2014 +0100 @@ -459,7 +459,8 @@ ML {* (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) -val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}; +fun Always_Int_tac ctxt = + dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}; (*Combines a list of invariance THEOREMS into one.*) val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}); @@ -468,7 +469,7 @@ fun constrains_tac ctxt = SELECT_GOAL - (EVERY [REPEAT (Always_Int_tac 1), + (EVERY [REPEAT (Always_Int_tac ctxt 1), REPEAT (etac @{thm Always_ConstrainsI} 1 ORELSE resolve_tac [@{thm StableI}, @{thm stableI}, diff -r 4bee6d8c1500 -r 26bf09b95dda src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/ZF/UNITY/SubstAx.thy Mon Nov 10 21:49:48 2014 +0100 @@ -352,7 +352,7 @@ (*proves "ensures/leadsTo" properties when the program is specified*) fun ensures_tac ctxt sact = SELECT_GOAL - (EVERY [REPEAT (Always_Int_tac 1), + (EVERY [REPEAT (Always_Int_tac ctxt 1), etac @{thm Always_LeadsTo_Basis} 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},