|
1 (* Title: isabelle/Bali/AxExample.thy |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 2000 Technische Universitaet Muenchen |
|
5 *) |
|
6 header {* Example of a proof based on the Bali axiomatic semantics *} |
|
7 |
|
8 theory AxExample = AxSem + Example: |
|
9 |
|
10 constdefs |
|
11 arr_inv :: "st \<Rightarrow> bool" |
|
12 "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and> |
|
13 values obj (Inl (arr, Base)) = Some (Addr a) \<and> |
|
14 heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>" |
|
15 |
|
16 lemma arr_inv_new_obj: |
|
17 "\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)" |
|
18 apply (unfold arr_inv_def) |
|
19 apply (force dest!: new_AddrD2) |
|
20 done |
|
21 |
|
22 lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s" |
|
23 apply (unfold arr_inv_def) |
|
24 apply (simp (no_asm)) |
|
25 done |
|
26 |
|
27 lemma arr_inv_gupd_Stat [simp]: |
|
28 "Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s" |
|
29 apply (unfold arr_inv_def) |
|
30 apply (simp (no_asm_simp)) |
|
31 done |
|
32 |
|
33 lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s" |
|
34 apply (unfold arr_inv_def) |
|
35 apply (simp (no_asm)) |
|
36 done |
|
37 |
|
38 |
|
39 declare split_if_asm [split del] |
|
40 declare lvar_def [simp] |
|
41 |
|
42 ML {* |
|
43 fun inst1_tac s t = instantiate_tac [(s,t)]; |
|
44 val ax_tac = REPEAT o rtac allI THEN' |
|
45 resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN":: |
|
46 thm "ax_Alloc"::thm "ax_Alloc_Arr":: |
|
47 thm "ax_SXAlloc_Normal":: |
|
48 funpow 7 tl (thms "ax_derivs.intros")) |
|
49 *} |
|
50 |
|
51 |
|
52 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> |
|
53 {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} |
|
54 .test [Class Base]. {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}" |
|
55 apply (unfold test_def arr_viewed_from_def) |
|
56 apply (tactic "ax_tac 1" (*;;*)) |
|
57 defer |
|
58 apply (tactic "ax_tac 1" (* Try *)) |
|
59 defer |
|
60 apply (tactic {* inst1_tac "Q1" |
|
61 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *}) |
|
62 prefer 2 |
|
63 apply simp |
|
64 apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1) |
|
65 prefer 2 |
|
66 apply clarsimp |
|
67 apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2) |
|
68 prefer 2 |
|
69 apply simp |
|
70 apply (tactic "ax_tac 1" (* While *)) |
|
71 prefer 2 |
|
72 apply (rule ax_impossible [THEN conseq1], clarsimp) |
|
73 apply (rule_tac P' = "Normal ?P" in conseq1) |
|
74 prefer 2 |
|
75 apply clarsimp |
|
76 apply (tactic "ax_tac 1") |
|
77 apply (tactic "ax_tac 1" (* AVar *)) |
|
78 prefer 2 |
|
79 apply (rule ax_subst_Val_allI) |
|
80 apply (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
|
81 apply (simp del: avar_def2 peek_and_def2) |
|
82 apply (tactic "ax_tac 1") |
|
83 apply (tactic "ax_tac 1") |
|
84 (* just for clarification: *) |
|
85 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) |
|
86 prefer 2 |
|
87 apply (clarsimp simp add: split_beta) |
|
88 apply (tactic "ax_tac 1" (* FVar *)) |
|
89 apply (tactic "ax_tac 2" (* StatRef *)) |
|
90 apply (rule ax_derivs.Done [THEN conseq1]) |
|
91 apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def) |
|
92 defer |
|
93 apply (rule ax_SXAlloc_catch_SXcpt) |
|
94 apply (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2) |
|
95 prefer 2 |
|
96 apply (simp add: arr_inv_new_obj) |
|
97 apply (tactic "ax_tac 1") |
|
98 apply (rule_tac C = "Ext" in ax_Call_known_DynT) |
|
99 apply (unfold DynT_prop_def) |
|
100 apply (simp (no_asm)) |
|
101 apply (intro strip) |
|
102 apply (rule_tac P' = "Normal ?P" in conseq1) |
|
103 apply (tactic "ax_tac 1" (* Methd *)) |
|
104 apply (rule ax_thin [OF _ empty_subsetI]) |
|
105 apply (simp (no_asm) add: body_def2) |
|
106 apply (tactic "ax_tac 1" (* Body *)) |
|
107 (* apply (rule_tac [2] ax_derivs.Abrupt) *) |
|
108 defer |
|
109 apply (simp (no_asm)) |
|
110 apply (tactic "ax_tac 1") |
|
111 apply (tactic "ax_tac 1") (* Ass *) |
|
112 prefer 2 |
|
113 apply (rule ax_subst_Var_allI) |
|
114 apply (tactic {* inst1_tac "P'27" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *}) |
|
115 apply (rule allI) |
|
116 apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *}) |
|
117 apply (rule ax_derivs.Abrupt) |
|
118 apply (simp (no_asm)) |
|
119 apply (tactic "ax_tac 1" (* FVar *)) |
|
120 apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") |
|
121 apply (tactic "ax_tac 1") |
|
122 apply clarsimp |
|
123 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> hd vs = Null) \<and>. heap_free two)" *}) |
|
124 prefer 5 |
|
125 apply (rule ax_derivs.Done [THEN conseq1], force) |
|
126 apply force |
|
127 apply (rule ax_subst_Val_allI) |
|
128 apply (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) |
|
129 apply (simp (no_asm) del: peek_and_def2) |
|
130 apply (tactic "ax_tac 1") |
|
131 prefer 2 |
|
132 apply (rule ax_subst_Val_allI) |
|
133 apply (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *}) |
|
134 apply (simp del: peek_and_def2) |
|
135 apply (tactic "ax_tac 1") |
|
136 apply (tactic "ax_tac 1") |
|
137 apply (tactic "ax_tac 1") |
|
138 apply (tactic "ax_tac 1") |
|
139 (* end method call *) |
|
140 apply (simp (no_asm)) |
|
141 (* just for clarification: *) |
|
142 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> |
|
143 invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base) |
|
144 \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)" |
|
145 in conseq2) |
|
146 prefer 2 |
|
147 apply clarsimp |
|
148 apply (tactic "ax_tac 1") |
|
149 apply (tactic "ax_tac 1") |
|
150 defer |
|
151 apply (rule ax_subst_Var_allI) |
|
152 apply (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *}) |
|
153 apply (simp (no_asm) del: split_paired_All peek_and_def2) |
|
154 apply (tactic "ax_tac 1" (* NewC *)) |
|
155 apply (tactic "ax_tac 1" (* ax_Alloc *)) |
|
156 (* just for clarification: *) |
|
157 apply (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2) |
|
158 prefer 2 |
|
159 apply (simp add: invocation_declclass_def dynmethd_def) |
|
160 apply (unfold dynlookup_def) |
|
161 apply (simp add: dynmethd_Ext_foo) |
|
162 apply (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken) |
|
163 (* begin init *) |
|
164 apply (rule ax_InitS) |
|
165 apply force |
|
166 apply (simp (no_asm)) |
|
167 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
|
168 apply (rule ax_Init_Skip_lemma) |
|
169 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
|
170 apply (rule ax_InitS [THEN conseq1] (* init Base *)) |
|
171 apply force |
|
172 apply (simp (no_asm)) |
|
173 apply (unfold arr_viewed_from_def) |
|
174 apply (rule allI) |
|
175 apply (rule_tac P' = "Normal ?P" in conseq1) |
|
176 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
|
177 apply (tactic "ax_tac 1") |
|
178 apply (tactic "ax_tac 1") |
|
179 apply (rule_tac [2] ax_subst_Var_allI) |
|
180 apply (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *}) |
|
181 apply (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *}) |
|
182 apply (tactic "ax_tac 2" (* NewA *)) |
|
183 apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) |
|
184 apply (tactic "ax_tac 3") |
|
185 apply (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *}) |
|
186 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *}) |
|
187 apply (tactic "ax_tac 2") |
|
188 apply (tactic "ax_tac 1" (* FVar *)) |
|
189 apply (tactic "ax_tac 2" (* StatRef *)) |
|
190 apply (rule ax_derivs.Done [THEN conseq1]) |
|
191 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)" *}) |
|
192 apply (clarsimp split del: split_if) |
|
193 apply (frule atleast_free_weaken [THEN atleast_free_weaken]) |
|
194 apply (drule initedD) |
|
195 apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) |
|
196 apply force |
|
197 apply (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *}) |
|
198 apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) |
|
199 apply (rule wf_tprg) |
|
200 apply clarsimp |
|
201 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)" *}) |
|
202 apply clarsimp |
|
203 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)" *}) |
|
204 apply clarsimp |
|
205 (* end init *) |
|
206 apply (rule conseq1) |
|
207 apply (tactic "ax_tac 1") |
|
208 apply clarsimp |
|
209 done |
|
210 |
|
211 (* |
|
212 while (true) { |
|
213 if (i) {throw xcpt;} |
|
214 else i=j |
|
215 } |
|
216 *) |
|
217 lemma Loop_Xcpt_benchmark: |
|
218 "Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow> |
|
219 G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)} |
|
220 .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else |
|
221 (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}" |
|
222 apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12) |
|
223 apply safe |
|
224 apply (tactic "ax_tac 1" (* Loop *)) |
|
225 apply (rule ax_Normal_cases) |
|
226 prefer 2 |
|
227 apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) |
|
228 apply (rule conseq1) |
|
229 apply (tactic "ax_tac 1") |
|
230 apply clarsimp |
|
231 prefer 2 |
|
232 apply clarsimp |
|
233 apply (tactic "ax_tac 1" (* If *)) |
|
234 apply (tactic |
|
235 {* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *}) |
|
236 apply (tactic "ax_tac 1") |
|
237 apply (rule conseq1) |
|
238 apply (tactic "ax_tac 1") |
|
239 apply clarsimp |
|
240 apply (rule allI) |
|
241 apply (rule ax_escape) |
|
242 apply auto |
|
243 apply (rule conseq1) |
|
244 apply (tactic "ax_tac 1" (* Throw *)) |
|
245 apply (tactic "ax_tac 1") |
|
246 apply (tactic "ax_tac 1") |
|
247 apply clarsimp |
|
248 apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2) |
|
249 prefer 2 |
|
250 apply clarsimp |
|
251 apply (rule conseq1) |
|
252 apply (tactic "ax_tac 1") |
|
253 apply (tactic "ax_tac 1") |
|
254 prefer 2 |
|
255 apply (rule ax_subst_Var_allI) |
|
256 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)" *}) |
|
257 apply (rule allI) |
|
258 apply (rule_tac P' = "Normal ?P" in conseq1) |
|
259 prefer 2 |
|
260 apply clarsimp |
|
261 apply (tactic "ax_tac 1") |
|
262 apply (rule conseq1) |
|
263 apply (tactic "ax_tac 1") |
|
264 apply clarsimp |
|
265 apply (tactic "ax_tac 1") |
|
266 apply clarsimp |
|
267 done |
|
268 |
|
269 end |
|
270 |