--- a/src/HOL/Bali/AxExample.thy Sat Jan 25 21:52:04 2014 +0100
+++ b/src/HOL/Bali/AxExample.thy Sat Jan 25 22:06:07 2014 +0100
@@ -41,9 +41,9 @@
declare lvar_def [simp]
ML {*
-fun inst1_tac ctxt s t st =
+fun inst1_tac ctxt s t xs st =
case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
- SOME i => instantiate_tac ctxt [((s, i), t)] st | NONE => Seq.empty;
+ SOME i => instantiate_tac ctxt [((s, i), t)] xs st | NONE => Seq.empty;
val ax_tac =
REPEAT o rtac allI THEN'
@@ -64,7 +64,7 @@
apply (tactic "ax_tac 1" (* Try *))
defer
apply (tactic {* inst1_tac @{context} "Q"
- "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
+ "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *})
prefer 2
apply simp
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
@@ -83,7 +83,7 @@
apply (tactic "ax_tac 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply (simp del: avar_def2 peek_and_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -124,7 +124,7 @@
apply (tactic "ax_tac 1") (* Ass *)
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "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" ["PP", "x", "p"] *})
apply (rule allI)
apply (tactic {* simp_tac (@{context} 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)
@@ -132,17 +132,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 @{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 (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 fastforce
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (?PP a\<leftarrow>?x)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
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 @{context} "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)" ["QQ", "y"] *})
apply (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -161,7 +161,7 @@
apply (tactic "ax_tac 1")
defer
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (?PP vf \<and>. ?p)" *})
+apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *})
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 *))
@@ -189,18 +189,18 @@
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "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)" ["P"] *})
apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm 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 @{context} "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>)" ["P"] *})
apply (tactic {* simp_tac (@{context} 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 @{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 (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)
@@ -210,9 +210,9 @@
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp
-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 (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 @{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 (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)
@@ -244,7 +244,7 @@
apply clarsimp
apply (tactic "ax_tac 1" (* If *))
apply (tactic
- {* inst1_tac @{context} "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")
@@ -265,7 +265,7 @@
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Var_allI)
-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 (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