author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 13337  f75dfc606ac7 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/AxSound.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12859  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 
header {* Soundness proof for Axiomatic semantics of Java expressions and 

7 
statements 

8 
*} 

9 

10 

11 

12 
theory AxSound = AxSem: 

13 

14 
section "validity" 

15 

16 
consts 

17 

18 
triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" 

19 
( "_\<Turnstile>_\<Colon>_"[61,0, 58] 57) 

20 
ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" 

21 
("_,_\<Turnstile>\<Colon>_" [61,58,58] 57) 

22 

23 
defs triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow> 

24 
\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 

25 
\<longrightarrow> (\<forall>T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<longrightarrow> 

26 
(\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))" 

27 

28 
defs ax_valids2_def: "G,A\<Turnstile>\<Colon>ts \<equiv> \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)" 

29 

30 
lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} = 

31 
(\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> 

32 
(\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<longrightarrow> 

33 
Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))" 

34 
apply (unfold triple_valid2_def) 

35 
apply (simp (no_asm) add: split_paired_All) 

36 
apply blast 

37 
done 

38 

39 
lemma triple_valid2_eq [rule_format (no_asm)]: 

40 
"wf_prog G ==> triple_valid2 G = triple_valid G" 

41 
apply (rule ext) 

42 
apply (rule ext) 

43 
apply (rule triple.induct) 

44 
apply (simp (no_asm) add: triple_valid_def2 triple_valid2_def2) 

45 
apply (rule iffI) 

46 
apply fast 

47 
apply clarify 

48 
apply (tactic "smp_tac 3 1") 

49 
apply (case_tac "normal s") 

50 
apply clarsimp 

51 
apply (blast dest: evaln_eval eval_type_sound [THEN conjunct1]) 

52 
apply clarsimp 

53 
done 

54 

55 
lemma ax_valids2_eq: "wf_prog G \<Longrightarrow> G,A\<Turnstile>\<Colon>ts = G,A\<Turnstile>ts" 

56 
apply (unfold ax_valids_def ax_valids2_def) 

57 
apply (force simp add: triple_valid2_eq) 

58 
done 

59 

60 
lemma triple_valid2_Suc [rule_format (no_asm)]: "G\<Turnstile>Suc n\<Colon>t \<longrightarrow> G\<Turnstile>n\<Colon>t" 

61 
apply (induct_tac "t") 

62 
apply (subst triple_valid2_def2) 

63 
apply (subst triple_valid2_def2) 

64 
apply (fast intro: evaln_nonstrict_Suc) 

65 
done 

66 

67 
lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig\<succ> {Q}" 

68 
apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2) 

69 
done 

70 

71 
lemma Methd_triple_valid2_SucI: 

72 
"\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig\<succ>{Q}\<rbrakk> 

73 
\<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig\<succ> {Q}" 

74 
apply (simp (no_asm_use) add: triple_valid2_def2) 

75 
apply (intro strip, tactic "smp_tac 3 1", clarify) 

76 
apply (erule wt_elim_cases, erule evaln_elim_cases) 

77 
apply (unfold body_def Let_def) 

78 
apply clarsimp 

79 
apply blast 

80 
done 

81 

82 
lemma triples_valid2_Suc: 

83 
"Ball ts (triple_valid2 G (Suc n)) \<Longrightarrow> Ball ts (triple_valid2 G n)" 

84 
apply (fast intro: triple_valid2_Suc) 

85 
done 

86 

87 
lemma "G\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G\<Turnstile>n:A)"; 

88 
oops 

89 

90 

91 
section "soundness" 

92 

93 
lemma Methd_sound: 

94 
"\<lbrakk>G,A\<union> {{P} Methd\<succ> {Q}  ms}\<Turnstile>\<Colon>{{P} body G\<succ> {Q}  ms}\<rbrakk> \<Longrightarrow> 

95 
G,A\<Turnstile>\<Colon>{{P} Methd\<succ> {Q}  ms}" 

96 
apply (unfold ax_valids2_def mtriples_def) 

97 
apply (rule allI) 

98 
apply (induct_tac "n") 

99 
apply (clarify, tactic {* pair_tac "x" 1 *}, simp (no_asm)) 

100 
apply (fast intro: Methd_triple_valid2_0) 

101 
apply (clarify, tactic {* pair_tac "xa" 1 *}, simp (no_asm)) 

102 
apply (drule triples_valid2_Suc) 

103 
apply (erule (1) notE impE) 

104 
apply (drule_tac x = na in spec) 

