author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44890  22f665a2e91c 
child 48262  a0d8abca8d7a 
permissions  rwrr 
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)" *}) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
37956
diff
changeset

136 
apply fastforce 
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

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 