--- 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