105 
apply (tactic {* auto_tac (claset() addSIs [thm "Methd_triple_valid2_SucI"], 

106 
simpset() addsimps [ball_Un] addloop ("split_all_tac", split_all_tac)) *}) 

107 
done 

108 

109 

110 
lemma valids2_inductI: "\<forall>s t n Y' s'. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> t = c \<longrightarrow> 

111 
Ball A (triple_valid2 G n) \<longrightarrow> (\<forall>Y Z. P Y s Z \<longrightarrow> 

112 
(\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<longrightarrow> 

113 
Q Y' s' Z \<and> s'\<Colon>\<preceq>(G, L)))) \<Longrightarrow> 

114 
G,A\<Turnstile>\<Colon>{ {P} c\<succ> {Q}}" 

115 
apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2) 

116 
apply clarsimp 

117 
done 

118 

119 
ML_setup {* 

120 
Delsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc] 

121 
*} 

122 

123 
lemma Loop_sound: "\<lbrakk>G,A\<Turnstile>\<Colon>{ {P} e\<succ> {P'}}; 

124 
G,A\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}}\<rbrakk> \<Longrightarrow> 

125 
G,A\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}}" 

126 
apply (rule valids2_inductI) 

127 
apply ((rule allI)+, rule impI, tactic {* pair_tac "s" 1*}, tactic {* pair_tac "s'" 1*}) 

128 
apply (erule evaln.induct) 

129 
apply simp_all (* takes half a minute *) 

130 
apply clarify 

131 
apply (erule_tac V = "G,A\<Turnstile>\<Colon>{ {?P'} .c. {?P}}" in thin_rl) 

132 
apply (simp_all (no_asm_use) add: ax_valids2_def triple_valid2_def2) 

133 
apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", force) 

134 
apply clarify 

135 
apply (rule wt_elim_cases, assumption) 

136 
apply (tactic "smp_tac 1 1", tactic "smp_tac 1 1", tactic "smp_tac 3 1", 

137 
tactic "smp_tac 2 1", tactic "smp_tac 1 1") 

138 
apply (erule impE,simp (no_asm),blast) 

139 
apply (simp add: imp_conjL split_tupled_all split_paired_All) 

140 
apply (case_tac "the_Bool b") 

141 
apply clarsimp 

142 
apply (case_tac "a") 

143 
apply (simp_all) 

144 
apply clarsimp 

145 
apply (erule_tac V = "c = l\<bullet> While(e) c \<longrightarrow> ?P" in thin_rl) 

146 
apply (blast intro: conforms_absorb) 

147 
apply blast+ 

148 
done 

149 

150 
declare subst_Bool_def2 [simp del] 

151 
lemma all_empty: "(!x. P) = P" 

152 
by simp 

153 
lemma sound_valid2_lemma: 

154 
"\<lbrakk>\<forall>v n. Ball A (triple_valid2 G n) \<longrightarrow> P v n; Ball A (triple_valid2 G n)\<rbrakk> 

155 
\<Longrightarrow>P v n" 

156 
by blast 

157 
ML {* 

158 
val fullsimptac = full_simp_tac(simpset() delsimps [thm "all_empty"]); 

159 
val sound_prepare_tac = EVERY'[REPEAT o thin_tac "?x \<in> ax_derivs G", 

160 
full_simp_tac (simpset()addsimps[thm "ax_valids2_def",thm "triple_valid2_def2", 

161 
thm "imp_conjL"] delsimps[thm "all_empty"]), 

162 
Clarify_tac]; 

163 
val sound_elim_tac = EVERY'[eresolve_tac (thms "evaln_elim_cases"), 

164 
TRY o eresolve_tac (thms "wt_elim_cases"), fullsimptac, Clarify_tac]; 

165 
val sound_valid2_tac = REPEAT o FIRST'[smp_tac 1, 

166 
datac (thm "sound_valid2_lemma") 1]; 

167 
val sound_forw_hyp_tac = 

168 
EVERY'[smp_tac 3 

169 
ORELSE' EVERY'[dtac spec,dtac spec, dtac spec,etac impE, Fast_tac] 

170 
ORELSE' EVERY'[dtac spec,dtac spec,etac impE, Fast_tac], 

171 
fullsimptac, 

172 
smp_tac 2,TRY o smp_tac 1, 

173 
TRY o EVERY'[etac impE, TRY o rtac impI, 

174 
atac ORELSE' (EVERY' [REPEAT o rtac exI,Blast_tac]), 

175 
fullsimptac, Clarify_tac, TRY o smp_tac 1]] 

