12854
|
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 |
|