proper context for tactics derived from res_inst_tac;
authorwenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 272085fe899199f85
parent 27207 548e2d3105b9
child 27209 388fd72e9f26
proper context for tactics derived from res_inst_tac;
doc-src/IsarRef/Thy/ML_Tactic.thy
src/CCL/CCL.thy
src/CCL/Hered.thy
src/CCL/Wfd.thy
src/CCL/ex/Stream.thy
src/CTT/Arith.thy
src/CTT/CTT.thy
src/CTT/ex/Equality.thy
src/HOL/Bali/WellType.thy
src/HOL/IMPP/Hoare.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/TLA.thy
src/HOL/Tools/split_rule.ML
src/HOL/UNITY/UNITY_tactics.ML
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Deadlock.thy
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/Tools/domain/domain_theorems.ML
src/LCF/LCF.thy
src/LCF/ex/Ex1.thy
src/LCF/ex/Ex2.thy
src/LCF/ex/Ex3.thy
src/LCF/ex/Ex4.thy
src/Sequents/LK0.thy
src/ZF/Tools/induct_tacs.ML
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Sat Jun 14 17:49:24 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Sat Jun 14 23:19:51 2008 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4    @{ML forward_tac}).
     1.5  
     1.6    \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
     1.7 -  @{ML res_inst_tac}).
     1.8 +  @{ML RuleInsts.res_inst_tac}).
     1.9  
    1.10    \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
    1.11    vs.\ @{ML rtac}).
    1.12 @@ -66,11 +66,11 @@
    1.13    \begin{tabular}{lll}
    1.14      @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
    1.15      @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
    1.16 -    @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    1.17 +    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    1.18      @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
    1.19      @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
    1.20      @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
    1.21 -    @{ML res_inst_tac}~@{text "[(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    1.22 +    @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    1.23      @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
    1.24    \end{tabular}
    1.25    \medskip
     2.1 --- a/src/CCL/CCL.thy	Sat Jun 14 17:49:24 2008 +0200
     2.2 +++ b/src/CCL/CCL.thy	Sat Jun 14 23:19:51 2008 +0200
     2.3 @@ -414,7 +414,8 @@
     2.4    done
     2.5  
     2.6  ML {*
     2.7 -  fun po_coinduct_tac s i = res_inst_tac [("R",s)] @{thm po_coinduct} i
     2.8 +  fun po_coinduct_tac ctxt s i =
     2.9 +    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
    2.10  *}
    2.11  
    2.12  
    2.13 @@ -459,8 +460,11 @@
    2.14    done
    2.15  
    2.16  ML {*
    2.17 -  fun eq_coinduct_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct} i
    2.18 -  fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm eq_coinduct3} i
    2.19 +  fun eq_coinduct_tac ctxt s i =
    2.20 +    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
    2.21 +
    2.22 +  fun eq_coinduct3_tac ctxt s i =
    2.23 +    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
    2.24  *}
    2.25  
    2.26  
     3.1 --- a/src/CCL/Hered.thy	Sat Jun 14 17:49:24 2008 +0200
     3.2 +++ b/src/CCL/Hered.thy	Sat Jun 14 23:19:51 2008 +0200
     3.3 @@ -97,7 +97,8 @@
     3.4    done
     3.5  
     3.6  ML {*
     3.7 -  fun HTT_coinduct_tac s i = res_inst_tac [("R", s)] @{thm HTT_coinduct} i
     3.8 +  fun HTT_coinduct_tac ctxt s i =
     3.9 +    RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
    3.10  *}
    3.11  
    3.12  lemma HTT_coinduct3:
    3.13 @@ -109,7 +110,8 @@
    3.14  ML {*
    3.15  val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
    3.16  
    3.17 -fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] @{thm HTT_coinduct3} i
    3.18 +fun HTT_coinduct3_tac ctxt s i =
    3.19 +  RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
    3.20  
    3.21  val HTTgenIs =
    3.22    map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
     4.1 --- a/src/CCL/Wfd.thy	Sat Jun 14 17:49:24 2008 +0200
     4.2 +++ b/src/CCL/Wfd.thy	Sat Jun 14 23:19:51 2008 +0200
     4.3 @@ -54,8 +54,8 @@
     4.4    done
     4.5  
     4.6  ML {*
     4.7 -  fun wfd_strengthen_tac s i =
     4.8 -    res_inst_tac [("Q",s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
     4.9 +  fun wfd_strengthen_tac ctxt s i =
    4.10 +    RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
    4.11  *}
    4.12  
    4.13  lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
    4.14 @@ -123,7 +123,7 @@
    4.15    shows "Wfd(R**S)"
    4.16    apply (unfold Wfd_def)
    4.17    apply safe
    4.18 -  apply (tactic {* wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1 *})
    4.19 +  apply (tactic {* wfd_strengthen_tac @{context} "%x. EX a b. x=<a,b>" 1 *})
    4.20     apply (blast elim!: lex_pair)
    4.21    apply (subgoal_tac "ALL a b.<a,b>:P")
    4.22     apply blast
    4.23 @@ -209,7 +209,7 @@
    4.24  lemma NatPR_wf: "Wfd(NatPR)"
    4.25    apply (unfold Wfd_def)
    4.26    apply clarify
    4.27 -  apply (tactic {* wfd_strengthen_tac "%x. x:Nat" 1 *})
    4.28 +  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:Nat" 1 *})
    4.29     apply (fastsimp iff: NatPRXH)
    4.30    apply (erule Nat_ind)
    4.31     apply (fastsimp iff: NatPRXH)+
    4.32 @@ -218,7 +218,7 @@
    4.33  lemma ListPR_wf: "Wfd(ListPR(A))"
    4.34    apply (unfold Wfd_def)
    4.35    apply clarify
    4.36 -  apply (tactic {* wfd_strengthen_tac "%x. x:List (A)" 1 *})
    4.37 +  apply (tactic {* wfd_strengthen_tac @{context} "%x. x:List (A)" 1 *})
    4.38     apply (fastsimp iff: ListPRXH)
    4.39    apply (erule List_ind)
    4.40     apply (fastsimp iff: ListPRXH)+
    4.41 @@ -465,7 +465,7 @@
    4.42         | _ => false
    4.43  in
    4.44  
    4.45 -fun rcall_tac i = let fun tac ps rl i = res_inst_tac ps rl i THEN atac i
    4.46 +fun rcall_tac i = let fun tac ps rl i = Tactic.res_inst_tac ps rl i THEN atac i
    4.47                         in IHinst tac rcallTs i end THEN
    4.48                    eresolve_tac rcall_lemmas i
    4.49  
    4.50 @@ -487,7 +487,7 @@
    4.51                                   hyp_subst_tac)
    4.52  
    4.53  val clean_ccs_tac =
    4.54 -       let fun tac ps rl i = eres_inst_tac ps rl i THEN atac i
    4.55 +       let fun tac ps rl i = Tactic.eres_inst_tac ps rl i THEN atac i
    4.56         in TRY (REPEAT_FIRST (IHinst tac hyprcallTs ORELSE'
    4.57                         eresolve_tac ([asm_rl,SubtypeE]@rmIHs) ORELSE'
    4.58                         hyp_subst_tac)) end
     5.1 --- a/src/CCL/ex/Stream.thy	Sat Jun 14 17:49:24 2008 +0200
     5.2 +++ b/src/CCL/ex/Stream.thy	Sat Jun 14 23:19:51 2008 +0200
     5.3 @@ -32,7 +32,7 @@
     5.4  lemma map_comp:
     5.5    assumes 1: "l:Lists(A)"
     5.6    shows "map(f o g,l) = map(f,map(g,l))"
     5.7 -  apply (tactic {* eq_coinduct3_tac
     5.8 +  apply (tactic {* eq_coinduct3_tac @{context}
     5.9      "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (f o g,l) & y=map (f,map (g,l)))}" 1 *})
    5.10     apply (blast intro: 1)
    5.11    apply safe
    5.12 @@ -46,7 +46,7 @@
    5.13  lemma map_id:
    5.14    assumes 1: "l:Lists(A)"
    5.15    shows "map(%x. x,l) = l"
    5.16 -  apply (tactic {* eq_coinduct3_tac
    5.17 +  apply (tactic {* eq_coinduct3_tac @{context}
    5.18      "{p. EX x y. p=<x,y> & (EX l:Lists (A) .x=map (%x. x,l) & y=l) }" 1 *})
    5.19    apply (blast intro: 1)
    5.20    apply safe
    5.21 @@ -62,7 +62,7 @@
    5.22    assumes "l:Lists(A)"
    5.23      and "m:Lists(A)"
    5.24    shows "map(f,l@m) = map(f,l) @ map(f,m)"
    5.25 -  apply (tactic {* eq_coinduct3_tac
    5.26 +  apply (tactic {* eq_coinduct3_tac @{context}
    5.27      "{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 *})
    5.28    apply (blast intro: prems)
    5.29    apply safe
    5.30 @@ -81,7 +81,7 @@
    5.31      and "l:Lists(A)"
    5.32      and "m:Lists(A)"
    5.33    shows "k @ l @ m = (k @ l) @ m"
    5.34 -  apply (tactic {* eq_coinduct3_tac
    5.35 +  apply (tactic {* eq_coinduct3_tac @{context}
    5.36      "{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*})
    5.37    apply (blast intro: prems)
    5.38    apply safe
    5.39 @@ -99,7 +99,7 @@
    5.40  lemma ilist_append:
    5.41    assumes "l:ILists(A)"
    5.42    shows "l @ m = l"
    5.43 -  apply (tactic {* eq_coinduct3_tac
    5.44 +  apply (tactic {* eq_coinduct3_tac @{context}
    5.45      "{p. EX x y. p=<x,y> & (EX l:ILists (A) .EX m. x=l@m & y=l)}" 1 *})
    5.46    apply (blast intro: prems)
    5.47    apply safe
    5.48 @@ -133,7 +133,7 @@
    5.49    done
    5.50  
    5.51  lemma iter1_iter2_eq: "iter1(f,a) = iter2(f,a)"
    5.52 -  apply (tactic {* eq_coinduct3_tac
    5.53 +  apply (tactic {* eq_coinduct3_tac @{context}
    5.54      "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
    5.55    apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
    5.56    apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
     6.1 --- a/src/CTT/Arith.thy	Sat Jun 14 17:49:24 2008 +0200
     6.2 +++ b/src/CTT/Arith.thy	Sat Jun 14 23:19:51 2008 +0200
     6.3 @@ -130,7 +130,7 @@
     6.4  
     6.5  lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
     6.6  apply (unfold arith_defs)
     6.7 -apply (tactic {* NE_tac "b" 1 *})
     6.8 +apply (tactic {* NE_tac @{context} "b" 1 *})
     6.9  apply (tactic "hyp_rew_tac []")
    6.10  done
    6.11  
    6.12 @@ -140,7 +140,7 @@
    6.13  lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
    6.14  apply (unfold arith_defs)
    6.15  apply (tactic "hyp_rew_tac []")
    6.16 -apply (tactic {* NE_tac "b" 1 *})
    6.17 +apply (tactic {* NE_tac @{context} "b" 1 *})
    6.18  apply (tactic "hyp_rew_tac []")
    6.19  done
    6.20  
    6.21 @@ -188,7 +188,7 @@
    6.22  
    6.23  (*Associative law for addition*)
    6.24  lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
    6.25 -apply (tactic {* NE_tac "a" 1 *})
    6.26 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.27  apply (tactic "hyp_arith_rew_tac []")
    6.28  done
    6.29  
    6.30 @@ -196,11 +196,11 @@
    6.31  (*Commutative law for addition.  Can be proved using three inductions.
    6.32    Must simplify after first induction!  Orientation of rewrites is delicate*)
    6.33  lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
    6.34 -apply (tactic {* NE_tac "a" 1 *})
    6.35 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.36  apply (tactic "hyp_arith_rew_tac []")
    6.37 -apply (tactic {* NE_tac "b" 2 *})
    6.38 +apply (tactic {* NE_tac @{context} "b" 2 *})
    6.39  apply (rule sym_elem)
    6.40 -apply (tactic {* NE_tac "b" 1 *})
    6.41 +apply (tactic {* NE_tac @{context} "b" 1 *})
    6.42  apply (tactic "hyp_arith_rew_tac []")
    6.43  done
    6.44  
    6.45 @@ -209,33 +209,33 @@
    6.46  
    6.47  (*right annihilation in product*)
    6.48  lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
    6.49 -apply (tactic {* NE_tac "a" 1 *})
    6.50 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.51  apply (tactic "hyp_arith_rew_tac []")
    6.52  done
    6.53  
    6.54  (*right successor law for multiplication*)
    6.55  lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
    6.56 -apply (tactic {* NE_tac "a" 1 *})
    6.57 -apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
    6.58 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.59 +apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
    6.60  apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
    6.61  done
    6.62  
    6.63  (*Commutative law for multiplication*)
    6.64  lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
    6.65 -apply (tactic {* NE_tac "a" 1 *})
    6.66 -apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
    6.67 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.68 +apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *})
    6.69  done
    6.70  
    6.71  (*addition distributes over multiplication*)
    6.72  lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
    6.73 -apply (tactic {* NE_tac "a" 1 *})
    6.74 -apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
    6.75 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.76 +apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
    6.77  done
    6.78  
    6.79  (*Associative law for multiplication*)
    6.80  lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
    6.81 -apply (tactic {* NE_tac "a" 1 *})
    6.82 -apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
    6.83 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.84 +apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *})
    6.85  done
    6.86  
    6.87  
    6.88 @@ -246,7 +246,7 @@
    6.89    a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
    6.90  
    6.91  lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
    6.92 -apply (tactic {* NE_tac "a" 1 *})
    6.93 +apply (tactic {* NE_tac @{context} "a" 1 *})
    6.94  apply (tactic "hyp_arith_rew_tac []")
    6.95  done
    6.96  
    6.97 @@ -258,12 +258,12 @@
    6.98    An example of induction over a quantified formula (a product).
    6.99    Uses rewriting with a quantified, implicative inductive hypothesis.*)
   6.100  lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
   6.101 -apply (tactic {* NE_tac "b" 1 *})
   6.102 +apply (tactic {* NE_tac @{context} "b" 1 *})
   6.103  (*strip one "universal quantifier" but not the "implication"*)
   6.104  apply (rule_tac [3] intr_rls)
   6.105  (*case analysis on x in
   6.106      (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   6.107 -apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
   6.108 +apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4")
   6.109  (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   6.110  apply (rule_tac [5] replace_type)
   6.111  apply (rule_tac [4] replace_type)
   6.112 @@ -326,7 +326,7 @@
   6.113  
   6.114  (*If a+b=0 then a=0.   Surprisingly tedious*)
   6.115  lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
   6.116 -apply (tactic {* NE_tac "a" 1 *})
   6.117 +apply (tactic {* NE_tac @{context} "a" 1 *})
   6.118  apply (rule_tac [3] replace_type)
   6.119  apply (tactic "arith_rew_tac []")
   6.120  apply (tactic "intr_tac []") (*strips remaining PRODs*)
   6.121 @@ -434,14 +434,14 @@
   6.122       succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   6.123  apply (rule divC_succ [THEN trans_elem])
   6.124  apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
   6.125 -apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *})
   6.126 +apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
   6.127  apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
   6.128  done
   6.129  
   6.130  (*for case analysis on whether a number is 0 or a successor*)
   6.131  lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
   6.132                        Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
   6.133 -apply (tactic {* NE_tac "a" 1 *})
   6.134 +apply (tactic {* NE_tac @{context} "a" 1 *})
   6.135  apply (rule_tac [3] PlusI_inr)
   6.136  apply (rule_tac [2] PlusI_inl)
   6.137  apply (tactic eqintr_tac)
   6.138 @@ -450,7 +450,7 @@
   6.139  
   6.140  (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   6.141  lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
   6.142 -apply (tactic {* NE_tac "a" 1 *})
   6.143 +apply (tactic {* NE_tac @{context} "a" 1 *})
   6.144  apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
   6.145    [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   6.146  apply (rule EqE)
     7.1 --- a/src/CTT/CTT.thy	Sat Jun 14 17:49:24 2008 +0200
     7.2 +++ b/src/CTT/CTT.thy	Sat Jun 14 23:19:51 2008 +0200
     7.3 @@ -354,29 +354,25 @@
     7.4  
     7.5  ML {*
     7.6  local
     7.7 -  val routine_rls = thms "routine_rls";
     7.8 -  val form_rls = thms "form_rls";
     7.9 -  val intr_rls = thms "intr_rls";
    7.10 -  val element_rls = thms "element_rls";
    7.11 -  val equal_rls = form_rls @ element_rls @ thms "intrL_rls" @
    7.12 -    thms "elimL_rls" @ thms "refl_elem"
    7.13 +  val equal_rls = @{thms form_rls} @ @{thms element_rls} @ @{thms intrL_rls} @
    7.14 +    @{thms elimL_rls} @ @{thms refl_elem}
    7.15  in
    7.16  
    7.17  fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
    7.18  
    7.19  (*Solve all subgoals "A type" using formation rules. *)
    7.20 -val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
    7.21 +val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac @{thms form_rls} 1));
    7.22  
    7.23  (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    7.24  fun typechk_tac thms =
    7.25 -  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
    7.26 +  let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
    7.27    in  REPEAT_FIRST (ASSUME tac)  end
    7.28  
    7.29  (*Solve a:A (a flexible, A rigid) by introduction rules.
    7.30    Cannot use stringtrees (filt_resolve_tac) since
    7.31    goals like ?a:SUM(A,B) have a trivial head-string *)
    7.32  fun intr_tac thms =
    7.33 -  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
    7.34 +  let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
    7.35    in  REPEAT_FIRST (ASSUME tac)  end
    7.36  
    7.37  (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
    7.38 @@ -412,55 +408,40 @@
    7.39  lemmas reduction_rls = comp_rls [THEN trans_elem]
    7.40  
    7.41  ML {*
    7.42 -local
    7.43 -  val EqI = thm "EqI";
    7.44 -  val EqE = thm "EqE";
    7.45 -  val NE = thm "NE";
    7.46 -  val FE = thm "FE";
    7.47 -  val ProdI = thm "ProdI";
    7.48 -  val SumI = thm "SumI";
    7.49 -  val SumE = thm "SumE";
    7.50 -  val PlusE = thm "PlusE";
    7.51 -  val PlusI_inl = thm "PlusI_inl";
    7.52 -  val PlusI_inr = thm "PlusI_inr";
    7.53 -  val subst_prodE = thm "subst_prodE";
    7.54 -  val intr_rls = thms "intr_rls";
    7.55 -in
    7.56 -
    7.57  (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
    7.58    Uses other intro rules to avoid changing flexible goals.*)
    7.59 -val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1))
    7.60 +val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
    7.61  
    7.62  (** Tactics that instantiate CTT-rules.
    7.63      Vars in the given terms will be incremented!
    7.64      The (rtac EqE i) lets them apply to equality judgements. **)
    7.65  
    7.66 -fun NE_tac (sp: string) i =
    7.67 -  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i
    7.68 +fun NE_tac ctxt sp i =
    7.69 +  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
    7.70  
    7.71 -fun SumE_tac (sp: string) i =
    7.72 -  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i
    7.73 +fun SumE_tac ctxt sp i =
    7.74 +  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
    7.75  
    7.76 -fun PlusE_tac (sp: string) i =
    7.77 -  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i
    7.78 +fun PlusE_tac ctxt sp i =
    7.79 +  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
    7.80  
    7.81  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    7.82  
    7.83  (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
    7.84  fun add_mp_tac i =
    7.85 -    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i
    7.86 +    rtac @{thm subst_prodE} i  THEN  assume_tac i  THEN  assume_tac i
    7.87  
    7.88  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    7.89 -fun mp_tac i = etac subst_prodE i  THEN  assume_tac i
    7.90 +fun mp_tac i = etac @{thm subst_prodE} i  THEN  assume_tac i
    7.91  
    7.92  (*"safe" when regarded as predicate calculus rules*)
    7.93  val safe_brls = sort (make_ord lessb)
    7.94 -    [ (true,FE), (true,asm_rl),
    7.95 -      (false,ProdI), (true,SumE), (true,PlusE) ]
    7.96 +    [ (true, @{thm FE}), (true,asm_rl),
    7.97 +      (false, @{thm ProdI}), (true, @{thm SumE}), (true, @{thm PlusE}) ]
    7.98  
    7.99  val unsafe_brls =
   7.100 -    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI),
   7.101 -      (true,subst_prodE) ]
   7.102 +    [ (false, @{thm PlusI_inl}), (false, @{thm PlusI_inr}), (false, @{thm SumI}),
   7.103 +      (true, @{thm subst_prodE}) ]
   7.104  
   7.105  (*0 subgoals vs 1 or more*)
   7.106  val (safe0_brls, safep_brls) =
   7.107 @@ -478,8 +459,6 @@
   7.108  
   7.109  (*Fails unless it solves the goal!*)
   7.110  fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
   7.111 -
   7.112 -end
   7.113  *}
   7.114  
   7.115  use "rew.ML"
     8.1 --- a/src/CTT/ex/Equality.thy	Sat Jun 14 17:49:24 2008 +0200
     8.2 +++ b/src/CTT/ex/Equality.thy	Sat Jun 14 23:19:51 2008 +0200
     8.3 @@ -40,7 +40,7 @@
     8.4  lemma "[| a:N;  b:N;  c:N |]
     8.5        ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
     8.6            rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
     8.7 -apply (tactic {* NE_tac "a" 1 *})
     8.8 +apply (tactic {* NE_tac @{context} "a" 1 *})
     8.9  apply (tactic "hyp_rew_tac []")
    8.10  done
    8.11  
     9.1 --- a/src/HOL/Bali/WellType.thy	Sat Jun 14 17:49:24 2008 +0200
     9.2 +++ b/src/HOL/Bali/WellType.thy	Sat Jun 14 23:19:51 2008 +0200
     9.3 @@ -652,9 +652,13 @@
     9.4  apply (simp_all (no_asm_use) split del: split_if_asm)
     9.5  apply (safe del: disjE)
     9.6  (* 17 subgoals *)
     9.7 -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) *})
     9.8 +apply (tactic {* ALLGOALS (fn i =>
     9.9 +  if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
    9.10 +    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
    9.11 +    RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
    9.12 +  else RuleInsts.thin_tac @{context} "All ?P" i) *})
    9.13  (*apply (safe del: disjE elim!: wt_elim_cases)*)
    9.14 -apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
    9.15 +apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
    9.16  apply (simp_all (no_asm_use) split del: split_if_asm)
    9.17  apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
    9.18  apply ((blast del: equalityCE dest: sym [THEN trans])+)
    10.1 --- a/src/HOL/IMPP/Hoare.thy	Sat Jun 14 17:49:24 2008 +0200
    10.2 +++ b/src/HOL/IMPP/Hoare.thy	Sat Jun 14 23:19:51 2008 +0200
    10.3 @@ -282,7 +282,9 @@
    10.4  apply          (blast) (* asm *)
    10.5  apply         (blast) (* cut *)
    10.6  apply        (blast) (* weaken *)
    10.7 -apply       (tactic {* ALLGOALS (EVERY'[REPEAT o thin_tac "hoare_derivs ?x ?y", SIMPSET' simp_tac, CLASET' clarify_tac, REPEAT o smp_tac 1]) *})
    10.8 +apply       (tactic {* ALLGOALS (EVERY'
    10.9 +  [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
   10.10 +   simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
   10.11  apply       (simp_all (no_asm_use) add: triple_valid_def2)
   10.12  apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
   10.13  apply      (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
    11.1 --- a/src/HOL/NanoJava/Equivalence.thy	Sat Jun 14 17:49:24 2008 +0200
    11.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Sat Jun 14 23:19:51 2008 +0200
    11.3 @@ -107,9 +107,9 @@
    11.4  apply (tactic "split_all_tac 1", rename_tac P e Q)
    11.5  apply (rule hoare_ehoare.induct)
    11.6  (*18*)
    11.7 -apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
    11.8 -apply (tactic {* ALLGOALS (REPEAT o thin_tac "hoare ?x ?y") *})
    11.9 -apply (tactic {* ALLGOALS (REPEAT o thin_tac "ehoare ?x ?y") *})
   11.10 +apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
   11.11 +apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
   11.12 +apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
   11.13  apply (simp_all only: cnvalid1_eq cenvalid_def2)
   11.14                   apply fast
   11.15                  apply fast
    12.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Jun 14 17:49:24 2008 +0200
    12.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sat Jun 14 23:19:51 2008 +0200
    12.3 @@ -762,12 +762,14 @@
    12.4     steps of the implementation, and try to solve the idling case by simplification
    12.5  *)
    12.6  ML {*
    12.7 -fun split_idle_tac ss simps i =
    12.8 -  TRY (rtac @{thm actionI} i) THEN
    12.9 -  case_split_tac "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
   12.10 -  rewrite_goals_tac @{thms action_rews} THEN
   12.11 -  forward_tac [temp_use @{thm Step1_4_7}] i THEN
   12.12 -  asm_full_simp_tac (ss addsimps simps) i
   12.13 +fun split_idle_tac ctxt simps i =
   12.14 +  let val ss = Simplifier.local_simpset_of ctxt in
   12.15 +    TRY (rtac @{thm actionI} i) THEN
   12.16 +    InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
   12.17 +    rewrite_goals_tac @{thms action_rews} THEN
   12.18 +    forward_tac [temp_use @{thm Step1_4_7}] i THEN
   12.19 +    asm_full_simp_tac (ss addsimps simps) i
   12.20 +  end
   12.21  *}
   12.22  (* ----------------------------------------------------------------------
   12.23     Combine steps 1.2 and 1.4 to prove that the implementation satisfies
   12.24 @@ -779,7 +781,7 @@
   12.25  lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
   12.26               --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
   12.27           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   12.28 -  apply (tactic {* split_idle_tac @{simpset} [thm "square_def"] 1 *})
   12.29 +  apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
   12.30    apply force
   12.31    done
   12.32  (* turn into (unsafe, looping!) introduction rule *)
   12.33 @@ -851,7 +853,7 @@
   12.34  
   12.35  lemma S1_successors: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   12.36           --> (S1 rmhist p)$ | (S2 rmhist p)$"
   12.37 -  apply (tactic "split_idle_tac @{simpset} [] 1")
   12.38 +  apply (tactic "split_idle_tac @{context} [] 1")
   12.39    apply (auto dest!: Step1_2_1 [temp_use])
   12.40    done
   12.41  
   12.42 @@ -885,7 +887,7 @@
   12.43  
   12.44  lemma S2_successors: "|- $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   12.45           --> (S2 rmhist p)$ | (S3 rmhist p)$"
   12.46 -  apply (tactic "split_idle_tac @{simpset} [] 1")
   12.47 +  apply (tactic "split_idle_tac @{context} [] 1")
   12.48    apply (auto dest!: Step1_2_2 [temp_use])
   12.49    done
   12.50  
   12.51 @@ -911,7 +913,7 @@
   12.52  
   12.53  lemma S3_successors: "|- $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   12.54           --> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
   12.55 -  apply (tactic "split_idle_tac @{simpset} [] 1")
   12.56 +  apply (tactic "split_idle_tac @{context} [] 1")
   12.57    apply (auto dest!: Step1_2_3 [temp_use])
   12.58    done
   12.59  
   12.60 @@ -939,7 +941,7 @@
   12.61  lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   12.62          & (ALL l. $MemInv mm l)
   12.63          --> (S4 rmhist p)$ | (S5 rmhist p)$"
   12.64 -  apply (tactic "split_idle_tac @{simpset} [] 1")
   12.65 +  apply (tactic "split_idle_tac @{context} [] 1")
   12.66    apply (auto dest!: Step1_2_4 [temp_use])
   12.67    done
   12.68  
   12.69 @@ -949,7 +951,7 @@
   12.70           & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
   12.71           --> (S4 rmhist p & ires!p = #NotAResult)$
   12.72               | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
   12.73 -  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
   12.74 +  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
   12.75    apply (auto dest!: Step1_2_4 [temp_use])
   12.76    done
   12.77  
   12.78 @@ -980,7 +982,7 @@
   12.79  lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
   12.80           & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
   12.81           --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
   12.82 -  apply (tactic {* split_idle_tac @{simpset} [thm "m_def"] 1 *})
   12.83 +  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
   12.84    apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   12.85    done
   12.86  
   12.87 @@ -1009,7 +1011,7 @@
   12.88  
   12.89  lemma S5_successors: "|- $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   12.90           --> (S5 rmhist p)$ | (S6 rmhist p)$"
   12.91 -  apply (tactic "split_idle_tac @{simpset} [] 1")
   12.92 +  apply (tactic "split_idle_tac @{context} [] 1")
   12.93    apply (auto dest!: Step1_2_5 [temp_use])
   12.94    done
   12.95  
   12.96 @@ -1035,7 +1037,7 @@
   12.97  
   12.98  lemma S6_successors: "|- $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
   12.99           --> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
  12.100 -  apply (tactic "split_idle_tac @{simpset} [] 1")
  12.101 +  apply (tactic "split_idle_tac @{context} [] 1")
  12.102    apply (auto dest!: Step1_2_6 [temp_use])
  12.103    done
  12.104  
  12.105 @@ -1250,7 +1252,7 @@
  12.106    apply clarsimp
  12.107    apply (drule WriteS4 [action_use])
  12.108     apply assumption
  12.109 -  apply (tactic "split_idle_tac @{simpset} [] 1")
  12.110 +  apply (tactic "split_idle_tac @{context} [] 1")
  12.111    apply (auto simp: ImpNext_def dest!: S4EnvUnch [temp_use] S4ClerkUnch [temp_use]
  12.112      S4RPCUnch [temp_use])
  12.113       apply (auto simp: square_def dest: S4Write [temp_use])
    13.1 --- a/src/HOL/TLA/TLA.thy	Sat Jun 14 17:49:24 2008 +0200
    13.2 +++ b/src/HOL/TLA/TLA.thy	Sat Jun 14 23:19:51 2008 +0200
    13.3 @@ -305,17 +305,17 @@
    13.4  fun merge_box_tac i =
    13.5     REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
    13.6  
    13.7 -fun merge_temp_box_tac i =
    13.8 +fun merge_temp_box_tac ctxt i =
    13.9     REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
   13.10 -                         eres_inst_tac [("'a","behavior")] @{thm box_thin} i])
   13.11 +                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
   13.12  
   13.13 -fun merge_stp_box_tac i =
   13.14 +fun merge_stp_box_tac ctxt i =
   13.15     REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
   13.16 -                         eres_inst_tac [("'a","state")] @{thm box_thin} i])
   13.17 +                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
   13.18  
   13.19 -fun merge_act_box_tac i =
   13.20 +fun merge_act_box_tac ctxt i =
   13.21     REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
   13.22 -                         eres_inst_tac [("'a","state * state")] @{thm box_thin} i])
   13.23 +                         RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
   13.24  *}
   13.25  
   13.26  (* rewrite rule to push universal quantification through box:
   13.27 @@ -947,7 +947,7 @@
   13.28    apply (clarsimp dest!: BoxSFI [temp_use])
   13.29    apply (erule (2) ensures [temp_use])
   13.30    apply (erule_tac F = F in dup_boxE)
   13.31 -  apply (tactic "merge_temp_box_tac 1")
   13.32 +  apply (tactic "merge_temp_box_tac @{context} 1")
   13.33    apply (erule STL4Edup)
   13.34    apply assumption
   13.35    apply (clarsimp simp: SF_def)
   13.36 @@ -966,7 +966,7 @@
   13.37    apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
   13.38      simp: WF_def [where A = M])
   13.39    apply (erule_tac F = F in dup_boxE)
   13.40 -  apply (tactic "merge_temp_box_tac 1")
   13.41 +  apply (tactic "merge_temp_box_tac @{context} 1")
   13.42    apply (erule STL4Edup)
   13.43     apply assumption
   13.44    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   13.45 @@ -975,7 +975,7 @@
   13.46     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   13.47    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   13.48    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
   13.49 -  apply (tactic "merge_act_box_tac 1")
   13.50 +  apply (tactic "merge_act_box_tac @{context} 1")
   13.51    apply (frule 4 [temp_use])
   13.52       apply assumption+
   13.53    apply (drule STL6 [temp_use])
   13.54 @@ -984,7 +984,7 @@
   13.55    apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   13.56    apply (drule BoxWFI [temp_use])
   13.57    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
   13.58 -  apply (tactic "merge_temp_box_tac 1")
   13.59 +  apply (tactic "merge_temp_box_tac @{context} 1")
   13.60    apply (erule DmdImpldup)
   13.61     apply assumption
   13.62    apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
   13.63 @@ -1004,7 +1004,7 @@
   13.64    apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
   13.65    apply (erule_tac F = F in dup_boxE)
   13.66    apply (erule_tac F = "TEMP <>Enabled (<M>_g) " in dup_boxE)
   13.67 -  apply (tactic "merge_temp_box_tac 1")
   13.68 +  apply (tactic "merge_temp_box_tac @{context} 1")
   13.69    apply (erule STL4Edup)
   13.70     apply assumption
   13.71    apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   13.72 @@ -1013,14 +1013,14 @@
   13.73     apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   13.74    apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   13.75    apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
   13.76 -  apply (tactic "merge_act_box_tac 1")
   13.77 +  apply (tactic "merge_act_box_tac @{context} 1")
   13.78    apply (frule 4 [temp_use])
   13.79       apply assumption+
   13.80    apply (erule_tac V = "sigmaa |= []F" in thin_rl)
   13.81    apply (drule BoxSFI [temp_use])
   13.82    apply (erule_tac F = "TEMP <>Enabled (<M>_g)" in dup_boxE)
   13.83    apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
   13.84 -  apply (tactic "merge_temp_box_tac 1")
   13.85 +  apply (tactic "merge_temp_box_tac @{context} 1")
   13.86    apply (erule DmdImpldup)
   13.87     apply assumption
   13.88    apply (auto simp: split_box_conj [try_rewrite] STL3 [try_rewrite]
    14.1 --- a/src/HOL/Tools/split_rule.ML	Sat Jun 14 17:49:24 2008 +0200
    14.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Jun 14 23:19:51 2008 +0200
    14.3 @@ -15,7 +15,7 @@
    14.4  sig
    14.5    include BASIC_SPLIT_RULE
    14.6    val split_rule_var: term -> thm -> thm
    14.7 -  val split_rule_goal: string list list -> thm -> thm
    14.8 +  val split_rule_goal: Proof.context -> string list list -> thm -> thm
    14.9    val setup: theory -> theory
   14.10  end;
   14.11  
   14.12 @@ -123,14 +123,16 @@
   14.13    end;
   14.14  
   14.15  
   14.16 -fun pair_tac s =
   14.17 -  EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac];
   14.18 +fun pair_tac ctxt s =
   14.19 +  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
   14.20 +  THEN' hyp_subst_tac
   14.21 +  THEN' K prune_params_tac;
   14.22  
   14.23  val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
   14.24  
   14.25 -fun split_rule_goal xss rl =
   14.26 +fun split_rule_goal ctxt xss rl =
   14.27    let
   14.28 -    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
   14.29 +    fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
   14.30      fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   14.31    in
   14.32      rl
   14.33 @@ -148,7 +150,8 @@
   14.34    (Scan.lift (Args.parens (Args.$$$ "complete"))
   14.35      >> K (Thm.rule_attribute (K complete_split_rule)) ||
   14.36    Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   14.37 -    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss))));
   14.38 +    >> (fn xss => Thm.rule_attribute (fn context =>
   14.39 +        split_rule_goal (Context.proof_of context) xss)));
   14.40  
   14.41  val setup =
   14.42    Attrib.add_attributes
    15.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 17:49:24 2008 +0200
    15.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 23:19:51 2008 +0200
    15.3 @@ -41,8 +41,10 @@
    15.4                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
    15.5                (*now there are two subgoals: co & transient*)
    15.6                simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
    15.7 -              res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
    15.8 -              ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
    15.9 +              RuleInsts.res_inst_tac (Simplifier.the_context ss)
   15.10 +                [(("act", 0), sact)] @{thm totalize_transientI} 2
   15.11 +              ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
   15.12 +                [(("act", 0), sact)] @{thm transientI} 2,
   15.13                   (*simplify the command's domain*)
   15.14                simp_tac (ss addsimps [@{thm Domain_def}]) 3,
   15.15                constrains_tac (cs,ss) 1,
    16.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Jun 14 17:49:24 2008 +0200
    16.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Sat Jun 14 23:19:51 2008 +0200
    16.3 @@ -104,7 +104,7 @@
    16.4    --> is_exec_frag A (cex_abs h (s,xs))"
    16.5  apply (unfold cex_abs_def)
    16.6  apply simp
    16.7 -apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
    16.8 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
    16.9  txt {* main case *}
   16.10  apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
   16.11  done
   16.12 @@ -204,7 +204,7 @@
   16.13           ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
   16.14  apply (unfold cex_abs_def mk_trace_def filter_act_def)
   16.15  apply simp
   16.16 -apply (tactic {* pair_induct_tac "xs" [] 1 *})
   16.17 +apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
   16.18  done
   16.19  
   16.20  
   16.21 @@ -220,13 +220,13 @@
   16.22  apply (rule_tac x = "cex_abs h ex" in exI)
   16.23  apply auto
   16.24    (* Traces coincide *)
   16.25 -  apply (tactic {* pair_tac "ex" 1 *})
   16.26 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   16.27    apply (rule traces_coincide_abs)
   16.28    apply (simp (no_asm) add: externals_def)
   16.29    apply (auto)[1]
   16.30  
   16.31    (* cex_abs is execution *)
   16.32 -  apply (tactic {* pair_tac "ex" 1 *})
   16.33 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   16.34    apply (simp add: executions_def)
   16.35    (* start state *)
   16.36    apply (rule conjI)
   16.37 @@ -237,7 +237,7 @@
   16.38  
   16.39   (* Liveness *)
   16.40  apply (simp add: temp_weakening_def2)
   16.41 - apply (tactic {* pair_tac "ex" 1 *})
   16.42 + apply (tactic {* pair_tac @{context} "ex" 1 *})
   16.43  done
   16.44  
   16.45  (* FIX: NAch Traces.ML bringen *)
   16.46 @@ -354,25 +354,25 @@
   16.47  
   16.48  (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   16.49  lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
   16.50 -apply (tactic {* Seq_case_simp_tac "x" 1 *})
   16.51 +apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
   16.52  done
   16.53  
   16.54  lemma ex2seqConc [rule_format]:
   16.55  "Finite s1 -->
   16.56    (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
   16.57  apply (rule impI)
   16.58 -apply (tactic {* Seq_Finite_induct_tac 1 *})
   16.59 +apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
   16.60  apply blast
   16.61  (* main case *)
   16.62  apply clarify
   16.63 -apply (tactic {* pair_tac "ex" 1 *})
   16.64 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
   16.65 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   16.66 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   16.67  (* UU case *)
   16.68  apply (simp add: nil_is_Conc)
   16.69  (* nil case *)
   16.70  apply (simp add: nil_is_Conc)
   16.71  (* cons case *)
   16.72 -apply (tactic {* pair_tac "aa" 1 *})
   16.73 +apply (tactic {* pair_tac @{context} "aa" 1 *})
   16.74  apply auto
   16.75  done
   16.76  
   16.77 @@ -390,11 +390,11 @@
   16.78  (* FIX: NAch Sequence.ML bringen *)
   16.79  
   16.80  lemma Mapnil: "(Map f$s = nil) = (s=nil)"
   16.81 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
   16.82 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   16.83  done
   16.84  
   16.85  lemma MapUU: "(Map f$s = UU) = (s=UU)"
   16.86 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
   16.87 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   16.88  done
   16.89  
   16.90  
   16.91 @@ -432,9 +432,9 @@
   16.92  apply (unfold temp_strengthening_def state_strengthening_def
   16.93    temp_sat_def satisfies_def Init_def unlift_def)
   16.94  apply auto
   16.95 -apply (tactic {* pair_tac "ex" 1 *})
   16.96 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
   16.97 -apply (tactic {* pair_tac "a" 1 *})
   16.98 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   16.99 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
  16.100 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.101  done
  16.102  
  16.103  
  16.104 @@ -442,25 +442,25 @@
  16.105  
  16.106  lemma TL_ex2seq_UU:
  16.107  "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
  16.108 -apply (tactic {* pair_tac "ex" 1 *})
  16.109 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
  16.110 -apply (tactic {* pair_tac "a" 1 *})
  16.111 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
  16.112 -apply (tactic {* pair_tac "a" 1 *})
  16.113 +apply (tactic {* pair_tac @{context} "ex" 1 *})
  16.114 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
  16.115 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.116 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
  16.117 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.118  done
  16.119  
  16.120  lemma TL_ex2seq_nil:
  16.121  "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
  16.122 -apply (tactic {* pair_tac "ex" 1 *})
  16.123 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
  16.124 -apply (tactic {* pair_tac "a" 1 *})
  16.125 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
  16.126 -apply (tactic {* pair_tac "a" 1 *})
  16.127 +apply (tactic {* pair_tac @{context} "ex" 1 *})
  16.128 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
  16.129 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.130 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
  16.131 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.132  done
  16.133  
  16.134  (* FIX: put to Sequence Lemmas *)
  16.135  lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
  16.136 -apply (tactic {* Seq_induct_tac "s" [] 1 *})
  16.137 +apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *})
  16.138  done
  16.139  
  16.140  (* important property of cex_absSeq: As it is a 1to1 correspondence,
  16.141 @@ -475,19 +475,19 @@
  16.142  (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
  16.143  
  16.144  lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
  16.145 -apply (tactic {* pair_tac "ex" 1 *})
  16.146 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
  16.147 -apply (tactic {* pair_tac "a" 1 *})
  16.148 +apply (tactic {* pair_tac @{context} "ex" 1 *})
  16.149 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
  16.150 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.151  apply auto
  16.152  done
  16.153  
  16.154  
  16.155  lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
  16.156 -apply (tactic {* pair_tac "ex" 1 *})
  16.157 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
  16.158 -apply (tactic {* pair_tac "a" 1 *})
  16.159 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
  16.160 -apply (tactic {* pair_tac "a" 1 *})
  16.161 +apply (tactic {* pair_tac @{context} "ex" 1 *})
  16.162 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
  16.163 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.164 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
  16.165 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.166  done
  16.167  
  16.168  
  16.169 @@ -518,9 +518,9 @@
  16.170  apply (simp add: temp_weakening_def2 state_weakening_def2
  16.171    temp_sat_def satisfies_def Init_def unlift_def)
  16.172  apply auto
  16.173 -apply (tactic {* pair_tac "ex" 1 *})
  16.174 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
  16.175 -apply (tactic {* pair_tac "a" 1 *})
  16.176 +apply (tactic {* pair_tac @{context} "ex" 1 *})
  16.177 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
  16.178 +apply (tactic {* pair_tac @{context} "a" 1 *})
  16.179  done
  16.180  
  16.181  
    17.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Sat Jun 14 17:49:24 2008 +0200
    17.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Sat Jun 14 23:19:51 2008 +0200
    17.3 @@ -216,7 +216,7 @@
    17.4         -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
    17.5              is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
    17.6  
    17.7 -apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
    17.8 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
    17.9  (* main case *)
   17.10  apply (auto simp add: trans_of_defs2)
   17.11  done
   17.12 @@ -230,7 +230,8 @@
   17.13         --> stutter (asig_of A) (fst s,ProjA2$xs)  &
   17.14             stutter (asig_of B) (snd s,ProjB2$xs)"
   17.15  
   17.16 -apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
   17.17 +apply (tactic {* pair_induct_tac @{context} "xs"
   17.18 +  [@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *})
   17.19  (* main case *)
   17.20  apply (auto simp add: trans_of_defs2)
   17.21  done
   17.22 @@ -243,8 +244,8 @@
   17.23  lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
   17.24     --> Forall (%x. fst x:act (A||B)) xs)"
   17.25  
   17.26 -apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
   17.27 -  thm "is_exec_frag_def"] 1 *})
   17.28 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
   17.29 +  @{thm is_exec_frag_def}] 1 *})
   17.30  (* main case *)
   17.31  apply auto
   17.32  apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
   17.33 @@ -263,8 +264,8 @@
   17.34       Forall (%x. fst x:act (A||B)) xs
   17.35       --> is_exec_frag (A||B) (s,xs)"
   17.36  
   17.37 -apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
   17.38 -  thm "is_exec_frag_def", thm "stutter_def"] 1 *})
   17.39 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
   17.40 +  @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
   17.41  apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
   17.42  done
   17.43  
   17.44 @@ -279,7 +280,7 @@
   17.45    Forall (%x. fst x:act (A||B)) (snd ex))"
   17.46  
   17.47  apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
   17.48 -apply (tactic {* pair_tac "ex" 1 *})
   17.49 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   17.50  apply (rule iffI)
   17.51  (* ==>  *)
   17.52  apply (erule conjE)+
    18.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Sat Jun 14 17:49:24 2008 +0200
    18.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Sat Jun 14 23:19:51 2008 +0200
    18.3 @@ -219,7 +219,7 @@
    18.4  lemma lemma_2_1b:
    18.5     "filter_act$(ProjA2$xs) =filter_act$xs &
    18.6      filter_act$(ProjB2$xs) =filter_act$xs"
    18.7 -apply (tactic {* pair_induct_tac "xs" [] 1 *})
    18.8 +apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
    18.9  done
   18.10  
   18.11  
   18.12 @@ -234,8 +234,8 @@
   18.13  lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
   18.14     --> Forall (%x. x:act (A||B)) (filter_act$xs)"
   18.15  
   18.16 -apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
   18.17 -  thm "sforall_def"] 1 *})
   18.18 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
   18.19 +  @{thm sforall_def}] 1 *})
   18.20  (* main case *)
   18.21  apply auto
   18.22  apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
   18.23 @@ -255,20 +255,20 @@
   18.24    Filter (%a. a:act B)$sch << filter_act$exB
   18.25    --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
   18.26  
   18.27 -apply (tactic {* Seq_induct_tac "sch" [thm "Filter_def", thm "Forall_def",
   18.28 -  thm "sforall_def", thm "mkex_def"] 1 *})
   18.29 +apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
   18.30 +  @{thm sforall_def}, @{thm mkex_def}] 1 *})
   18.31  
   18.32  (* main case *)
   18.33  (* splitting into 4 cases according to a:A, a:B *)
   18.34  apply auto
   18.35  
   18.36  (* Case y:A, y:B *)
   18.37 -apply (tactic {* Seq_case_simp_tac "exA" 1 *})
   18.38 +apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
   18.39  (* Case exA=UU, Case exA=nil*)
   18.40  (* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
   18.41     is used! --> to generate a contradiction using  ~a>>ss<< UU(nil), using theorems
   18.42     Cons_not_less_UU and Cons_not_less_nil  *)
   18.43 -apply (tactic {* Seq_case_simp_tac "exB" 1 *})
   18.44 +apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
   18.45  (* Case exA=a>>x, exB=b>>y *)
   18.46  (* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
   18.47     as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic
   18.48 @@ -276,11 +276,11 @@
   18.49  apply simp
   18.50  
   18.51  (* Case y:A, y~:B *)
   18.52 -apply (tactic {* Seq_case_simp_tac "exA" 1 *})
   18.53 +apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
   18.54  apply simp
   18.55  
   18.56  (* Case y~:A, y:B *)
   18.57 -apply (tactic {* Seq_case_simp_tac "exB" 1 *})
   18.58 +apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
   18.59  apply simp
   18.60  
   18.61  (* Case y~:A, y~:B *)
   18.62 @@ -298,19 +298,21 @@
   18.63    val asigs = [thm "asig_of_par", thm "actions_asig_comp"]
   18.64  in
   18.65  
   18.66 -fun mkex_induct_tac sch exA exB =
   18.67 -    EVERY1[Seq_induct_tac sch defs,
   18.68 -           SIMPSET' asm_full_simp_tac,
   18.69 +fun mkex_induct_tac ctxt sch exA exB =
   18.70 +  let val ss = Simplifier.local_simpset_of ctxt in
   18.71 +    EVERY1[Seq_induct_tac ctxt sch defs,
   18.72 +           asm_full_simp_tac ss,
   18.73             SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
   18.74 -           Seq_case_simp_tac exA,
   18.75 -           Seq_case_simp_tac exB,
   18.76 -           SIMPSET' asm_full_simp_tac,
   18.77 -           Seq_case_simp_tac exA,
   18.78 -           SIMPSET' asm_full_simp_tac,
   18.79 -           Seq_case_simp_tac exB,
   18.80 -           SIMPSET' asm_full_simp_tac,
   18.81 -           SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps asigs))
   18.82 +           Seq_case_simp_tac ctxt exA,
   18.83 +           Seq_case_simp_tac ctxt exB,
   18.84 +           asm_full_simp_tac ss,
   18.85 +           Seq_case_simp_tac ctxt exA,
   18.86 +           asm_full_simp_tac ss,
   18.87 +           Seq_case_simp_tac ctxt exB,
   18.88 +           asm_full_simp_tac ss,
   18.89 +           asm_full_simp_tac (ss addsimps asigs)
   18.90            ]
   18.91 +  end
   18.92  
   18.93  end
   18.94  *}
   18.95 @@ -327,7 +329,7 @@
   18.96    Filter (%a. a:act B)$sch << filter_act$exB
   18.97    --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
   18.98  
   18.99 -apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
  18.100 +apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
  18.101  done
  18.102  
  18.103  
  18.104 @@ -356,7 +358,7 @@
  18.105    Filter (%a. a:act A)$sch << filter_act$exA &
  18.106    Filter (%a. a:act B)$sch << filter_act$exB
  18.107    --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
  18.108 -apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
  18.109 +apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
  18.110  done
  18.111  
  18.112  
  18.113 @@ -387,7 +389,7 @@
  18.114    Filter (%a. a:act B)$sch << filter_act$exB
  18.115    --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
  18.116        Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
  18.117 -apply (tactic {* mkex_induct_tac "sch" "exB" "exA" *})
  18.118 +apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
  18.119  done
  18.120  
  18.121  (*---------------------------------------------------------------------------
  18.122 @@ -396,7 +398,7 @@
  18.123    --------------------------------------------------------------------------- *)
  18.124  
  18.125  lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
  18.126 -apply (tactic {* Seq_induct_tac "y" [] 1 *})
  18.127 +apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
  18.128  done
  18.129  
  18.130  
  18.131 @@ -424,8 +426,8 @@
  18.132    Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
  18.133    ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
  18.134  apply (simp add: ProjA_def Filter_ex_def)
  18.135 -apply (tactic {* pair_tac "exA" 1 *})
  18.136 -apply (tactic {* pair_tac "exB" 1 *})
  18.137 +apply (tactic {* pair_tac @{context} "exA" 1 *})
  18.138 +apply (tactic {* pair_tac @{context} "exB" 1 *})
  18.139  apply (rule conjI)
  18.140  apply (simp (no_asm) add: mkex_def)
  18.141  apply (simplesubst trick_against_eq_in_ass)
  18.142 @@ -450,7 +452,7 @@
  18.143        Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
  18.144  
  18.145  (* notice necessary change of arguments exA and exB *)
  18.146 -apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
  18.147 +apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
  18.148  done
  18.149  
  18.150  
  18.151 @@ -466,8 +468,8 @@
  18.152    Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
  18.153    ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
  18.154  apply (simp add: ProjB_def Filter_ex_def)
  18.155 -apply (tactic {* pair_tac "exA" 1 *})
  18.156 -apply (tactic {* pair_tac "exB" 1 *})
  18.157 +apply (tactic {* pair_tac @{context} "exA" 1 *})
  18.158 +apply (tactic {* pair_tac @{context} "exB" 1 *})
  18.159  apply (rule conjI)
  18.160  apply (simp (no_asm) add: mkex_def)
  18.161  apply (simplesubst trick_against_eq_in_ass)
  18.162 @@ -487,7 +489,7 @@
  18.163    Filter (%a. a:act B)$sch << filter_act$exB
  18.164     --> Forall (%x. fst x : act (A ||B))
  18.165           (snd (mkex A B sch (s,exA) (t,exB)))"
  18.166 -apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
  18.167 +apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
  18.168  done
  18.169  
  18.170  
  18.171 @@ -513,7 +515,7 @@
  18.172  apply (simp add: compositionality_ex)
  18.173  apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
  18.174  apply (simp add: executions_def)
  18.175 -apply (tactic {* pair_tac "ex" 1 *})
  18.176 +apply (tactic {* pair_tac @{context} "ex" 1 *})
  18.177  apply (erule conjE)
  18.178  apply (simp add: sch_actions_in_AorB)
  18.179  
  18.180 @@ -524,15 +526,15 @@
  18.181  apply (rename_tac exA exB)
  18.182  apply (rule_tac x = "mkex A B sch exA exB" in bexI)
  18.183  (* mkex actions are just the oracle *)
  18.184 -apply (tactic {* pair_tac "exA" 1 *})
  18.185 -apply (tactic {* pair_tac "exB" 1 *})
  18.186 +apply (tactic {* pair_tac @{context} "exA" 1 *})
  18.187 +apply (tactic {* pair_tac @{context} "exB" 1 *})
  18.188  apply (simp add: Mapfst_mkex_is_sch)
  18.189  
  18.190  (* mkex is an execution -- use compositionality on ex-level *)
  18.191  apply (simp add: compositionality_ex)
  18.192  apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
  18.193 -apply (tactic {* pair_tac "exA" 1 *})
  18.194 -apply (tactic {* pair_tac "exB" 1 *})
  18.195 +apply (tactic {* pair_tac @{context} "exA" 1 *})
  18.196 +apply (tactic {* pair_tac @{context} "exB" 1 *})
  18.197  apply (simp add: mkex_actions_in_AorB)
  18.198  done
  18.199  
    19.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Jun 14 17:49:24 2008 +0200
    19.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Jun 14 23:19:51 2008 +0200
    19.3 @@ -199,7 +199,8 @@
    19.4    "!!A B. compatible A B ==>  
    19.5      ! schA schB. Forall (%x. x:act (A||B)) tr  
    19.6      --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
    19.7 -apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
    19.8 +apply (tactic {* Seq_induct_tac @{context} "tr"
    19.9 +  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   19.10  apply auto
   19.11  apply (simp add: actions_of_par)
   19.12  apply (case_tac "a:act A")
   19.13 @@ -226,7 +227,8 @@
   19.14  lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A  ==>  
   19.15      ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
   19.16      --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
   19.17 -apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
   19.18 +apply (tactic {* Seq_induct_tac @{context} "tr"
   19.19 +  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   19.20  apply auto
   19.21  apply (rule Forall_Conc_impl [THEN mp])
   19.22  apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
   19.23 @@ -235,7 +237,8 @@
   19.24  lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
   19.25      ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
   19.26      --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
   19.27 -apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
   19.28 +apply (tactic {* Seq_induct_tac @{context} "tr"
   19.29 +  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   19.30  apply auto
   19.31  apply (rule Forall_Conc_impl [THEN mp])
   19.32  apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
   19.33 @@ -411,7 +414,8 @@
   19.34    Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
   19.35    --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
   19.36  
   19.37 -apply (tactic {* Seq_induct_tac "tr" [thm "Forall_def", thm "sforall_def", thm "mksch_def"] 1 *})
   19.38 +apply (tactic {* Seq_induct_tac @{context} "tr"
   19.39 +  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   19.40  (* main case *)
   19.41  (* splitting into 4 cases according to a:A, a:B *)
   19.42  apply auto
    20.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Sat Jun 14 17:49:24 2008 +0200
    20.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Sat Jun 14 23:19:51 2008 +0200
    20.3 @@ -18,7 +18,7 @@
    20.4  apply auto
    20.5  apply (frule inp_is_act)
    20.6  apply (simp add: executions_def)
    20.7 -apply (tactic {* pair_tac "ex" 1 *})
    20.8 +apply (tactic {* pair_tac @{context} "ex" 1 *})
    20.9  apply (rename_tac s ex)
   20.10  apply (subgoal_tac "Finite ex")
   20.11  prefer 2
    21.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jun 14 17:49:24 2008 +0200
    21.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jun 14 23:19:51 2008 +0200
    21.3 @@ -64,14 +64,14 @@
    21.4  apply (rule_tac x = "corresp_ex A f ex" in exI)
    21.5  apply auto
    21.6    (* Traces coincide, Lemma 1 *)
    21.7 -  apply (tactic {* pair_tac "ex" 1 *})
    21.8 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
    21.9    apply (erule lemma_1 [THEN spec, THEN mp])
   21.10    apply (simp (no_asm) add: externals_def)
   21.11    apply (auto)[1]
   21.12    apply (simp add: executions_def reachable.reachable_0)
   21.13  
   21.14    (* corresp_ex is execution, Lemma 2 *)
   21.15 -  apply (tactic {* pair_tac "ex" 1 *})
   21.16 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   21.17    apply (simp add: executions_def)
   21.18    (* start state *)
   21.19    apply (rule conjI)
    22.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sat Jun 14 17:49:24 2008 +0200
    22.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Sat Jun 14 23:19:51 2008 +0200
    22.3 @@ -181,7 +181,7 @@
    22.4           !s. reachable C s & is_exec_frag C (s,xs) -->
    22.5               mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
    22.6  apply (unfold corresp_ex_def)
    22.7 -apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
    22.8 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
    22.9  (* cons case *)
   22.10  apply (auto simp add: mk_traceConc)
   22.11  apply (frule reachable.reachable_n)
   22.12 @@ -210,7 +210,7 @@
   22.13    --> is_exec_frag A (s,xs @@ ys))"
   22.14  
   22.15  apply (rule impI)
   22.16 -apply (tactic {* Seq_Finite_induct_tac 1 *})
   22.17 +apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
   22.18  (* main case *)
   22.19  apply (auto simp add: split_paired_all)
   22.20  done
   22.21 @@ -230,7 +230,7 @@
   22.22  apply (unfold corresp_ex_def)
   22.23  
   22.24  apply simp
   22.25 -apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
   22.26 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
   22.27  (* main case *)
   22.28  apply auto
   22.29  apply (rule_tac t = "f y" in lemma_2_1)
   22.30 @@ -273,13 +273,13 @@
   22.31    apply (rule_tac x = "corresp_ex A f ex" in bexI)
   22.32  
   22.33    (* Traces coincide, Lemma 1 *)
   22.34 -  apply (tactic {* pair_tac "ex" 1 *})
   22.35 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.36    apply (erule lemma_1 [THEN spec, THEN mp])
   22.37    apply assumption+
   22.38    apply (simp add: executions_def reachable.reachable_0)
   22.39  
   22.40    (* corresp_ex is execution, Lemma 2 *)
   22.41 -  apply (tactic {* pair_tac "ex" 1 *})
   22.42 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.43    apply (simp add: executions_def)
   22.44    (* start state *)
   22.45    apply (rule conjI)
   22.46 @@ -324,13 +324,13 @@
   22.47  apply auto
   22.48  
   22.49    (* Traces coincide, Lemma 1 *)
   22.50 -  apply (tactic {* pair_tac "ex" 1 *})
   22.51 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.52    apply (erule lemma_1 [THEN spec, THEN mp])
   22.53    apply assumption+
   22.54    apply (simp add: executions_def reachable.reachable_0)
   22.55  
   22.56    (* corresp_ex is execution, Lemma 2 *)
   22.57 -  apply (tactic {* pair_tac "ex" 1 *})
   22.58 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.59    apply (simp add: executions_def)
   22.60    (* start state *)
   22.61    apply (rule conjI)
   22.62 @@ -351,14 +351,14 @@
   22.63  apply auto
   22.64  
   22.65    (* Traces coincide, Lemma 1 *)
   22.66 -  apply (tactic {* pair_tac "ex" 1 *})
   22.67 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.68    apply (erule lemma_1 [THEN spec, THEN mp])
   22.69    apply (simp (no_asm) add: externals_def)
   22.70    apply (auto)[1]
   22.71    apply (simp add: executions_def reachable.reachable_0)
   22.72  
   22.73    (* corresp_ex is execution, Lemma 2 *)
   22.74 -  apply (tactic {* pair_tac "ex" 1 *})
   22.75 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   22.76    apply (simp add: executions_def)
   22.77    (* start state *)
   22.78    apply (rule conjI)
   22.79 @@ -369,5 +369,4 @@
   22.80  
   22.81  done
   22.82  
   22.83 -
   22.84  end
    23.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jun 14 17:49:24 2008 +0200
    23.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jun 14 23:19:51 2008 +0200
    23.3 @@ -1086,44 +1086,46 @@
    23.4  done
    23.5  
    23.6  
    23.7 -
    23.8  ML {*
    23.9  
   23.10 -local
   23.11 -  val Seq_cases = thm "Seq_cases"
   23.12 -  val Seq_induct = thm "Seq_induct"
   23.13 -  val Seq_Finite_ind = thm "Seq_Finite_ind"
   23.14 -in
   23.15 -
   23.16 -fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
   23.17 -          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
   23.18 +fun Seq_case_tac ctxt s i =
   23.19 +  RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
   23.20 +  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
   23.21  
   23.22  (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
   23.23 -fun Seq_case_simp_tac s i = Seq_case_tac s i THEN SIMPSET' asm_simp_tac (i+2)
   23.24 -                                             THEN SIMPSET' asm_full_simp_tac (i+1)
   23.25 -                                             THEN SIMPSET' asm_full_simp_tac i;
   23.26 +fun Seq_case_simp_tac ctxt s i =
   23.27 +  let val ss = Simplifier.local_simpset_of ctxt in
   23.28 +    Seq_case_tac ctxt s i
   23.29 +    THEN asm_simp_tac ss (i+2)
   23.30 +    THEN asm_full_simp_tac ss (i+1)
   23.31 +    THEN asm_full_simp_tac ss i
   23.32 +  end;
   23.33  
   23.34  (* rws are definitions to be unfolded for admissibility check *)
   23.35 -fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
   23.36 -                         THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac (i+1))))
   23.37 -                         THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
   23.38 +fun Seq_induct_tac ctxt s rws i =
   23.39 +  let val ss = Simplifier.local_simpset_of ctxt in
   23.40 +    RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   23.41 +    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
   23.42 +    THEN simp_tac (ss addsimps rws) i
   23.43 +  end;
   23.44  
   23.45 -fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
   23.46 -                              THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac i)));
   23.47 +fun Seq_Finite_induct_tac ctxt i =
   23.48 +  etac @{thm Seq_Finite_ind} i
   23.49 +  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
   23.50  
   23.51 -fun pair_tac s = res_inst_tac [("p",s)] PairE
   23.52 -                          THEN' hyp_subst_tac THEN' SIMPSET' asm_full_simp_tac;
   23.53 +fun pair_tac ctxt s =
   23.54 +  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE
   23.55 +  THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
   23.56  
   23.57  (* induction on a sequence of pairs with pairsplitting and simplification *)
   23.58 -fun pair_induct_tac s rws i =
   23.59 -           res_inst_tac [("x",s)] Seq_induct i
   23.60 -           THEN pair_tac "a" (i+3)
   23.61 -           THEN (REPEAT_DETERM (CHANGED (SIMPSET' simp_tac (i+1))))
   23.62 -           THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
   23.63 -
   23.64 -end
   23.65 +fun pair_induct_tac ctxt s rws i =
   23.66 +  let val ss = Simplifier.local_simpset_of ctxt in
   23.67 +    RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   23.68 +    THEN pair_tac ctxt "a" (i+3)
   23.69 +    THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
   23.70 +    THEN simp_tac (ss addsimps rws) i
   23.71 +  end;
   23.72  
   23.73  *}
   23.74  
   23.75 -
   23.76  end
    24.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Jun 14 17:49:24 2008 +0200
    24.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Jun 14 23:19:51 2008 +0200
    24.3 @@ -226,7 +226,7 @@
    24.4  apply auto
    24.5  apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
    24.6  apply (simp add: executions_def)
    24.7 -apply (tactic {* pair_tac "ex" 1 *})
    24.8 +apply (tactic {* pair_tac @{context} "ex" 1 *})
    24.9  apply auto
   24.10  apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI)
   24.11  apply (simp (no_asm_simp))
    25.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sat Jun 14 17:49:24 2008 +0200
    25.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Sat Jun 14 23:19:51 2008 +0200
    25.3 @@ -172,7 +172,7 @@
    25.4           !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
    25.5               mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
    25.6  
    25.7 -apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
    25.8 +apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *})
    25.9  (* cons case *)
   25.10  apply auto
   25.11  apply (rename_tac ex a t s s')
   25.12 @@ -197,7 +197,7 @@
   25.13    !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
   25.14    --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
   25.15  
   25.16 -apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
   25.17 +apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
   25.18  (* main case *)
   25.19  apply auto
   25.20  apply (rename_tac ex a t s s')
   25.21 @@ -267,7 +267,7 @@
   25.22    apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
   25.23  
   25.24    (* Traces coincide, Lemma 1 *)
   25.25 -  apply (tactic {* pair_tac "ex" 1 *})
   25.26 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   25.27    apply (rename_tac s ex)
   25.28    apply (simp (no_asm) add: corresp_ex_sim_def)
   25.29    apply (rule_tac s = "s" in traces_coincide_sim)
   25.30 @@ -275,7 +275,7 @@
   25.31    apply (simp add: executions_def reachable.reachable_0 sim_starts1)
   25.32  
   25.33    (* corresp_ex_sim is execution, Lemma 2 *)
   25.34 -  apply (tactic {* pair_tac "ex" 1 *})
   25.35 +  apply (tactic {* pair_tac @{context} "ex" 1 *})
   25.36    apply (simp add: executions_def)
   25.37    apply (rename_tac s ex)
   25.38  
    26.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Sat Jun 14 17:49:24 2008 +0200
    26.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sat Jun 14 23:19:51 2008 +0200
    26.3 @@ -155,7 +155,7 @@
    26.4  "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
    26.5  apply (unfold tsuffix_def suffix_def)
    26.6  apply auto
    26.7 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
    26.8 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
    26.9  apply (rule_tac x = "a>>s1" in exI)
   26.10  apply auto
   26.11  done
    27.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Jun 14 17:49:24 2008 +0200
    27.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Sat Jun 14 23:19:51 2008 +0200
    27.3 @@ -149,9 +149,9 @@
    27.4  
    27.5  
    27.6  lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
    27.7 -apply (tactic {* pair_tac "exec" 1 *})
    27.8 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
    27.9 -apply (tactic {* pair_tac "a" 1 *})
   27.10 +apply (tactic {* pair_tac @{context} "exec" 1 *})
   27.11 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   27.12 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.13  done
   27.14  
   27.15  
   27.16 @@ -170,33 +170,33 @@
   27.17  apply (simp split add: split_if)
   27.18  (* TL = UU *)
   27.19  apply (rule conjI)
   27.20 -apply (tactic {* pair_tac "ex" 1 *})
   27.21 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
   27.22 -apply (tactic {* pair_tac "a" 1 *})
   27.23 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
   27.24 -apply (tactic {* pair_tac "a" 1 *})
   27.25 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   27.26 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   27.27 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.28 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   27.29 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.30  (* TL = nil *)
   27.31  apply (rule conjI)
   27.32 -apply (tactic {* pair_tac "ex" 1 *})
   27.33 -apply (tactic {* Seq_case_tac "y" 1 *})
   27.34 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   27.35 +apply (tactic {* Seq_case_tac @{context} "y" 1 *})
   27.36  apply (simp add: unlift_def)
   27.37  apply fast
   27.38  apply (simp add: unlift_def)
   27.39  apply fast
   27.40  apply (simp add: unlift_def)
   27.41 -apply (tactic {* pair_tac "a" 1 *})
   27.42 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
   27.43 -apply (tactic {* pair_tac "a" 1 *})
   27.44 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.45 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   27.46 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.47  (* TL =cons *)
   27.48  apply (simp add: unlift_def)
   27.49  
   27.50 -apply (tactic {* pair_tac "ex" 1 *})
   27.51 -apply (tactic {* Seq_case_simp_tac "y" 1 *})
   27.52 -apply (tactic {* pair_tac "a" 1 *})
   27.53 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
   27.54 +apply (tactic {* pair_tac @{context} "ex" 1 *})
   27.55 +apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
   27.56 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.57 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   27.58  apply blast
   27.59  apply fastsimp
   27.60 -apply (tactic {* pair_tac "a" 1 *})
   27.61 +apply (tactic {* pair_tac @{context} "a" 1 *})
   27.62   apply fastsimp
   27.63  done
   27.64  
    28.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Jun 14 17:49:24 2008 +0200
    28.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Sat Jun 14 23:19:51 2008 +0200
    28.3 @@ -333,7 +333,7 @@
    28.4  declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
    28.5  
    28.6  lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
    28.7 -apply (tactic "Seq_Finite_induct_tac 1")
    28.8 +apply (tactic "Seq_Finite_induct_tac @{context} 1")
    28.9  done
   28.10  
   28.11  
   28.12 @@ -359,8 +359,8 @@
   28.13  lemma execfrag_in_sig: 
   28.14    "!! A. is_trans_of A ==>  
   28.15    ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
   28.16 -apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def",
   28.17 -  thm "Forall_def", thm "sforall_def"] 1 *})
   28.18 +apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
   28.19 +  @{thm Forall_def}, @{thm sforall_def}] 1 *})
   28.20  (* main case *)
   28.21  apply (auto simp add: is_trans_of_def)
   28.22  done
   28.23 @@ -369,7 +369,7 @@
   28.24    "!! A.[|  is_trans_of A; x:executions A |] ==>  
   28.25    Forall (%a. a:act A) (filter_act$(snd x))"
   28.26  apply (simp add: executions_def)
   28.27 -apply (tactic {* pair_tac "x" 1 *})
   28.28 +apply (tactic {* pair_tac @{context} "x" 1 *})
   28.29  apply (rule execfrag_in_sig [THEN spec, THEN mp])
   28.30  apply auto
   28.31  done
   28.32 @@ -386,10 +386,10 @@
   28.33  
   28.34  (* only admissible in y, not if done in x !! *)
   28.35  lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
   28.36 -apply (tactic {* pair_induct_tac "y" [thm "is_exec_frag_def"] 1 *})
   28.37 +apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
   28.38  apply (intro strip)
   28.39 -apply (tactic {* Seq_case_simp_tac "xa" 1 *})
   28.40 -apply (tactic {* pair_tac "a" 1 *})
   28.41 +apply (tactic {* Seq_case_simp_tac @{context} "xa" 1 *})
   28.42 +apply (tactic {* pair_tac @{context} "a" 1 *})
   28.43  apply auto
   28.44  done
   28.45  
   28.46 @@ -401,12 +401,11 @@
   28.47  
   28.48  lemma exec_prefix2closed [rule_format]:
   28.49    "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
   28.50 -apply (tactic {* pair_induct_tac "x" [thm "is_exec_frag_def"] 1 *})
   28.51 +apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *})
   28.52  apply (intro strip)
   28.53 -apply (tactic {* Seq_case_simp_tac "s" 1 *})
   28.54 -apply (tactic {* pair_tac "a" 1 *})
   28.55 +apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
   28.56 +apply (tactic {* pair_tac @{context} "a" 1 *})
   28.57  apply auto
   28.58  done
   28.59  
   28.60 -
   28.61  end
    29.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jun 14 17:49:24 2008 +0200
    29.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jun 14 23:19:51 2008 +0200
    29.3 @@ -86,17 +86,18 @@
    29.4      val prop = Logic.strip_imp_concl t';
    29.5      fun tac {prems, context} =
    29.6        rewrite_goals_tac defs THEN
    29.7 -      EVERY (tacs (map (rewrite_rule defs) prems));
    29.8 +      EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context})
    29.9    in Goal.prove_global thy [] asms prop tac end;
   29.10  
   29.11  fun pg' thy defs t tacsf =
   29.12    let
   29.13 -    fun tacs [] = tacsf
   29.14 -      | tacs prems = cut_facts_tac prems 1 :: tacsf;
   29.15 +    fun tacs {prems, context} =
   29.16 +      if null prems then tacsf context
   29.17 +      else cut_facts_tac prems 1 :: tacsf context;
   29.18    in pg'' thy defs t tacs end;
   29.19  
   29.20 -fun case_UU_tac rews i v =
   29.21 -  case_split_tac (v^"=UU") i THEN
   29.22 +fun case_UU_tac ctxt rews i v =
   29.23 +  InductTacs.case_tac ctxt (v^"=UU") i THEN
   29.24    asm_simp_tac (HOLCF_ss addsimps rews) i;
   29.25  
   29.26  val chain_tac =
   29.27 @@ -181,7 +182,7 @@
   29.28        val appl = bind_fun vars (lhs == rhs);
   29.29        val cs = ContProc.cont_thms lam;
   29.30        val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
   29.31 -    in pg (def::betas) appl [rtac reflexive_thm 1] end;
   29.32 +    in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
   29.33  end;
   29.34  
   29.35  val when_appl = appl_of_def ax_when_def;
   29.36 @@ -234,7 +235,7 @@
   29.37      rewrite_goals_tac [mk_meta_eq iso_swap],
   29.38      rtac thm3 1];
   29.39  in
   29.40 -  val exhaust = pg con_appls (mk_trp exh) tacs;
   29.41 +  val exhaust = pg con_appls (mk_trp exh) (K tacs);
   29.42    val casedist =
   29.43      standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
   29.44  end;
   29.45 @@ -249,7 +250,7 @@
   29.46        val axs = [when_appl, mk_meta_eq rep_strict];
   29.47        val goal = bind_fun (mk_trp (strict when_app));
   29.48        val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
   29.49 -    in pg axs goal tacs end;
   29.50 +    in pg axs goal (K tacs) end;
   29.51  
   29.52    val when_apps =
   29.53      let
   29.54 @@ -260,7 +261,7 @@
   29.55                  mk_trp (when_app`(con_app con args) ===
   29.56                         list_ccomb (bound_fun n 0, map %# args))));
   29.57            val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
   29.58 -        in pg axs goal tacs end;
   29.59 +        in pg axs goal (K tacs) end;
   29.60      in mapn one_when 1 cons end;
   29.61  end;
   29.62  val when_rews = when_strict :: when_apps;
   29.63 @@ -271,7 +272,7 @@
   29.64    fun dis_strict (con, _) =
   29.65      let
   29.66        val goal = mk_trp (strict (%%:(dis_name con)));
   29.67 -    in pg axs_dis_def goal [rtac when_strict 1] end;
   29.68 +    in pg axs_dis_def goal (K [rtac when_strict 1]) end;
   29.69  
   29.70    fun dis_app c (con, args) =
   29.71      let
   29.72 @@ -279,7 +280,7 @@
   29.73        val rhs = if con = c then TT else FF;
   29.74        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
   29.75        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
   29.76 -    in pg axs_dis_def goal tacs end;
   29.77 +    in pg axs_dis_def goal (K tacs) end;
   29.78  
   29.79    val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
   29.80  
   29.81 @@ -291,7 +292,7 @@
   29.82           contr_tac 1,
   29.83           DETERM_UNTIL_SOLVED (CHANGED
   29.84            (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
   29.85 -    in pg [] goal tacs end;
   29.86 +    in pg [] goal (K tacs) end;
   29.87  
   29.88    val dis_stricts = map dis_strict cons;
   29.89    val dis_defins = map dis_defin cons;
   29.90 @@ -304,7 +305,7 @@
   29.91      let
   29.92        val goal = mk_trp (strict (%%:(mat_name con)));
   29.93        val tacs = [rtac when_strict 1];
   29.94 -    in pg axs_mat_def goal tacs end;
   29.95 +    in pg axs_mat_def goal (K tacs) end;
   29.96  
   29.97    val mat_stricts = map mat_strict cons;
   29.98  
   29.99 @@ -317,7 +318,7 @@
  29.100          else mk_fail;
  29.101        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
  29.102        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
  29.103 -    in pg axs_mat_def goal tacs end;
  29.104 +    in pg axs_mat_def goal (K tacs) end;
  29.105  
  29.106    val mat_apps =
  29.107      maps (fn (c,_) => map (one_mat c) cons) cons;
  29.108 @@ -340,7 +341,7 @@
  29.109        val axs = @{thm branch_def} :: axs_pat_def;
  29.110        val goal = mk_trp (strict (pat_lhs c ` (%:"rhs")));
  29.111        val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
  29.112 -    in pg axs goal tacs end;
  29.113 +    in pg axs goal (K tacs) end;
  29.114  
  29.115    fun pat_app c (con, args) =
  29.116      let
  29.117 @@ -349,7 +350,7 @@
  29.118        val rhs = if con = fst c then pat_rhs c else mk_fail;
  29.119        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
  29.120        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
  29.121 -    in pg axs goal tacs end;
  29.122 +    in pg axs goal (K tacs) end;
  29.123  
  29.124    val pat_stricts = map pat_strict cons;
  29.125    val pat_apps = maps (fn c => map (pat_app c) cons) cons;
  29.126 @@ -366,16 +367,16 @@
  29.127            fun f arg = if vname arg = vn then UU else %# arg;
  29.128            val goal = mk_trp (con_app2 con f args === UU);
  29.129            val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
  29.130 -        in pg con_appls goal tacs end;
  29.131 +        in pg con_appls goal (K tacs) end;
  29.132      in map one_strict (nonlazy args) end;
  29.133  
  29.134    fun con_defin (con, args) =
  29.135      let
  29.136        val concl = mk_trp (defined (con_app con args));
  29.137        val goal = lift_defined %: (nonlazy args, concl);
  29.138 -      val tacs = [
  29.139 +      fun tacs ctxt = [
  29.140          rtac @{thm rev_contrapos} 1,
  29.141 -        eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
  29.142 +        RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
  29.143          asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
  29.144      in pg [] goal tacs end;
  29.145  in
  29.146 @@ -394,7 +395,7 @@
  29.147        val tacs = [
  29.148          rtac (iso_locale RS iso_compact_abs) 1,
  29.149          REPEAT (resolve_tac rules 1 ORELSE atac 1)];
  29.150 -    in pg con_appls goal tacs end;
  29.151 +    in pg con_appls goal (K tacs) end;
  29.152  in
  29.153    val con_compacts = map con_compact cons;
  29.154  end;
  29.155 @@ -402,7 +403,7 @@
  29.156  local
  29.157    fun one_sel sel =
  29.158      pg axs_sel_def (mk_trp (strict (%%:sel)))
  29.159 -      [simp_tac (HOLCF_ss addsimps when_rews) 1];
  29.160 +      (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
  29.161  
  29.162    fun sel_strict (_, args) =
  29.163      List.mapPartial (Option.map one_sel o sel_of) args;
  29.164 @@ -419,20 +420,20 @@
  29.165        val nlas' = List.filter (fn v => v <> vnn) nlas;
  29.166        val lhs = (%%:sel)`(con_app con args);
  29.167        val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
  29.168 -      val tacs1 =
  29.169 +      fun tacs1 ctxt =
  29.170          if vnn mem nlas
  29.171 -        then [case_UU_tac (when_rews @ con_stricts) 1 vnn]
  29.172 +        then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn]
  29.173          else [];
  29.174        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
  29.175 -    in pg axs_sel_def goal (tacs1 @ tacs2) end;
  29.176 +    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
  29.177  
  29.178    fun sel_app_diff c n sel (con, args) =
  29.179      let
  29.180        val nlas = nonlazy args;
  29.181        val goal = mk_trp (%%:sel ` con_app con args === UU);
  29.182 -      val tacs1 = map (case_UU_tac (when_rews @ con_stricts) 1) nlas;
  29.183 +      fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas;
  29.184        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
  29.185 -    in pg axs_sel_def goal (tacs1 @ tacs2) end;
  29.186 +    in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
  29.187  
  29.188    fun sel_app c n sel (con, args) =
  29.189      if con = c
  29.190 @@ -456,7 +457,7 @@
  29.191          contr_tac 1,
  29.192          DETERM_UNTIL_SOLVED (CHANGED
  29.193            (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
  29.194 -    in pg [] goal tacs end;
  29.195 +    in pg [] goal (K tacs) end;
  29.196  in
  29.197    val sel_defins =
  29.198      if length cons = 1
  29.199 @@ -474,10 +475,10 @@
  29.200        let
  29.201          val goal = lift_defined %: (nonlazy args1,
  29.202                          mk_trp (con_app con1 args1 ~<< con_app con2 args2));
  29.203 -        val tacs = [
  29.204 +        fun tacs ctxt = [
  29.205            rtac @{thm rev_contrapos} 1,
  29.206 -          eres_inst_tac [("f", dis_name con1)] monofun_cfun_arg 1]
  29.207 -          @ map (case_UU_tac (con_stricts @ dis_rews) 1) (nonlazy args2)
  29.208 +          RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
  29.209 +          @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
  29.210            @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
  29.211        in pg [] goal tacs end;
  29.212  
  29.213 @@ -527,13 +528,13 @@
  29.214        val abs_less = ax_abs_iso RS (allI RS injection_less);
  29.215        val tacs =
  29.216          [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
  29.217 -    in map (fn (con, args) => pgterm (op <<) con args tacs) cons' end;
  29.218 +    in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
  29.219  
  29.220    val injects =
  29.221      let
  29.222        val abs_eq = ax_abs_iso RS (allI RS injection_eq);
  29.223        val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
  29.224 -    in map (fn (con, args) => pgterm (op ===) con args tacs) cons' end;
  29.225 +    in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
  29.226  end;
  29.227  
  29.228  (* ----- theorems concerning one induction step ----------------------------- *)
  29.229 @@ -542,7 +543,7 @@
  29.230    let
  29.231      val goal = mk_trp (strict (dc_copy `% "f"));
  29.232      val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict, when_strict]) 1];
  29.233 -  in pg [ax_copy_def] goal tacs end;
  29.234 +  in pg [ax_copy_def] goal (K tacs) end;
  29.235  
  29.236  local
  29.237    fun copy_app (con, args) =
  29.238 @@ -552,9 +553,9 @@
  29.239        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
  29.240        val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
  29.241        val stricts = abs_strict::when_strict::con_stricts;
  29.242 -      val tacs1 = map (case_UU_tac stricts 1 o vname) args';
  29.243 +      fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
  29.244        val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
  29.245 -    in pg [ax_copy_def] goal (tacs1 @ tacs2) end;
  29.246 +    in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
  29.247  in
  29.248    val copy_apps = map copy_app cons;
  29.249  end;
  29.250 @@ -564,7 +565,7 @@
  29.251      let
  29.252        val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
  29.253        val rews = copy_strict :: copy_apps @ con_rews;
  29.254 -      val tacs = map (case_UU_tac rews 1) (nonlazy args) @
  29.255 +      fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
  29.256          [asm_simp_tac (HOLCF_ss addsimps rews) 1];
  29.257      in pg [] goal tacs end;
  29.258  
  29.259 @@ -646,8 +647,8 @@
  29.260      let
  29.261        fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
  29.262        val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
  29.263 -      val tacs = [
  29.264 -        nat_induct_tac "n" 1,
  29.265 +      fun tacs ctxt = [
  29.266 +        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
  29.267          simp_tac iterate_Cprod_ss 1,
  29.268          asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
  29.269      in pg copy_take_defs goal tacs end;
  29.270 @@ -656,9 +657,9 @@
  29.271    fun take_0 n dn =
  29.272      let
  29.273        val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
  29.274 -    in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
  29.275 +    in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
  29.276    val take_0s = mapn take_0 1 dnames;
  29.277 -  val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
  29.278 +  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
  29.279    val take_apps =
  29.280      let
  29.281        fun mk_eqn dn (con, args) =
  29.282 @@ -670,19 +671,19 @@
  29.283        fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
  29.284        val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
  29.285        val simps = List.filter (has_fewer_prems 1) copy_rews;
  29.286 -      fun con_tac (con, args) =
  29.287 +      fun con_tac ctxt (con, args) =
  29.288          if nonlazy_rec args = []
  29.289          then all_tac
  29.290 -        else EVERY (map c_UU_tac (nonlazy_rec args)) THEN
  29.291 +        else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
  29.292            asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
  29.293 -      fun eq_tacs ((dn, _), cons) = map con_tac cons;
  29.294 -      val tacs =
  29.295 +      fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
  29.296 +      fun tacs ctxt =
  29.297          simp_tac iterate_Cprod_ss 1 ::
  29.298 -        nat_induct_tac "n" 1 ::
  29.299 +        InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
  29.300          simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
  29.301          asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
  29.302          TRY (safe_tac HOL_cs) ::
  29.303 -        maps eq_tacs eqs;
  29.304 +        maps (eq_tacs ctxt) eqs;
  29.305      in pg copy_take_defs goal tacs end;
  29.306  in
  29.307    val take_rews = map standard
  29.308 @@ -705,8 +706,8 @@
  29.309      (mapn (fn n => fn x => (P_name n, x)) 1 conss,
  29.310       mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
  29.311    val take_ss = HOL_ss addsimps take_rews;
  29.312 -  fun quant_tac i = EVERY
  29.313 -    (mapn (fn n => fn _ => res_inst_tac [("x", x_name n)] spec i) 1 dnames);
  29.314 +  fun quant_tac ctxt i = EVERY
  29.315 +    (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
  29.316  
  29.317    fun ind_prems_tac prems = EVERY
  29.318      (maps (fn cons =>
  29.319 @@ -745,16 +746,16 @@
  29.320        fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
  29.321        val goal = ind_term concf;
  29.322  
  29.323 -      fun tacf prems =
  29.324 +      fun tacf {prems, context} =
  29.325          let
  29.326            val tacs1 = [
  29.327 -            quant_tac 1,
  29.328 +            quant_tac context 1,
  29.329              simp_tac HOL_ss 1,
  29.330 -            nat_induct_tac "n" 1,
  29.331 +            InductTacs.induct_tac context [[SOME "n"]] 1,
  29.332              simp_tac (take_ss addsimps prems) 1,
  29.333              TRY (safe_tac HOL_cs)];
  29.334            fun arg_tac arg =
  29.335 -            case_UU_tac (prems @ con_rews) 1
  29.336 +            case_UU_tac context (prems @ con_rews) 1
  29.337                (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
  29.338            fun con_tacs (con, args) = 
  29.339              asm_simp_tac take_ss 1 ::
  29.340 @@ -763,7 +764,7 @@
  29.341              map (K (atac 1))      (nonlazy args) @
  29.342              map (K (etac spec 1)) (List.filter is_rec args);
  29.343            fun cases_tacs (cons, cases) =
  29.344 -            res_inst_tac [("x","x")] cases 1 ::
  29.345 +            RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
  29.346              asm_simp_tac (take_ss addsimps prems) 1 ::
  29.347              maps con_tacs cons;
  29.348          in
  29.349 @@ -779,9 +780,9 @@
  29.350            val rhs = dc_take dn $ Bound 0 `%(x_name n^"'");
  29.351            val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
  29.352            val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
  29.353 -          fun tacf prems = [
  29.354 -            res_inst_tac [("t", x_name n    )] (ax_reach RS subst) 1,
  29.355 -            res_inst_tac [("t", x_name n^"'")] (ax_reach RS subst) 1,
  29.356 +          fun tacf {prems, context} = [
  29.357 +            RuleInsts.res_inst_tac context [(("t", 0), x_name n    )] (ax_reach RS subst) 1,
  29.358 +            RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
  29.359              stac fix_def2 1,
  29.360              REPEAT (CHANGED
  29.361                (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
  29.362 @@ -814,7 +815,7 @@
  29.363                resolve_tac take_lemmas 1,
  29.364                asm_simp_tac take_ss 1,
  29.365                atac 1];
  29.366 -          in pg [] goal tacs end;
  29.367 +          in pg [] goal (K tacs) end;
  29.368          val finite_lemmas1a = map dname_lemma dnames;
  29.369   
  29.370          val finite_lemma1b =
  29.371 @@ -829,33 +830,33 @@
  29.372                end;
  29.373              val goal =
  29.374                mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
  29.375 -            fun arg_tacs vn = [
  29.376 -              eres_inst_tac [("x", vn)] all_dupE 1,
  29.377 +            fun arg_tacs ctxt vn = [
  29.378 +              RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
  29.379                etac disjE 1,
  29.380                asm_simp_tac (HOL_ss addsimps con_rews) 1,
  29.381                asm_simp_tac take_ss 1];
  29.382 -            fun con_tacs (con, args) =
  29.383 +            fun con_tacs ctxt (con, args) =
  29.384                asm_simp_tac take_ss 1 ::
  29.385 -              maps arg_tacs (nonlazy_rec args);
  29.386 -            fun foo_tacs n (cons, cases) =
  29.387 +              maps (arg_tacs ctxt) (nonlazy_rec args);
  29.388 +            fun foo_tacs ctxt n (cons, cases) =
  29.389                simp_tac take_ss 1 ::
  29.390                rtac allI 1 ::
  29.391 -              res_inst_tac [("x",x_name n)] cases 1 ::
  29.392 +              RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
  29.393                asm_simp_tac take_ss 1 ::
  29.394 -              maps con_tacs cons;
  29.395 -            val tacs =
  29.396 +              maps (con_tacs ctxt) cons;
  29.397 +            fun tacs ctxt =
  29.398                rtac allI 1 ::
  29.399 -              nat_induct_tac "n" 1 ::
  29.400 +              InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
  29.401                simp_tac take_ss 1 ::
  29.402                TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
  29.403 -              flat (mapn foo_tacs 1 (conss ~~ cases));
  29.404 +              flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
  29.405            in pg [] goal tacs end;
  29.406  
  29.407          fun one_finite (dn, l1b) =
  29.408            let
  29.409              val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
  29.410 -            val tacs = [
  29.411 -              case_UU_tac take_rews 1 "x",
  29.412 +            fun tacs ctxt = [
  29.413 +              case_UU_tac ctxt take_rews 1 "x",
  29.414                eresolve_tac finite_lemmas1a 1,
  29.415                step_tac HOL_cs 1,
  29.416                step_tac HOL_cs 1,
  29.417 @@ -867,7 +868,7 @@
  29.418          val ind =
  29.419            let
  29.420              fun concf n dn = %:(P_name n) $ %:(x_name n);
  29.421 -            fun tacf prems =
  29.422 +            fun tacf {prems, context} =
  29.423                let
  29.424                  fun finite_tacs (finite, fin_ind) = [
  29.425                    rtac(rewrite_rule axs_finite_def finite RS exE)1,
  29.426 @@ -893,9 +894,9 @@
  29.427              fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
  29.428              fun concf n dn = %:(P_name n) $ %:(x_name n);
  29.429            in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
  29.430 -        fun tacf prems =
  29.431 +        fun tacf {prems, context} =
  29.432            map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
  29.433 -          quant_tac 1,
  29.434 +          quant_tac context 1,
  29.435            rtac (adm_impl_admw RS wfix_ind) 1,
  29.436            REPEAT_DETERM (rtac adm_all 1),
  29.437            REPEAT_DETERM (
  29.438 @@ -930,18 +931,18 @@
  29.439            Library.foldr mk_all2 (xs,
  29.440              Library.foldr mk_imp (mapn mk_prj 0 dnames,
  29.441                foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
  29.442 -      fun x_tacs n x = [
  29.443 +      fun x_tacs ctxt n x = [
  29.444          rotate_tac (n+1) 1,
  29.445          etac all2E 1,
  29.446 -        eres_inst_tac [("P1", sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
  29.447 +        RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
  29.448          TRY (safe_tac HOL_cs),
  29.449          REPEAT (CHANGED (asm_simp_tac take_ss 1))];
  29.450 -      val tacs = [
  29.451 +      fun tacs ctxt = [
  29.452          rtac impI 1,
  29.453 -        nat_induct_tac "n" 1,
  29.454 +        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
  29.455          simp_tac take_ss 1,
  29.456          safe_tac HOL_cs] @
  29.457 -        flat (mapn x_tacs 0 xs);
  29.458 +        flat (mapn (x_tacs ctxt) 0 xs);
  29.459      in pg [ax_bisim_def] goal tacs end;
  29.460  in
  29.461    val coind = 
  29.462 @@ -959,7 +960,7 @@
  29.463            cut_facts_tac [coind_lemma] 1,
  29.464            fast_tac HOL_cs 1])
  29.465          take_lemmas;
  29.466 -    in pg [] goal tacs end;
  29.467 +    in pg [] goal (K tacs) end;
  29.468  end; (* local *)
  29.469  
  29.470  in thy |> Sign.add_path comp_dnam
    30.1 --- a/src/LCF/LCF.thy	Sat Jun 14 17:49:24 2008 +0200
    30.2 +++ b/src/LCF/LCF.thy	Sat Jun 14 23:19:51 2008 +0200
    30.3 @@ -23,7 +23,7 @@
    30.4  typedecl ('a,'b) "+"    (infixl 5)
    30.5  
    30.6  arities
    30.7 -  fun :: (cpo, cpo) cpo
    30.8 +  "fun" :: (cpo, cpo) cpo
    30.9    "*" :: (cpo, cpo) cpo
   30.10    "+" :: (cpo, cpo) cpo
   30.11    tr :: cpo
   30.12 @@ -316,13 +316,13 @@
   30.13  
   30.14  
   30.15  ML {*
   30.16 -  fun induct_tac v i =
   30.17 -    res_inst_tac[("f",v)] @{thm induct} i THEN
   30.18 +  fun induct_tac ctxt v i =
   30.19 +    RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
   30.20      REPEAT (resolve_tac @{thms adm_lemmas} i)
   30.21  *}
   30.22  
   30.23  lemma least_FIX: "f(p) = p ==> FIX(f) << p"
   30.24 -  apply (tactic {* induct_tac "f" 1 *})
   30.25 +  apply (tactic {* induct_tac @{context} "f" 1 *})
   30.26    apply (rule minimal)
   30.27    apply (intro strip)
   30.28    apply (erule subst)
   30.29 @@ -375,8 +375,8 @@
   30.30    done
   30.31  
   30.32  ML {*
   30.33 -fun induct2_tac (f,g) i =
   30.34 -  res_inst_tac[("f",f),("g",g)] @{thm induct2} i THEN
   30.35 +fun induct2_tac ctxt (f, g) i =
   30.36 +  RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
   30.37    REPEAT(resolve_tac @{thms adm_lemmas} i)
   30.38  *}
   30.39  
    31.1 --- a/src/LCF/ex/Ex1.thy	Sat Jun 14 17:49:24 2008 +0200
    31.2 +++ b/src/LCF/ex/Ex1.thy	Sat Jun 14 23:19:51 2008 +0200
    31.3 @@ -32,7 +32,7 @@
    31.4    done
    31.5  
    31.6  lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
    31.7 -  apply (tactic {* induct_tac "K" 1 *})
    31.8 +  apply (tactic {* induct_tac @{context} "K" 1 *})
    31.9    apply (simp (no_asm))
   31.10    apply (simp (no_asm) split: COND_cases_iff)
   31.11    apply (intro strip)
    32.1 --- a/src/LCF/ex/Ex2.thy	Sat Jun 14 17:49:24 2008 +0200
    32.2 +++ b/src/LCF/ex/Ex2.thy	Sat Jun 14 23:19:51 2008 +0200
    32.3 @@ -23,7 +23,7 @@
    32.4  
    32.5  lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
    32.6    apply (simplesubst H)
    32.7 -  apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
    32.8 +  apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
    32.9    apply (simp (no_asm))
   32.10    apply (simp (no_asm_simp) split: COND_cases_iff)
   32.11    done
    33.1 --- a/src/LCF/ex/Ex3.thy	Sat Jun 14 17:49:24 2008 +0200
    33.2 +++ b/src/LCF/ex/Ex3.thy	Sat Jun 14 23:19:51 2008 +0200
    33.3 @@ -18,7 +18,7 @@
    33.4  declare p_strict [simp] p_s [simp]
    33.5  
    33.6  lemma example: "p(FIX(s),y) = FIX(s)"
    33.7 -  apply (tactic {* induct_tac "s" 1 *})
    33.8 +  apply (tactic {* induct_tac @{context} "s" 1 *})
    33.9    apply (simp (no_asm))
   33.10    apply (simp (no_asm))
   33.11    done
    34.1 --- a/src/LCF/ex/Ex4.thy	Sat Jun 14 17:49:24 2008 +0200
    34.2 +++ b/src/LCF/ex/Ex4.thy	Sat Jun 14 23:19:51 2008 +0200
    34.3 @@ -10,7 +10,7 @@
    34.4    shows "FIX(f)=p"
    34.5    apply (unfold eq_def)
    34.6    apply (rule conjI)
    34.7 -  apply (tactic {* induct_tac "f" 1 *})
    34.8 +  apply (tactic {* induct_tac @{context} "f" 1 *})
    34.9    apply (rule minimal)
   34.10    apply (intro strip)
   34.11    apply (rule less_trans)
    35.1 --- a/src/Sequents/LK0.thy	Sat Jun 14 17:49:24 2008 +0200
    35.2 +++ b/src/Sequents/LK0.thy	Sat Jun 14 23:19:51 2008 +0200
    35.3 @@ -156,12 +156,12 @@
    35.4  
    35.5  ML {*
    35.6  (*Cut and thin, replacing the right-side formula*)
    35.7 -fun cutR_tac s i =
    35.8 -  res_inst_tac [ ("P", s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
    35.9 +fun cutR_tac ctxt s i =
   35.10 +  RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
   35.11  
   35.12  (*Cut and thin, replacing the left-side formula*)
   35.13 -fun cutL_tac s i =
   35.14 -  res_inst_tac [("P", s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
   35.15 +fun cutL_tac ctxt s i =
   35.16 +  RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
   35.17  *}
   35.18  
   35.19  
    36.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Jun 14 17:49:24 2008 +0200
    36.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jun 14 23:19:51 2008 +0200
    36.3 @@ -10,8 +10,8 @@
    36.4  
    36.5  signature DATATYPE_TACTICS =
    36.6  sig
    36.7 -  val induct_tac: string -> int -> tactic
    36.8 -  val exhaust_tac: string -> int -> tactic
    36.9 +  val induct_tac: Proof.context -> string -> int -> tactic
   36.10 +  val exhaust_tac: Proof.context -> string -> int -> tactic
   36.11    val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
   36.12    val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list ->
   36.13      (Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory
   36.14 @@ -89,10 +89,10 @@
   36.15        (2) exhaustion works for VARIABLES in the premises, not general terms
   36.16  **)
   36.17  
   36.18 -fun exhaust_induct_tac exh var i state =
   36.19 +fun exhaust_induct_tac exh ctxt var i state =
   36.20    let
   36.21 +    val thy = ProofContext.theory_of ctxt
   36.22      val (_, _, Bi, _) = dest_state (state, i)
   36.23 -    val thy = Thm.theory_of_thm state
   36.24      val tn = find_tname var Bi
   36.25      val rule =
   36.26          if exh then #exhaustion (datatype_info thy tn)
   36.27 @@ -102,11 +102,11 @@
   36.28               [] => error "induction is not available for this datatype"
   36.29             | major::_ => FOLogic.dest_Trueprop major)
   36.30    in
   36.31 -    Tactic.eres_inst_tac' [(ixn, var)] rule i state
   36.32 +    RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
   36.33    end
   36.34    handle Find_tname msg =>
   36.35              if exh then (*try boolean case analysis instead*)
   36.36 -                case_tac var i state
   36.37 +                case_tac ctxt var i state
   36.38              else error msg;
   36.39  
   36.40  val exhaust_tac = exhaust_induct_tac true;
   36.41 @@ -178,9 +178,9 @@
   36.42  
   36.43  val setup =
   36.44    Method.add_methods
   36.45 -    [("induct_tac", Method.goal_args Args.name induct_tac,
   36.46 +    [("induct_tac", Method.goal_args_ctxt Args.name induct_tac,
   36.47        "induct_tac emulation (dynamic instantiation!)"),
   36.48 -     ("case_tac", Method.goal_args Args.name exhaust_tac,
   36.49 +     ("case_tac", Method.goal_args_ctxt Args.name exhaust_tac,
   36.50        "datatype case_tac emulation (dynamic instantiation!)")];
   36.51  
   36.52  
    37.1 --- a/src/ZF/UNITY/SubstAx.thy	Sat Jun 14 17:49:24 2008 +0200
    37.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sat Jun 14 23:19:51 2008 +0200
    37.3 @@ -360,7 +360,7 @@
    37.4                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
    37.5                (*now there are two subgoals: co & transient*)
    37.6                simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
    37.7 -              res_inst_tac [("act", sact)] @{thm transientI} 2,
    37.8 +              RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
    37.9                   (*simplify the command's domain*)
   37.10                simp_tac (ss addsimps [@{thm domain_def}]) 3, 
   37.11                (* proving the domain part *)