--- 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.
--- 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); <a,x>:r; <x,a>:r |] ==> P"
--- 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
--- 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
--- 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
--- 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(<x,y>))"
-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(<x,y>))
--> (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(<kd,ke>) *)
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
--- 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) ==> <split(p,%x y. x), split(p,%x y. y)> = 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.<w,v>)) ` <a,b> = <b,a> : 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
--- 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,j>, 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)), <succ(0), 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,j>)), i)
* Eq(?A, ?b(inr(<i,j>)), 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
--- 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. <w,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
--- 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));
--- 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
--- 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 \<open>
fun subgoaler_tac ctxt =
- assume_tac ORELSE'
+ assume_tac ctxt ORELSE'
resolve_tac (Simplifier.prems_of ctxt) ORELSE'
asm_simp_tac ctxt
\<close>
--- 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 \<subseteq> 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 \<notin> 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 \<notin> synth (analz (knows Spy evs)) --> P"
(*>*)
--- 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
*}
--- 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));
--- 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*)
--- 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
--- 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;
--- 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
--- 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
--- 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
--- 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;
--- 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);
--- 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 \<notin> 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 \<notin> synth (analz (knows Spy evs)) --> P"
end
--- 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
--- 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)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>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}) *})
--- 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 @@
"\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk>
\<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {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\<Colon>\<preceq>(G, L)"
proof (cases "normal s0")
@@ -2065,7 +2065,7 @@
(abupd (absorb (Cont l')) s2') \<diamondsuit> 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
--- 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\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (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)
--- 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+
--- 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
--- 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) $ _ =>
--- 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) $ _ =>
--- 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
--- 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)
--- 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
--- 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) *})
--- 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 *)
--- 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<Y>" 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
--- 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,s> -c-> t ==> ? n. <c,s> -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
--- 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"
--- 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' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^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: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
--- 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
--- 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
--- 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);
--- 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)]))
*}
--- 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 \<notin> analz (knows Spy evs) --> P"
end
--- 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)]))
*}
--- 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 {*
--- 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);
*}
--- 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) =
--- 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;
--- 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;
--- 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;
--- 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;
--- 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]))
--- 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 =
--- 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
--- 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
--- 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 =
--- 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
--- 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 =
--- 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],
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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
--- 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)" *)
--- 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*)
--- 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},
--- 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
--- 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
--- 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
--- 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.*)
--- 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;
--- 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;
--- 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
--- 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);
--- 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;
--- 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*)
--- 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);
--- 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 =
--- 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));
--- 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 =
--- 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 =>
--- 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},
--- 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},