author | berghofe |
Mon, 30 Sep 2002 16:14:02 +0200 | |
changeset 13601 | fd3e3d6b37b2 |
parent 13384 | a34e38154413 |
child 13688 | a0b16d42d489 |
permissions | -rw-r--r-- |
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) |
|
13601 | 105 |
apply (rule Methd_triple_valid2_SucI) |
106 |
apply (simp (no_asm_use) add: ball_Un) |
|
107 |
apply auto |
|
12854 | 108 |
done |
109 |
||
110 |
||
111 |
lemma valids2_inductI: "\<forall>s t n Y' s'. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> t = c \<longrightarrow> |
|
112 |
Ball A (triple_valid2 G n) \<longrightarrow> (\<forall>Y Z. P Y s Z \<longrightarrow> |
|
113 |
(\<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> |
|
114 |
Q Y' s' Z \<and> s'\<Colon>\<preceq>(G, L)))) \<Longrightarrow> |
|
115 |
G,A|\<Turnstile>\<Colon>{ {P} c\<succ> {Q}}" |
|
116 |
apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2) |
|
117 |
apply clarsimp |
|
118 |
done |
|
119 |
||
120 |
ML_setup {* |
|
121 |
Delsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc] |
|
122 |
*} |
|
123 |
||
124 |
lemma Loop_sound: "\<lbrakk>G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'}}; |
|
125 |
G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}}\<rbrakk> \<Longrightarrow> |
|
126 |
G,A|\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}}" |
|
127 |
apply (rule valids2_inductI) |
|
128 |
apply ((rule allI)+, rule impI, tactic {* pair_tac "s" 1*}, tactic {* pair_tac "s'" 1*}) |
|
129 |
apply (erule evaln.induct) |
|
130 |
apply simp_all (* takes half a minute *) |
|
131 |
apply clarify |
|
132 |
apply (erule_tac V = "G,A|\<Turnstile>\<Colon>{ {?P'} .c. {?P}}" in thin_rl) |
|
133 |
apply (simp_all (no_asm_use) add: ax_valids2_def triple_valid2_def2) |
|
134 |
apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", force) |
|
135 |
apply clarify |
|
136 |
apply (rule wt_elim_cases, assumption) |
|
137 |
apply (tactic "smp_tac 1 1", tactic "smp_tac 1 1", tactic "smp_tac 3 1", |
|
138 |
tactic "smp_tac 2 1", tactic "smp_tac 1 1") |
|
139 |
apply (erule impE,simp (no_asm),blast) |
|
140 |
apply (simp add: imp_conjL split_tupled_all split_paired_All) |
|
141 |
apply (case_tac "the_Bool b") |
|
142 |
apply clarsimp |
|
143 |
apply (case_tac "a") |
|
144 |
apply (simp_all) |
|
145 |
apply clarsimp |
|
146 |
apply (erule_tac V = "c = l\<bullet> While(e) c \<longrightarrow> ?P" in thin_rl) |
|
147 |
apply (blast intro: conforms_absorb) |
|
148 |
apply blast+ |
|
149 |
done |
|
150 |
||
151 |
declare subst_Bool_def2 [simp del] |
|
152 |
lemma all_empty: "(!x. P) = P" |
|
153 |
by simp |
|
154 |
lemma sound_valid2_lemma: |
|
155 |
"\<lbrakk>\<forall>v n. Ball A (triple_valid2 G n) \<longrightarrow> P v n; Ball A (triple_valid2 G n)\<rbrakk> |
|
156 |
\<Longrightarrow>P v n" |
|
157 |
by blast |
|
158 |
ML {* |
|
159 |
val fullsimptac = full_simp_tac(simpset() delsimps [thm "all_empty"]); |
|
160 |
val sound_prepare_tac = EVERY'[REPEAT o thin_tac "?x \<in> ax_derivs G", |
|
161 |
full_simp_tac (simpset()addsimps[thm "ax_valids2_def",thm "triple_valid2_def2", |
|
162 |
thm "imp_conjL"] delsimps[thm "all_empty"]), |
|
163 |
Clarify_tac]; |
|
164 |
val sound_elim_tac = EVERY'[eresolve_tac (thms "evaln_elim_cases"), |
|
165 |
TRY o eresolve_tac (thms "wt_elim_cases"), fullsimptac, Clarify_tac]; |
|
166 |
val sound_valid2_tac = REPEAT o FIRST'[smp_tac 1, |
|
167 |
datac (thm "sound_valid2_lemma") 1]; |
|
168 |
val sound_forw_hyp_tac = |
|
169 |
EVERY'[smp_tac 3 |
|
170 |
ORELSE' EVERY'[dtac spec,dtac spec, dtac spec,etac impE, Fast_tac] |
|
171 |
ORELSE' EVERY'[dtac spec,dtac spec,etac impE, Fast_tac], |
|
172 |
fullsimptac, |
|
173 |
smp_tac 2,TRY o smp_tac 1, |
|
174 |
TRY o EVERY'[etac impE, TRY o rtac impI, |
|
175 |
atac ORELSE' (EVERY' [REPEAT o rtac exI,Blast_tac]), |
|
176 |
fullsimptac, Clarify_tac, TRY o smp_tac 1]] |
|
177 |
*} |
|
178 |
(* ### rtac conjI,rtac HOL.refl *) |
|
179 |
lemma Call_sound: |
|
180 |
"\<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}}; |
|
181 |
\<forall>a vs invC declC l. G,A|\<Turnstile>\<Colon>{ {(R a\<leftarrow>Vals vs \<and>. |
|
182 |
(\<lambda>s. declC = invocation_declclass |
|
183 |
G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and> |
|
184 |
invC = invocation_class mode (store s) a statT \<and> |
|
185 |
l = locals (store s)) ;. |
|
186 |
init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>. |
|
187 |
(\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)} |
|
188 |
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
|
189 |
G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ> {S}}" |
12854 | 190 |
apply (tactic "EVERY'[sound_prepare_tac, sound_elim_tac, sound_valid2_tac] 1") |
191 |
apply (rename_tac x1 s1 x2 s2 ab bb v vs m pTsa statDeclC) |
|
192 |
apply (tactic "smp_tac 6 1") |
|
193 |
apply (tactic "sound_forw_hyp_tac 1") |
|
194 |
apply (tactic "sound_forw_hyp_tac 1") |
|
195 |
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
|
196 |
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
|
197 |
apply (drule (3) evaln_eval, frule (3) evals_ts) |
12854 | 198 |
apply (drule spec,erule impE,rule exI, blast) |
199 |
(* 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
|
200 |
apply (case_tac "if is_static m then x2 else (np a') x2") |
12854 | 201 |
defer 1 |
202 |
apply (rename_tac x, subgoal_tac "(Some x, s2)\<Colon>\<preceq>(G, L)" (* used two times *)) |
|
203 |
prefer 2 |
|
204 |
apply (force split add: split_if_asm) |
|
205 |
apply (simp del: if_raise_if_None) |
|
206 |
apply (tactic "smp_tac 2 1") |
|
207 |
apply (simp only: init_lvars_def2 invmode_Static_eq) |
|
208 |
apply (clarsimp simp del: resTy_mthd) |
|
209 |
apply (drule spec,erule swap,erule conforms_set_locals [OF _ lconf_empty]) |
|
210 |
apply clarsimp |
|
211 |
apply (drule Null_staticD) |
|
212 |
apply (drule eval_gext', drule (1) conf_gext, frule (3) DynT_propI) |
|
213 |
apply (erule impE) apply blast |
|
214 |
apply (subgoal_tac |
|
215 |
"G\<turnstile>invmode (mhd (statDeclC,m)) e |
|
216 |
\<rightarrow>invocation_class (invmode m e) s2 a' statT\<preceq>statT") |
|
217 |
defer apply simp |
|
218 |
apply (drule (3) DynT_mheadsD,simp,simp) |
|
219 |
apply (clarify, drule wf_mdeclD1, clarify) |
|
220 |
apply (frule ty_expr_is_type) apply simp |
|
221 |
apply (subgoal_tac "invmode (mhd (statDeclC,m)) e = IntVir \<longrightarrow> a' \<noteq> Null") |
|
222 |
defer apply simp |
|
223 |
apply (frule (2) wt_MethdI) |
|
224 |
apply clarify |
|
225 |
apply (drule (2) conforms_init_lvars) |
|
226 |
apply (simp) |
|
227 |
apply (assumption)+ |
|
228 |
apply simp |
|
229 |
apply (assumption)+ |
|
230 |
apply (rule impI) apply simp |
|
231 |
apply simp |
|
232 |
apply simp |
|
233 |
apply (rule Ball_weaken) |
|
234 |
apply assumption |
|
235 |
apply (force simp add: is_acc_type_def) |
|
236 |
apply (tactic "smp_tac 2 1") |
|
237 |
apply simp |
|
238 |
apply (tactic "smp_tac 1 1") |
|
239 |
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl) |
|
240 |
apply (erule impE) |
|
241 |
apply (rule exI)+ |
|
242 |
apply (subgoal_tac "is_static dm = (static m)") |
|
243 |
prefer 2 apply (simp add: member_is_static_simp) |
|
244 |
apply (simp only: ) |
|
245 |
apply (simp only: sig.simps) |
|
246 |
apply (force dest!: evaln_eval eval_gext' elim: conforms_return |
|
247 |
del: impCE simp add: init_lvars_def2) |
|
248 |
done |
|
249 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
250 |
corollary evaln_type_sound: |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
251 |
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
|
252 |
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
|
253 |
conf_s0: "s0\<Colon>\<preceq>(G,L)" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
254 |
wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
255 |
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
|
256 |
(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
|
257 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
258 |
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
|
259 |
show ?thesis |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
260 |
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
|
261 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
262 |
|
12854 | 263 |
lemma Init_sound: "\<lbrakk>wf_prog G; the (class G C) = c; |
264 |
G,A|\<Turnstile>\<Colon>{ {Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))} |
|
265 |
.(if C = Object then Skip else Init (super c)). {Q}}; |
|
266 |
\<forall>l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty} |
|
267 |
.init c. {set_lvars l .; R}}\<rbrakk> \<Longrightarrow> |
|
268 |
G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}}" |
|
269 |
apply (tactic "EVERY'[sound_prepare_tac, sound_elim_tac,sound_valid2_tac] 1") |
|
270 |
apply (tactic {* instantiate_tac [("l24","\<lambda> n Y Z sa Y' s' L y a b aa ba ab bb. locals b")]*}) |
|
271 |
apply (clarsimp simp add: split_paired_Ex) |
|
272 |
apply (drule spec, drule spec, drule spec, erule impE) |
|
273 |
apply (erule_tac V = "All ?P" in thin_rl, fast) |
|
274 |
apply clarsimp |
|
275 |
apply (tactic "smp_tac 2 1", drule spec, erule impE, |
|
276 |
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
|
277 |
apply (frule (1) wf_prog_cdecl) |
12854 | 278 |
apply (erule impE, rule exI,erule_tac V = "All ?P" in thin_rl, |
279 |
force dest: wf_cdecl_supD split add: split_if simp add: is_acc_class_def) |
|
280 |
apply clarify |
|
281 |
apply (drule spec) |
|
282 |
apply (drule spec) |
|
283 |
apply (drule spec) |
|
284 |
apply (erule impE) |
|
285 |
apply ( fast) |
|
286 |
apply (simp (no_asm_use) del: empty_def2) |
|
287 |
apply (tactic "smp_tac 2 1") |
|
288 |
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
|
289 |
apply (erule impE,rule impI,rule exI,erule wf_cdecl_wt_init) |
12854 | 290 |
apply clarsimp |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
291 |
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
|
292 |
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
|
293 |
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
|
294 |
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
|
295 |
apply (drule eval_gext') |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
296 |
apply force |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
297 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
298 |
(* 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
|
299 |
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
|
300 |
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
|
301 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
302 |
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
|
303 |
apply (cases "C=Object") |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
304 |
apply force |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
305 |
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
|
306 |
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
|
307 |
apply blast |
12854 | 308 |
done |
309 |
||
310 |
lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l" |
|
311 |
by fast |
|
312 |
||
313 |
lemma all4_conjunct2: |
|
314 |
"\<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" |
|
315 |
by fast |
|
316 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
317 |
|
12854 | 318 |
lemmas sound_lemmas = Init_sound Loop_sound Methd_sound |
319 |
||
320 |
lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts" |
|
321 |
apply (erule ax_derivs.induct) |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
322 |
prefer 22 (* Call *) |
12854 | 323 |
apply (erule (1) Call_sound) apply simp apply force apply force |
324 |
||
325 |
apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW |
|
326 |
eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *}) |
|
327 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
328 |
apply(tactic "COND (has_fewer_prems(30+9)) (ALLGOALS sound_prepare_tac) no_tac") |
12854 | 329 |
|
330 |
(*empty*) |
|
331 |
apply fast (* insert *) |
|
332 |
apply fast (* asm *) |
|
333 |
(*apply fast *) (* cut *) |
|
334 |
apply fast (* weaken *) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
335 |
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
|
336 |
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
|
337 |
clarsimp) (* conseq *) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
338 |
apply (simp (no_asm_use) add: type_ok_def,fast)(* hazard *) |
12854 | 339 |
apply force (* Abrupt *) |
340 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
341 |
prefer 28 apply (simp add: evaln_InsInitV) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
342 |
prefer 28 apply (simp add: evaln_InsInitE) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
343 |
prefer 28 apply (simp add: evaln_Callee) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
344 |
prefer 28 apply (simp add: evaln_FinA) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
345 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
346 |
(* 27 subgoals *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
347 |
apply (tactic {* sound_elim_tac 1 *}) |
12854 | 348 |
apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *) |
349 |
apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() |
|
350 |
delsimps [thm "all_empty"])) *}) (* Done *) |
|
351 |
(* for FVar *) |
|
352 |
apply (frule wf_ws_prog) |
|
353 |
apply (frule ty_expr_is_type [THEN type_is_class, |
|
354 |
THEN accfield_declC_is_class]) |
|
13601 | 355 |
apply (simp (no_asm_use), simp (no_asm_use), simp (no_asm_use)) |
12854 | 356 |
apply (frule_tac [4] wt_init_comp_ty) (* for NewA*) |
357 |
apply (tactic "ALLGOALS sound_valid2_tac") |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
358 |
apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *) |
12854 | 359 |
apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, |
360 |
dtac spec], dtac conjunct2, smp_tac 1, |
|
361 |
TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *}) |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
362 |
apply (frule_tac [15] x = x1 in conforms_NormI) (* for Fin *) |
12854 | 363 |
|
364 |
(* 15 subgoals *) |
|
365 |
(* FVar *) |
|
366 |
apply (tactic "sound_forw_hyp_tac 1") |
|
367 |
apply (clarsimp simp add: fvar_def2 Let_def split add: split_if_asm) |
|
368 |
||
369 |
(* AVar *) |
|
370 |
(* |
|
371 |
apply (drule spec, drule spec, erule impE, fast) |
|
372 |
apply (simp) |
|
373 |
apply (tactic "smp_tac 2 1") |
|
374 |
apply (tactic "smp_tac 1 1") |
|
375 |
apply (erule impE) |
|
376 |
apply (rule impI) |
|
377 |
apply (rule exI)+ |
|
378 |
apply blast |
|
379 |
apply (clarsimp simp add: avar_def2) |
|
380 |
*) |
|
381 |
apply (tactic "sound_forw_hyp_tac 1") |
|
382 |
apply (clarsimp simp add: avar_def2) |
|
383 |
||
384 |
(* NewC *) |
|
385 |
apply (clarsimp simp add: is_acc_class_def) |
|
386 |
apply (erule (1) halloc_conforms, simp, simp) |
|
387 |
||
388 |
(* NewA *) |
|
389 |
apply (tactic "sound_forw_hyp_tac 1") |
|
390 |
apply (rule conjI,blast) |
|
391 |
apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def) |
|
392 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
393 |
(* BinOp *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
394 |
apply (tactic "sound_forw_hyp_tac 1") |
13384 | 395 |
apply (case_tac "need_second_arg binop v1") |
396 |
apply fastsimp |
|
397 |
apply simp |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12937
diff
changeset
|
398 |
|
12854 | 399 |
(* Ass *) |
400 |
apply (tactic "sound_forw_hyp_tac 1") |
|
401 |
apply (case_tac "aa") |
|
402 |
prefer 2 |
|
403 |
apply clarsimp |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
apply (frule (3) eval_type_sound) |
12854 | 407 |
apply clarsimp |
408 |
apply (frule wf_ws_prog) |
|
409 |
apply (drule (2) conf_widen) |
|
410 |
apply (drule_tac "s1.0" = b in eval_gext') |
|
411 |
apply (clarsimp simp add: assign_conforms_def) |
|
412 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
413 |
|
12854 | 414 |
(* Cond *) |
415 |
apply (tactic "smp_tac 3 1") apply (tactic "smp_tac 2 1") |
|
416 |
apply (tactic "smp_tac 1 1") apply (erule impE) |
|
417 |
apply (rule impI,rule exI) |
|
418 |
apply (rule_tac x = "if the_Bool b then T1 else T2" in exI) |
|
419 |
apply (force split add: split_if) |
|
420 |
apply assumption |
|
421 |
||
422 |
(* Body *) |
|
423 |
apply (tactic "sound_forw_hyp_tac 1") |
|
424 |
apply (rule conforms_absorb,assumption) |
|
425 |
||
426 |
(* Lab *) |
|
427 |
apply (tactic "sound_forw_hyp_tac 1") |
|
428 |
apply (rule conforms_absorb,assumption) |
|
429 |
||
430 |
(* If *) |
|
431 |
apply (tactic "sound_forw_hyp_tac 1") |
|
432 |
apply (tactic "sound_forw_hyp_tac 1") |
|
433 |
apply (force split add: split_if) |
|
434 |
||
435 |
(* Throw *) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
436 |
apply (drule (3) evaln_type_sound) |
12854 | 437 |
apply clarsimp |
438 |
apply (drule (3) Throw_lemma) |
|
439 |
apply clarsimp |
|
440 |
||
441 |
(* Try *) |
|
442 |
apply (frule (1) sxalloc_type_sound) |
|
443 |
apply (erule sxalloc_elim_cases2) |
|
444 |
apply (tactic "smp_tac 3 1") |
|
445 |
apply (clarsimp split add: option.split_asm) |
|
446 |
apply (clarsimp split add: option.split_asm) |
|
447 |
apply (tactic "smp_tac 1 1") |
|
448 |
apply (simp only: split add: split_if_asm) |
|
449 |
prefer 2 |
|
450 |
apply (tactic "smp_tac 3 1", erule_tac V = "All ?P" in thin_rl, clarsimp) |
|
451 |
apply (drule spec, erule_tac V = "All ?P" in thin_rl, drule spec, drule spec, |
|
452 |
erule impE, force) |
|
453 |
apply (frule (2) Try_lemma) |
|
454 |
apply clarsimp |
|
455 |
apply (fast elim!: conforms_deallocL) |
|
456 |
||
457 |
(* Fin *) |
|
458 |
apply (tactic "sound_forw_hyp_tac 1") |
|
459 |
apply (case_tac "x1", force) |
|
460 |
apply clarsimp |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
461 |
apply (drule (3) evaln_eval, drule (4) Fin_lemma) |
12854 | 462 |
done |
463 |
||
464 |
||
465 |
||
466 |
declare subst_Bool_def2 [simp] |
|
467 |
||
468 |
theorem ax_sound: |
|
469 |
"wf_prog G \<Longrightarrow> G,(A::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> G,A|\<Turnstile>ts" |
|
470 |
apply (subst ax_valids2_eq [symmetric]) |
|
471 |
apply assumption |
|
472 |
apply (erule (1) ax_sound2) |
|
473 |
done |
|
474 |
||
475 |
||
476 |
end |