176 
*} 

177 
(* ### rtac conjI,rtac HOL.refl *) 

178 
lemma Call_sound: 

179 
"\<lbrakk>wf_prog G; G,A\<Turnstile>\<Colon>{ {Normal P} e\<succ> {Q}}; \<forall>a. G,A\<Turnstile>\<Colon>{ {Q\<leftarrow>Val a} ps\<doteq>\<succ> {R a}}; 

180 
\<forall>a vs invC declC l. G,A\<Turnstile>\<Colon>{ {(R a\<leftarrow>Vals vs \<and>. 

181 
(\<lambda>s. declC = invocation_declclass 

182 
G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and> 

183 
invC = invocation_class mode (store s) a statT \<and> 

184 
l = locals (store s)) ;. 

185 
init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>. 

186 
(\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)} 

187 
Methd declC \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S}}\<rbrakk> \<Longrightarrow> 

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

188 
G,A\<Turnstile>\<Colon>{ {Normal P} {accC,statT,mode}e\<cdot>mn({pTs}ps)\<succ> {S}}" 
12854  189 
apply (tactic "EVERY'[sound_prepare_tac, sound_elim_tac, sound_valid2_tac] 1") 
190 
apply (rename_tac x1 s1 x2 s2 ab bb v vs m pTsa statDeclC) 

191 
apply (tactic "smp_tac 6 1") 

192 
apply (tactic "sound_forw_hyp_tac 1") 

193 
apply (tactic "sound_forw_hyp_tac 1") 

194 
apply (drule max_spec2mheads) 

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

195 
apply (drule (3) evaln_eval, drule (3) eval_ts) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

196 
apply (drule (3) evaln_eval, frule (3) evals_ts) 
12854  197 
apply (drule spec,erule impE,rule exI, blast) 
198 
(* apply (drule spec,drule spec,drule spec,erule impE,rule exI,blast) *) 

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

199 
apply (case_tac "if is_static m then x2 else (np a') x2") 
12854  200 
defer 1 
201 
apply (rename_tac x, subgoal_tac "(Some x, s2)\<Colon>\<preceq>(G, L)" (* used two times *)) 

202 
prefer 2 

203 
apply (force split add: split_if_asm) 

204 
apply (simp del: if_raise_if_None) 

205 
apply (tactic "smp_tac 2 1") 

206 
apply (simp only: init_lvars_def2 invmode_Static_eq) 

207 
apply (clarsimp simp del: resTy_mthd) 

208 
apply (drule spec,erule swap,erule conforms_set_locals [OF _ lconf_empty]) 

209 
apply clarsimp 

210 
apply (drule Null_staticD) 

211 
apply (drule eval_gext', drule (1) conf_gext, frule (3) DynT_propI) 

212 
apply (erule impE) apply blast 

213 
apply (subgoal_tac 

214 
"G\<turnstile>invmode (mhd (statDeclC,m)) e 

215 
\<rightarrow>invocation_class (invmode m e) s2 a' statT\<preceq>statT") 

216 
defer apply simp 

217 
apply (drule (3) DynT_mheadsD,simp,simp) 

218 
apply (clarify, drule wf_mdeclD1, clarify) 

219 
apply (frule ty_expr_is_type) apply simp 

220 
apply (subgoal_tac "invmode (mhd (statDeclC,m)) e = IntVir \<longrightarrow> a' \<noteq> Null") 

221 
defer apply simp 

222 
apply (frule (2) wt_MethdI) 

223 
apply clarify 

224 
apply (drule (2) conforms_init_lvars) 

225 
apply (simp) 

226 
apply (assumption)+ 

227 
apply simp 

228 
apply (assumption)+ 

229 
apply (rule impI) apply simp 

230 
apply simp 

231 
apply simp 

232 
apply (rule Ball_weaken) 

233 
apply assumption 

234 
apply (force simp add: is_acc_type_def) 

235 
apply (tactic "smp_tac 2 1") 

236 
apply simp 

237 
apply (tactic "smp_tac 1 1") 

238 
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl) 

239 
apply (erule impE) 

240 
apply (rule exI)+ 

241 
apply (subgoal_tac "is_static dm = (static m)") 

242 
prefer 2 apply (simp add: member_is_static_simp) 

243 
apply (simp only: ) 

244 
apply (simp only: sig.simps) 

245 
apply (force dest!: evaln_eval eval_gext' elim: conforms_return 

246 
del: impCE simp add: init_lvars_def2) 

247 
done 

248 

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

249 
corollary evaln_type_sound: 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

250 
assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

251 
wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

252 
conf_s0: "s0\<Colon>\<preceq>(G,L)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

253 
wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

254 
shows "s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

255 
(error_free s0 = error_free s1)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

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

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

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

261 

12854  262 
lemma Init_sound: "\<lbrakk>wf_prog G; the (class G C) = c; 
263 
G,A\<Turnstile>\<Colon>{ {Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))} 

264 
.(if C = Object then Skip else Init (super c)). {Q}}; 

