author  wenzelm 
Mon, 16 Jun 2008 22:13:46 +0200  
changeset 27240  1caa6726168a 
parent 26810  255a347eae43 
child 29258  bce03c644efb 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/AxExample.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

4 
*) 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

5 

12854  6 
header {* Example of a proof based on the Bali axiomatic semantics *} 
7 

16417  8 
theory AxExample imports AxSem Example begin 
12854  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 

16121  42 
ML {* 
27240  43 
fun inst1_tac ctxt s t st = 
44 
case AList.lookup (op =) (rev (Term.add_varnames (Thm.prop_of st) [])) s of 

45 
SOME i => instantiate_tac ctxt [((s, i), t)] st  NONE => Seq.empty; 

20195  46 

47 
val ax_tac = 

48 
REPEAT o rtac allI THEN' 

27240  49 
resolve_tac (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: 
50 
@{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8)}); 

12854  51 
*} 
52 

53 

54 
theorem ax_test: "tprg,({}::'a triple set)\<turnstile> 

55 
{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

56 
.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

57 
{\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}" 
12854  58 
apply (unfold test_def arr_viewed_from_def) 
59 
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

60 
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

61 
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

62 
precondition. *) 
12854  63 
apply (tactic "ax_tac 1" (* Try *)) 
64 
defer 

27240  65 
apply (tactic {* inst1_tac @{context} "Q" 
12854  66 
"\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *}) 
67 
prefer 2 

68 
apply simp 

69 
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1) 

70 
prefer 2 

71 
apply clarsimp 

72 
apply (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2) 

73 
prefer 2 

74 
apply simp 

75 
apply (tactic "ax_tac 1" (* While *)) 

76 
prefer 2 

77 
apply (rule ax_impossible [THEN conseq1], clarsimp) 

78 
apply (rule_tac P' = "Normal ?P" in conseq1) 

79 
prefer 2 

80 
apply clarsimp 

81 
apply (tactic "ax_tac 1") 

82 
apply (tactic "ax_tac 1" (* AVar *)) 

83 
prefer 2 

84 
apply (rule ax_subst_Val_allI) 

27240  85 
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *}) 
12854  86 
apply (simp del: avar_def2 peek_and_def2) 
87 
apply (tactic "ax_tac 1") 

88 
apply (tactic "ax_tac 1") 

89 
(* just for clarification: *) 

90 
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) 

91 
prefer 2 

92 
apply (clarsimp simp add: split_beta) 

93 
apply (tactic "ax_tac 1" (* FVar *)) 

94 
apply (tactic "ax_tac 2" (* StatRef *)) 

95 
apply (rule ax_derivs.Done [THEN conseq1]) 

96 
apply (clarsimp simp add: arr_inv_def inited_def in_bounds_def) 

97 
defer 

98 
apply (rule ax_SXAlloc_catch_SXcpt) 

99 
apply (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2) 

100 
prefer 2 

101 
apply (simp add: arr_inv_new_obj) 

102 
apply (tactic "ax_tac 1") 

103 
apply (rule_tac C = "Ext" in ax_Call_known_DynT) 

104 
apply (unfold DynT_prop_def) 

105 
apply (simp (no_asm)) 

106 
apply (intro strip) 

107 
apply (rule_tac P' = "Normal ?P" in conseq1) 

108 
apply (tactic "ax_tac 1" (* Methd *)) 

109 
apply (rule ax_thin [OF _ empty_subsetI]) 

110 
apply (simp (no_asm) add: body_def2) 

111 
apply (tactic "ax_tac 1" (* Body *)) 

112 
(* apply (rule_tac [2] ax_derivs.Abrupt) *) 

113 
defer 

114 
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

115 
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

116 
(* 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

117 
((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

118 
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

119 
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

120 
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

121 

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 
apply (rule ax_derivs.Expr) (* Expr *) 
12854  123 
apply (tactic "ax_tac 1") (* Ass *) 
124 
prefer 2 

125 
apply (rule ax_subst_Var_allI) 

27240  126 
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *}) 
12854  127 
apply (rule allI) 
26810
255a347eae43
Locally deleted some definitions that were applied too eagerly because
berghofe
parents:
26342
diff
changeset

128 
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  129 
apply (rule ax_derivs.Abrupt) 
130 
apply (simp (no_asm)) 

131 
apply (tactic "ax_tac 1" (* FVar *)) 

132 
apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") 

133 
apply (tactic "ax_tac 1") 

27240  134 
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

135 
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

136 
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

137 
apply (rule ax_derivs.Done [THEN conseq1],force) 
12854  138 
apply (rule ax_subst_Val_allI) 
27240  139 
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

140 
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply) 
12854  141 
apply (tactic "ax_tac 1") 
142 
prefer 2 

143 
apply (rule ax_subst_Val_allI) 

27240  144 
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

145 
apply (simp del: peek_and_def2 heap_free_def2 normal_def2) 
12854  146 
apply (tactic "ax_tac 1") 
147 
apply (tactic "ax_tac 1") 

148 
apply (tactic "ax_tac 1") 

149 
apply (tactic "ax_tac 1") 

150 
(* end method call *) 

151 
apply (simp (no_asm)) 

152 
(* just for clarification: *) 

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

154 
invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base) 

