author  berghofe 
Mon, 30 Sep 2002 16:14:02 +0200  
changeset 13601  fd3e3d6b37b2 
parent 13524  604d0f3622d6 
child 13688  a0b16d42d489 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/AxCompl.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12859  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 

7 
header {* 

8 
Completeness proof for Axiomatic semantics of Java expressions and statements 

9 
*} 

10 

11 
theory AxCompl = AxSem: 

12 

13 
text {* 

14 
design issues: 

15 
\begin{itemize} 

16 
\item proof structured by Most General Formulas (> Thomas Kleymann) 

17 
\end{itemize} 

18 
*} 

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

19 

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

20 

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

21 

12854  22 
section "set of not yet initialzed classes" 
23 

24 
constdefs 

25 

26 
nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" 

27 
"nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}" 

28 

29 
lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}" 

30 
apply (unfold nyinitcls_def) 

31 
apply fast 

32 
done 

33 

34 
lemmas finite_nyinitcls [simp] = 

35 
finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard] 

36 

37 
lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}" 

38 
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]]) 

39 
done 

40 

41 
lemma nyinitcls_set_locals_cong [simp]: 

42 
"nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)" 

43 
apply (unfold nyinitcls_def) 

44 
apply (simp (no_asm)) 

45 
done 

46 

47 
lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)" 

48 
apply (unfold nyinitcls_def) 

49 
apply (simp (no_asm)) 

50 
done 

51 

52 
lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s" 

53 
apply (unfold nyinitcls_def) 

54 
apply (simp (no_asm_simp) only: split_tupled_all) 

55 
apply (simp (no_asm)) 

56 
done 

57 

58 
lemma card_nyinitcls_abrupt_congE [elim!]: 

59 
"card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n" 

60 
apply (unfold nyinitcls_def) 

61 
apply auto 

62 
done 

63 

64 
lemma nyinitcls_new_xcpt_var [simp]: 

65 
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s" 

66 
apply (unfold nyinitcls_def) 

67 
apply (induct_tac "s") 

68 
apply (simp (no_asm)) 

69 
done 

70 

71 
lemma nyinitcls_init_lvars [simp]: 

72 
"nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s" 

73 
apply (induct_tac "s") 

74 
apply (simp (no_asm) add: init_lvars_def2 split add: split_if) 

75 
done 

76 

77 
lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s" 

78 
apply (unfold nyinitcls_def) 

79 
apply fast 

80 
done 

81 

82 
lemma card_Suc_lemma: "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n" 

83 
apply (rotate_tac 1) 

84 
apply clarsimp 

85 
done 

86 

87 
lemma nyinitcls_le_SucD: 

88 
"\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 

89 
card (nyinitcls G (x,init_class_obj G C s)) \<le> n" 

90 
apply (subgoal_tac 

91 
"nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))") 

92 
apply clarsimp 

13601  93 
apply (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl) 
12854  94 
apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls]) 
95 
apply (auto dest!: not_initedD elim!: 

96 
simp add: nyinitcls_def inited_def split add: split_if_asm) 

97 
done 

98 

99 
ML {* bind_thm("inited_gext'",permute_prems 0 1 (thm "inited_gext")) *} 

100 

101 
lemma nyinitcls_gext: "snd s\<le>snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s" 

102 
apply (unfold nyinitcls_def) 

103 
apply (force dest!: inited_gext') 

104 
done 

105 

106 
lemma card_nyinitcls_gext: 

107 
"\<lbrakk>snd s\<le>snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n" 

108 
apply (rule le_trans) 

109 
apply (rule card_mono) 

110 
apply (rule finite_nyinitcls) 

111 
apply (erule nyinitcls_gext) 

112 
apply assumption 

113 
done 

114 

115 

116 
section "initle" 

117 

118 
constdefs 

119 
init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_" [51,51] 50) 

120 
"G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n" 

121 

122 
lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)" 

123 
apply (unfold init_le_def) 

124 
apply auto 

125 
done 

126 

127 
lemma All_init_leD: "\<forall>n::nat. G,A\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}" 

128 
apply (drule spec) 

129 
apply (erule conseq1) 

130 
apply clarsimp 

131 
apply (rule card_nyinitcls_bound) 

132 
done 

133 

134 
section "Most General Triples and Formulas" 

135 

136 
constdefs 

137 

