# 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" "\Y s Z. arr_inv (snd s) \ tprg,s\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'" "\u a. Normal (?PP a\?x) u" *}) +apply (tactic {* inst1_tac @{context} "P'" "\u a. Normal (?PP a\?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'" "\a vs l vf. ?PP a vs l vf\?x \. ?p" *}) +apply (tactic {* inst1_tac @{context} "P'" "\a vs l vf. ?PP a vs l vf\?x \. ?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" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. heap_free two)" *}) +apply (tactic {* inst1_tac @{context} "R" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. 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'" "\u a. Normal (?PP a\?x) u" *}) +apply (tactic {* inst1_tac @{context} "P'" "\u a. Normal (?PP a\?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'" "\aa v. Normal (?QQ aa v\?y)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\aa v. Normal (?QQ aa v\?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'" "\u vf. Normal (?PP vf \. ?p) u" *}) +apply (tactic {* inst1_tac @{context} "P'" "\u vf. Normal (?PP vf \. ?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'" "\vf l vfa. Normal (?P vf l vfa)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\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" "\vf l vfa. Normal (?P vf l vfa\\)" *}) +apply (tactic {* inst1_tac @{context} "P" "\vf l vfa. Normal (?P vf l vfa\\)" *}) 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" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" *}) +apply (tactic {* inst1_tac @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. 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" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" *}) +apply (tactic {* inst1_tac @{context} "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" *}) apply clarsimp -apply (tactic {* inst1_tac "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ initd Base)" *}) +apply (tactic {* inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ 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 (\s.. (\Y s Z. True)\=Val (the (locals s i)))" *}) + {* inst1_tac @{context} "P'" "Normal (\s.. (\Y s Z. True)\=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'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" *}) +apply (tactic {* inst1_tac @{context} "P'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" *}) apply (rule allI) apply (rule_tac P' = "Normal ?P" in conseq1) prefer 2