src/HOL/Bali/AxExample.thy
 author wenzelm Wed Nov 01 20:46:23 2017 +0100 (23 months ago) changeset 66983 df83b66f1d94 parent 62390 842917225d56 child 67399 eab6ce8368fa permissions -rw-r--r--
proper merge (amending fb46c031c841);
 wenzelm@12857 ` 1` ```(* Title: HOL/Bali/AxExample.thy ``` schirmer@12854 ` 2` ``` Author: David von Oheimb ``` schirmer@12854 ` 3` ```*) ``` schirmer@12925 ` 4` wenzelm@62042 ` 5` ```subsection \Example of a proof based on the Bali axiomatic semantics\ ``` schirmer@12854 ` 6` haftmann@33965 ` 7` ```theory AxExample ``` haftmann@33965 ` 8` ```imports AxSem Example ``` haftmann@33965 ` 9` ```begin ``` schirmer@12854 ` 10` wenzelm@37956 ` 11` ```definition ``` wenzelm@37956 ` 12` ``` arr_inv :: "st \ bool" where ``` wenzelm@37956 ` 13` ``` "arr_inv = (\s. \obj a T el. globs s (Stat Base) = Some obj \ ``` schirmer@12854 ` 14` ``` values obj (Inl (arr, Base)) = Some (Addr a) \ ``` wenzelm@37956 ` 15` ``` heap s a = Some \tag=Arr T 2,values=el\)" ``` schirmer@12854 ` 16` schirmer@12854 ` 17` ```lemma arr_inv_new_obj: ``` schirmer@12854 ` 18` ```"\a. \arr_inv s; new_Addr (heap s)=Some a\ \ arr_inv (gupd(Inl a\x) s)" ``` schirmer@12854 ` 19` ```apply (unfold arr_inv_def) ``` schirmer@12854 ` 20` ```apply (force dest!: new_AddrD2) ``` schirmer@12854 ` 21` ```done ``` schirmer@12854 ` 22` schirmer@12854 ` 23` ```lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s" ``` schirmer@12854 ` 24` ```apply (unfold arr_inv_def) ``` schirmer@12854 ` 25` ```apply (simp (no_asm)) ``` schirmer@12854 ` 26` ```done ``` schirmer@12854 ` 27` schirmer@12854 ` 28` ```lemma arr_inv_gupd_Stat [simp]: ``` schirmer@12854 ` 29` ``` "Base \ C \ arr_inv (gupd(Stat C\obj) s) = arr_inv s" ``` schirmer@12854 ` 30` ```apply (unfold arr_inv_def) ``` schirmer@12854 ` 31` ```apply (simp (no_asm_simp)) ``` schirmer@12854 ` 32` ```done ``` schirmer@12854 ` 33` schirmer@12854 ` 34` ```lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\y) s) = arr_inv s" ``` schirmer@12854 ` 35` ```apply (unfold arr_inv_def) ``` schirmer@12854 ` 36` ```apply (simp (no_asm)) ``` schirmer@12854 ` 37` ```done ``` schirmer@12854 ` 38` schirmer@12854 ` 39` nipkow@62390 ` 40` ```declare if_split_asm [split del] ``` schirmer@12854 ` 41` ```declare lvar_def [simp] ``` schirmer@12854 ` 42` wenzelm@62042 ` 43` ```ML \ ``` wenzelm@55143 ` 44` ```fun inst1_tac ctxt s t xs st = ``` wenzelm@55151 ` 45` ``` (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of ``` wenzelm@59761 ` 46` ``` SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st ``` wenzelm@55151 ` 47` ``` | NONE => Seq.empty); ``` wenzelm@20195 ` 48` wenzelm@59498 ` 49` ```fun ax_tac ctxt = ``` wenzelm@60754 ` 50` ``` REPEAT o resolve_tac ctxt [allI] THEN' ``` wenzelm@59762 ` 51` ``` resolve_tac ctxt ``` wenzelm@59762 ` 52` ``` @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)}; ``` wenzelm@62042 ` 53` ```\ ``` schirmer@12854 ` 54` schirmer@12854 ` 55` schirmer@12854 ` 56` ```theorem ax_test: "tprg,({}::'a triple set)\ ``` schirmer@12854 ` 57` ``` {Normal (\Y s Z::'a. heap_free four s \ \initd Base s \ \ initd Ext s)} ``` schirmer@13688 ` 58` ``` .test [Class Base]. ``` schirmer@13688 ` 59` ``` {\Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}" ``` schirmer@12854 ` 60` ```apply (unfold test_def arr_viewed_from_def) ``` wenzelm@59498 ` 61` ```apply (tactic "ax_tac @{context} 1" (*;;*)) ``` schirmer@13688 ` 62` ```defer (* We begin with the last assertion, to synthesise the intermediate ``` schirmer@13688 ` 63` ``` assertions, like in the fashion of the weakest ``` schirmer@13688 ` 64` ``` precondition. *) ``` wenzelm@59498 ` 65` ```apply (tactic "ax_tac @{context} 1" (* Try *)) ``` schirmer@12854 ` 66` ```defer ``` wenzelm@62042 ` 67` ```apply (tactic \inst1_tac @{context} "Q" ``` wenzelm@62042 ` 68` ``` "\Y s Z. arr_inv (snd s) \ tprg,s\catch SXcpt NullPointer" []\) ``` schirmer@12854 ` 69` ```prefer 2 ``` schirmer@12854 ` 70` ```apply simp ``` schirmer@12854 ` 71` ```apply (rule_tac P' = "Normal (\Y s Z. arr_inv (snd s))" in conseq1) ``` schirmer@12854 ` 72` ```prefer 2 ``` schirmer@12854 ` 73` ```apply clarsimp ``` wenzelm@59807 ` 74` ```apply (rule_tac Q' = "(\Y s Z. Q Y s Z)\=False\=\" and Q = Q for Q in conseq2) ``` schirmer@12854 ` 75` ```prefer 2 ``` schirmer@12854 ` 76` ```apply simp ``` wenzelm@59498 ` 77` ```apply (tactic "ax_tac @{context} 1" (* While *)) ``` schirmer@12854 ` 78` ```prefer 2 ``` schirmer@12854 ` 79` ```apply (rule ax_impossible [THEN conseq1], clarsimp) ``` wenzelm@59807 ` 80` ```apply (rule_tac P' = "Normal P" and P = P for P in conseq1) ``` schirmer@12854 ` 81` ```prefer 2 ``` schirmer@12854 ` 82` ```apply clarsimp ``` wenzelm@59498 ` 83` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 84` ```apply (tactic "ax_tac @{context} 1" (* AVar *)) ``` schirmer@12854 ` 85` ```prefer 2 ``` schirmer@12854 ` 86` ```apply (rule ax_subst_Val_allI) ``` wenzelm@62042 ` 87` ```apply (tactic \inst1_tac @{context} "P'" "\a. Normal (PP a\x)" ["PP", "x"]\) ``` schirmer@12854 ` 88` ```apply (simp del: avar_def2 peek_and_def2) ``` wenzelm@59498 ` 89` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 90` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 91` ``` (* just for clarification: *) ``` schirmer@12854 ` 92` ```apply (rule_tac Q' = "Normal (\Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2) ``` schirmer@12854 ` 93` ```prefer 2 ``` schirmer@12854 ` 94` ```apply (clarsimp simp add: split_beta) ``` wenzelm@59498 ` 95` ```apply (tactic "ax_tac @{context} 1" (* FVar *)) ``` wenzelm@59498 ` 96` ```apply (tactic "ax_tac @{context} 2" (* StatRef *)) ``` schirmer@12854 ` 97` ```apply (rule ax_derivs.Done [THEN conseq1]) ``` schirmer@12854 ` 98` ```apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def) ``` schirmer@12854 ` 99` ```defer ``` schirmer@12854 ` 100` ```apply (rule ax_SXAlloc_catch_SXcpt) ``` schirmer@12854 ` 101` ```apply (rule_tac Q' = "(\Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \ arr_inv s) \. heap_free two" in conseq2) ``` schirmer@12854 ` 102` ```prefer 2 ``` schirmer@12854 ` 103` ```apply (simp add: arr_inv_new_obj) ``` wenzelm@59498 ` 104` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 105` ```apply (rule_tac C = "Ext" in ax_Call_known_DynT) ``` schirmer@12854 ` 106` ```apply (unfold DynT_prop_def) ``` schirmer@12854 ` 107` ```apply (simp (no_asm)) ``` schirmer@12854 ` 108` ```apply (intro strip) ``` wenzelm@59807 ` 109` ```apply (rule_tac P' = "Normal P" and P = P for P in conseq1) ``` wenzelm@59498 ` 110` ```apply (tactic "ax_tac @{context} 1" (* Methd *)) ``` schirmer@12854 ` 111` ```apply (rule ax_thin [OF _ empty_subsetI]) ``` schirmer@12854 ` 112` ```apply (simp (no_asm) add: body_def2) ``` wenzelm@59498 ` 113` ```apply (tactic "ax_tac @{context} 1" (* Body *)) ``` schirmer@12854 ` 114` ```(* apply (rule_tac [2] ax_derivs.Abrupt) *) ``` schirmer@12854 ` 115` ```defer ``` schirmer@12854 ` 116` ```apply (simp (no_asm)) ``` wenzelm@59498 ` 117` ```apply (tactic "ax_tac @{context} 1") (* Comp *) ``` schirmer@13688 ` 118` ``` (* The first statement in the composition ``` schirmer@13688 ` 119` ``` ((Ext)z).vee = 1; Return Null ``` schirmer@13688 ` 120` ``` will throw an exception (since z is null). So we can handle ``` schirmer@13688 ` 121` ``` Return Null with the Abrupt rule *) ``` schirmer@13688 ` 122` ```apply (rule_tac [2] ax_derivs.Abrupt) ``` schirmer@13688 ` 123` ``` ``` schirmer@13688 ` 124` ```apply (rule ax_derivs.Expr) (* Expr *) ``` wenzelm@59498 ` 125` ```apply (tactic "ax_tac @{context} 1") (* Ass *) ``` schirmer@12854 ` 126` ```prefer 2 ``` schirmer@12854 ` 127` ```apply (rule ax_subst_Var_allI) ``` wenzelm@62042 ` 128` ```apply (tactic \inst1_tac @{context} "P'" "\a vs l vf. PP a vs l vf\x \. p" ["PP", "x", "p"]\) ``` schirmer@12854 ` 129` ```apply (rule allI) ``` wenzelm@62042 ` 130` ```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\) ``` schirmer@12854 ` 131` ```apply (rule ax_derivs.Abrupt) ``` schirmer@12854 ` 132` ```apply (simp (no_asm)) ``` wenzelm@59498 ` 133` ```apply (tactic "ax_tac @{context} 1" (* FVar *)) ``` wenzelm@59498 ` 134` ```apply (tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2") ``` wenzelm@59498 ` 135` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@62042 ` 136` ```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)" []\) ``` nipkow@44890 ` 137` ```apply fastforce ``` schirmer@13688 ` 138` ```prefer 4 ``` schirmer@13688 ` 139` ```apply (rule ax_derivs.Done [THEN conseq1],force) ``` schirmer@12854 ` 140` ```apply (rule ax_subst_Val_allI) ``` wenzelm@62042 ` 141` ```apply (tactic \inst1_tac @{context} "P'" "\a. Normal (PP a\x)" ["PP", "x"]\) ``` berghofe@26810 ` 142` ```apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) ``` wenzelm@59498 ` 143` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 144` ```prefer 2 ``` schirmer@12854 ` 145` ```apply (rule ax_subst_Val_allI) ``` wenzelm@62042 ` 146` ```apply (tactic \inst1_tac @{context} "P'" "\aa v. Normal (QQ aa v\y)" ["QQ", "y"]\) ``` berghofe@26810 ` 147` ```apply (simp del: peek_and_def2 heap_free_def2 normal_def2) ``` wenzelm@59498 ` 148` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 149` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 150` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 151` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 152` ```(* end method call *) ``` schirmer@12854 ` 153` ```apply (simp (no_asm)) ``` schirmer@12854 ` 154` ``` (* just for clarification: *) ``` schirmer@12854 ` 155` ```apply (rule_tac Q' = "Normal ((\Y (x, s) Z. arr_inv s \ (\a. the (locals s (VName e)) = Addr a \ obj_class (the (globs s (Inl a))) = Ext \ ``` schirmer@12854 ` 156` ``` invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base) ``` schirmer@12854 ` 157` ``` \name = foo, parTs = [Class Base]\ = Ext)) \. initd Ext \. heap_free two)" ``` schirmer@12854 ` 158` ``` in conseq2) ``` schirmer@12854 ` 159` ```prefer 2 ``` schirmer@12854 ` 160` ```apply clarsimp ``` wenzelm@59498 ` 161` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 162` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 163` ```defer ``` schirmer@12854 ` 164` ```apply (rule ax_subst_Var_allI) ``` wenzelm@62042 ` 165` ```apply (tactic \inst1_tac @{context} "P'" "\vf. Normal (PP vf \. p)" ["PP", "p"]\) ``` berghofe@26810 ` 166` ```apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) ``` wenzelm@59498 ` 167` ```apply (tactic "ax_tac @{context} 1" (* NewC *)) ``` wenzelm@59498 ` 168` ```apply (tactic "ax_tac @{context} 1" (* ax_Alloc *)) ``` schirmer@12854 ` 169` ``` (* just for clarification: *) ``` wenzelm@35067 ` 170` ```apply (rule_tac Q' = "Normal ((\Y s Z. arr_inv (store s) \ vf=lvar (VName e) (store s)) \. heap_free three \. initd Ext)" in conseq2) ``` schirmer@12854 ` 171` ```prefer 2 ``` schirmer@12854 ` 172` ```apply (simp add: invocation_declclass_def dynmethd_def) ``` schirmer@12854 ` 173` ```apply (unfold dynlookup_def) ``` schirmer@12854 ` 174` ```apply (simp add: dynmethd_Ext_foo) ``` schirmer@12854 ` 175` ```apply (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken) ``` schirmer@12854 ` 176` ``` (* begin init *) ``` schirmer@12854 ` 177` ```apply (rule ax_InitS) ``` schirmer@12854 ` 178` ```apply force ``` schirmer@12854 ` 179` ```apply (simp (no_asm)) ``` wenzelm@62042 ` 180` ```apply (tactic \simp_tac (@{context} delloop "split_all_tac") 1\) ``` schirmer@12854 ` 181` ```apply (rule ax_Init_Skip_lemma) ``` wenzelm@62042 ` 182` ```apply (tactic \simp_tac (@{context} delloop "split_all_tac") 1\) ``` schirmer@12854 ` 183` ```apply (rule ax_InitS [THEN conseq1] (* init Base *)) ``` schirmer@12854 ` 184` ```apply force ``` schirmer@12854 ` 185` ```apply (simp (no_asm)) ``` schirmer@12854 ` 186` ```apply (unfold arr_viewed_from_def) ``` schirmer@12854 ` 187` ```apply (rule allI) ``` wenzelm@59807 ` 188` ```apply (rule_tac P' = "Normal P" and P = P for P in conseq1) ``` wenzelm@62042 ` 189` ```apply (tactic \simp_tac (@{context} delloop "split_all_tac") 1\) ``` wenzelm@59498 ` 190` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 191` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 192` ```apply (rule_tac [2] ax_subst_Var_allI) ``` wenzelm@62042 ` 193` ```apply (tactic \inst1_tac @{context} "P'" "\vf l vfa. Normal (P vf l vfa)" ["P"]\) ``` wenzelm@62042 ` 194` ```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\) ``` wenzelm@59498 ` 195` ```apply (tactic "ax_tac @{context} 2" (* NewA *)) ``` wenzelm@59498 ` 196` ```apply (tactic "ax_tac @{context} 3" (* ax_Alloc_Arr *)) ``` wenzelm@59498 ` 197` ```apply (tactic "ax_tac @{context} 3") ``` wenzelm@62042 ` 198` ```apply (tactic \inst1_tac @{context} "P" "\vf l vfa. Normal (P vf l vfa\\)" ["P"]\) ``` wenzelm@62042 ` 199` ```apply (tactic \simp_tac (@{context} delloop "split_all_tac") 2\) ``` wenzelm@59498 ` 200` ```apply (tactic "ax_tac @{context} 2") ``` wenzelm@59498 ` 201` ```apply (tactic "ax_tac @{context} 1" (* FVar *)) ``` wenzelm@59498 ` 202` ```apply (tactic "ax_tac @{context} 2" (* StatRef *)) ``` schirmer@12854 ` 203` ```apply (rule ax_derivs.Done [THEN conseq1]) ``` wenzelm@62042 ` 204` ```apply (tactic \inst1_tac @{context} "Q" "\vf. Normal ((\Y s Z. vf=lvar (VName e) (snd s)) \. heap_free four \. initd Base \. initd Ext)" []\) ``` nipkow@62390 ` 205` ```apply (clarsimp split del: if_split) ``` schirmer@12854 ` 206` ```apply (frule atleast_free_weaken [THEN atleast_free_weaken]) ``` schirmer@12854 ` 207` ```apply (drule initedD) ``` schirmer@12854 ` 208` ```apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) ``` schirmer@12854 ` 209` ```apply force ``` wenzelm@62042 ` 210` ```apply (tactic \simp_tac (@{context} delloop "split_all_tac") 1\) ``` schirmer@12854 ` 211` ```apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) ``` schirmer@12854 ` 212` ```apply (rule wf_tprg) ``` schirmer@12854 ` 213` ```apply clarsimp ``` wenzelm@62042 ` 214` ```apply (tactic \inst1_tac @{context} "P" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. initd Ext)" []\) ``` schirmer@12854 ` 215` ```apply clarsimp ``` wenzelm@62042 ` 216` ```apply (tactic \inst1_tac @{context} "PP" "\vf. Normal ((\Y s Z. vf = lvar (VName e) (snd s)) \. heap_free four \. Not \ initd Base)" []\) ``` schirmer@12854 ` 217` ```apply clarsimp ``` schirmer@12854 ` 218` ``` (* end init *) ``` schirmer@12854 ` 219` ```apply (rule conseq1) ``` wenzelm@59498 ` 220` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 221` ```apply clarsimp ``` schirmer@12854 ` 222` ```done ``` schirmer@12854 ` 223` schirmer@12854 ` 224` ```(* ``` schirmer@12854 ` 225` ```while (true) { ``` schirmer@12854 ` 226` ``` if (i) {throw xcpt;} ``` schirmer@12854 ` 227` ``` else i=j ``` schirmer@12854 ` 228` ```} ``` schirmer@12854 ` 229` ```*) ``` schirmer@12854 ` 230` ```lemma Loop_Xcpt_benchmark: ``` schirmer@12854 ` 231` ``` "Q = (\Y (x,s) Z. x \ None \ the_Bool (the (locals s i))) \ ``` schirmer@12854 ` 232` ``` G,({}::'a triple set)\{Normal (\Y s Z::'a. True)} ``` schirmer@12854 ` 233` ``` .lab1\ While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else ``` schirmer@12854 ` 234` ``` (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}" ``` schirmer@12854 ` 235` ```apply (rule_tac P' = "Q" and Q' = "Q\=False\=\" in conseq12) ``` schirmer@12854 ` 236` ```apply safe ``` wenzelm@59498 ` 237` ```apply (tactic "ax_tac @{context} 1" (* Loop *)) ``` schirmer@12854 ` 238` ```apply (rule ax_Normal_cases) ``` schirmer@12854 ` 239` ```prefer 2 ``` schirmer@12854 ` 240` ```apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) ``` schirmer@12854 ` 241` ```apply (rule conseq1) ``` wenzelm@59498 ` 242` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 243` ```apply clarsimp ``` schirmer@12854 ` 244` ```prefer 2 ``` schirmer@12854 ` 245` ```apply clarsimp ``` wenzelm@59498 ` 246` ```apply (tactic "ax_tac @{context} 1" (* If *)) ``` schirmer@12854 ` 247` ```apply (tactic ``` wenzelm@62042 ` 248` ``` \inst1_tac @{context} "P'" "Normal (\s.. (\Y s Z. True)\=Val (the (locals s i)))" []\) ``` wenzelm@59498 ` 249` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 250` ```apply (rule conseq1) ``` wenzelm@59498 ` 251` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 252` ```apply clarsimp ``` schirmer@12854 ` 253` ```apply (rule allI) ``` schirmer@12854 ` 254` ```apply (rule ax_escape) ``` schirmer@12854 ` 255` ```apply auto ``` schirmer@12854 ` 256` ```apply (rule conseq1) ``` wenzelm@59498 ` 257` ```apply (tactic "ax_tac @{context} 1" (* Throw *)) ``` wenzelm@59498 ` 258` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 259` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 260` ```apply clarsimp ``` schirmer@12854 ` 261` ```apply (rule_tac Q' = "Normal (\Y s Z. True)" in conseq2) ``` schirmer@12854 ` 262` ```prefer 2 ``` schirmer@12854 ` 263` ```apply clarsimp ``` schirmer@12854 ` 264` ```apply (rule conseq1) ``` wenzelm@59498 ` 265` ```apply (tactic "ax_tac @{context} 1") ``` wenzelm@59498 ` 266` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 267` ```prefer 2 ``` schirmer@12854 ` 268` ```apply (rule ax_subst_Var_allI) ``` wenzelm@62042 ` 269` ```apply (tactic \inst1_tac @{context} "P'" "\b Y ba Z vf. \Y (x,s) Z. x=None \ snd vf = snd (lvar i s)" []\) ``` schirmer@12854 ` 270` ```apply (rule allI) ``` wenzelm@59807 ` 271` ```apply (rule_tac P' = "Normal P" and P = P for P in conseq1) ``` schirmer@12854 ` 272` ```prefer 2 ``` schirmer@12854 ` 273` ```apply clarsimp ``` wenzelm@59498 ` 274` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 275` ```apply (rule conseq1) ``` wenzelm@59498 ` 276` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 277` ```apply clarsimp ``` wenzelm@59498 ` 278` ```apply (tactic "ax_tac @{context} 1") ``` schirmer@12854 ` 279` ```apply clarsimp ``` schirmer@12854 ` 280` ```done ``` schirmer@12854 ` 281` schirmer@12854 ` 282` ```end ``` schirmer@12854 ` 283`