138 
remember_init_state :: "state assn" ("\<doteq>") 

139 
"\<doteq> \<equiv> \<lambda>Y s Z. s = Z" 

140 

141 
lemma remember_init_state_def2 [simp]: "\<doteq> Y = op =" 

142 
apply (unfold remember_init_state_def) 

143 
apply (simp (no_asm)) 

144 
done 

145 

146 
consts 

147 

148 
MGF ::"[state assn, term, prog] \<Rightarrow> state triple" ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62) 

149 
MGFn::"[nat , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62) 

150 

151 
defs 

152 

153 

154 
MGF_def: 

155 
"{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}" 

156 

157 
MGFn_def: 

158 
"{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}" 

159 

160 
(* unused *) 

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

161 

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

162 
lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" 
12854  163 
apply (unfold MGF_def) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

164 
apply (simp add: ax_valids_def triple_valid_def2) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

165 
apply (auto elim: evaln_eval) 
12854  166 
done 
167 

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

168 

12854  169 
lemma MGF_res_eq_lemma [simp]: 
170 
"(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)" 

171 
apply auto 

172 
done 

173 

174 
lemma MGFn_def2: 

175 
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 

176 
t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}" 

177 
apply (unfold MGFn_def MGF_def) 

178 
apply fast 

179 
done 

180 

181 
lemma MGF_MGFn_iff: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})" 

182 
apply (simp (no_asm_use) add: MGFn_def2 MGF_def) 

183 
apply safe 

184 
apply (erule_tac [2] All_init_leD) 

185 
apply (erule conseq1) 

186 
apply clarsimp 

187 
done 

188 

189 
lemma MGFnD: 

190 
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow> 

191 
G,A\<turnstile>{(\<lambda>Y' s' s. s' = s \<and> P s) \<and>. G\<turnstile>init\<le>n} 

192 
t\<succ> {(\<lambda>Y' s' s. G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(Y',s') \<and> P s) \<and>. G\<turnstile>init\<le>n}" 

193 
apply (unfold init_le_def) 

194 
apply (simp (no_asm_use) add: MGFn_def2) 

195 
apply (erule conseq12) 

196 
apply clarsimp 

197 
apply (erule (1) eval_gext [THEN card_nyinitcls_gext]) 

198 
done 

199 
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 

200 

201 
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> 

202 
G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}" 

203 
apply (unfold MGF_def) 

204 
apply (rule ax_Normal_cases) 

205 
apply (erule conseq1) 

206 
apply clarsimp 

207 
apply (rule ax_derivs.Abrupt [THEN conseq1]) 

208 
apply (clarsimp simp add: Let_def) 

209 
done 

210 

211 
lemma MGFNormalD: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}" 

212 
apply (unfold MGF_def) 

213 
apply (erule conseq1) 

214 
apply clarsimp 

215 
done 

216 

217 
lemma MGFn_NormalI: 

218 
"G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ> 

219 
{\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}" 

220 
apply (simp (no_asm_use) add: MGFn_def2) 

221 
apply (rule ax_Normal_cases) 

222 
apply (erule conseq1) 

223 
apply clarsimp 

224 
apply (rule ax_derivs.Abrupt [THEN conseq1]) 

225 
apply (clarsimp simp add: Let_def) 

226 
done 

227 

228 
lemma MGFn_free_wt: 

229 
"(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 

230 
\<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 

231 
\<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}" 

232 
apply (rule MGFn_NormalI) 

233 
apply (rule ax_free_wt) 

234 
apply (auto elim: conseq12 simp add: MGFn_def MGF_def) 

235 
done 

236 

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

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

238 
"(\<forall> T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

239 
\<longrightarrow> G,(A::state triple set) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

240 
\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n) \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))} 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

241 
t\<succ> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

