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