265 
\<forall>l. G,A\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty} 

266 
.init c. {set_lvars l .; R}}\<rbrakk> \<Longrightarrow> 

267 
G,A\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}}" 

268 
apply (tactic "EVERY'[sound_prepare_tac, sound_elim_tac,sound_valid2_tac] 1") 

269 
apply (tactic {* instantiate_tac [("l24","\<lambda> n Y Z sa Y' s' L y a b aa ba ab bb. locals b")]*}) 

270 
apply (clarsimp simp add: split_paired_Ex) 

271 
apply (drule spec, drule spec, drule spec, erule impE) 

272 
apply (erule_tac V = "All ?P" in thin_rl, fast) 

273 
apply clarsimp 

274 
apply (tactic "smp_tac 2 1", drule spec, erule impE, 

275 
erule (3) conforms_init_class_obj) 

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

276 
apply (frule (1) wf_prog_cdecl) 
12854  277 
apply (erule impE, rule exI,erule_tac V = "All ?P" in thin_rl, 
278 
force dest: wf_cdecl_supD split add: split_if simp add: is_acc_class_def) 

279 
apply clarify 

280 
apply (drule spec) 

281 
apply (drule spec) 

282 
apply (drule spec) 

283 
apply (erule impE) 

284 
apply ( fast) 

285 
apply (simp (no_asm_use) del: empty_def2) 

286 
apply (tactic "smp_tac 2 1") 

287 
apply (drule spec, erule impE, erule conforms_set_locals, rule lconf_empty) 

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

288 
apply (erule impE,rule impI,rule exI,erule wf_cdecl_wt_init) 
12854  289 
apply clarsimp 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

292 
apply (subgoal_tac "(a, set_locals empty b)\<Colon>\<preceq>(G, empty)") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

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

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

296 

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

297 
(* refer to case Init in eval_type_sound proof, to see whats going on*) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

298 
apply (subgoal_tac "(a,b)\<Colon>\<preceq>(G, L)") 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

300 

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

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

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

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

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

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

306 
apply blast 
12854  307 
done 
308 

309 
lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" 

310 
by fast 

311 

312 
lemma all4_conjunct2: 

313 
"\<forall>a vs D l. (P' a vs D l \<and> P a vs D l) \<Longrightarrow> \<forall>a vs D l. P a vs D l" 

314 
by fast 

315 

316 
lemmas sound_lemmas = Init_sound Loop_sound Methd_sound 

317 

318 
lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A\<turnstile>ts \<Longrightarrow> G,A\<Turnstile>\<Colon>ts" 

319 
apply (erule ax_derivs.induct) 

320 
prefer 20 (* Call *) 

321 
apply (erule (1) Call_sound) apply simp apply force apply force 

322 

323 
apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW 

324 
eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *}) 

325 

326 
apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac") 

327 

328 
(*empty*) 

329 
apply fast (* insert *) 

330 
apply fast (* asm *) 

331 
(*apply fast *) (* cut *) 

332 
apply fast (* weaken *) 

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

333 
apply (tactic "smp_tac 3 1", clarify, tactic "smp_tac 1 1", 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

334 
case_tac"fst s",clarsimp,erule (3) evaln_type_sound [THEN conjunct1], 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

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

336 
apply (simp (no_asm_use) add: type_ok_def,fast)(* hazard *) 
12854  337 
apply force (* Abrupt *) 
338 

339 
(* 25 subgoals *) 

340 
apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *) 

341 
apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() 

342 
delsimps [thm "all_empty"])) *}) (* Done *) 

343 
(* for FVar *) 

344 
apply (frule wf_ws_prog) 

345 
apply (frule ty_expr_is_type [THEN type_is_class, 

346 
THEN accfield_declC_is_class]) 

347 
apply (simp,simp,simp) 

348 
apply (frule_tac [4] wt_init_comp_ty) (* for NewA*) 

349 
apply (tactic "ALLGOALS sound_valid2_tac") 

350 
apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *) 

351 
apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, 