242 
{\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

243 
\<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

244 
apply (rule MGFn_NormalI) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

245 
apply (rule ax_no_hazard) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

246 
apply (rule ax_escape) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

247 
apply (intro strip) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

248 
apply (simp only: type_ok_def peek_and_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

249 
apply (erule conjE)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

250 
apply (erule exE,erule exE, erule exE,erule conjE,drule (1) mp) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

251 
apply (drule spec,drule spec, drule spec, drule (1) mp) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

252 
apply (erule conseq12) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

255 

12854  256 

257 
section "main lemmas" 

258 

259 
declare fun_upd_apply [simp del] 

260 
declare splitI2 [rule del] (*prevents ugly renaming of state variables*) 

261 

262 
ML_setup {* 

263 
Delsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc] 

264 
*} (*prevents modifying rhs of MGF*) 

265 
ML {* 

266 
val eval_css = (claset() delrules [thm "eval.Abrupt"] addSIs (thms "eval.intros") 

267 
delrules[thm "eval.Expr", thm "eval.Init", thm "eval.Try"] 

268 
addIs [thm "eval.Expr", thm "eval.Init"] 

269 
addSEs[thm "eval.Try"] delrules[equalityCE], 

270 
simpset() addsimps [split_paired_all,Let_def] 

271 
addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]); 

272 
val eval_Force_tac = force_tac eval_css; 

273 

274 
val wt_prepare_tac = EVERY'[ 

275 
rtac (thm "MGFn_free_wt"), 

276 
clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())] 

277 
val compl_prepare_tac = EVERY'[rtac (thm "MGFn_NormalI"), Simp_tac] 

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

278 
val wt_conf_prepare_tac = EVERY'[ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

279 
rtac (thm "MGFn_free_wt_NormalConformI"), 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

280 
clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())] 
12854  281 
val forw_hyp_tac = EVERY'[etac (thm "MGFnD'" RS thm "conseq12"), Clarsimp_tac] 
282 
val forw_hyp_eval_Force_tac = 

283 
EVERY'[TRY o rtac allI, forw_hyp_tac, eval_Force_tac] 

284 
*} 

285 

286 
lemma MGFn_Init: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}) \<Longrightarrow> 

287 
G,(A::state triple set)\<turnstile>{=:n} In1r (Init C)\<succ> {G\<rightarrow>}" 

288 
apply (tactic "wt_prepare_tac 1") 

289 
(* requires is_class G C two times for nyinitcls *) 

290 
apply (tactic "compl_prepare_tac 1") 

291 
apply (rule_tac C = "initd C" in ax_cases) 

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

293 
apply (clarsimp intro!: init_done) 

294 
apply (rule_tac y = n in nat.exhaust, clarsimp) 

295 
apply (rule ax_impossible [THEN conseq1]) 

296 
apply (force dest!: nyinitcls_emptyD) 

297 
apply clarsimp 

298 
apply (drule_tac x = "nat" in spec) 

299 
apply clarsimp 

300 
apply (rule_tac Q = " (\<lambda>Y s' (x,s) . G\<turnstile> (x,init_class_obj G C s) \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s' \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>nat" in ax_derivs.Init) 

301 
apply simp 

302 
apply (rule_tac P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>nat) " in conseq1) 

303 
prefer 2 

304 
apply (force elim!: nyinitcls_le_SucD) 

305 
apply (simp split add: split_if, rule conjI, clarify) 

306 
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1") 

307 
apply clarify 

308 
apply (drule spec) 

