# HG changeset patch
# User wenzelm
# Date 1213647226 -7200
# Node ID 1caa6726168a71cc1039f490c5f00e92737cce4f
# Parent  f2f42f9fa09dd6d0be23911077c5dc10ac684bc9
inst1_tac: proper context;

diff -r f2f42f9fa09d -r 1caa6726168a src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Mon Jun 16 22:13:39 2008 +0200
+++ b/src/HOL/Bali/AxExample.thy	Mon Jun 16 22:13:46 2008 +0200
@@ -40,25 +40,14 @@
 declare lvar_def [simp]
 
 ML {*
-local
-  val ax_Skip = thm "ax_Skip";
-  val ax_StatRef = thm "ax_StatRef";
-  val ax_MethdN = thm "ax_MethdN";
-  val ax_Alloc = thm "ax_Alloc";
-  val ax_Alloc_Arr = thm "ax_Alloc_Arr";
-  val ax_SXAlloc_Normal = thm "ax_SXAlloc_Normal";
-  val ax_derivs_intros = funpow 7 tl (thms "ax_derivs.intros");
-in
-
-fun inst1_tac s t st =
-  case AList.lookup (op =) (rev (Term.add_varnames (prop_of st) [])) s of
-  SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
+fun inst1_tac ctxt s t st =
+  case AList.lookup (op =) (rev (Term.add_varnames (Thm.prop_of st) [])) s of
+  SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
 
 val ax_tac =
   REPEAT o rtac allI THEN'
-  resolve_tac (ax_Skip :: ax_StatRef :: ax_MethdN :: ax_Alloc ::
-    ax_Alloc_Arr :: ax_SXAlloc_Normal :: ax_derivs_intros);
-end;
+  resolve_tac (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} ::
+    @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)});
 *}
 
 
@@ -73,7 +62,7 @@
          precondition. *)
 apply  (tactic "ax_tac 1" (* Try *))
 defer
-apply    (tactic {* inst1_tac "Q" 
+apply    (tactic {* inst1_tac @{context} "Q" 
                  "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
 prefer 2
 apply    simp
@@ -93,7 +82,7 @@
 apply   (tactic "ax_tac 1" (* AVar *))
 prefer 2
 apply    (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
 apply    (simp del: avar_def2 peek_and_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -134,7 +123,7 @@
 apply      (tactic "ax_tac 1") (* Ass *)
 prefer 2
 apply       (rule ax_subst_Var_allI)
-apply       (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+apply       (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
 apply       (rule allI)
 apply       (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
 apply       (rule ax_derivs.Abrupt)
@@ -142,17 +131,17 @@
 apply      (tactic "ax_tac 1" (* FVar *))
 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
 apply      (tactic "ax_tac 1")
-apply     (tactic {* inst1_tac "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
+apply     (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
 apply     fastsimp
 prefer 4
 apply    (rule ax_derivs.Done [THEN conseq1],force)
 apply   (rule ax_subst_Val_allI)
-apply   (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
 apply   (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
 apply   (tactic "ax_tac 1")
 prefer 2
 apply   (rule ax_subst_Val_allI)
-apply    (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
+apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
 apply    (simp del: peek_and_def2 heap_free_def2 normal_def2)
 apply    (tactic "ax_tac 1")
 apply   (tactic "ax_tac 1")
@@ -171,7 +160,7 @@
 apply (tactic "ax_tac 1")
 defer
 apply  (rule ax_subst_Var_allI)
-apply  (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
+apply  (tactic {* inst1_tac @{context} "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
 apply  (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
 apply  (tactic "ax_tac 1" (* NewC *))
 apply  (tactic "ax_tac 1" (* ax_Alloc *))
@@ -199,18 +188,18 @@
 apply     (tactic "ax_tac 1")
 apply     (tactic "ax_tac 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
-apply      (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
+apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
 apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
 apply      (tactic "ax_tac 2" (* NewA *))
 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
 apply       (tactic "ax_tac 3")
-apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
+apply      (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
 apply      (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *})
 apply      (tactic "ax_tac 2")
 apply     (tactic "ax_tac 1" (* FVar *))
 apply      (tactic "ax_tac 2" (* StatRef *))
 apply     (rule ax_derivs.Done [THEN conseq1])
-apply     (tactic {* inst1_tac "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
+apply     (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
 apply     (clarsimp split del: split_if)
 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
 apply     (drule initedD)
@@ -220,9 +209,9 @@
 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
 apply     (rule wf_tprg)
 apply    clarsimp
-apply   (tactic {* inst1_tac "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
+apply   (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
 apply   clarsimp
-apply  (tactic {* inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
+apply  (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
 apply  clarsimp
      (* end init *)
 apply (rule conseq1)
@@ -254,7 +243,7 @@
 apply  clarsimp
 apply (tactic "ax_tac 1" (* If *))
 apply  (tactic 
-  {* inst1_tac "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
+  {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
 apply  (tactic "ax_tac 1")
 apply  (rule conseq1)
 apply   (tactic "ax_tac 1")
@@ -275,7 +264,7 @@
 apply  (tactic "ax_tac 1")
 prefer 2
 apply   (rule ax_subst_Var_allI)
-apply   (tactic {* inst1_tac "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
+apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
 apply   (rule allI)
 apply   (rule_tac P' = "Normal ?P" in conseq1)
 prefer 2