352 
dtac spec], dtac conjunct2, smp_tac 1, 

353 
TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *}) 

354 
apply (frule_tac [14] x = x1 in conforms_NormI) (* for Fin *) 

355 

356 

357 
(* 15 subgoals *) 

358 
(* FVar *) 

359 
apply (tactic "sound_forw_hyp_tac 1") 

360 
apply (clarsimp simp add: fvar_def2 Let_def split add: split_if_asm) 

361 

362 
(* AVar *) 

363 
(* 

364 
apply (drule spec, drule spec, erule impE, fast) 

365 
apply (simp) 

366 
apply (tactic "smp_tac 2 1") 

367 
apply (tactic "smp_tac 1 1") 

368 
apply (erule impE) 

369 
apply (rule impI) 

370 
apply (rule exI)+ 

371 
apply blast 

372 
apply (clarsimp simp add: avar_def2) 

373 
*) 

374 
apply (tactic "sound_forw_hyp_tac 1") 

375 
apply (clarsimp simp add: avar_def2) 

376 

377 
(* NewC *) 

378 
apply (clarsimp simp add: is_acc_class_def) 

379 
apply (erule (1) halloc_conforms, simp, simp) 

380 

381 
(* NewA *) 

382 
apply (tactic "sound_forw_hyp_tac 1") 

383 
apply (rule conjI,blast) 

384 
apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def) 

385 

386 
(* Ass *) 

387 
apply (tactic "sound_forw_hyp_tac 1") 

388 
apply (case_tac "aa") 

389 
prefer 2 

390 
apply clarsimp 

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

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

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

393 
apply (frule (3) eval_type_sound) 
12854  394 
apply clarsimp 
395 
apply (frule wf_ws_prog) 

396 
apply (drule (2) conf_widen) 

397 
apply (drule_tac "s1.0" = b in eval_gext') 

398 
apply (clarsimp simp add: assign_conforms_def) 

399 

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

400 

12854  401 
(* Cond *) 
402 
apply (tactic "smp_tac 3 1") apply (tactic "smp_tac 2 1") 

403 
apply (tactic "smp_tac 1 1") apply (erule impE) 

404 
apply (rule impI,rule exI) 

405 
apply (rule_tac x = "if the_Bool b then T1 else T2" in exI) 

406 
apply (force split add: split_if) 

407 
apply assumption 

408 

409 
(* Body *) 

410 
apply (tactic "sound_forw_hyp_tac 1") 

411 
apply (rule conforms_absorb,assumption) 

412 

413 
(* Lab *) 

414 
apply (tactic "sound_forw_hyp_tac 1") 

415 
apply (rule conforms_absorb,assumption) 

416 

417 
(* If *) 

418 
apply (tactic "sound_forw_hyp_tac 1") 

419 
apply (tactic "sound_forw_hyp_tac 1") 

420 
apply (force split add: split_if) 

421 

422 
(* Throw *) 

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

423 
apply (drule (3) evaln_type_sound) 
12854  424 
apply clarsimp 
425 
apply (drule (3) Throw_lemma) 

426 
apply clarsimp 

427 

428 
(* Try *) 

429 
apply (frule (1) sxalloc_type_sound) 

430 
apply (erule sxalloc_elim_cases2) 

431 
apply (tactic "smp_tac 3 1") 

432 
apply (clarsimp split add: option.split_asm) 

433 
apply (clarsimp split add: option.split_asm) 

434 
apply (tactic "smp_tac 1 1") 

435 
apply (simp only: split add: split_if_asm) 

436 
prefer 2 

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

438 
apply (drule spec, erule_tac V = "All ?P" in thin_rl, drule spec, drule spec, 

439 
erule impE, force) 

440 
apply (frule (2) Try_lemma) 

441 
apply clarsimp 

442 
apply (fast elim!: conforms_deallocL) 

443 

444 
(* Fin *) 

445 
apply (tactic "sound_forw_hyp_tac 1") 

446 
apply (case_tac "x1", force) 

447 
apply clarsimp 

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

448 
apply (drule (3) evaln_eval, drule (4) Fin_lemma) 
12854  449 
done 
450 

451 

452 

453 
declare subst_Bool_def2 [simp] 

454 

455 
theorem ax_sound: 

456 
"wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>(ts::'a triple set) \<Longrightarrow> G,A\<Turnstile>ts" 

457 
apply (subst ax_valids2_eq [symmetric]) 

458 
apply assumption 

459 
apply (erule (1) ax_sound2) 

460 
done 

461 

462 

463 
end 