309 
apply (erule MGFnD' [THEN conseq12]) 

310 
apply (tactic "force_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1") 

311 
apply (rule allI) 

312 
apply (drule spec) 

313 
apply (erule MGFnD' [THEN conseq12]) 

314 
apply clarsimp 

315 
apply (tactic {* pair_tac "sa" 1 *}) 

316 
apply (tactic"clarsimp_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1") 

317 
apply (rule eval_Init, force+) 

318 
done 

319 
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD] 

320 

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

321 
text {* For @{text MGFn_Call} we need the wellformedness of the program to 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

322 
switch from the evalnsemantics to the evalsemantics *} 
12854  323 
lemma MGFn_Call: 
324 
"\<lbrakk>\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>}; 

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

325 
G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In3 ps\<succ> {G\<rightarrow>};wf_prog G\<rbrakk> \<Longrightarrow> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

326 
G,A\<turnstile>{=:n} In1l ({accC,statT,mode}e\<cdot>mn({pTs'}ps))\<succ> {G\<rightarrow>}" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

327 
apply (tactic "wt_conf_prepare_tac 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

329 
Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

330 
(\<exists>a. G\<turnstile>Norm s \<midarrow>e\<succ>a\<rightarrow> s1 \<and> (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

331 
\<and> Y = In1 a)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

332 
\<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" and 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

333 
R = "\<lambda>a'. (\<lambda>Y (x2,s2) (x,s) . x = None \<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

334 
(\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e\<succ>a'\<rightarrow> s1 \<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

335 
(normal s1 \<longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT)\<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

336 
Y = In3 pvs \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

337 
\<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" in ax_derivs.Call) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

338 
apply (tactic "forw_hyp_tac 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

339 
apply (tactic "clarsimp_tac eval_css 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

340 
apply (frule (3) eval_type_sound) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

342 

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

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

344 
apply (tactic "forw_hyp_tac 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

345 
apply (tactic "clarsimp_tac eval_css 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

346 
apply (frule (3) eval_type_sound) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

347 
apply (rule conjI) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

348 
apply (rule exI,rule conjI) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

350 

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

351 
apply (rule conjI) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

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

355 

12854  356 
apply (drule spec, drule spec) 
357 
apply (erule MGFnD' [THEN conseq12]) 

358 
apply (tactic "clarsimp_tac eval_css 1") 

359 
apply (erule (1) eval_Call) 

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

360 
apply (rule HOL.refl)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

361 
apply (subgoal_tac "check_method_access G C statT (invmode m e) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

362 
\<lparr>name = mn, parTs = pTs'\<rparr> a 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

364 
(invocation_declclass G (invmode m e) (snd (ab, ba)) a statT 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

365 
\<lparr>name = mn, parTs = pTs'\<rparr>) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

366 
\<lparr>name = mn, parTs = pTs'\<rparr> (invmode m e) a vs 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

368 
ba)) = (init_lvars G 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

369 
(invocation_declclass G (invmode m e) (snd (ab, ba)) a statT 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

370 
\<lparr>name = mn, parTs = pTs'\<rparr>) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

371 
\<lparr>name = mn, parTs = pTs'\<rparr> (invmode m e) a vs 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

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

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

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

377 
apply (erule (3) error_free_call_access) (* now showing the subgoal *) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

378 
apply auto 
12854  379 
done 
380 

381 
lemma MGF_altern: "G,A\<turnstile>{Normal (\<doteq> \<and>. p)} t\<succ> {G\<rightarrow>} = 

382 
G,A\<turnstile>{Normal ((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) \<and>. p)} 

383 
t\<succ> {\<lambda>Y s Z. (Y,s) = Z}" 

384 
apply (unfold MGF_def) 

385 
apply (auto del: conjI elim!: conseq12) 

386 
apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ") 

387 
apply (fast dest: unique_eval) 

388 
apply clarsimp 

389 
apply (drule split_paired_All [THEN subst]) 

390 
apply (clarsimp elim!: state_not_single) 

391 
done 

392 

393 

394 
lemma MGFn_Loop: 

395 
"\<lbrakk>G,(A::state triple set)\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>};G,A\<turnstile>{=:n} In1r stmnt\<succ> {G\<rightarrow>} \<rbrakk> 

396 
\<Longrightarrow> 

397 
G,A\<turnstile>{=:n} In1r (l\<bullet> While(expr) stmnt)\<succ> {G\<rightarrow>}" 

398 
apply (rule MGFn_NormalI, simp) 

399 
apply (rule_tac p2 = "\<lambda>s. card (nyinitcls G s) \<le> n" in 

400 
MGF_altern [unfolded MGF_def, THEN iffD2, THEN conseq1]) 

401 
prefer 2 

402 
apply clarsimp 

403 
apply (rule_tac P' = 

404 
"((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>In1r (l\<bullet> While(expr) stmnt) \<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) 

405 
\<and>. (\<lambda>s. card (nyinitcls G s) \<le> n))" in conseq12) 

406 
prefer 2 

407 
apply clarsimp 

408 
apply (tactic "smp_tac 1 1", erule_tac V = "All ?P" in thin_rl) 

409 
apply (rule_tac [2] P' = " (\<lambda>b s (Y',s') . (\<exists>s0. G\<turnstile>s0 \<midarrow>In1l expr\<succ>\<rightarrow> (b,s)) \<and> (if normal s \<and> the_Bool (the_In1 b) then (\<forall>s'' w s0. G\<turnstile>s \<midarrow>stmnt\<rightarrow> s'' \<and> G\<turnstile>(abupd (absorb (Cont l)) s'') \<midarrow>In1r (l\<bullet> While(expr) stmnt) \<succ>\<rightarrow> (w,s0) \<longrightarrow> (w,s0) = (Y',s')) else (\<diamondsuit>,s) = (Y',s'))) \<and>. G\<turnstile>init\<le>n" in polymorphic_Loop) 

410 
apply (force dest!: eval.Loop split add: split_if_asm) 

411 
prefer 2 

412 
apply (erule MGFnD' [THEN conseq12]) 

413 
apply clarsimp 

414 
apply (erule_tac V = "card (nyinitcls G s') \<le> n" in thin_rl) 

415 
apply (tactic "eval_Force_tac 1") 

416 
apply (erule MGFnD' [THEN conseq12] , clarsimp) 

417 
apply (rule conjI, erule exI) 

418 
apply (tactic "clarsimp_tac eval_css 1") 

419 
apply (case_tac "a") 

420 
prefer 2 

421 
apply (clarsimp) 

422 
apply (clarsimp split add: split_if) 

423 
apply (rule conjI, (tactic {* force_tac (claset() addSDs [thm "eval.Loop"], 

424 
simpset() addsimps [split_paired_all] addsimprocs [eval_stmt_proc]) 1*})+) 

425 
done 

426 

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

427 
text {* For @{text MGFn_FVar} we need the wellformedness of the program to 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

428 
switch from the evalnsemantics to the evalsemantics *} 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

430 
"\<lbrakk>G,A\<turnstile>{=:n} In1r (Init statDeclC)\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

431 
\<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In2 ({accC,statDeclC,stat}e..fn)\<succ> {G\<rightarrow>}" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

432 
apply (tactic "wt_conf_prepare_tac 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

434 
Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

435 
(G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

436 
)) \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

438 
apply (tactic "forw_hyp_tac 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

439 
apply (tactic "clarsimp_tac eval_css 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

440 
apply (subgoal_tac "is_class G statDeclC") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

441 
apply (force dest: eval_type_sound) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

442 
apply (force dest: ty_expr_is_type [THEN type_is_class] 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

443 
accfield_fields [THEN fields_declC]) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

444 
apply (tactic "forw_hyp_tac 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

445 
apply (tactic "clarsimp_tac eval_css 1") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

446 
apply (subgoal_tac "(\<exists> v' s2' s3. 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

447 
( fvar statDeclC (is_static f) fn v (aa, ba) = (v',s2') ) \<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

448 
(s3 = check_field_access G C statDeclC fn (is_static f) v s2') \<and> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

449 
(s3 = s2'))") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

450 
apply (erule exE)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

451 
apply (erule conjE)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

452 
apply (erule (1) eval.FVar) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

455 

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

456 
apply (case_tac "fvar statDeclC (is_static f) fn v (aa, ba)") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

457 
apply (rule exI)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

458 
apply (rule context_conjI) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

460 

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

461 
apply (rule context_conjI) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

463 

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

464 
apply (erule (3) error_free_field_access) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

465 
apply (auto dest: eval_type_sound) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

467 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

468 
text {* For @{text MGFn_Fin} we need the wellformedness of the program to 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

469 
switch from the evalnsemantics to the evalsemantics *} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

470 
lemma MGFn_Fin: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

471 
"\<lbrakk>wf_prog G; G,A\<turnstile>{=:n} In1r stmt1\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt2\<succ> {G\<rightarrow>}\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

472 
\<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In1r (stmt1 Finally stmt2)\<succ> {G\<rightarrow>}" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

473 
apply (tactic "wt_conf_prepare_tac 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

474 
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s' \<and> s\<Colon>\<preceq>(G, L)) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

475 
\<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

476 
apply (tactic "forw_hyp_tac 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

477 
apply (tactic "clarsimp_tac eval_css 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

478 
apply (rule allI) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

479 
apply (tactic "clarsimp_tac eval_css 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

480 
apply (tactic "forw_hyp_tac 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

481 
apply (tactic {* pair_tac "sb" 1 *}) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

482 
apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

483 
apply (rule wf_eval_Fin) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

484 
apply auto 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

485 
done 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

486 

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

487 
text {* For @{text MGFn_lemma} we need the wellformedness of the program to 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

488 
switch from the evalnsemantics to the evalsemantics cf. @{text MGFn_call}, 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

489 
@{text MGFn_FVar}*} 
12854  490 
lemma MGFn_lemma [rule_format (no_asm)]: 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

491 
"\<lbrakk>\<forall>n C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>}; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

492 
wf_prog G\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

493 
\<Longrightarrow> \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}" 
12854  494 
apply (rule full_nat_induct) 
495 
apply (rule allI) 

496 
apply (drule_tac x = n in spec) 

497 
apply (drule_tac psi = "All ?P" in asm_rl) 

498 
apply (subgoal_tac "\<forall>v e c es. G,A\<turnstile>{=:n} In2 v\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1r c\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In3 es\<succ> {G\<rightarrow>}") 

499 
apply (tactic "Clarify_tac 2") 

500 
apply (induct_tac "t") 

501 
apply (induct_tac "a") 

502 
apply fast+ 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

503 
apply (rule var_expr_stmt.induct) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

504 
(* 34 subgoals *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

505 
prefer 17 apply fast (* Methd *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

506 
prefer 16 apply (erule (3) MGFn_Call) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

507 
prefer 2 apply (drule MGFn_Init,erule (2) MGFn_FVar) 
12854  508 
apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

509 
apply (erule_tac [29] MGFn_Init) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

510 
prefer 23 apply (erule (1) MGFn_Loop) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

511 
prefer 26 apply (erule (2) MGFn_Fin) 
12854  512 
apply (tactic "ALLGOALS compl_prepare_tac") 
513 

514 
apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1") 

515 

516 
apply (rule ax_derivs.AVar) 

517 
apply (erule MGFnD [THEN ax_NormalD]) 

518 
apply (tactic "forw_hyp_eval_Force_tac 1") 

519 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

520 
apply (rule ax_derivs.InstInitV) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

521 

12854  522 
apply (rule ax_derivs.NewC) 
523 
apply (erule MGFn_InitD [THEN conseq2]) 

524 
apply (tactic "eval_Force_tac 1") 

525 

526 
apply (rule_tac Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty ty) \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.NewA) 

527 
apply (simp add: init_comp_ty_def split add: split_if) 

528 
apply (rule conjI, clarsimp) 

529 
apply (erule MGFn_InitD [THEN conseq2]) 

530 
apply (tactic "clarsimp_tac eval_css 1") 

531 
apply clarsimp 

532 
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1") 

533 
apply (tactic "forw_hyp_eval_Force_tac 1") 

534 

535 
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast],tactic"eval_Force_tac 1") 

536 

537 
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1") 

538 
apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1") 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

539 
apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1") 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

540 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

541 
apply (rule ax_derivs.BinOp) 
13384  542 
apply (erule MGFnD [THEN ax_NormalD]) 
543 

544 
apply (rule allI) 

545 
apply (case_tac "need_second_arg binop v1") 

546 
apply simp 

547 
apply (tactic "forw_hyp_eval_Force_tac 1") 

548 

549 
apply simp 

550 
apply (rule ax_Normal_cases) 

551 
apply (rule ax_derivs.Skip [THEN conseq1]) 

552 
apply clarsimp 

553 

554 
apply (rule eval_BinOp_arg2_indepI) 

555 
apply simp 

556 
apply simp 

557 

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

559 
apply (tactic "eval_Force_tac 1") 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

560 

12854  561 
apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1") 
562 
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1") 

563 

564 
apply (rule ax_derivs.Ass) 

565 
apply (erule MGFnD [THEN ax_NormalD]) 

566 
apply (tactic "forw_hyp_eval_Force_tac 1") 

567 

568 
apply (rule ax_derivs.Cond) 

569 
apply (erule MGFnD [THEN ax_NormalD]) 

570 
apply (rule allI) 

571 
apply (rule ax_Normal_cases) 

572 
prefer 2 

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

574 
apply (tactic "eval_Force_tac 1") 

575 
apply (case_tac "b") 

576 
apply (simp, tactic "forw_hyp_eval_Force_tac 1") 

577 
apply (simp, tactic "forw_hyp_eval_Force_tac 1") 

578 

579 
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init pid_field_type\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Body) 

580 
apply (erule MGFn_InitD [THEN conseq2]) 

581 
apply (tactic "eval_Force_tac 1") 

582 
apply (tactic "forw_hyp_tac 1") 

583 
apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *}) 

584 
apply (erule (1) eval.Body) 

585 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

586 
apply (rule ax_derivs.InstInitE) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

587 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

588 
apply (rule ax_derivs.Callee) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

589 

12854  590 
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1") 
591 

592 
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1") 

593 

594 
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab]) 

595 
apply (tactic "clarsimp_tac eval_css 1") 

596 

597 
apply (rule ax_derivs.Comp) 

598 
apply (erule MGFnD [THEN ax_NormalD]) 

599 
apply (tactic "forw_hyp_eval_Force_tac 1") 

600 

601 
apply (rule ax_derivs.If) 

602 
apply (erule MGFnD [THEN ax_NormalD]) 

603 
apply (rule allI) 

604 
apply (rule ax_Normal_cases) 

605 
prefer 2 

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

607 
apply (tactic "eval_Force_tac 1") 

608 
apply (case_tac "b") 

609 
apply (simp, tactic "forw_hyp_eval_Force_tac 1") 

610 
apply (simp, tactic "forw_hyp_eval_Force_tac 1") 

611 

612 
apply (rule ax_derivs.Do [THEN conseq1]) 

613 
apply (tactic {* force_tac (eval_css addsimps2 [thm "abupd_def2"]) 1 *}) 

614 

615 
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw]) 

616 
apply (tactic "clarsimp_tac eval_css 1") 

617 

618 
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>In1r stmt1\<succ>\<rightarrow> (Y',s'') \<and> G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.Try) 

619 
apply (tactic "eval_Force_tac 3") 

620 
apply (tactic "forw_hyp_eval_Force_tac 2") 

621 
apply (erule MGFnD [THEN ax_NormalD, THEN conseq2]) 

622 
apply (tactic "clarsimp_tac eval_css 1") 

623 
apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext]) 

624 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

625 
apply (rule ax_derivs.FinA) 
12854  626 

627 
apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1") 

628 

629 
apply (rule ax_derivs.Cons) 

630 
apply (erule MGFnD [THEN ax_NormalD]) 

631 
apply (tactic "forw_hyp_eval_Force_tac 1") 

632 
done 

633 

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

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

635 
"\<lbrakk>\<forall>C sig. is_methd G C sig \<longrightarrow> G,A\<turnstile>{\<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

636 
\<Longrightarrow> G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" 
12854  637 
apply (simp (no_asm_use) add: MGF_MGFn_iff) 
638 
apply (rule allI) 

639 
apply (rule MGFn_lemma) 

640 
apply (intro strip) 

641 
apply (rule MGFn_free_wt) 

642 
apply (force dest: wt_Methd_is_methd) 

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

643 
apply assumption (* wf_prog G *) 
12854  644 
done 
645 

646 
declare splitI2 [intro!] 

647 
ML_setup {* 

648 
Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc] 

649 
*} 

650 

651 

652 
section "nested version" 

653 

654 
lemma nesting_lemma' [rule_format (no_asm)]: "[ !!A ts. ts <= A ==> P A ts; 

655 
!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn}; 

656 
!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}; 

657 
finite U; uA = mgf_call`U ] ==> 

658 
!A. A <= uA > n <= card uA > card A = card uA  n > (!t. P A {mgf t})" 

659 
proof  

660 
assume ax_derivs_asm: "!!A ts. ts <= A ==> P A ts" 

661 
assume MGF_nested_Methd: "!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) 

662 
{mgf b} ==> P A {mgf_call pn}" 

663 
assume MGF_asm: "!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}" 

664 
assume "finite U" "uA = mgf_call`U" 

665 
then show ?thesis 

666 
apply  

667 
apply (induct_tac "n") 

668 
apply (tactic "ALLGOALS Clarsimp_tac") 

669 
apply (tactic "dtac (permute_prems 0 1 card_seteq) 1") 

670 
apply simp 

671 
apply (erule finite_imageI) 

672 
apply (simp add: MGF_asm ax_derivs_asm) 

673 
apply (rule MGF_asm) 

674 
apply (rule ballI) 

675 
apply (case_tac "mgf_call pn : A") 

676 
apply (fast intro: ax_derivs_asm) 

677 
apply (rule MGF_nested_Methd) 

678 
apply (rule ballI) 

13601  679 
apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec) 
12854  680 
apply fast 
681 
apply (drule finite_subset) 

682 
apply (erule finite_imageI) 

683 
apply auto 

684 
apply arith 

685 
done 

686 
qed 

687 

688 
lemma nesting_lemma [rule_format (no_asm)]: "[ !!A ts. ts <= A ==> P A ts; 

689 
!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}; 

690 
!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}; 

691 
finite U ] ==> P {} {mgf t}" 

692 
proof  

693 
assume 2: "!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}" 

694 
assume 3: "!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}" 

695 
assume "!!A ts. ts <= A ==> P A ts" "finite U" 

696 
then show ?thesis 

697 
apply  

698 
apply (rule_tac mgf = "mgf" in nesting_lemma') 

699 
apply (erule_tac [2] 2) 

700 
apply (rule_tac [2] 3) 

701 
apply (rule_tac [6] le_refl) 

702 
apply auto 

703 
done 

704 
qed 

705 

706 
lemma MGF_nested_Methd: "\<lbrakk> 

707 
G,insert ({Normal \<doteq>} In1l (Methd C sig) \<succ>{G\<rightarrow>}) A\<turnstile> 

708 
{Normal \<doteq>} In1l (body G C sig) \<succ>{G\<rightarrow>} 

709 
\<rbrakk> \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} In1l (Methd C sig) \<succ>{G\<rightarrow>}" 

710 
apply (unfold MGF_def) 

711 
apply (rule ax_MethdN) 

712 
apply (erule conseq2) 

713 
apply clarsimp 

714 
apply (erule MethdI) 

715 
done 

716 

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

717 
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" 
12854  718 
apply (rule MGFNormalI) 
719 
apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and 

720 
bdy = "\<lambda> (C,sig) .{In1l (body G C sig) }" and 

721 
f = "\<lambda> (C,sig) . In1l (Methd C sig) " in nesting_lemma) 

722 
apply (erule ax_derivs.asm) 

723 
apply (clarsimp simp add: split_tupled_all) 

724 
apply (erule MGF_nested_Methd) 

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

725 
apply (erule_tac [2] finite_is_methd [OF wf_ws_prog]) 
12854  726 
apply (rule MGF_asm [THEN MGFNormalD]) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

727 
apply (auto intro: MGFNormalI) 
12854  728 
done 
729 

730 

731 
section "simultaneous version" 

732 

733 
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow> 

734 
G,A\<union> (\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ` ms 

735 
\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow> 

736 
G,A\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ` ms" 

737 
apply (unfold MGF_def) 

738 
apply (rule ax_derivs.Methd [unfolded mtriples_def]) 

739 
apply (erule ax_finite_pointwise) 

740 
prefer 2 

741 
apply (rule ax_derivs.asm) 

742 
apply fast 

743 
apply clarsimp 

744 
apply (rule conseq2) 

745 
apply (erule (1) ax_methods_spec) 

746 
apply clarsimp 

747 
apply (erule eval_Methd) 

748 
done 

749 

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

750 
lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow> 
12854  751 
G,({}::state triple set)\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) 
752 
` Collect (split (is_methd G)) " 

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

753 
apply (frule finite_is_methd [OF wf_ws_prog]) 
12854  754 
apply (rule MGF_simult_Methd_lemma) 
755 
apply assumption 

756 
apply (erule ax_finite_pointwise) 

757 
prefer 2 

758 
apply (rule ax_derivs.asm) 

759 
apply blast 

760 
apply clarsimp 

761 
apply (rule MGF_asm [THEN MGFNormalD]) 

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

762 
apply (auto intro: MGFNormalI) 
12854  763 
done 
764 

765 

766 
section "corollaries" 

767 

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

768 
lemma eval_to_evaln: "\<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s');type_ok G t s; wf_prog G\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

769 
\<Longrightarrow> \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

770 
apply (cases "normal s") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

771 
apply (force simp add: type_ok_def intro: eval_evaln) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

772 
apply (force intro: evaln.Abrupt) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

774 

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

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

776 
"\<lbrakk>G,{}\<Turnstile>{P} t\<succ> {Q}; G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

777 
\<Longrightarrow> G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}" 
12854  778 
apply (rule ax_no_hazard) 
779 
apply (unfold MGF_def) 

780 
apply (erule conseq12) 

781 
apply (simp (no_asm_use) add: ax_valids_def triple_valid_def) 

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

782 
apply (blast dest: eval_to_evaln) 
12854  783 
done 
784 

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

785 
theorem ax_complete: "wf_prog G \<Longrightarrow> 
12854  786 
G,{}\<Turnstile>{P::state assn} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}" 
787 
apply (erule MGF_complete) 

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

788 
apply (erule (1) MGF_deriv) 
12854  789 
done 
790 

791 
end 