--- a/doc-src/IsarRef/Thy/ML_Tactic.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Sat Jun 14 23:19:51 2008 +0200
@@ -41,7 +41,7 @@
@{ML forward_tac}).
\item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
- @{ML res_inst_tac}).
+ @{ML RuleInsts.res_inst_tac}).
\item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
vs.\ @{ML rtac}).
@@ -66,11 +66,11 @@
\begin{tabular}{lll}
@{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
@{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
- @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
+ @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
@{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
@{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
@{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
- @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
+ @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
@{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
\end{tabular}
\medskip
--- a/src/CCL/CCL.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/CCL.thy Sat Jun 14 23:19:51 2008 +0200
@@ -414,7 +414,8 @@
done
ML {*
- fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
+ fun po_coinduct_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
*}
@@ -459,8 +460,11 @@
done
ML {*
- fun eq_coinduct_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct} i
- fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct3} i
+ fun eq_coinduct_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
+
+ fun eq_coinduct3_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
*}
--- a/src/CCL/Hered.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/Hered.thy Sat Jun 14 23:19:51 2008 +0200
@@ -97,7 +97,8 @@
done
ML {*
- fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
+ fun HTT_coinduct_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
*}
lemma HTT_coinduct3:
@@ -109,7 +110,8 @@
ML {*
val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
-fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
+fun HTT_coinduct3_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
val HTTgenIs =
map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
--- a/src/CCL/Wfd.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/Wfd.thy Sat Jun 14 23:19:51 2008 +0200
@@ -54,8 +54,8 @@
done
ML {*
- fun wfd_strengthen_tac s i =
- res_inst_tac [("Q",s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
+ fun wfd_strengthen_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
*}
lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"
@@ -123,7 +123,7 @@
shows "Wfd(R**S)"
apply (unfold Wfd_def)
apply safe
- apply (tactic {* wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1 *})
+ apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
apply (blast elim!: lex_pair)
apply (subgoal_tac "ALL a b.<a,b>:P")
apply blast
@@ -209,7 +209,7 @@
lemma NatPR_wf: "Wfd(NatPR)"
apply (unfold Wfd_def)
apply clarify
- apply (tactic {* wfd_strengthen_tac "%x. x:Nat" 1 *})
+ apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
apply (fastsimp iff: NatPRXH)
apply (erule Nat_ind)
apply (fastsimp iff: NatPRXH)+
@@ -218,7 +218,7 @@
lemma ListPR_wf: "Wfd(ListPR(A))"
apply (unfold Wfd_def)
apply clarify
- apply (tactic {* wfd_strengthen_tac "%x. x:List (A)" 1 *})
+ apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
apply (fastsimp iff: ListPRXH)
apply (erule List_ind)
apply (fastsimp iff: ListPRXH)+
@@ -465,7 +465,7 @@
| _ => false
in
-fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i
+fun rcall_tac i = let fun tac ps rl i = Tactic.res_inst_tac ps rl i THEN atac i
in IHinst tac rcallTs i end THEN
eresolve_tac rcall_lemmas i
@@ -487,7 +487,7 @@
hyp_subst_tac)
val clean_ccs_tac =
- let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i
+ let fun tac ps rl i = Tactic.eres_inst_tac ps rl i THEN atac i
in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
hyp_subst_tac)) end
--- a/src/CCL/ex/Stream.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CCL/ex/Stream.thy Sat Jun 14 23:19:51 2008 +0200
@@ -32,7 +32,7 @@
lemma map_comp:
assumes 1: "l:Lists(A)"
shows "map(f o g,l) = map(f,map(g,l))"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
apply (blast intro: 1)
apply safe
@@ -46,7 +46,7 @@
lemma map_id:
assumes 1: "l:Lists(A)"
shows "map(%x. x,l) = l"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *})
apply (blast intro: 1)
apply safe
@@ -62,7 +62,7 @@
assumes "l:Lists(A)"
and "m:Lists(A)"
shows "map(f,l@m) = map(f,l) @ map(f,m)"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:Lists (A). EX m:Lists (A). x=map (f,l@m) & y=map (f,l) @ map (f,m))}" 1 *})
apply (blast intro: prems)
apply safe
@@ -81,7 +81,7 @@
and "l:Lists(A)"
and "m:Lists(A)"
shows "k @ l @ m = (k @ l) @ m"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX k:Lists (A). EX l:Lists (A). EX m:Lists (A). x=k @ l @ m & y= (k @ l) @ m) }" 1*})
apply (blast intro: prems)
apply safe
@@ -99,7 +99,7 @@
lemma ilist_append:
assumes "l:ILists(A)"
shows "l @ m = l"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
apply (blast intro: prems)
apply safe
@@ -133,7 +133,7 @@
done
lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
- apply (tactic {* eq_coinduct3_tac
+ apply (tactic {* eq_coinduct3_tac @{context}
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
--- a/src/CTT/Arith.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CTT/Arith.thy Sat Jun 14 23:19:51 2008 +0200
@@ -130,7 +130,7 @@
lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
apply (unfold arith_defs)
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
apply (tactic "hyp_rew_tac []")
done
@@ -140,7 +140,7 @@
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 {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
apply (tactic "hyp_rew_tac []")
done
@@ -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 "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (tactic "hyp_arith_rew_tac []")
done
@@ -196,11 +196,11 @@
(*Commutative law for addition. Can be proved using three inductions.
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 "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (tactic "hyp_arith_rew_tac []")
-apply (tactic {* NE_tac "b" 2 *})
+apply (tactic {* NE_tac @{context} "b" 2 *})
apply (rule sym_elem)
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
apply (tactic "hyp_arith_rew_tac []")
done
@@ -209,33 +209,33 @@
(*right annihilation in product*)
lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (tactic "hyp_arith_rew_tac []")
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 "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{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 "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{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 "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{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 "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
+apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *})
done
@@ -246,7 +246,7 @@
a - b = 0 iff a<=b a - b = succ(c) iff a>b *}
lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (tactic "hyp_arith_rew_tac []")
done
@@ -258,12 +258,12 @@
An example of induction over a quantified formula (a product).
Uses rewriting with a quantified, implicative inductive hypothesis.*)
lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
-apply (tactic {* NE_tac "b" 1 *})
+apply (tactic {* NE_tac @{context} "b" 1 *})
(*strip one "universal quantifier" but not the "implication"*)
apply (rule_tac [3] intr_rls)
(*case analysis on x in
(succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
-apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
+apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4")
(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
apply (rule_tac [5] replace_type)
apply (rule_tac [4] replace_type)
@@ -326,7 +326,7 @@
(*If a+b=0 then a=0. Surprisingly tedious*)
lemma add_eq0_lemma: "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"
-apply (tactic {* NE_tac "a" 1 *})
+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*)
@@ -434,14 +434,14 @@
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 {* NE_tac "succ (a mod b) |-|b" 1 *})
+apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
done
(*for case analysis on whether a number is 0 or a successor*)
lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
-apply (tactic {* NE_tac "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (rule_tac [3] PlusI_inr)
apply (rule_tac [2] PlusI_inl)
apply (tactic eqintr_tac)
@@ -450,7 +450,7 @@
(*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 "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
[thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
apply (rule EqE)
--- a/src/CTT/CTT.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CTT/CTT.thy Sat Jun 14 23:19:51 2008 +0200
@@ -354,29 +354,25 @@
ML {*
local
- val routine_rls = thms "routine_rls";
- val form_rls = thms "form_rls";
- val intr_rls = thms "intr_rls";
- val element_rls = thms "element_rls";
- val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @
- thms "elimL_rls" @ thms "refl_elem"
+ val equal_rls = @{thms form_rls} @ @{thms element_rls} @ @{thms intrL_rls} @
+ @{thms elimL_rls} @ @{thms refl_elem}
in
fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
(*Solve all subgoals "A type" using formation rules. *)
-val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
+val form_tac = REPEAT_FIRST (ASSUME (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 =
- let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
+ let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
in REPEAT_FIRST (ASSUME 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 =
- let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
+ let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
in REPEAT_FIRST (ASSUME tac) end
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
@@ -412,55 +408,40 @@
lemmas reduction_rls = comp_rls [THEN trans_elem]
ML {*
-local
- val EqI = thm "EqI";
- val EqE = thm "EqE";
- val NE = thm "NE";
- val FE = thm "FE";
- val ProdI = thm "ProdI";
- val SumI = thm "SumI";
- val SumE = thm "SumE";
- val PlusE = thm "PlusE";
- val PlusI_inl = thm "PlusI_inl";
- val PlusI_inr = thm "PlusI_inr";
- val subst_prodE = thm "subst_prodE";
- val intr_rls = thms "intr_rls";
-in
-
(*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(EqI::intr_rls) 1))
+val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
(** Tactics that instantiate CTT-rules.
Vars in the given terms will be incremented!
The (rtac EqE i) lets them apply to equality judgements. **)
-fun NE_tac (sp: string) i =
- TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i
+fun NE_tac ctxt sp i =
+ TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
-fun SumE_tac (sp: string) i =
- TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i
+fun SumE_tac ctxt sp i =
+ TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
-fun PlusE_tac (sp: string) i =
- TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i
+fun PlusE_tac ctxt sp i =
+ TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
(** 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 subst_prodE i THEN assume_tac i THEN assume_tac i
+ rtac @{thm subst_prodE} i THEN assume_tac i THEN assume_tac i
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = etac subst_prodE i THEN assume_tac i
+fun mp_tac i = etac @{thm subst_prodE} i THEN assume_tac i
(*"safe" when regarded as predicate calculus rules*)
val safe_brls = sort (make_ord lessb)
- [ (true,FE), (true,asm_rl),
- (false,ProdI), (true,SumE), (true,PlusE) ]
+ [ (true, @{thm FE}), (true,asm_rl),
+ (false, @{thm ProdI}), (true, @{thm SumE}), (true, @{thm PlusE}) ]
val unsafe_brls =
- [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
- (true,subst_prodE) ]
+ [ (false, @{thm PlusI_inl}), (false, @{thm PlusI_inr}), (false, @{thm SumI}),
+ (true, @{thm subst_prodE}) ]
(*0 subgoals vs 1 or more*)
val (safe0_brls, safep_brls) =
@@ -478,8 +459,6 @@
(*Fails unless it solves the goal!*)
fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
-
-end
*}
use "rew.ML"
--- a/src/CTT/ex/Equality.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/CTT/ex/Equality.thy Sat Jun 14 23:19:51 2008 +0200
@@ -40,7 +40,7 @@
lemma "[| a:N; b:N; c:N |]
==> 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 "a" 1 *})
+apply (tactic {* NE_tac @{context} "a" 1 *})
apply (tactic "hyp_rew_tac []")
done
--- a/src/HOL/Bali/WellType.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/Bali/WellType.thy Sat Jun 14 23:19:51 2008 +0200
@@ -652,9 +652,13 @@
apply (simp_all (no_asm_use) split del: split_if_asm)
apply (safe del: disjE)
(* 17 subgoals *)
-apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
+apply (tactic {* ALLGOALS (fn i =>
+ if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
+ RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
+ RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
+ else RuleInsts.thin_tac @{context} "All ?P" i) *})
(*apply (safe del: disjE elim!: wt_elim_cases)*)
-apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
+apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
apply (simp_all (no_asm_use) split del: split_if_asm)
apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
apply ((blast del: equalityCE dest: sym [THEN trans])+)
--- a/src/HOL/IMPP/Hoare.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/IMPP/Hoare.thy Sat Jun 14 23:19:51 2008 +0200
@@ -282,7 +282,9 @@
apply (blast) (* asm *)
apply (blast) (* cut *)
apply (blast) (* weaken *)
-apply (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *})
+apply (tactic {* ALLGOALS (EVERY'
+ [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
+ simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
apply (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
--- a/src/HOL/NanoJava/Equivalence.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Sat Jun 14 23:19:51 2008 +0200
@@ -107,9 +107,9 @@
apply (tactic "split_all_tac 1", rename_tac P e Q)
apply (rule hoare_ehoare.induct)
(*18*)
-apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
-apply (tactic {* ALLGOALS (REPEAT o thin_tac "hoare ?x ?y") *})
-apply (tactic {* ALLGOALS (REPEAT o thin_tac "ehoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
+apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
apply (simp_all only: cnvalid1_eq cenvalid_def2)
apply fast
apply fast
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Jun 14 23:19:51 2008 +0200
@@ -762,12 +762,14 @@
steps of the implementation, and try to solve the idling case by simplification
*)
ML {*
-fun split_idle_tac ss simps i =
- TRY (rtac @{thm actionI} i) THEN
- case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
- rewrite_goals_tac @{thms action_rews} THEN
- forward_tac [temp_use @{thm Step1_4_7}] i THEN
- asm_full_simp_tac (ss addsimps simps) i
+fun split_idle_tac ctxt simps i =
+ let val ss = Simplifier.local_simpset_of ctxt in
+ TRY (rtac @{thm actionI} i) THEN
+ InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
+ rewrite_goals_tac @{thms action_rews} THEN
+ forward_tac [temp_use @{thm Step1_4_7}] i THEN
+ asm_full_simp_tac (ss addsimps simps) i
+ end
*}
(* ----------------------------------------------------------------------
Combine steps 1.2 and 1.4 to prove that the implementation satisfies
@@ -779,7 +781,7 @@
lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
- apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
@@ -851,7 +853,7 @@
lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S1 rmhist p)$ | (S2 rmhist p)$"
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto dest!: Step1_2_1 [temp_use])
done
@@ -885,7 +887,7 @@
lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S2 rmhist p)$ | (S3 rmhist p)$"
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto dest!: Step1_2_2 [temp_use])
done
@@ -911,7 +913,7 @@
lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto dest!: Step1_2_3 [temp_use])
done
@@ -939,7 +941,7 @@
lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
& (ALL l. $MemInv mm l)
--> (S4 rmhist p)$ | (S5 rmhist p)$"
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto dest!: Step1_2_4 [temp_use])
done
@@ -949,7 +951,7 @@
& ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p = #NotAResult)$
| ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
apply (auto dest!: Step1_2_4 [temp_use])
done
@@ -980,7 +982,7 @@
lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
& ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
--> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
- apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
+ apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
done
@@ -1009,7 +1011,7 @@
lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S5 rmhist p)$ | (S6 rmhist p)$"
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto dest!: Step1_2_5 [temp_use])
done
@@ -1035,7 +1037,7 @@
lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto dest!: Step1_2_6 [temp_use])
done
@@ -1250,7 +1252,7 @@
apply clarsimp
apply (drule WriteS4 [action_use])
apply assumption
- apply (tactic "split_idle_tac @{simpset} [] 1")
+ apply (tactic "split_idle_tac @{context} [] 1")
apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
S4RPCUnch [temp_use])
apply (auto simp: square_def dest: S4Write [temp_use])
--- a/src/HOL/TLA/TLA.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/TLA/TLA.thy Sat Jun 14 23:19:51 2008 +0200
@@ -305,17 +305,17 @@
fun merge_box_tac i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
-fun merge_temp_box_tac i =
+fun merge_temp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
- eres_inst_tac [("'a","behavior")] @{thm box_thin} i])
+ RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
-fun merge_stp_box_tac i =
+fun merge_stp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
- eres_inst_tac [("'a","state")] @{thm box_thin} i])
+ RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
-fun merge_act_box_tac i =
+fun merge_act_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
- eres_inst_tac [("'a","state * state")] @{thm box_thin} i])
+ RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
*}
(* rewrite rule to push universal quantification through box:
@@ -947,7 +947,7 @@
apply (clarsimp dest!: BoxSFI [temp_use])
apply (erule (2) ensures [temp_use])
apply (erule_tac F = F in dup_boxE)
- apply (tactic "merge_temp_box_tac 1")
+ apply (tactic "merge_temp_box_tac @{context} 1")
apply (erule STL4Edup)
apply assumption
apply (clarsimp simp: SF_def)
@@ -966,7 +966,7 @@
apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
simp: WF_def [where A = M])
apply (erule_tac F = F in dup_boxE)
- apply (tactic "merge_temp_box_tac 1")
+ apply (tactic "merge_temp_box_tac @{context} 1")
apply (erule STL4Edup)
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -975,7 +975,7 @@
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
- apply (tactic "merge_act_box_tac 1")
+ apply (tactic "merge_act_box_tac @{context} 1")
apply (frule 4 [temp_use])
apply assumption+
apply (drule STL6 [temp_use])
@@ -984,7 +984,7 @@
apply (erule_tac V = "sigmaa |= []F" in thin_rl)
apply (drule BoxWFI [temp_use])
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
- apply (tactic "merge_temp_box_tac 1")
+ apply (tactic "merge_temp_box_tac @{context} 1")
apply (erule DmdImpldup)
apply assumption
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
@@ -1004,7 +1004,7 @@
apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
apply (erule_tac F = F in dup_boxE)
apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
- apply (tactic "merge_temp_box_tac 1")
+ apply (tactic "merge_temp_box_tac @{context} 1")
apply (erule STL4Edup)
apply assumption
apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
@@ -1013,14 +1013,14 @@
apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
- apply (tactic "merge_act_box_tac 1")
+ apply (tactic "merge_act_box_tac @{context} 1")
apply (frule 4 [temp_use])
apply assumption+
apply (erule_tac V = "sigmaa |= []F" in thin_rl)
apply (drule BoxSFI [temp_use])
apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
- apply (tactic "merge_temp_box_tac 1")
+ apply (tactic "merge_temp_box_tac @{context} 1")
apply (erule DmdImpldup)
apply assumption
apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
--- a/src/HOL/Tools/split_rule.ML Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML Sat Jun 14 23:19:51 2008 +0200
@@ -15,7 +15,7 @@
sig
include BASIC_SPLIT_RULE
val split_rule_var: term -> thm -> thm
- val split_rule_goal: string list list -> thm -> thm
+ val split_rule_goal: Proof.context -> string list list -> thm -> thm
val setup: theory -> theory
end;
@@ -123,14 +123,16 @@
end;
-fun pair_tac s =
- EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac];
+fun pair_tac ctxt s =
+ RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
+ THEN' hyp_subst_tac
+ THEN' K prune_params_tac;
val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
-fun split_rule_goal xss rl =
+fun split_rule_goal ctxt xss rl =
let
- fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
+ fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
in
rl
@@ -148,7 +150,8 @@
(Scan.lift (Args.parens (Args.$$$ "complete"))
>> K (Thm.rule_attribute (K complete_split_rule)) ||
Args.and_list1 (Scan.lift (Scan.repeat Args.name))
- >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss))));
+ >> (fn xss => Thm.rule_attribute (fn context =>
+ split_rule_goal (Context.proof_of context) xss)));
val setup =
Attrib.add_attributes
--- a/src/HOL/UNITY/UNITY_tactics.ML Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Jun 14 23:19:51 2008 +0200
@@ -41,8 +41,10 @@
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
- res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
- ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
+ RuleInsts.res_inst_tac (Simplifier.the_context ss)
+ [(("act", 0), sact)] @{thm totalize_transientI} 2
+ ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
+ [(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm Domain_def}]) 3,
constrains_tac (cs,ss) 1,
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Jun 14 23:19:51 2008 +0200
@@ -104,7 +104,7 @@
--> is_exec_frag A (cex_abs h (s,xs))"
apply (unfold cex_abs_def)
apply simp
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
txt {* main case *}
apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
done
@@ -204,7 +204,7 @@
==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
apply (unfold cex_abs_def mk_trace_def filter_act_def)
apply simp
-apply (tactic {* pair_induct_tac "xs" [] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
done
@@ -220,13 +220,13 @@
apply (rule_tac x = "cex_abs h ex" in exI)
apply auto
(* Traces coincide *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (rule traces_coincide_abs)
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
(* cex_abs is execution *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -237,7 +237,7 @@
(* Liveness *)
apply (simp add: temp_weakening_def2)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
done
(* FIX: NAch Traces.ML bringen *)
@@ -354,25 +354,25 @@
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
-apply (tactic {* Seq_case_simp_tac "x" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
done
lemma ex2seqConc [rule_format]:
"Finite s1 -->
(! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac 1 *})
+apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
apply blast
(* main case *)
apply clarify
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
(* UU case *)
apply (simp add: nil_is_Conc)
(* nil case *)
apply (simp add: nil_is_Conc)
(* cons case *)
-apply (tactic {* pair_tac "aa" 1 *})
+apply (tactic {* pair_tac @{context} "aa" 1 *})
apply auto
done
@@ -390,11 +390,11 @@
(* FIX: NAch Sequence.ML bringen *)
lemma Mapnil: "(Map f$s = nil) = (s=nil)"
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
done
lemma MapUU: "(Map f$s = UU) = (s=UU)"
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
done
@@ -432,9 +432,9 @@
apply (unfold temp_strengthening_def state_strengthening_def
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
done
@@ -442,25 +442,25 @@
lemma TL_ex2seq_UU:
"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
done
lemma TL_ex2seq_nil:
"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
done
(* FIX: put to Sequence Lemmas *)
lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
-apply (tactic {* Seq_induct_tac "s" [] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *})
done
(* important property of cex_absSeq: As it is a 1to1 correspondence,
@@ -475,19 +475,19 @@
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
apply auto
done
lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
done
@@ -518,9 +518,9 @@
apply (simp add: temp_weakening_def2 state_weakening_def2
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
done
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sat Jun 14 23:19:51 2008 +0200
@@ -216,7 +216,7 @@
--> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
(* main case *)
apply (auto simp add: trans_of_defs2)
done
@@ -230,7 +230,8 @@
--> stutter (asig_of A) (fst s,ProjA2$xs) &
stutter (asig_of B) (snd s,ProjB2$xs)"
-apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs"
+ [@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *})
(* main case *)
apply (auto simp add: trans_of_defs2)
done
@@ -243,8 +244,8 @@
lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
--> Forall (%x. fst x:act (A||B)) xs)"
-apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
- thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+ @{thm is_exec_frag_def}] 1 *})
(* main case *)
apply auto
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -263,8 +264,8 @@
Forall (%x. fst x:act (A||B)) xs
--> is_exec_frag (A||B) (s,xs)"
-apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
- thm "is_exec_frag_def", thm "stutter_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+ @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
done
@@ -279,7 +280,7 @@
Forall (%x. fst x:act (A||B)) (snd ex))"
apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (rule iffI)
(* ==> *)
apply (erule conjE)+
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Sat Jun 14 23:19:51 2008 +0200
@@ -219,7 +219,7 @@
lemma lemma_2_1b:
"filter_act$(ProjA2$xs) =filter_act$xs &
filter_act$(ProjB2$xs) =filter_act$xs"
-apply (tactic {* pair_induct_tac "xs" [] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
done
@@ -234,8 +234,8 @@
lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
--> Forall (%x. x:act (A||B)) (filter_act$xs)"
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
- thm "sforall_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
+ @{thm sforall_def}] 1 *})
(* main case *)
apply auto
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -255,20 +255,20 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
-apply (tactic {* Seq_induct_tac "sch" [thm "Filter_def", thm "Forall_def",
- thm "sforall_def", thm "mkex_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
+ @{thm sforall_def}, @{thm mkex_def}] 1 *})
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
apply auto
(* Case y:A, y:B *)
-apply (tactic {* Seq_case_simp_tac "exA" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
(* Case exA=UU, Case exA=nil*)
(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
is used! --> to generate a contradiction using ~a>>ss<< UU(nil), using theorems
Cons_not_less_UU and Cons_not_less_nil *)
-apply (tactic {* Seq_case_simp_tac "exB" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
(* Case exA=a>>x, exB=b>>y *)
(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic
@@ -276,11 +276,11 @@
apply simp
(* Case y:A, y~:B *)
-apply (tactic {* Seq_case_simp_tac "exA" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
apply simp
(* Case y~:A, y:B *)
-apply (tactic {* Seq_case_simp_tac "exB" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
apply simp
(* Case y~:A, y~:B *)
@@ -298,19 +298,21 @@
val asigs = [thm "asig_of_par", thm "actions_asig_comp"]
in
-fun mkex_induct_tac sch exA exB =
- EVERY1[Seq_induct_tac sch defs,
- SIMPSET' asm_full_simp_tac,
+fun mkex_induct_tac ctxt sch exA exB =
+ let val ss = Simplifier.local_simpset_of ctxt in
+ EVERY1[Seq_induct_tac ctxt sch defs,
+ asm_full_simp_tac ss,
SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
- Seq_case_simp_tac exA,
- Seq_case_simp_tac exB,
- SIMPSET' asm_full_simp_tac,
- Seq_case_simp_tac exA,
- SIMPSET' asm_full_simp_tac,
- Seq_case_simp_tac exB,
- SIMPSET' asm_full_simp_tac,
- SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps asigs))
+ Seq_case_simp_tac ctxt exA,
+ Seq_case_simp_tac ctxt exB,
+ asm_full_simp_tac ss,
+ Seq_case_simp_tac ctxt exA,
+ asm_full_simp_tac ss,
+ Seq_case_simp_tac ctxt exB,
+ asm_full_simp_tac ss,
+ asm_full_simp_tac (ss addsimps asigs)
]
+ end
end
*}
@@ -327,7 +329,7 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
done
@@ -356,7 +358,7 @@
Filter (%a. a:act A)$sch << filter_act$exA &
Filter (%a. a:act B)$sch << filter_act$exB
--> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
done
@@ -387,7 +389,7 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
-apply (tactic {* mkex_induct_tac "sch" "exB" "exA" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
done
(*---------------------------------------------------------------------------
@@ -396,7 +398,7 @@
--------------------------------------------------------------------------- *)
lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
-apply (tactic {* Seq_induct_tac "y" [] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
done
@@ -424,8 +426,8 @@
Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
apply (simp add: ProjA_def Filter_ex_def)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
apply (rule conjI)
apply (simp (no_asm) add: mkex_def)
apply (simplesubst trick_against_eq_in_ass)
@@ -450,7 +452,7 @@
Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
(* notice necessary change of arguments exA and exB *)
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
done
@@ -466,8 +468,8 @@
Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
apply (simp add: ProjB_def Filter_ex_def)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
apply (rule conjI)
apply (simp (no_asm) add: mkex_def)
apply (simplesubst trick_against_eq_in_ass)
@@ -487,7 +489,7 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> Forall (%x. fst x : act (A ||B))
(snd (mkex A B sch (s,exA) (t,exB)))"
-apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
+apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
done
@@ -513,7 +515,7 @@
apply (simp add: compositionality_ex)
apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
apply (simp add: executions_def)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (erule conjE)
apply (simp add: sch_actions_in_AorB)
@@ -524,15 +526,15 @@
apply (rename_tac exA exB)
apply (rule_tac x = "mkex A B sch exA exB" in bexI)
(* mkex actions are just the oracle *)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
apply (simp add: Mapfst_mkex_is_sch)
(* mkex is an execution -- use compositionality on ex-level *)
apply (simp add: compositionality_ex)
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
-apply (tactic {* pair_tac "exA" 1 *})
-apply (tactic {* pair_tac "exB" 1 *})
+apply (tactic {* pair_tac @{context} "exA" 1 *})
+apply (tactic {* pair_tac @{context} "exB" 1 *})
apply (simp add: mkex_actions_in_AorB)
done
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Jun 14 23:19:51 2008 +0200
@@ -199,7 +199,8 @@
"!!A B. compatible A B ==>
! schA schB. Forall (%x. x:act (A||B)) tr
--> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
apply auto
apply (simp add: actions_of_par)
apply (case_tac "a:act A")
@@ -226,7 +227,8 @@
lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>
! schA schB. (Forall (%x. x:act B & x~:act A) tr
--> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
@@ -235,7 +237,8 @@
lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
! schA schB. (Forall (%x. x:act A & x~:act B) tr
--> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
@@ -411,7 +414,8 @@
Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
--> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
-apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
+apply (tactic {* Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
apply auto
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy Sat Jun 14 23:19:51 2008 +0200
@@ -18,7 +18,7 @@
apply auto
apply (frule inp_is_act)
apply (simp add: executions_def)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (rename_tac s ex)
apply (subgoal_tac "Finite ex")
prefer 2
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sat Jun 14 23:19:51 2008 +0200
@@ -64,14 +64,14 @@
apply (rule_tac x = "corresp_ex A f ex" in exI)
apply auto
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (erule lemma_1 [THEN spec, THEN mp])
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Sat Jun 14 23:19:51 2008 +0200
@@ -181,7 +181,7 @@
!s. reachable C s & is_exec_frag C (s,xs) -->
mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
apply (unfold corresp_ex_def)
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
(* cons case *)
apply (auto simp add: mk_traceConc)
apply (frule reachable.reachable_n)
@@ -210,7 +210,7 @@
--> is_exec_frag A (s,xs @@ ys))"
apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac 1 *})
+apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
(* main case *)
apply (auto simp add: split_paired_all)
done
@@ -230,7 +230,7 @@
apply (unfold corresp_ex_def)
apply simp
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
(* main case *)
apply auto
apply (rule_tac t = "f y" in lemma_2_1)
@@ -273,13 +273,13 @@
apply (rule_tac x = "corresp_ex A f ex" in bexI)
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -324,13 +324,13 @@
apply auto
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -351,14 +351,14 @@
apply auto
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (erule lemma_1 [THEN spec, THEN mp])
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -369,5 +369,4 @@
done
-
end
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Jun 14 23:19:51 2008 +0200
@@ -1086,44 +1086,46 @@
done
-
ML {*
-local
- val Seq_cases = thm "Seq_cases"
- val Seq_induct = thm "Seq_induct"
- val Seq_Finite_ind = thm "Seq_Finite_ind"
-in
-
-fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
- THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+fun Seq_case_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
+ THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
-fun Seq_case_simp_tac s i = Seq_case_tac s i THEN SIMPSET' asm_simp_tac (i+2)
- THEN SIMPSET' asm_full_simp_tac (i+1)
- THEN SIMPSET' asm_full_simp_tac i;
+fun Seq_case_simp_tac ctxt s i =
+ let val ss = Simplifier.local_simpset_of ctxt in
+ Seq_case_tac ctxt s i
+ THEN asm_simp_tac ss (i+2)
+ THEN asm_full_simp_tac ss (i+1)
+ THEN asm_full_simp_tac ss i
+ end;
(* rws are definitions to be unfolded for admissibility check *)
-fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
- THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac (i+1))))
- THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
+fun Seq_induct_tac ctxt s rws i =
+ let val ss = Simplifier.local_simpset_of ctxt in
+ RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
+ THEN simp_tac (ss addsimps rws) i
+ end;
-fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
- THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac i)));
+fun Seq_Finite_induct_tac ctxt i =
+ etac @{thm Seq_Finite_ind} i
+ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
-fun pair_tac s = res_inst_tac [("p",s)] PairE
- THEN' hyp_subst_tac THEN' SIMPSET' asm_full_simp_tac;
+fun pair_tac ctxt s =
+ RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE
+ THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
(* induction on a sequence of pairs with pairsplitting and simplification *)
-fun pair_induct_tac s rws i =
- res_inst_tac [("x",s)] Seq_induct i
- THEN pair_tac "a" (i+3)
- THEN (REPEAT_DETERM (CHANGED (SIMPSET' simp_tac (i+1))))
- THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
-
-end
+fun pair_induct_tac ctxt s rws i =
+ let val ss = Simplifier.local_simpset_of ctxt in
+ RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+ THEN pair_tac ctxt "a" (i+3)
+ THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
+ THEN simp_tac (ss addsimps rws) i
+ end;
*}
-
end
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sat Jun 14 23:19:51 2008 +0200
@@ -226,7 +226,7 @@
apply auto
apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
apply (simp add: executions_def)
-apply (tactic {* pair_tac "ex" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
apply auto
apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
apply (simp (no_asm_simp))
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Sat Jun 14 23:19:51 2008 +0200
@@ -172,7 +172,7 @@
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
-apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *})
(* cons case *)
apply auto
apply (rename_tac ex a t s s')
@@ -197,7 +197,7 @@
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
--> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
-apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
(* main case *)
apply auto
apply (rename_tac ex a t s s')
@@ -267,7 +267,7 @@
apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (rename_tac s ex)
apply (simp (no_asm) add: corresp_ex_sim_def)
apply (rule_tac s = "s" in traces_coincide_sim)
@@ -275,7 +275,7 @@
apply (simp add: executions_def reachable.reachable_0 sim_starts1)
(* corresp_ex_sim is execution, Lemma 2 *)
- apply (tactic {* pair_tac "ex" 1 *})
+ apply (tactic {* pair_tac @{context} "ex" 1 *})
apply (simp add: executions_def)
apply (rename_tac s ex)
--- a/src/HOLCF/IOA/meta_theory/TL.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Sat Jun 14 23:19:51 2008 +0200
@@ -155,7 +155,7 @@
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
apply (unfold tsuffix_def suffix_def)
apply auto
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply (rule_tac x = "a>>s1" in exI)
apply auto
done
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Sat Jun 14 23:19:51 2008 +0200
@@ -149,9 +149,9 @@
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
-apply (tactic {* pair_tac "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "exec" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
done
@@ -170,33 +170,33 @@
apply (simp split add: split_if)
(* TL = UU *)
apply (rule conjI)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
(* TL = nil *)
apply (rule conjI)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_tac "y" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_tac @{context} "y" 1 *})
apply (simp add: unlift_def)
apply fast
apply (simp add: unlift_def)
apply fast
apply (simp add: unlift_def)
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
(* TL =cons *)
apply (simp add: unlift_def)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply blast
apply fastsimp
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
apply fastsimp
done
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Sat Jun 14 23:19:51 2008 +0200
@@ -333,7 +333,7 @@
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
-apply (tactic "Seq_Finite_induct_tac 1")
+apply (tactic "Seq_Finite_induct_tac @{context} 1")
done
@@ -359,8 +359,8 @@
lemma execfrag_in_sig:
"!! A. is_trans_of A ==>
! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
- thm "Forall_def", thm "sforall_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
+ @{thm Forall_def}, @{thm sforall_def}] 1 *})
(* main case *)
apply (auto simp add: is_trans_of_def)
done
@@ -369,7 +369,7 @@
"!! A.[| is_trans_of A; x:executions A |] ==>
Forall (%a. a:act A) (filter_act$(snd x))"
apply (simp add: executions_def)
-apply (tactic {* pair_tac "x" 1 *})
+apply (tactic {* pair_tac @{context} "x" 1 *})
apply (rule execfrag_in_sig [THEN spec, THEN mp])
apply auto
done
@@ -386,10 +386,10 @@
(* only admissible in y, not if done in x !! *)
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)"
-apply (tactic {* pair_induct_tac "y" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
apply (intro strip)
-apply (tactic {* Seq_case_simp_tac "xa" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
apply auto
done
@@ -401,12 +401,11 @@
lemma exec_prefix2closed [rule_format]:
"! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
-apply (tactic {* pair_induct_tac "x" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *})
apply (intro strip)
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
apply auto
done
-
end
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sat Jun 14 23:19:51 2008 +0200
@@ -86,17 +86,18 @@
val prop = Logic.strip_imp_concl t';
fun tac {prems, context} =
rewrite_goals_tac defs THEN
- EVERY (tacs (map (rewrite_rule defs) prems));
+ EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
in Goal.prove_global thy [] asms prop tac end;
fun pg' thy defs t tacsf =
let
- fun tacs [] = tacsf
- | tacs prems = cut_facts_tac prems 1 :: tacsf;
+ fun tacs {prems, context} =
+ if null prems then tacsf context
+ else cut_facts_tac prems 1 :: tacsf context;
in pg'' thy defs t tacs end;
-fun case_UU_tac rews i v =
- case_split_tac (v^"=UU") i THEN
+fun case_UU_tac ctxt rews i v =
+ InductTacs.case_tac ctxt (v^"=UU") i THEN
asm_simp_tac (HOLCF_ss addsimps rews) i;
val chain_tac =
@@ -181,7 +182,7 @@
val appl = bind_fun vars (lhs == rhs);
val cs = ContProc.cont_thms lam;
val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
- in pg (def::betas) appl [rtac reflexive_thm 1] end;
+ in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
end;
val when_appl = appl_of_def ax_when_def;
@@ -234,7 +235,7 @@
rewrite_goals_tac [mk_meta_eq iso_swap],
rtac thm3 1];
in
- val exhaust = pg con_appls (mk_trp exh) tacs;
+ val exhaust = pg con_appls (mk_trp exh) (K tacs);
val casedist =
standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
end;
@@ -249,7 +250,7 @@
val axs = [when_appl, mk_meta_eq rep_strict];
val goal = bind_fun (mk_trp (strict when_app));
val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
- in pg axs goal tacs end;
+ in pg axs goal (K tacs) end;
val when_apps =
let
@@ -260,7 +261,7 @@
mk_trp (when_app`(con_app con args) ===
list_ccomb (bound_fun n 0, map %# args))));
val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
- in pg axs goal tacs end;
+ in pg axs goal (K tacs) end;
in mapn one_when 1 cons end;
end;
val when_rews = when_strict :: when_apps;
@@ -271,7 +272,7 @@
fun dis_strict (con, _) =
let
val goal = mk_trp (strict (%%:(dis_name con)));
- in pg axs_dis_def goal [rtac when_strict 1] end;
+ in pg axs_dis_def goal (K [rtac when_strict 1]) end;
fun dis_app c (con, args) =
let
@@ -279,7 +280,7 @@
val rhs = if con = c then TT else FF;
val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_dis_def goal tacs end;
+ in pg axs_dis_def goal (K tacs) end;
val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
@@ -291,7 +292,7 @@
contr_tac 1,
DETERM_UNTIL_SOLVED (CHANGED
(asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
- in pg [] goal tacs end;
+ in pg [] goal (K tacs) end;
val dis_stricts = map dis_strict cons;
val dis_defins = map dis_defin cons;
@@ -304,7 +305,7 @@
let
val goal = mk_trp (strict (%%:(mat_name con)));
val tacs = [rtac when_strict 1];
- in pg axs_mat_def goal tacs end;
+ in pg axs_mat_def goal (K tacs) end;
val mat_stricts = map mat_strict cons;
@@ -317,7 +318,7 @@
else mk_fail;
val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_mat_def goal tacs end;
+ in pg axs_mat_def goal (K tacs) end;
val mat_apps =
maps (fn (c,_) => map (one_mat c) cons) cons;
@@ -340,7 +341,7 @@
val axs = @{thm branch_def} :: axs_pat_def;
val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
- in pg axs goal tacs end;
+ in pg axs goal (K tacs) end;
fun pat_app c (con, args) =
let
@@ -349,7 +350,7 @@
val rhs = if con = fst c then pat_rhs c else mk_fail;
val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs goal tacs end;
+ in pg axs goal (K tacs) end;
val pat_stricts = map pat_strict cons;
val pat_apps = maps (fn c => map (pat_app c) cons) cons;
@@ -366,16 +367,16 @@
fun f arg = if vname arg = vn then UU else %# arg;
val goal = mk_trp (con_app2 con f args === UU);
val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
- in pg con_appls goal tacs end;
+ in pg con_appls goal (K tacs) end;
in map one_strict (nonlazy args) end;
fun con_defin (con, args) =
let
val concl = mk_trp (defined (con_app con args));
val goal = lift_defined %: (nonlazy args, concl);
- val tacs = [
+ fun tacs ctxt = [
rtac @{thm rev_contrapos} 1,
- eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
+ RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
in
@@ -394,7 +395,7 @@
val tacs = [
rtac (iso_locale RS iso_compact_abs) 1,
REPEAT (resolve_tac rules 1 ORELSE atac 1)];
- in pg con_appls goal tacs end;
+ in pg con_appls goal (K tacs) end;
in
val con_compacts = map con_compact cons;
end;
@@ -402,7 +403,7 @@
local
fun one_sel sel =
pg axs_sel_def (mk_trp (strict (%%:sel)))
- [simp_tac (HOLCF_ss addsimps when_rews) 1];
+ (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
fun sel_strict (_, args) =
List.mapPartial (Option.map one_sel o sel_of) args;
@@ -419,20 +420,20 @@
val nlas' = List.filter (fn v => v <> vnn) nlas;
val lhs = (%%:sel)`(con_app con args);
val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
- val tacs1 =
+ fun tacs1 ctxt =
if vnn mem nlas
- then [case_UU_tac (when_rews @ con_stricts) 1 vnn]
+ then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
else [];
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (tacs1 @ tacs2) end;
+ in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
fun sel_app_diff c n sel (con, args) =
let
val nlas = nonlazy args;
val goal = mk_trp (%%:sel ` con_app con args === UU);
- val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas;
+ fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in pg axs_sel_def goal (tacs1 @ tacs2) end;
+ in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
fun sel_app c n sel (con, args) =
if con = c
@@ -456,7 +457,7 @@
contr_tac 1,
DETERM_UNTIL_SOLVED (CHANGED
(asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
- in pg [] goal tacs end;
+ in pg [] goal (K tacs) end;
in
val sel_defins =
if length cons = 1
@@ -474,10 +475,10 @@
let
val goal = lift_defined %: (nonlazy args1,
mk_trp (con_app con1 args1 ~<< con_app con2 args2));
- val tacs = [
+ fun tacs ctxt = [
rtac @{thm rev_contrapos} 1,
- eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
- @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
+ RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
+ @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
@ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
@@ -527,13 +528,13 @@
val abs_less = ax_abs_iso RS (allI RS injection_less);
val tacs =
[asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
- in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end;
+ in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
val injects =
let
val abs_eq = ax_abs_iso RS (allI RS injection_eq);
val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
- in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end;
+ in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
end;
(* ----- theorems concerning one induction step ----------------------------- *)
@@ -542,7 +543,7 @@
let
val goal = mk_trp (strict (dc_copy `% "f"));
val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1];
- in pg [ax_copy_def] goal tacs end;
+ in pg [ax_copy_def] goal (K tacs) end;
local
fun copy_app (con, args) =
@@ -552,9 +553,9 @@
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
val stricts = abs_strict::when_strict::con_stricts;
- val tacs1 = map (case_UU_tac stricts 1 o vname) args';
+ fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
- in pg [ax_copy_def] goal (tacs1 @ tacs2) end;
+ in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
in
val copy_apps = map copy_app cons;
end;
@@ -564,7 +565,7 @@
let
val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
val rews = copy_strict :: copy_apps @ con_rews;
- val tacs = map (case_UU_tac rews 1) (nonlazy args) @
+ fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
[asm_simp_tac (HOLCF_ss addsimps rews) 1];
in pg [] goal tacs end;
@@ -646,8 +647,8 @@
let
fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
- val tacs = [
- nat_induct_tac "n" 1,
+ fun tacs ctxt = [
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
simp_tac iterate_Cprod_ss 1,
asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
in pg copy_take_defs goal tacs end;
@@ -656,9 +657,9 @@
fun take_0 n dn =
let
val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
- in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
+ in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
val take_0s = mapn take_0 1 dnames;
- val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
+ fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
val take_apps =
let
fun mk_eqn dn (con, args) =
@@ -670,19 +671,19 @@
fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
val simps = List.filter (has_fewer_prems 1) copy_rews;
- fun con_tac (con, args) =
+ fun con_tac ctxt (con, args) =
if nonlazy_rec args = []
then all_tac
- else EVERY (map c_UU_tac (nonlazy_rec args)) THEN
+ else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
- fun eq_tacs ((dn, _), cons) = map con_tac cons;
- val tacs =
+ fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
+ fun tacs ctxt =
simp_tac iterate_Cprod_ss 1 ::
- nat_induct_tac "n" 1 ::
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
TRY (safe_tac HOL_cs) ::
- maps eq_tacs eqs;
+ maps (eq_tacs ctxt) eqs;
in pg copy_take_defs goal tacs end;
in
val take_rews = map standard
@@ -705,8 +706,8 @@
(mapn (fn n => fn x => (P_name n, x)) 1 conss,
mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
val take_ss = HOL_ss addsimps take_rews;
- fun quant_tac i = EVERY
- (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
+ fun quant_tac ctxt i = EVERY
+ (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
fun ind_prems_tac prems = EVERY
(maps (fn cons =>
@@ -745,16 +746,16 @@
fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
val goal = ind_term concf;
- fun tacf prems =
+ fun tacf {prems, context} =
let
val tacs1 = [
- quant_tac 1,
+ quant_tac context 1,
simp_tac HOL_ss 1,
- nat_induct_tac "n" 1,
+ InductTacs.induct_tac context [[SOME "n"]] 1,
simp_tac (take_ss addsimps prems) 1,
TRY (safe_tac HOL_cs)];
fun arg_tac arg =
- case_UU_tac (prems @ con_rews) 1
+ case_UU_tac context (prems @ con_rews) 1
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
fun con_tacs (con, args) =
asm_simp_tac take_ss 1 ::
@@ -763,7 +764,7 @@
map (K (atac 1)) (nonlazy args) @
map (K (etac spec 1)) (List.filter is_rec args);
fun cases_tacs (cons, cases) =
- res_inst_tac [("x","x")] cases 1 ::
+ RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
maps con_tacs cons;
in
@@ -779,9 +780,9 @@
val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
- fun tacf prems = [
- res_inst_tac [("t", x_name n )] (ax_reach RS subst) 1,
- res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1,
+ fun tacf {prems, context} = [
+ RuleInsts.res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
+ RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
stac fix_def2 1,
REPEAT (CHANGED
(rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
@@ -814,7 +815,7 @@
resolve_tac take_lemmas 1,
asm_simp_tac take_ss 1,
atac 1];
- in pg [] goal tacs end;
+ in pg [] goal (K tacs) end;
val finite_lemmas1a = map dname_lemma dnames;
val finite_lemma1b =
@@ -829,33 +830,33 @@
end;
val goal =
mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
- fun arg_tacs vn = [
- eres_inst_tac [("x", vn)] all_dupE 1,
+ fun arg_tacs ctxt vn = [
+ RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
etac disjE 1,
asm_simp_tac (HOL_ss addsimps con_rews) 1,
asm_simp_tac take_ss 1];
- fun con_tacs (con, args) =
+ fun con_tacs ctxt (con, args) =
asm_simp_tac take_ss 1 ::
- maps arg_tacs (nonlazy_rec args);
- fun foo_tacs n (cons, cases) =
+ maps (arg_tacs ctxt) (nonlazy_rec args);
+ fun foo_tacs ctxt n (cons, cases) =
simp_tac take_ss 1 ::
rtac allI 1 ::
- res_inst_tac [("x",x_name n)] cases 1 ::
+ RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
asm_simp_tac take_ss 1 ::
- maps con_tacs cons;
- val tacs =
+ maps (con_tacs ctxt) cons;
+ fun tacs ctxt =
rtac allI 1 ::
- nat_induct_tac "n" 1 ::
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
simp_tac take_ss 1 ::
TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
- flat (mapn foo_tacs 1 (conss ~~ cases));
+ flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
in pg [] goal tacs end;
fun one_finite (dn, l1b) =
let
val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
- val tacs = [
- case_UU_tac take_rews 1 "x",
+ fun tacs ctxt = [
+ case_UU_tac ctxt take_rews 1 "x",
eresolve_tac finite_lemmas1a 1,
step_tac HOL_cs 1,
step_tac HOL_cs 1,
@@ -867,7 +868,7 @@
val ind =
let
fun concf n dn = %:(P_name n) $ %:(x_name n);
- fun tacf prems =
+ fun tacf {prems, context} =
let
fun finite_tacs (finite, fin_ind) = [
rtac(rewrite_rule axs_finite_def finite RS exE)1,
@@ -893,9 +894,9 @@
fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
fun concf n dn = %:(P_name n) $ %:(x_name n);
in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
- fun tacf prems =
+ fun tacf {prems, context} =
map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
- quant_tac 1,
+ quant_tac context 1,
rtac (adm_impl_admw RS wfix_ind) 1,
REPEAT_DETERM (rtac adm_all 1),
REPEAT_DETERM (
@@ -930,18 +931,18 @@
Library.foldr mk_all2 (xs,
Library.foldr mk_imp (mapn mk_prj 0 dnames,
foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
- fun x_tacs n x = [
+ fun x_tacs ctxt n x = [
rotate_tac (n+1) 1,
etac all2E 1,
- eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+ RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
TRY (safe_tac HOL_cs),
REPEAT (CHANGED (asm_simp_tac take_ss 1))];
- val tacs = [
+ fun tacs ctxt = [
rtac impI 1,
- nat_induct_tac "n" 1,
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
simp_tac take_ss 1,
safe_tac HOL_cs] @
- flat (mapn x_tacs 0 xs);
+ flat (mapn (x_tacs ctxt) 0 xs);
in pg [ax_bisim_def] goal tacs end;
in
val coind =
@@ -959,7 +960,7 @@
cut_facts_tac [coind_lemma] 1,
fast_tac HOL_cs 1])
take_lemmas;
- in pg [] goal tacs end;
+ in pg [] goal (K tacs) end;
end; (* local *)
in thy |> Sign.add_path comp_dnam
--- a/src/LCF/LCF.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/LCF.thy Sat Jun 14 23:19:51 2008 +0200
@@ -23,7 +23,7 @@
typedecl ('a,'b) "+" (infixl 5)
arities
- fun :: (cpo, cpo) cpo
+ "fun" :: (cpo, cpo) cpo
"*" :: (cpo, cpo) cpo
"+" :: (cpo, cpo) cpo
tr :: cpo
@@ -316,13 +316,13 @@
ML {*
- fun induct_tac v i =
- res_inst_tac[("f",v)] @{thm induct} i THEN
+ fun induct_tac ctxt v i =
+ RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
REPEAT (resolve_tac @{thms adm_lemmas} i)
*}
lemma least_FIX: "f(p) = p ==> FIX(f) << p"
- apply (tactic {* induct_tac "f" 1 *})
+ apply (tactic {* induct_tac @{context} "f" 1 *})
apply (rule minimal)
apply (intro strip)
apply (erule subst)
@@ -375,8 +375,8 @@
done
ML {*
-fun induct2_tac (f,g) i =
- res_inst_tac[("f",f),("g",g)] @{thm induct2} i THEN
+fun induct2_tac ctxt (f, g) i =
+ RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
REPEAT(resolve_tac @{thms adm_lemmas} i)
*}
--- a/src/LCF/ex/Ex1.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex1.thy Sat Jun 14 23:19:51 2008 +0200
@@ -32,7 +32,7 @@
done
lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
- apply (tactic {* induct_tac "K" 1 *})
+ apply (tactic {* induct_tac @{context} "K" 1 *})
apply (simp (no_asm))
apply (simp (no_asm) split: COND_cases_iff)
apply (intro strip)
--- a/src/LCF/ex/Ex2.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex2.thy Sat Jun 14 23:19:51 2008 +0200
@@ -23,7 +23,7 @@
lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
apply (simplesubst H)
- apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
+ apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
apply (simp (no_asm))
apply (simp (no_asm_simp) split: COND_cases_iff)
done
--- a/src/LCF/ex/Ex3.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex3.thy Sat Jun 14 23:19:51 2008 +0200
@@ -18,7 +18,7 @@
declare p_strict [simp] p_s [simp]
lemma example: "p(FIX(s),y) = FIX(s)"
- apply (tactic {* induct_tac "s" 1 *})
+ apply (tactic {* induct_tac @{context} "s" 1 *})
apply (simp (no_asm))
apply (simp (no_asm))
done
--- a/src/LCF/ex/Ex4.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/LCF/ex/Ex4.thy Sat Jun 14 23:19:51 2008 +0200
@@ -10,7 +10,7 @@
shows "FIX(f)=p"
apply (unfold eq_def)
apply (rule conjI)
- apply (tactic {* induct_tac "f" 1 *})
+ apply (tactic {* induct_tac @{context} "f" 1 *})
apply (rule minimal)
apply (intro strip)
apply (rule less_trans)
--- a/src/Sequents/LK0.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/Sequents/LK0.thy Sat Jun 14 23:19:51 2008 +0200
@@ -156,12 +156,12 @@
ML {*
(*Cut and thin, replacing the right-side formula*)
-fun cutR_tac s i =
- res_inst_tac [ ("P", s) ] @{thm cut} i THEN rtac @{thm thinR} i
+fun cutR_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
(*Cut and thin, replacing the left-side formula*)
-fun cutL_tac s i =
- res_inst_tac [("P", s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
+fun cutL_tac ctxt s i =
+ RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
*}
--- a/src/ZF/Tools/induct_tacs.ML Sat Jun 14 17:49:24 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Sat Jun 14 23:19:51 2008 +0200
@@ -10,8 +10,8 @@
signature DATATYPE_TACTICS =
sig
- val induct_tac: string -> int -> tactic
- val exhaust_tac: string -> int -> tactic
+ val induct_tac: Proof.context -> string -> int -> tactic
+ val exhaust_tac: Proof.context -> string -> int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
(Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
@@ -89,10 +89,10 @@
(2) exhaustion works for VARIABLES in the premises, not general terms
**)
-fun exhaust_induct_tac exh var i state =
+fun exhaust_induct_tac exh ctxt var i state =
let
+ val thy = ProofContext.theory_of ctxt
val (_, _, Bi, _) = dest_state (state, i)
- val thy = Thm.theory_of_thm state
val tn = find_tname var Bi
val rule =
if exh then #exhaustion (datatype_info thy tn)
@@ -102,11 +102,11 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- Tactic.eres_inst_tac' [(ixn, var)] rule i state
+ RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
- case_tac var i state
+ case_tac ctxt var i state
else error msg;
val exhaust_tac = exhaust_induct_tac true;
@@ -178,9 +178,9 @@
val setup =
Method.add_methods
- [("induct_tac", Method.goal_args Args.name induct_tac,
+ [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
"induct_tac emulation (dynamic instantiation!)"),
- ("case_tac", Method.goal_args Args.name exhaust_tac,
+ ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
"datatype case_tac emulation (dynamic instantiation!)")];
--- a/src/ZF/UNITY/SubstAx.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Sat Jun 14 23:19:51 2008 +0200
@@ -360,7 +360,7 @@
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
- res_inst_tac [("act", sact)] @{thm transientI} 2,
+ RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)