--- a/src/HOL/Bali/AxExample.thy Thu Apr 21 17:22:23 2005 +0200
+++ b/src/HOL/Bali/AxExample.thy Thu Apr 21 18:56:03 2005 +0200
@@ -39,8 +39,9 @@
declare split_if_asm [split del]
declare lvar_def [simp]
-ML {*
-fun inst1_tac s t = instantiate_tac [(s,t)];
+ML_setup {*
+fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
+ SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
val ax_tac = REPEAT o rtac allI THEN'
resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
thm "ax_Alloc"::thm "ax_Alloc_Arr"::
@@ -60,7 +61,7 @@
precondition. *)
apply (tactic "ax_tac 1" (* Try *))
defer
-apply (tactic {* inst1_tac "Q1"
+apply (tactic {* inst1_tac "Q"
"\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
prefer 2
apply simp
@@ -80,7 +81,7 @@
apply (tactic "ax_tac 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply (tactic {* inst1_tac "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")
@@ -121,7 +122,7 @@
apply (tactic "ax_tac 1") (* Ass *)
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac "P'29" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
+apply (tactic {* inst1_tac "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"]) 1 *})
apply (rule ax_derivs.Abrupt)
@@ -129,17 +130,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 "R14" "\<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 "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'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
apply (simp (no_asm) del: peek_and_def2)
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
+apply (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
apply (simp del: peek_and_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -158,7 +159,7 @@
apply (tactic "ax_tac 1")
defer
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
+apply (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
apply (simp (no_asm) del: split_paired_All peek_and_def2)
apply (tactic "ax_tac 1" (* NewC *))
apply (tactic "ax_tac 1" (* ax_Alloc *))
@@ -186,7 +187,7 @@
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
-apply (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
+apply (tactic {* inst1_tac "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"]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
@@ -197,7 +198,7 @@
apply (tactic "ax_tac 1" (* FVar *))
apply (tactic "ax_tac 2" (* StatRef *))
apply (rule ax_derivs.Done [THEN conseq1])
-apply (tactic {* inst1_tac "Q22" "\<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 "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)
@@ -207,7 +208,7 @@
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp
-apply (tactic {* inst1_tac "P22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
+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 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 clarsimp
@@ -241,7 +242,7 @@
apply clarsimp
apply (tactic "ax_tac 1" (* If *))
apply (tactic
- {* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
+ {* inst1_tac "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")
@@ -262,7 +263,7 @@
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac "P'29" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
+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 (rule allI)
apply (rule_tac P' = "Normal ?P" in conseq1)
prefer 2