author | schirmer |
Fri, 22 Feb 2002 11:26:44 +0100 | |
changeset 12925 | 99131847fb93 |
parent 12859 | f63315dfffd4 |
child 13337 | f75dfc606ac7 |
permissions | -rw-r--r-- |
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 |
|
93 |
apply (erule thin_rl) |
|
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 "init-le" |
|
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 evaln-semantics to the eval-semantics *} |
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 (erule thin_rl) |
|
390 |
apply (erule thin_rl) |
|
391 |
apply (drule split_paired_All [THEN subst]) |
|
392 |
apply (clarsimp elim!: state_not_single) |
|
393 |
done |
|
394 |
||
395 |
||
396 |
lemma MGFn_Loop: |
|
397 |
"\<lbrakk>G,(A::state triple set)\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>};G,A\<turnstile>{=:n} In1r stmnt\<succ> {G\<rightarrow>} \<rbrakk> |
|
398 |
\<Longrightarrow> |
|
399 |
G,A\<turnstile>{=:n} In1r (l\<bullet> While(expr) stmnt)\<succ> {G\<rightarrow>}" |
|
400 |
apply (rule MGFn_NormalI, simp) |
|
401 |
apply (rule_tac p2 = "\<lambda>s. card (nyinitcls G s) \<le> n" in |
|
402 |
MGF_altern [unfolded MGF_def, THEN iffD2, THEN conseq1]) |
|
403 |
prefer 2 |
|
404 |
apply clarsimp |
|
405 |
apply (rule_tac P' = |
|
406 |
"((\<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) |
|
407 |
\<and>. (\<lambda>s. card (nyinitcls G s) \<le> n))" in conseq12) |
|
408 |
prefer 2 |
|
409 |
apply clarsimp |
|
410 |
apply (tactic "smp_tac 1 1", erule_tac V = "All ?P" in thin_rl) |
|
411 |
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) |
|
412 |
apply (force dest!: eval.Loop split add: split_if_asm) |
|
413 |
prefer 2 |
|
414 |
apply (erule MGFnD' [THEN conseq12]) |
|
415 |
apply clarsimp |
|
416 |
apply (erule_tac V = "card (nyinitcls G s') \<le> n" in thin_rl) |
|
417 |
apply (tactic "eval_Force_tac 1") |
|
418 |
apply (erule MGFnD' [THEN conseq12] , clarsimp) |
|
419 |
apply (rule conjI, erule exI) |
|
420 |
apply (tactic "clarsimp_tac eval_css 1") |
|
421 |
apply (case_tac "a") |
|
422 |
prefer 2 |
|
423 |
apply (clarsimp) |
|
424 |
apply (clarsimp split add: split_if) |
|
425 |
apply (rule conjI, (tactic {* force_tac (claset() addSDs [thm "eval.Loop"], |
|
426 |
simpset() addsimps [split_paired_all] addsimprocs [eval_stmt_proc]) 1*})+) |
|
427 |
done |
|
428 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
429 |
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
|
430 |
switch from the evaln-semantics to the eval-semantics *} |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
431 |
lemma MGFn_FVar: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
432 |
"\<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
|
433 |
\<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
|
434 |
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
|
435 |
apply (rule_tac |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
436 |
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
|
437 |
(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
|
438 |
)) \<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
|
439 |
in ax_derivs.FVar) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
440 |
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
|
441 |
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
|
442 |
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
|
443 |
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
|
444 |
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
|
445 |
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
|
446 |
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
|
447 |
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
|
448 |
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
|
449 |
( 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
|
450 |
(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
|
451 |
(s3 = s2'))") |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
452 |
apply (erule exE)+ |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
453 |
apply (erule conjE)+ |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
454 |
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
|
455 |
apply simp |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
456 |
apply simp |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
457 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
458 |
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
|
459 |
apply (rule exI)+ |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
460 |
apply (rule context_conjI) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
461 |
apply force |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
462 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
463 |
apply (rule context_conjI) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
464 |
apply simp |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
465 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
466 |
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
|
467 |
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
|
468 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
469 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
470 |
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
|
471 |
switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call}, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
472 |
@{text MGFn_FVar}*} |
12854 | 473 |
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
|
474 |
"\<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
|
475 |
wf_prog G\<rbrakk> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
476 |
\<Longrightarrow> \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}" |
12854 | 477 |
apply (rule full_nat_induct) |
478 |
apply (rule allI) |
|
479 |
apply (drule_tac x = n in spec) |
|
480 |
apply (drule_tac psi = "All ?P" in asm_rl) |
|
481 |
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>}") |
|
482 |
apply (tactic "Clarify_tac 2") |
|
483 |
apply (induct_tac "t") |
|
484 |
apply (induct_tac "a") |
|
485 |
apply fast+ |
|
486 |
apply (rule var_expr_stmt.induct) |
|
487 |
(* 28 subgoals *) |
|
488 |
prefer 14 apply fast (* Methd *) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
489 |
prefer 13 apply (erule (3) MGFn_Call) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
490 |
prefer 2 apply (drule MGFn_Init,erule (2) MGFn_FVar) |
12854 | 491 |
apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *) |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
492 |
apply (erule_tac [23] MGFn_Init) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
493 |
prefer 18 apply (erule (1) MGFn_Loop) |
12854 | 494 |
apply (tactic "ALLGOALS compl_prepare_tac") |
495 |
||
496 |
apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1") |
|
497 |
||
498 |
apply (rule ax_derivs.AVar) |
|
499 |
apply (erule MGFnD [THEN ax_NormalD]) |
|
500 |
apply (tactic "forw_hyp_eval_Force_tac 1") |
|
501 |
||
502 |
apply (rule ax_derivs.NewC) |
|
503 |
apply (erule MGFn_InitD [THEN conseq2]) |
|
504 |
apply (tactic "eval_Force_tac 1") |
|
505 |
||
506 |
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) |
|
507 |
apply (simp add: init_comp_ty_def split add: split_if) |
|
508 |
apply (rule conjI, clarsimp) |
|
509 |
apply (erule MGFn_InitD [THEN conseq2]) |
|
510 |
apply (tactic "clarsimp_tac eval_css 1") |
|
511 |
apply clarsimp |
|
512 |
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1") |
|
513 |
apply (tactic "forw_hyp_eval_Force_tac 1") |
|
514 |
||
515 |
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast],tactic"eval_Force_tac 1") |
|
516 |
||
517 |
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1") |
|
518 |
apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1") |
|
519 |
apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1") |
|
520 |
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1") |
|
521 |
||
522 |
apply (rule ax_derivs.Ass) |
|
523 |
apply (erule MGFnD [THEN ax_NormalD]) |
|
524 |
apply (tactic "forw_hyp_eval_Force_tac 1") |
|
525 |
||
526 |
apply (rule ax_derivs.Cond) |
|
527 |
apply (erule MGFnD [THEN ax_NormalD]) |
|
528 |
apply (rule allI) |
|
529 |
apply (rule ax_Normal_cases) |
|
530 |
prefer 2 |
|
531 |
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) |
|
532 |
apply (tactic "eval_Force_tac 1") |
|
533 |
apply (case_tac "b") |
|
534 |
apply (simp, tactic "forw_hyp_eval_Force_tac 1") |
|
535 |
apply (simp, tactic "forw_hyp_eval_Force_tac 1") |
|
536 |
||
537 |
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) |
|
538 |
apply (erule MGFn_InitD [THEN conseq2]) |
|
539 |
apply (tactic "eval_Force_tac 1") |
|
540 |
apply (tactic "forw_hyp_tac 1") |
|
541 |
apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *}) |
|
542 |
apply (erule (1) eval.Body) |
|
543 |
||
544 |
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1") |
|
545 |
||
546 |
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1") |
|
547 |
||
548 |
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab]) |
|
549 |
apply (tactic "clarsimp_tac eval_css 1") |
|
550 |
||
551 |
apply (rule ax_derivs.Comp) |
|
552 |
apply (erule MGFnD [THEN ax_NormalD]) |
|
553 |
apply (tactic "forw_hyp_eval_Force_tac 1") |
|
554 |
||
555 |
apply (rule ax_derivs.If) |
|
556 |
apply (erule MGFnD [THEN ax_NormalD]) |
|
557 |
apply (rule allI) |
|
558 |
apply (rule ax_Normal_cases) |
|
559 |
prefer 2 |
|
560 |
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def) |
|
561 |
apply (tactic "eval_Force_tac 1") |
|
562 |
apply (case_tac "b") |
|
563 |
apply (simp, tactic "forw_hyp_eval_Force_tac 1") |
|
564 |
apply (simp, tactic "forw_hyp_eval_Force_tac 1") |
|
565 |
||
566 |
apply (rule ax_derivs.Do [THEN conseq1]) |
|
567 |
apply (tactic {* force_tac (eval_css addsimps2 [thm "abupd_def2"]) 1 *}) |
|
568 |
||
569 |
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw]) |
|
570 |
apply (tactic "clarsimp_tac eval_css 1") |
|
571 |
||
572 |
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) |
|
573 |
apply (tactic "eval_Force_tac 3") |
|
574 |
apply (tactic "forw_hyp_eval_Force_tac 2") |
|
575 |
apply (erule MGFnD [THEN ax_NormalD, THEN conseq2]) |
|
576 |
apply (tactic "clarsimp_tac eval_css 1") |
|
577 |
apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext]) |
|
578 |
||
579 |
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin) |
|
580 |
apply (tactic "forw_hyp_eval_Force_tac 1") |
|
581 |
apply (rule allI) |
|
582 |
apply (tactic "forw_hyp_tac 1") |
|
583 |
apply (tactic {* pair_tac "sb" 1 *}) |
|
584 |
apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1") |
|
585 |
apply (drule (1) eval.Fin) |
|
586 |
apply clarsimp |
|
587 |
||
588 |
apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1") |
|
589 |
||
590 |
apply (rule ax_derivs.Cons) |
|
591 |
apply (erule MGFnD [THEN ax_NormalD]) |
|
592 |
apply (tactic "forw_hyp_eval_Force_tac 1") |
|
593 |
done |
|
594 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
595 |
lemma MGF_asm: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
596 |
"\<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
|
597 |
\<Longrightarrow> G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" |
12854 | 598 |
apply (simp (no_asm_use) add: MGF_MGFn_iff) |
599 |
apply (rule allI) |
|
600 |
apply (rule MGFn_lemma) |
|
601 |
apply (intro strip) |
|
602 |
apply (rule MGFn_free_wt) |
|
603 |
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
|
604 |
apply assumption (* wf_prog G *) |
12854 | 605 |
done |
606 |
||
607 |
declare splitI2 [intro!] |
|
608 |
ML_setup {* |
|
609 |
Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc] |
|
610 |
*} |
|
611 |
||
612 |
||
613 |
section "nested version" |
|
614 |
||
615 |
lemma nesting_lemma' [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; |
|
616 |
!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn}; |
|
617 |
!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}; |
|
618 |
finite U; uA = mgf_call`U |] ==> |
|
619 |
!A. A <= uA --> n <= card uA --> card A = card uA - n --> (!t. P A {mgf t})" |
|
620 |
proof - |
|
621 |
assume ax_derivs_asm: "!!A ts. ts <= A ==> P A ts" |
|
622 |
assume MGF_nested_Methd: "!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) |
|
623 |
{mgf b} ==> P A {mgf_call pn}" |
|
624 |
assume MGF_asm: "!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}" |
|
625 |
assume "finite U" "uA = mgf_call`U" |
|
626 |
then show ?thesis |
|
627 |
apply - |
|
628 |
apply (induct_tac "n") |
|
629 |
apply (tactic "ALLGOALS Clarsimp_tac") |
|
630 |
apply (tactic "dtac (permute_prems 0 1 card_seteq) 1") |
|
631 |
apply simp |
|
632 |
apply (erule finite_imageI) |
|
633 |
apply (simp add: MGF_asm ax_derivs_asm) |
|
634 |
apply (rule MGF_asm) |
|
635 |
apply (rule ballI) |
|
636 |
apply (case_tac "mgf_call pn : A") |
|
637 |
apply (fast intro: ax_derivs_asm) |
|
638 |
apply (rule MGF_nested_Methd) |
|
639 |
apply (rule ballI) |
|
640 |
apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE, |
|
641 |
erule_tac [4] spec) |
|
642 |
apply fast |
|
643 |
apply (erule Suc_leD) |
|
644 |
apply (drule finite_subset) |
|
645 |
apply (erule finite_imageI) |
|
646 |
apply auto |
|
647 |
apply arith |
|
648 |
done |
|
649 |
qed |
|
650 |
||
651 |
lemma nesting_lemma [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; |
|
652 |
!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}; |
|
653 |
!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}; |
|
654 |
finite U |] ==> P {} {mgf t}" |
|
655 |
proof - |
|
656 |
assume 2: "!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}" |
|
657 |
assume 3: "!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}" |
|
658 |
assume "!!A ts. ts <= A ==> P A ts" "finite U" |
|
659 |
then show ?thesis |
|
660 |
apply - |
|
661 |
apply (rule_tac mgf = "mgf" in nesting_lemma') |
|
662 |
apply (erule_tac [2] 2) |
|
663 |
apply (rule_tac [2] 3) |
|
664 |
apply (rule_tac [6] le_refl) |
|
665 |
apply auto |
|
666 |
done |
|
667 |
qed |
|
668 |
||
669 |
lemma MGF_nested_Methd: "\<lbrakk> |
|
670 |
G,insert ({Normal \<doteq>} In1l (Methd C sig) \<succ>{G\<rightarrow>}) A\<turnstile> |
|
671 |
{Normal \<doteq>} In1l (body G C sig) \<succ>{G\<rightarrow>} |
|
672 |
\<rbrakk> \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} In1l (Methd C sig) \<succ>{G\<rightarrow>}" |
|
673 |
apply (unfold MGF_def) |
|
674 |
apply (rule ax_MethdN) |
|
675 |
apply (erule conseq2) |
|
676 |
apply clarsimp |
|
677 |
apply (erule MethdI) |
|
678 |
done |
|
679 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
680 |
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" |
12854 | 681 |
apply (rule MGFNormalI) |
682 |
apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and |
|
683 |
bdy = "\<lambda> (C,sig) .{In1l (body G C sig) }" and |
|
684 |
f = "\<lambda> (C,sig) . In1l (Methd C sig) " in nesting_lemma) |
|
685 |
apply (erule ax_derivs.asm) |
|
686 |
apply (clarsimp simp add: split_tupled_all) |
|
687 |
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
|
688 |
apply (erule_tac [2] finite_is_methd [OF wf_ws_prog]) |
12854 | 689 |
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
|
690 |
apply (auto intro: MGFNormalI) |
12854 | 691 |
done |
692 |
||
693 |
||
694 |
section "simultaneous version" |
|
695 |
||
696 |
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow> |
|
697 |
G,A\<union> (\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ` ms |
|
698 |
|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow> |
|
699 |
G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ` ms" |
|
700 |
apply (unfold MGF_def) |
|
701 |
apply (rule ax_derivs.Methd [unfolded mtriples_def]) |
|
702 |
apply (erule ax_finite_pointwise) |
|
703 |
prefer 2 |
|
704 |
apply (rule ax_derivs.asm) |
|
705 |
apply fast |
|
706 |
apply clarsimp |
|
707 |
apply (rule conseq2) |
|
708 |
apply (erule (1) ax_methods_spec) |
|
709 |
apply clarsimp |
|
710 |
apply (erule eval_Methd) |
|
711 |
done |
|
712 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
713 |
lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow> |
12854 | 714 |
G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) |
715 |
` 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
|
716 |
apply (frule finite_is_methd [OF wf_ws_prog]) |
12854 | 717 |
apply (rule MGF_simult_Methd_lemma) |
718 |
apply assumption |
|
719 |
apply (erule ax_finite_pointwise) |
|
720 |
prefer 2 |
|
721 |
apply (rule ax_derivs.asm) |
|
722 |
apply blast |
|
723 |
apply clarsimp |
|
724 |
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
|
725 |
apply (auto intro: MGFNormalI) |
12854 | 726 |
done |
727 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
728 |
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" |
12854 | 729 |
apply (rule MGF_asm) |
730 |
apply (intro strip) |
|
731 |
apply (rule MGFNormalI) |
|
732 |
apply (rule ax_derivs.weaken) |
|
733 |
apply (erule MGF_simult_Methd) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
734 |
apply auto |
12854 | 735 |
done |
736 |
||
737 |
||
738 |
section "corollaries" |
|
739 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
740 |
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
|
741 |
\<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
|
742 |
apply (cases "normal s") |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
743 |
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
|
744 |
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
|
745 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
746 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
747 |
lemma MGF_complete: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
748 |
"\<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
|
749 |
\<Longrightarrow> G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}" |
12854 | 750 |
apply (rule ax_no_hazard) |
751 |
apply (unfold MGF_def) |
|
752 |
apply (erule conseq12) |
|
753 |
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
|
754 |
apply (blast dest: eval_to_evaln) |
12854 | 755 |
done |
756 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset
|
757 |
theorem ax_complete: "wf_prog G \<Longrightarrow> |
12854 | 758 |
G,{}\<Turnstile>{P::state assn} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}" |
759 |
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
|
760 |
apply (erule (1) MGF_deriv) |
12854 | 761 |
done |
762 |
||
763 |
end |