155 
\<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)" 

156 
in conseq2) 

157 
prefer 2 

158 
apply clarsimp 

159 
apply (tactic "ax_tac 1") 

160 
apply (tactic "ax_tac 1") 

161 
defer 

162 
apply (rule ax_subst_Var_allI) 

27240  163 
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

164 
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2) 
12854  165 
apply (tactic "ax_tac 1" (* NewC *)) 
166 
apply (tactic "ax_tac 1" (* ax_Alloc *)) 

167 
(* just for clarification: *) 

168 
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) 

169 
prefer 2 

170 
apply (simp add: invocation_declclass_def dynmethd_def) 

171 
apply (unfold dynlookup_def) 

172 
apply (simp add: dynmethd_Ext_foo) 

173 
apply (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken) 

174 
(* begin init *) 

175 
apply (rule ax_InitS) 

176 
apply force 

177 
apply (simp (no_asm)) 

26342  178 
apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *}) 
12854  179 
apply (rule ax_Init_Skip_lemma) 
26342  180 
apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *}) 
12854  181 
apply (rule ax_InitS [THEN conseq1] (* init Base *)) 
182 
apply force 

183 
apply (simp (no_asm)) 

184 
apply (unfold arr_viewed_from_def) 

185 
apply (rule allI) 

186 
apply (rule_tac P' = "Normal ?P" in conseq1) 

26342  187 
apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *}) 
12854  188 
apply (tactic "ax_tac 1") 
189 
apply (tactic "ax_tac 1") 

190 
apply (rule_tac [2] ax_subst_Var_allI) 

27240  191 
apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *}) 
26810
255a347eae43
Locally deleted some definitions that were applied too eagerly because
berghofe
parents:
26342
diff
changeset

192 
apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *}) 
12854  193 
apply (tactic "ax_tac 2" (* NewA *)) 
194 
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *)) 

195 
apply (tactic "ax_tac 3") 

27240  196 
apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *}) 
26342  197 
apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *}) 
12854  198 
apply (tactic "ax_tac 2") 
199 
apply (tactic "ax_tac 1" (* FVar *)) 

200 
apply (tactic "ax_tac 2" (* StatRef *)) 

201 
apply (rule ax_derivs.Done [THEN conseq1]) 

27240  202 
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  203 
apply (clarsimp split del: split_if) 
204 
apply (frule atleast_free_weaken [THEN atleast_free_weaken]) 

205 
apply (drule initedD) 

206 
apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def) 

207 
apply force 

26342  208 
apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *}) 
12854  209 
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) 
210 
apply (rule wf_tprg) 

211 
apply clarsimp 

27240  212 
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  213 
apply clarsimp 
27240  214 
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  215 
apply clarsimp 
216 
(* end init *) 

217 
apply (rule conseq1) 

218 
apply (tactic "ax_tac 1") 

219 
apply clarsimp 

220 
done 

221 

222 
(* 

223 
while (true) { 

224 
if (i) {throw xcpt;} 

225 
else i=j 

226 
} 

227 
*) 

228 
lemma Loop_Xcpt_benchmark: 

229 
"Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow> 

230 
G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)} 

231 
.lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else 

232 
(Expr (Ass (LVar i) (Acc (LVar j))))). {Q}" 

233 
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12) 

234 
apply safe 

235 
apply (tactic "ax_tac 1" (* Loop *)) 

236 
apply (rule ax_Normal_cases) 

237 
prefer 2 

238 
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) 

239 
apply (rule conseq1) 

240 
apply (tactic "ax_tac 1") 

241 
apply clarsimp 

242 
prefer 2 

243 
apply clarsimp 

244 
apply (tactic "ax_tac 1" (* If *)) 

245 
apply (tactic 

27240  246 
{* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *}) 
12854  247 
apply (tactic "ax_tac 1") 
248 
apply (rule conseq1) 

249 
apply (tactic "ax_tac 1") 

250 
apply clarsimp 

251 
apply (rule allI) 

252 
apply (rule ax_escape) 

253 
apply auto 

254 
apply (rule conseq1) 

255 
apply (tactic "ax_tac 1" (* Throw *)) 

256 
apply (tactic "ax_tac 1") 

257 
apply (tactic "ax_tac 1") 

258 
apply clarsimp 

259 
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2) 

260 
prefer 2 

261 
apply clarsimp 

262 
apply (rule conseq1) 

263 
apply (tactic "ax_tac 1") 

264 
apply (tactic "ax_tac 1") 

265 
prefer 2 

266 
apply (rule ax_subst_Var_allI) 

27240  267 
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  268 
apply (rule allI) 
269 
apply (rule_tac P' = "Normal ?P" in conseq1) 

270 
prefer 2 

271 
apply clarsimp 

272 
apply (tactic "ax_tac 1") 

273 
apply (rule conseq1) 

274 
apply (tactic "ax_tac 1") 

275 
apply clarsimp 

276 
apply (tactic "ax_tac 1") 

277 
apply clarsimp 

278 
done 

279 

280 
end 

281 