|
1 header {* Definite Assignment *} |
|
2 |
|
3 theory DefiniteAssignment = WellType: |
|
4 |
|
5 text {* Definite Assignment Analysis (cf. 16) |
|
6 |
|
7 The definite assignment analysis approximates the sets of local |
|
8 variables that will be assigned at a certain point of evaluation, and ensures |
|
9 that we will only read variables which previously were assigned. |
|
10 It should conform to the following idea: |
|
11 If the evaluation of a term completes normally (no abruption (exception, |
|
12 break, continue, return) appeared) , the set of local variables calculated |
|
13 by the analysis is a subset of the |
|
14 variables that were actually assigned during evaluation. |
|
15 |
|
16 To get more precise information about the sets of assigned variables the |
|
17 analysis includes the following optimisations: |
|
18 \begin{itemize} |
|
19 \item Inside of a while loop we also take care of the variables assigned |
|
20 before break statements, since the break causes the while loop to |
|
21 continue normally. |
|
22 \item For conditional statements we take care of constant conditions to |
|
23 statically determine the path of evaluation. |
|
24 \item Inside a distinct path of a conditional statements we know to which |
|
25 boolean value the condition has evaluated to, and so can retrieve more |
|
26 information about the variables assigned during evaluation of the |
|
27 boolean condition. |
|
28 \end{itemize} |
|
29 |
|
30 Since in our model of Java the return values of methods are stored in a local |
|
31 variable we also ensure that every path of (normal) evaluation will assign the |
|
32 result variable, or in the sense of real Java every path ends up in and |
|
33 return instruction. |
|
34 |
|
35 Not covered yet: |
|
36 \begin{itemize} |
|
37 \item analysis of definite unassigned |
|
38 \item special treatment of final fields |
|
39 \end{itemize} |
|
40 *} |
|
41 |
|
42 section {* Correct nesting of jump statements *} |
|
43 |
|
44 text {* For definite assignment it becomes crucial, that jumps (break, |
|
45 continue, return) are nested correctly i.e. a continue jump is nested in a |
|
46 matching while statement, a break jump is nested in a proper label statement, |
|
47 a class initialiser does not terminate abruptly with a return. With this we |
|
48 can for example ensure that evaluation of an expression will never end up |
|
49 with a jump, since no breaks, continues or returns are allowed in an |
|
50 expression. *} |
|
51 |
|
52 consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool" |
|
53 primrec |
|
54 "jumpNestingOkS jmps (Skip) = True" |
|
55 "jumpNestingOkS jmps (Expr e) = True" |
|
56 "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s" |
|
57 "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and> |
|
58 jumpNestingOkS jmps c2)" |
|
59 "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and> |
|
60 jumpNestingOkS jmps c2)" |
|
61 "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c" |
|
62 --{* The label of the while loop only handles continue jumps. Breaks are only |
|
63 handled by @{term Lab} *} |
|
64 "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)" |
|
65 "jumpNestingOkS jmps (Throw e) = True" |
|
66 "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and> |
|
67 jumpNestingOkS jmps c2)" |
|
68 "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and> |
|
69 jumpNestingOkS jmps c2)" |
|
70 "jumpNestingOkS jmps (Init C) = True" |
|
71 --{* wellformedness of the program must enshure that for all initializers |
|
72 jumpNestingOkS {} holds *} |
|
73 --{* Dummy analysis for intermediate smallstep term @{term FinA} *} |
|
74 "jumpNestingOkS jmps (FinA a c) = False" |
|
75 |
|
76 |
|
77 constdefs jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" |
|
78 "jumpNestingOk jmps t \<equiv> (case t of |
|
79 In1 se \<Rightarrow> (case se of |
|
80 Inl e \<Rightarrow> True |
|
81 | Inr s \<Rightarrow> jumpNestingOkS jmps s) |
|
82 | In2 v \<Rightarrow> True |
|
83 | In3 es \<Rightarrow> True)" |
|
84 |
|
85 lemma jumpNestingOk_expr_simp [simp]: "jumpNestingOk jmps (In1l e) = True" |
|
86 by (simp add: jumpNestingOk_def) |
|
87 |
|
88 lemma jumpNestingOk_expr_simp1 [simp]: "jumpNestingOk jmps \<langle>e::expr\<rangle> = True" |
|
89 by (simp add: inj_term_simps) |
|
90 |
|
91 lemma jumpNestingOk_stmt_simp [simp]: |
|
92 "jumpNestingOk jmps (In1r s) = jumpNestingOkS jmps s" |
|
93 by (simp add: jumpNestingOk_def) |
|
94 |
|
95 lemma jumpNestingOk_stmt_simp1 [simp]: |
|
96 "jumpNestingOk jmps \<langle>s::stmt\<rangle> = jumpNestingOkS jmps s" |
|
97 by (simp add: inj_term_simps) |
|
98 |
|
99 lemma jumpNestingOk_var_simp [simp]: "jumpNestingOk jmps (In2 v) = True" |
|
100 by (simp add: jumpNestingOk_def) |
|
101 |
|
102 lemma jumpNestingOk_var_simp1 [simp]: "jumpNestingOk jmps \<langle>v::var\<rangle> = True" |
|
103 by (simp add: inj_term_simps) |
|
104 |
|
105 lemma jumpNestingOk_expr_list_simp [simp]: "jumpNestingOk jmps (In3 es) = True" |
|
106 by (simp add: jumpNestingOk_def) |
|
107 |
|
108 lemma jumpNestingOk_expr_list_simp1 [simp]: |
|
109 "jumpNestingOk jmps \<langle>es::expr list\<rangle> = True" |
|
110 by (simp add: inj_term_simps) |
|
111 |
|
112 |
|
113 |
|
114 section {* Calculation of assigned variables for boolean expressions*} |
|
115 |
|
116 |
|
117 subsection {* Very restricted calculation fallback calculation *} |
|
118 |
|
119 consts the_LVar_name:: "var \<Rightarrow> lname" |
|
120 primrec |
|
121 "the_LVar_name (LVar n) = n" |
|
122 |
|
123 consts assignsE :: "expr \<Rightarrow> lname set" |
|
124 assignsV :: "var \<Rightarrow> lname set" |
|
125 assignsEs:: "expr list \<Rightarrow> lname set" |
|
126 text {* *} |
|
127 primrec |
|
128 "assignsE (NewC c) = {}" |
|
129 "assignsE (NewA t e) = assignsE e" |
|
130 "assignsE (Cast t e) = assignsE e" |
|
131 "assignsE (e InstOf r) = assignsE e" |
|
132 "assignsE (Lit val) = {}" |
|
133 "assignsE (UnOp unop e) = assignsE e" |
|
134 "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr |
|
135 then (assignsE e1) |
|
136 else (assignsE e1) \<union> (assignsE e2))" |
|
137 "assignsE (Super) = {}" |
|
138 "assignsE (Acc v) = assignsV v" |
|
139 "assignsE (v:=e) = (assignsV v) \<union> (assignsE e) \<union> |
|
140 (if \<exists> n. v=(LVar n) then {the_LVar_name v} |
|
141 else {})" |
|
142 "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))" |
|
143 "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) |
|
144 = (assignsE objRef) \<union> (assignsEs args)" |
|
145 -- {* Only dummy analysis for intermediate expressions |
|
146 @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *} |
|
147 "assignsE (Methd C sig) = {}" |
|
148 "assignsE (Body C s) = {}" |
|
149 "assignsE (InsInitE s e) = {}" |
|
150 "assignsE (Callee l e) = {}" |
|
151 |
|
152 "assignsV (LVar n) = {}" |
|
153 "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef" |
|
154 "assignsV (e1.[e2]) = assignsE e1 \<union> assignsE e2" |
|
155 |
|
156 "assignsEs [] = {}" |
|
157 "assignsEs (e#es) = assignsE e \<union> assignsEs es" |
|
158 |
|
159 constdefs assigns:: "term \<Rightarrow> lname set" |
|
160 "assigns t \<equiv> (case t of |
|
161 In1 se \<Rightarrow> (case se of |
|
162 Inl e \<Rightarrow> assignsE e |
|
163 | Inr s \<Rightarrow> {}) |
|
164 | In2 v \<Rightarrow> assignsV v |
|
165 | In3 es \<Rightarrow> assignsEs es)" |
|
166 |
|
167 lemma assigns_expr_simp [simp]: "assigns (In1l e) = assignsE e" |
|
168 by (simp add: assigns_def) |
|
169 |
|
170 lemma assigns_expr_simp1 [simp]: "assigns (\<langle>e\<rangle>) = assignsE e" |
|
171 by (simp add: inj_term_simps) |
|
172 |
|
173 lemma assigns_stmt_simp [simp]: "assigns (In1r s) = {}" |
|
174 by (simp add: assigns_def) |
|
175 |
|
176 lemma assigns_stmt_simp1 [simp]: "assigns (\<langle>s::stmt\<rangle>) = {}" |
|
177 by (simp add: inj_term_simps) |
|
178 |
|
179 lemma assigns_var_simp [simp]: "assigns (In2 v) = assignsV v" |
|
180 by (simp add: assigns_def) |
|
181 |
|
182 lemma assigns_var_simp1 [simp]: "assigns (\<langle>v\<rangle>) = assignsV v" |
|
183 by (simp add: inj_term_simps) |
|
184 |
|
185 lemma assigns_expr_list_simp [simp]: "assigns (In3 es) = assignsEs es" |
|
186 by (simp add: assigns_def) |
|
187 |
|
188 lemma assigns_expr_list_simp1 [simp]: "assigns (\<langle>es\<rangle>) = assignsEs es" |
|
189 by (simp add: inj_term_simps) |
|
190 |
|
191 subsection "Analysis of constant expressions" |
|
192 |
|
193 consts constVal :: "expr \<Rightarrow> val option" |
|
194 primrec |
|
195 "constVal (NewC c) = None" |
|
196 "constVal (NewA t e) = None" |
|
197 "constVal (Cast t e) = None" |
|
198 "constVal (Inst e r) = None" |
|
199 "constVal (Lit val) = Some val" |
|
200 "constVal (UnOp unop e) = (case (constVal e) of |
|
201 None \<Rightarrow> None |
|
202 | Some v \<Rightarrow> Some (eval_unop unop v))" |
|
203 "constVal (BinOp binop e1 e2) = (case (constVal e1) of |
|
204 None \<Rightarrow> None |
|
205 | Some v1 \<Rightarrow> (case (constVal e2) of |
|
206 None \<Rightarrow> None |
|
207 | Some v2 \<Rightarrow> Some (eval_binop |
|
208 binop v1 v2)))" |
|
209 "constVal (Super) = None" |
|
210 "constVal (Acc v) = None" |
|
211 "constVal (Ass v e) = None" |
|
212 "constVal (Cond b e1 e2) = (case (constVal b) of |
|
213 None \<Rightarrow> None |
|
214 | Some bv\<Rightarrow> (case the_Bool bv of |
|
215 True \<Rightarrow> (case (constVal e2) of |
|
216 None \<Rightarrow> None |
|
217 | Some v \<Rightarrow> constVal e1) |
|
218 | False\<Rightarrow> (case (constVal e1) of |
|
219 None \<Rightarrow> None |
|
220 | Some v \<Rightarrow> constVal e2)))" |
|
221 --{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be. |
|
222 It requires that all tree expressions are constant even if we can decide |
|
223 which branch to choose, provided the constant value of @{term b} *} |
|
224 "constVal (Call accC statT mode objRef mn pTs args) = None" |
|
225 "constVal (Methd C sig) = None" |
|
226 "constVal (Body C s) = None" |
|
227 "constVal (InsInitE s e) = None" |
|
228 "constVal (Callee l e) = None" |
|
229 |
|
230 lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]: |
|
231 assumes const: "constVal e = Some v" and |
|
232 hyp_Lit: "\<And> v. P (Lit v)" and |
|
233 hyp_UnOp: "\<And> unop e'. P e' \<Longrightarrow> P (UnOp unop e')" and |
|
234 hyp_BinOp: "\<And> binop e1 e2. \<lbrakk>P e1; P e2\<rbrakk> \<Longrightarrow> P (BinOp binop e1 e2)" and |
|
235 hyp_CondL: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; the_Bool bv; P b; P e1\<rbrakk> |
|
236 \<Longrightarrow> P (b? e1 : e2)" and |
|
237 hyp_CondR: "\<And> b bv e1 e2. \<lbrakk>constVal b = Some bv; \<not>the_Bool bv; P b; P e2\<rbrakk> |
|
238 \<Longrightarrow> P (b? e1 : e2)" |
|
239 shows "P e" |
|
240 proof - |
|
241 have "True" and "\<And> v. constVal e = Some v \<Longrightarrow> P e" and "True" and "True" |
|
242 proof (induct "x::var" and e and "s::stmt" and "es::expr list") |
|
243 case Lit |
|
244 show ?case by (rule hyp_Lit) |
|
245 next |
|
246 case UnOp |
|
247 thus ?case |
|
248 by (auto intro: hyp_UnOp) |
|
249 next |
|
250 case BinOp |
|
251 thus ?case |
|
252 by (auto intro: hyp_BinOp) |
|
253 next |
|
254 case (Cond b e1 e2) |
|
255 then obtain v where v: "constVal (b ? e1 : e2) = Some v" |
|
256 by blast |
|
257 then obtain bv where bv: "constVal b = Some bv" |
|
258 by simp |
|
259 show ?case |
|
260 proof (cases "the_Bool bv") |
|
261 case True |
|
262 with Cond show ?thesis using v bv |
|
263 by (auto intro: hyp_CondL) |
|
264 next |
|
265 case False |
|
266 with Cond show ?thesis using v bv |
|
267 by (auto intro: hyp_CondR) |
|
268 qed |
|
269 qed (simp_all) |
|
270 with const |
|
271 show ?thesis |
|
272 by blast |
|
273 qed |
|
274 |
|
275 lemma assignsE_const_simp: "constVal e = Some v \<Longrightarrow> assignsE e = {}" |
|
276 by (induct rule: constVal_Some_induct) simp_all |
|
277 |
|
278 |
|
279 subsection {* Main analysis for boolean expressions *} |
|
280 |
|
281 text {* Assigned local variables after evaluating the expression if it evaluates |
|
282 to a specific boolean value. If the expression cannot evaluate to a |
|
283 @{term Boolean} value UNIV is returned. If we expect true/false the opposite |
|
284 constant false/true will also lead to UNIV. *} |
|
285 consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set" |
|
286 primrec |
|
287 "assigns_if b (NewC c) = UNIV" --{*can never evaluate to Boolean*} |
|
288 "assigns_if b (NewA t e) = UNIV" --{*can never evaluate to Boolean*} |
|
289 "assigns_if b (Cast t e) = assigns_if b e" |
|
290 "assigns_if b (Inst e r) = assignsE e" --{*Inst has type Boolean but |
|
291 e is a reference type*} |
|
292 "assigns_if b (Lit val) = (if val=Bool b then {} else UNIV)" |
|
293 "assigns_if b (UnOp unop e) = (case constVal (UnOp unop e) of |
|
294 None \<Rightarrow> (if unop = UNot |
|
295 then assigns_if (\<not>b) e |
|
296 else UNIV) |
|
297 | Some v \<Rightarrow> (if v=Bool b |
|
298 then {} |
|
299 else UNIV))" |
|
300 "assigns_if b (BinOp binop e1 e2) |
|
301 = (case constVal (BinOp binop e1 e2) of |
|
302 None \<Rightarrow> (if binop=CondAnd then |
|
303 (case b of |
|
304 True \<Rightarrow> assigns_if True e1 \<union> assigns_if True e2 |
|
305 | False \<Rightarrow> assigns_if False e1 \<inter> |
|
306 (assigns_if True e1 \<union> assigns_if False e2)) |
|
307 else |
|
308 (if binop=CondOr then |
|
309 (case b of |
|
310 True \<Rightarrow> assigns_if True e1 \<inter> |
|
311 (assigns_if False e1 \<union> assigns_if True e2) |
|
312 | False \<Rightarrow> assigns_if False e1 \<union> assigns_if False e2) |
|
313 else assignsE e1 \<union> assignsE e2)) |
|
314 | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))" |
|
315 |
|
316 "assigns_if b (Super) = UNIV" --{*can never evaluate to Boolean*} |
|
317 "assigns_if b (Acc v) = (assignsV v)" |
|
318 "assigns_if b (v := e) = (assignsE (Ass v e))" |
|
319 "assigns_if b (c? e1 : e2) = (assignsE c) \<union> |
|
320 (case (constVal c) of |
|
321 None \<Rightarrow> (assigns_if b e1) \<inter> |
|
322 (assigns_if b e2) |
|
323 | Some bv \<Rightarrow> (case the_Bool bv of |
|
324 True \<Rightarrow> assigns_if b e1 |
|
325 | False \<Rightarrow> assigns_if b e2))" |
|
326 "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) |
|
327 = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) " |
|
328 -- {* Only dummy analysis for intermediate expressions |
|
329 @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *} |
|
330 "assigns_if b (Methd C sig) = {}" |
|
331 "assigns_if b (Body C s) = {}" |
|
332 "assigns_if b (InsInitE s e) = {}" |
|
333 "assigns_if b (Callee l e) = {}" |
|
334 |
|
335 lemma assigns_if_const_b_simp: |
|
336 assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e") |
|
337 shows "assigns_if b e = {}" (is "?Ass b e") |
|
338 proof - |
|
339 have "True" and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and "True" and "True" |
|
340 proof (induct _ and e and _ and _ rule: var_expr_stmt.induct) |
|
341 case Lit |
|
342 thus ?case by simp |
|
343 next |
|
344 case UnOp |
|
345 thus ?case by simp |
|
346 next |
|
347 case (BinOp binop) |
|
348 thus ?case |
|
349 by (cases binop) (simp_all) |
|
350 next |
|
351 case (Cond c e1 e2 b) |
|
352 have hyp_c: "\<And> b. ?Const b c \<Longrightarrow> ?Ass b c" . |
|
353 have hyp_e1: "\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1" . |
|
354 have hyp_e2: "\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2" . |
|
355 have const: "constVal (c ? e1 : e2) = Some (Bool b)" . |
|
356 then obtain bv where bv: "constVal c = Some bv" |
|
357 by simp |
|
358 hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp) |
|
359 show ?case |
|
360 proof (cases "the_Bool bv") |
|
361 case True |
|
362 with const bv |
|
363 have "?Const b e1" by simp |
|
364 hence "?Ass b e1" by (rule hyp_e1) |
|
365 with emptyC bv True |
|
366 show ?thesis |
|
367 by simp |
|
368 next |
|
369 case False |
|
370 with const bv |
|
371 have "?Const b e2" by simp |
|
372 hence "?Ass b e2" by (rule hyp_e2) |
|
373 with emptyC bv False |
|
374 show ?thesis |
|
375 by simp |
|
376 qed |
|
377 qed (simp_all) |
|
378 with boolConst |
|
379 show ?thesis |
|
380 by blast |
|
381 qed |
|
382 |
|
383 lemma assigns_if_const_not_b_simp: |
|
384 assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e") |
|
385 shows "assigns_if (\<not>b) e = UNIV" (is "?Ass b e") |
|
386 proof - |
|
387 have True and "\<And> b. ?Const b e \<Longrightarrow> ?Ass b e" and True and True |
|
388 proof (induct _ and e and _ and _ rule: var_expr_stmt.induct) |
|
389 case Lit |
|
390 thus ?case by simp |
|
391 next |
|
392 case UnOp |
|
393 thus ?case by simp |
|
394 next |
|
395 case (BinOp binop) |
|
396 thus ?case |
|
397 by (cases binop) (simp_all) |
|
398 next |
|
399 case (Cond c e1 e2 b) |
|
400 have hyp_c: "\<And> b. ?Const b c \<Longrightarrow> ?Ass b c" . |
|
401 have hyp_e1: "\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1" . |
|
402 have hyp_e2: "\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2" . |
|
403 have const: "constVal (c ? e1 : e2) = Some (Bool b)" . |
|
404 then obtain bv where bv: "constVal c = Some bv" |
|
405 by simp |
|
406 show ?case |
|
407 proof (cases "the_Bool bv") |
|
408 case True |
|
409 with const bv |
|
410 have "?Const b e1" by simp |
|
411 hence "?Ass b e1" by (rule hyp_e1) |
|
412 with bv True |
|
413 show ?thesis |
|
414 by simp |
|
415 next |
|
416 case False |
|
417 with const bv |
|
418 have "?Const b e2" by simp |
|
419 hence "?Ass b e2" by (rule hyp_e2) |
|
420 with bv False |
|
421 show ?thesis |
|
422 by simp |
|
423 qed |
|
424 qed (simp_all) |
|
425 with boolConst |
|
426 show ?thesis |
|
427 by blast |
|
428 qed |
|
429 |
|
430 subsection {* Lifting set operations to range of tables (map to a set) *} |
|
431 |
|
432 constdefs |
|
433 union_ts:: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" |
|
434 ("_ \<Rightarrow>\<union> _" [67,67] 65) |
|
435 "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k" |
|
436 |
|
437 constdefs |
|
438 intersect_ts:: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" |
|
439 ("_ \<Rightarrow>\<inter> _" [72,72] 71) |
|
440 "A \<Rightarrow>\<inter> B \<equiv> \<lambda> k. A k \<inter> B k" |
|
441 |
|
442 constdefs |
|
443 all_union_ts:: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" |
|
444 (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40) |
|
445 "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B" |
|
446 |
|
447 subsubsection {* Binary union of tables *} |
|
448 |
|
449 lemma union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union> B) k) = (c \<in> A k \<or> c \<in> B k)" |
|
450 by (unfold union_ts_def) blast |
|
451 |
|
452 lemma union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k" |
|
453 by simp |
|
454 |
|
455 lemma union_tsI2 [elim?]: "c \<in> B k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k" |
|
456 by simp |
|
457 |
|
458 lemma union_tsCI [intro!]: "(c \<notin> B k \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union> B) k" |
|
459 by auto |
|
460 |
|
461 lemma union_tsE [elim!]: |
|
462 "\<lbrakk>c \<in> (A \<Rightarrow>\<union> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B k \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P" |
|
463 by (unfold union_ts_def) blast |
|
464 |
|
465 subsubsection {* Binary intersection of tables *} |
|
466 |
|
467 lemma intersect_ts_iff [simp]: "c \<in> (A \<Rightarrow>\<inter> B) k = (c \<in> A k \<and> c \<in> B k)" |
|
468 by (unfold intersect_ts_def) blast |
|
469 |
|
470 lemma intersect_tsI [intro!]: "\<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> c \<in> (A \<Rightarrow>\<inter> B) k" |
|
471 by simp |
|
472 |
|
473 lemma intersect_tsD1: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> A k" |
|
474 by simp |
|
475 |
|
476 lemma intersect_tsD2: "c \<in> (A \<Rightarrow>\<inter> B) k \<Longrightarrow> c \<in> B k" |
|
477 by simp |
|
478 |
|
479 lemma intersect_tsE [elim!]: |
|
480 "\<lbrakk>c \<in> (A \<Rightarrow>\<inter> B) k; \<lbrakk>c \<in> A k; c \<in> B k\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
481 by simp |
|
482 |
|
483 |
|
484 subsubsection {* All-Union of tables and set *} |
|
485 |
|
486 lemma all_union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k) = (c \<in> A k \<or> c \<in> B)" |
|
487 by (unfold all_union_ts_def) blast |
|
488 |
|
489 lemma all_union_tsI1 [elim?]: "c \<in> A k \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k" |
|
490 by simp |
|
491 |
|
492 lemma all_union_tsI2 [elim?]: "c \<in> B \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k" |
|
493 by simp |
|
494 |
|
495 lemma all_union_tsCI [intro!]: "(c \<notin> B \<Longrightarrow> c \<in> A k) \<Longrightarrow> c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k" |
|
496 by auto |
|
497 |
|
498 lemma all_union_tsE [elim!]: |
|
499 "\<lbrakk>c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P" |
|
500 by (unfold all_union_ts_def) blast |
|
501 |
|
502 |
|
503 section "The rules of definite assignment" |
|
504 |
|
505 |
|
506 types breakass = "(label, lname) tables" |
|
507 --{* Mapping from a break label, to the set of variables that will be assigned |
|
508 if the evaluation terminates with this break *} |
|
509 |
|
510 record assigned = |
|
511 nrm :: "lname set" --{* Definetly assigned variables |
|
512 for normal completion*} |
|
513 brk :: "breakass" --{* Definetly assigned variables for |
|
514 abnormal completion with a break *} |
|
515 |
|
516 consts da :: "(env \<times> lname set \<times> term \<times> assigned) set" |
|
517 text {* The environment @{term env} is only needed for the |
|
518 conditional @{text "_ ? _ : _"}. |
|
519 The definite assignment rules refer to the typing rules here to |
|
520 distinguish boolean and other expressions. |
|
521 *} |
|
522 |
|
523 syntax |
|
524 da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" |
|
525 ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71) |
|
526 |
|
527 translations |
|
528 "E\<turnstile> B \<guillemotright>t\<guillemotright> A" == "(E,B,t,A) \<in> da" |
|
529 |
|
530 text {* @{text B}: the ''assigned'' variables before evaluating term @{text t}; |
|
531 @{text A}: the ''assigned'' variables after evaluating term @{text t} |
|
532 *} |
|
533 |
|
534 |
|
535 constdefs rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" |
|
536 "rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x" |
|
537 |
|
538 (* |
|
539 constdefs setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" |
|
540 "setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}" |
|
541 *) |
|
542 |
|
543 constdefs range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) |
|
544 "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}" |
|
545 |
|
546 inductive "da" intros |
|
547 |
|
548 Skip: "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
|
549 |
|
550 Expr: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
|
551 \<Longrightarrow> |
|
552 Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A" |
|
553 Lab: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; nrm A = nrm C \<inter> (brk C) l; brk A = rmlab l (brk C)\<rbrakk> |
|
554 \<Longrightarrow> |
|
555 Env\<turnstile> B \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A" |
|
556 |
|
557 Comp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
|
558 nrm A = nrm C2; brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)\<rbrakk> |
|
559 \<Longrightarrow> |
|
560 Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A" |
|
561 |
|
562 If: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; |
|
563 Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
|
564 Env\<turnstile> (B \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
|
565 nrm A = nrm C1 \<inter> nrm C2; |
|
566 brk A = brk C1 \<Rightarrow>\<inter> brk C2 \<rbrakk> |
|
567 \<Longrightarrow> |
|
568 Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A" |
|
569 |
|
570 --{* Note that @{term E} is not further used, because we take the specialized |
|
571 sets that also consider if the expression evaluates to true or false. |
|
572 Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break |
|
573 map of @{term E} will be the trivial one. So |
|
574 @{term "Env\<turnstile>B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"} is just used to enshure the definite assignment in |
|
575 expression @{term e}. |
|
576 Notice the implicit analysis of a constant boolean expression @{term e} |
|
577 in this rule. For example, if @{term e} is constantly @{term True} then |
|
578 @{term "assigns_if False e = UNIV"} and therefor @{term "nrm C2=UNIV"}. |
|
579 So finally @{term "nrm A = nrm C1"}. For the break maps this trick |
|
580 workd too, because the trival break map will map all labels to |
|
581 @{term UNIV}. In the example, if no break occurs in @{term c2} the break |
|
582 maps will trivially map to @{term UNIV} and if a break occurs it will map |
|
583 to @{term UNIV} too, because @{term "assigns_if False e = UNIV"}. So |
|
584 in the intersection of the break maps the path @{term c2} will have no |
|
585 contribution. |
|
586 *} |
|
587 |
|
588 Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; |
|
589 Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
|
590 nrm A = nrm C \<inter> (B \<union> assigns_if False e); |
|
591 brk A = brk C\<rbrakk> |
|
592 \<Longrightarrow> |
|
593 Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A" |
|
594 --{* The @{text Loop} rule resembles some of the ideas of the @{text If} rule. |
|
595 For the @{term "nrm A"} the set @{term "B \<union> assigns_if False e"} |
|
596 will be @{term UNIV} if the condition is constantly true. To normally exit |
|
597 the while loop, we must consider the body @{term c} to be completed |
|
598 normally (@{term "nrm C"}) or with a break. But in this model, |
|
599 the label @{term l} of the loop |
|
600 only handles continue labels, not break labels. The break label will be |
|
601 handled by an enclosing @{term Lab} statement. So we don't have to |
|
602 handle the breaks specially. |
|
603 *} |
|
604 |
|
605 Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B; |
|
606 nrm A = UNIV; |
|
607 brk A = (case jump of |
|
608 Break l \<Rightarrow> \<lambda> k. if k=l then B else UNIV |
|
609 | Cont l \<Rightarrow> \<lambda> k. UNIV |
|
610 | Ret \<Rightarrow> \<lambda> k. UNIV)\<rbrakk> |
|
611 \<Longrightarrow> |
|
612 Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A" |
|
613 --{* In case of a break to label @{term l} the corresponding break set is all |
|
614 variables assigned before the break. The assigned variables for normal |
|
615 completion of the @{term Jmp} is @{term UNIV}, because the statement will |
|
616 never complete normally. For continue and return the break map is the |
|
617 trivial one. In case of a return we enshure that the result value is |
|
618 assigned. |
|
619 *} |
|
620 |
|
621 Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk> |
|
622 \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A" |
|
623 |
|
624 Try: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
|
625 Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> (B \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
|
626 nrm A = nrm C1 \<inter> nrm C2; |
|
627 brk A = brk C1 \<Rightarrow>\<inter> brk C2\<rbrakk> |
|
628 \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A" |
|
629 |
|
630 Fin: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1; |
|
631 Env\<turnstile> B \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2; |
|
632 nrm A = nrm C1 \<union> nrm C2; |
|
633 brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk> |
|
634 \<Longrightarrow> |
|
635 Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" |
|
636 --{* The set of assigned variables before execution @{term c2} are the same |
|
637 as before execution @{term c1}, because @{term c1} could throw an exception |
|
638 and so we can't guarantee that any variable will be assigned in @{term c1}. |
|
639 The @{text Finally} statement completes |
|
640 normally if both @{term c1} and @{term c2} complete normally. If @{term c1} |
|
641 completes abnormally with a break, then @{term c2} also will be executed |
|
642 and may terminate normally or with a break. The overall break map then is |
|
643 the intersection of the maps of both paths. If @{term c2} terminates |
|
644 normally we have to extend all break sets in @{term "brk C1"} with |
|
645 @{term "nrm C2"} (@{text "\<Rightarrow>\<union>\<^sub>\<forall>"}). If @{term c2} exits with a break this |
|
646 break will appear in the overall result state. We don't know if |
|
647 @{term c1} completed normally or abruptly (maybe with an exception not only |
|
648 a break) so @{term c1} has no contribution to the break map following this |
|
649 path. |
|
650 *} |
|
651 |
|
652 --{* Evaluation of expressions and the break sets of definite assignment: |
|
653 Thinking of a Java expression we assume that we can never have |
|
654 a break statement inside of a expression. So for all expressions the |
|
655 break sets could be set to the trivial one: @{term "\<lambda> l. UNIV"}. |
|
656 But we can't |
|
657 trivially proof, that evaluating an expression will never result in a |
|
658 break, allthough Java expressions allready syntactically don't allow |
|
659 nested stetements in them. The reason are the nested class initialzation |
|
660 statements which are inserted by the evaluation rules. So to proof the |
|
661 absence of a break we need to ensure, that the initialization statements |
|
662 will never end up in a break. In a wellfromed initialization statement, |
|
663 of course, were breaks are nested correctly inside of @{term Lab} |
|
664 or @{term Loop} statements evaluation of the whole initialization |
|
665 statement will never result in a break, because this break will be |
|
666 handled inside of the statement. But for simplicity we haven't added |
|
667 the analysis of the correct nesting of breaks in the typing judgments |
|
668 right now. So we have decided to adjust the rules of definite assignment |
|
669 to fit to these circumstances. If an initialization is involved during |
|
670 evaluation of the expression (evaluation rules @{text FVar}, @{text NewC} |
|
671 and @{text NewA} |
|
672 *} |
|
673 |
|
674 Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
|
675 --{* Wellformedness of a program will ensure, that every static initialiser |
|
676 is definetly assigned and the jumps are nested correctly. The case here |
|
677 for @{term Init} is just for convenience, to get a proper precondition |
|
678 for the induction hypothesis in various proofs, so that we don't have to |
|
679 expand the initialisation on every point where it is triggerred by the |
|
680 evaluation rules. |
|
681 *} |
|
682 NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
|
683 |
|
684 NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
|
685 \<Longrightarrow> |
|
686 Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A" |
|
687 |
|
688 Cast: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
|
689 \<Longrightarrow> |
|
690 Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A" |
|
691 |
|
692 Inst: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
|
693 \<Longrightarrow> |
|
694 Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A" |
|
695 |
|
696 Lit: "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
|
697 |
|
698 UnOp: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
|
699 \<Longrightarrow> |
|
700 Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A" |
|
701 |
|
702 CondAnd: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if True e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
|
703 nrm A = B \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> |
|
704 assigns_if False (BinOp CondAnd e1 e2)); |
|
705 brk A = (\<lambda> l. UNIV) \<rbrakk> |
|
706 \<Longrightarrow> |
|
707 Env\<turnstile> B \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A" |
|
708 |
|
709 CondOr: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> (B \<union> assigns_if False e1) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
|
710 nrm A = B \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> |
|
711 assigns_if False (BinOp CondOr e1 e2)); |
|
712 brk A = (\<lambda> l. UNIV) \<rbrakk> |
|
713 \<Longrightarrow> |
|
714 Env\<turnstile> B \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A" |
|
715 |
|
716 BinOp: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A; |
|
717 binop \<noteq> CondAnd; binop \<noteq> CondOr\<rbrakk> |
|
718 \<Longrightarrow> |
|
719 Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A" |
|
720 |
|
721 Super: "This \<in> B |
|
722 \<Longrightarrow> |
|
723 Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>" |
|
724 |
|
725 AccLVar: "\<lbrakk>vn \<in> B; |
|
726 nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk> |
|
727 \<Longrightarrow> |
|
728 Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A" |
|
729 --{* To properly access a local variable we have to test the definite |
|
730 assignment here. The variable must occur in the set @{term B} |
|
731 *} |
|
732 |
|
733 Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; |
|
734 Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk> |
|
735 \<Longrightarrow> |
|
736 Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A" |
|
737 |
|
738 AssLVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = nrm E \<union> {vn}; brk A = brk E\<rbrakk> |
|
739 \<Longrightarrow> |
|
740 Env\<turnstile> B \<guillemotright>\<langle>(LVar vn) := e\<rangle>\<guillemotright> A" |
|
741 |
|
742 Ass: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn; Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V; Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A\<rbrakk> |
|
743 \<Longrightarrow> |
|
744 Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A" |
|
745 |
|
746 CondBool: "\<lbrakk>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean); |
|
747 Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
|
748 Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; |
|
749 Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
|
750 nrm A = B \<union> (assigns_if True (c ? e1 : e2) \<inter> |
|
751 assigns_if False (c ? e1 : e2)); |
|
752 brk A = (\<lambda> l. UNIV)\<rbrakk> |
|
753 \<Longrightarrow> |
|
754 Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
|
755 |
|
756 Cond: "\<lbrakk>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean); |
|
757 Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; |
|
758 Env\<turnstile> (B \<union> assigns_if True c) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; |
|
759 Env\<turnstile> (B \<union> assigns_if False c) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2; |
|
760 nrm A = nrm E1 \<inter> nrm E2; brk A = (\<lambda> l. UNIV)\<rbrakk> |
|
761 \<Longrightarrow> |
|
762 Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
|
763 |
|
764 Call: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A\<rbrakk> |
|
765 \<Longrightarrow> |
|
766 Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A" |
|
767 |
|
768 -- {* The interplay of @{term Call}, @{term Methd} and @{term Body}: |
|
769 Why rules for @{term Methd} and @{term Body} at all? Note that a |
|
770 Java source program will not include bare @{term Methd} or @{term Body} |
|
771 terms. These terms are just introduced during evaluation. So definite |
|
772 assignment of @{term Call} does not consider @{term Methd} or |
|
773 @{term Body} at all. So for definite assignment alone we could omit the |
|
774 rules for @{term Methd} and @{term Body}. |
|
775 But since evaluation of the method invocation is |
|
776 split up into three rules we must ensure that we have enough information |
|
777 about the call even in the @{term Body} term to make sure that we can |
|
778 proof type safety. Also we must be able transport this information |
|
779 from @{term Call} to @{term Methd} and then further to @{term Body} |
|
780 during evaluation to establish the definite assignment of @{term Methd} |
|
781 during evaluation of @{term Call}, and of @{term Body} during evaluation |
|
782 of @{term Methd}. This is necessary since definite assignment will be |
|
783 a precondition for each induction hypothesis coming out of the evaluation |
|
784 rules, and therefor we have to establish the definite assignment of the |
|
785 sub-evaluation during the type-safety proof. Note that well-typedness is |
|
786 also a precondition for type-safety and so we can omit some assertion |
|
787 that are already ensured by well-typedness. |
|
788 *} |
|
789 Methd: "\<lbrakk>methd (prg Env) D sig = Some m; |
|
790 Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A |
|
791 \<rbrakk> |
|
792 \<Longrightarrow> |
|
793 Env\<turnstile> B \<guillemotright>\<langle>Methd D sig\<rangle>\<guillemotright> A" |
|
794 |
|
795 Body: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C; jumpNestingOkS {Ret} c; Result \<in> nrm C; |
|
796 nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk> |
|
797 \<Longrightarrow> |
|
798 Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A" |
|
799 -- {* Note that @{term A} is not correlated to @{term C}. If the body |
|
800 statement returns abruptly with return, evaluation of @{term Body} |
|
801 will absorb this return and complete normally. So we cannot trivially |
|
802 get the assigned variables of the body statement since it has not |
|
803 completed normally or with a break. |
|
804 If the body completes normally we guarantee that the result variable |
|
805 is set with this rule. But if the body completes abruptly with a return |
|
806 we can't guarantee that the result variable is set here, since |
|
807 definite assignment only talks about normal completion and breaks. So |
|
808 for a return the @{term Jump} rule ensures that the result variable is |
|
809 set and then this information must be carried over to the @{term Body} |
|
810 rule by the conformance predicate of the state. |
|
811 *} |
|
812 LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" |
|
813 |
|
814 FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A |
|
815 \<Longrightarrow> |
|
816 Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" |
|
817 |
|
818 AVar: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1; Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A\<rbrakk> |
|
819 \<Longrightarrow> |
|
820 Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" |
|
821 |
|
822 Nil: "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>" |
|
823 |
|
824 Cons: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e::expr\<rangle>\<guillemotright> E; Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A\<rbrakk> |
|
825 \<Longrightarrow> |
|
826 Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A" |
|
827 |
|
828 |
|
829 declare inj_term_sym_simps [simp] |
|
830 declare assigns_if.simps [simp del] |
|
831 declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
832 ML_setup {* |
|
833 simpset_ref() := simpset() delloop "split_all_tac" |
|
834 *} |
|
835 inductive_cases da_elim_cases [cases set]: |
|
836 "Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" |
|
837 "Env\<turnstile> B \<guillemotright>In1r Skip\<guillemotright> A" |
|
838 "Env\<turnstile> B \<guillemotright>\<langle>Expr e\<rangle>\<guillemotright> A" |
|
839 "Env\<turnstile> B \<guillemotright>In1r (Expr e)\<guillemotright> A" |
|
840 "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> c\<rangle>\<guillemotright> A" |
|
841 "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> c)\<guillemotright> A" |
|
842 "Env\<turnstile> B \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A" |
|
843 "Env\<turnstile> B \<guillemotright>In1r (c1;; c2)\<guillemotright> A" |
|
844 "Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A" |
|
845 "Env\<turnstile> B \<guillemotright>In1r (If(e) c1 Else c2)\<guillemotright> A" |
|
846 "Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A" |
|
847 "Env\<turnstile> B \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A" |
|
848 "Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A" |
|
849 "Env\<turnstile> B \<guillemotright>In1r (Jmp jump)\<guillemotright> A" |
|
850 "Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A" |
|
851 "Env\<turnstile> B \<guillemotright>In1r (Throw e)\<guillemotright> A" |
|
852 "Env\<turnstile> B \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A" |
|
853 "Env\<turnstile> B \<guillemotright>In1r (Try c1 Catch(C vn) c2)\<guillemotright> A" |
|
854 "Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A" |
|
855 "Env\<turnstile> B \<guillemotright>In1r (c1 Finally c2)\<guillemotright> A" |
|
856 "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A" |
|
857 "Env\<turnstile> B \<guillemotright>In1r (Init C)\<guillemotright> A" |
|
858 "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A" |
|
859 "Env\<turnstile> B \<guillemotright>In1l (NewC C)\<guillemotright> A" |
|
860 "Env\<turnstile> B \<guillemotright>\<langle>New T[e]\<rangle>\<guillemotright> A" |
|
861 "Env\<turnstile> B \<guillemotright>In1l (New T[e])\<guillemotright> A" |
|
862 "Env\<turnstile> B \<guillemotright>\<langle>Cast T e\<rangle>\<guillemotright> A" |
|
863 "Env\<turnstile> B \<guillemotright>In1l (Cast T e)\<guillemotright> A" |
|
864 "Env\<turnstile> B \<guillemotright>\<langle>e InstOf T\<rangle>\<guillemotright> A" |
|
865 "Env\<turnstile> B \<guillemotright>In1l (e InstOf T)\<guillemotright> A" |
|
866 "Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A" |
|
867 "Env\<turnstile> B \<guillemotright>In1l (Lit v)\<guillemotright> A" |
|
868 "Env\<turnstile> B \<guillemotright>\<langle>UnOp unop e\<rangle>\<guillemotright> A" |
|
869 "Env\<turnstile> B \<guillemotright>In1l (UnOp unop e)\<guillemotright> A" |
|
870 "Env\<turnstile> B \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A" |
|
871 "Env\<turnstile> B \<guillemotright>In1l (BinOp binop e1 e2)\<guillemotright> A" |
|
872 "Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A" |
|
873 "Env\<turnstile> B \<guillemotright>In1l (Super)\<guillemotright> A" |
|
874 "Env\<turnstile> B \<guillemotright>\<langle>Acc v\<rangle>\<guillemotright> A" |
|
875 "Env\<turnstile> B \<guillemotright>In1l (Acc v)\<guillemotright> A" |
|
876 "Env\<turnstile> B \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A" |
|
877 "Env\<turnstile> B \<guillemotright>In1l (v := e)\<guillemotright> A" |
|
878 "Env\<turnstile> B \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A" |
|
879 "Env\<turnstile> B \<guillemotright>In1l (c ? e1 : e2)\<guillemotright> A" |
|
880 "Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A" |
|
881 "Env\<turnstile> B \<guillemotright>In1l ({accC,statT,mode}e\<cdot>mn({pTs}args))\<guillemotright> A" |
|
882 "Env\<turnstile> B \<guillemotright>\<langle>Methd C sig\<rangle>\<guillemotright> A" |
|
883 "Env\<turnstile> B \<guillemotright>In1l (Methd C sig)\<guillemotright> A" |
|
884 "Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A" |
|
885 "Env\<turnstile> B \<guillemotright>In1l (Body D c)\<guillemotright> A" |
|
886 "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> A" |
|
887 "Env\<turnstile> B \<guillemotright>In2 (LVar vn)\<guillemotright> A" |
|
888 "Env\<turnstile> B \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<guillemotright> A" |
|
889 "Env\<turnstile> B \<guillemotright>In2 ({accC,statDeclC,stat}e..fn)\<guillemotright> A" |
|
890 "Env\<turnstile> B \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A" |
|
891 "Env\<turnstile> B \<guillemotright>In2 (e1.[e2])\<guillemotright> A" |
|
892 "Env\<turnstile> B \<guillemotright>\<langle>[]::expr list\<rangle>\<guillemotright> A" |
|
893 "Env\<turnstile> B \<guillemotright>In3 ([]::expr list)\<guillemotright> A" |
|
894 "Env\<turnstile> B \<guillemotright>\<langle>e#es\<rangle>\<guillemotright> A" |
|
895 "Env\<turnstile> B \<guillemotright>In3 (e#es)\<guillemotright> A" |
|
896 declare inj_term_sym_simps [simp del] |
|
897 declare assigns_if.simps [simp] |
|
898 declare split_paired_All [simp] split_paired_Ex [simp] |
|
899 ML_setup {* |
|
900 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
|
901 *} |
|
902 (* To be able to eliminate both the versions with the overloaded brackets: |
|
903 (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), |
|
904 every rule appears in both versions |
|
905 *) |
|
906 |
|
907 lemma da_Skip: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" |
|
908 by (auto intro: da.Skip) |
|
909 |
|
910 lemma da_NewC: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> A" |
|
911 by (auto intro: da.NewC) |
|
912 |
|
913 lemma da_Lit: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Lit v\<rangle>\<guillemotright> A" |
|
914 by (auto intro: da.Lit) |
|
915 |
|
916 lemma da_Super: "\<lbrakk>This \<in> B;A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>\<rbrakk> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Super\<rangle>\<guillemotright> A" |
|
917 by (auto intro: da.Super) |
|
918 |
|
919 lemma da_Init: "A = \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr> \<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> A" |
|
920 by (auto intro: da.Init) |
|
921 |
|
922 |
|
923 (* |
|
924 For boolean expressions: |
|
925 |
|
926 The following holds: "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" |
|
927 but not vice versa: |
|
928 "assigns_if True e \<inter> assigns_if False e \<subseteq> assignsE e" |
|
929 |
|
930 Example: |
|
931 e = ((x < 5) || (y = true)) && (y = true) |
|
932 |
|
933 = ( a || b ) && c |
|
934 |
|
935 assigns_if True a = {} |
|
936 assigns_if False a = {} |
|
937 |
|
938 assigns_if True b = {y} |
|
939 assigns_if False b = {y} |
|
940 |
|
941 assigns_if True c = {y} |
|
942 assigns_if False c = {y} |
|
943 |
|
944 assigns_if True (a || b) = assigns_if True a \<inter> |
|
945 (assigns_if False a \<union> assigns_if True b) |
|
946 = {} \<inter> ({} \<union> {y}) = {} |
|
947 assigns_if False (a || b) = assigns_if False a \<union> assigns_if False b |
|
948 = {} \<union> {y} = {y} |
|
949 |
|
950 |
|
951 |
|
952 assigns_ifE True e = assigns_if True (a || b) \<union> assigns_if True c |
|
953 = {} \<union> {y} = {y} |
|
954 assigns_ifE False e = assigns_if False (a || b) \<inter> |
|
955 (assigns_if True (a || b) \<union> assigns_if False c) |
|
956 = {y} \<inter> ({} \<union> {y}) = {y} |
|
957 |
|
958 assignsE e = {} |
|
959 *) |
|
960 |
|
961 lemma assignsE_subseteq_assigns_ifs: |
|
962 assumes boolEx: "E\<turnstile>e\<Colon>-PrimT Boolean" (is "?Boolean e") |
|
963 shows "assignsE e \<subseteq> assigns_if True e \<inter> assigns_if False e" (is "?Incl e") |
|
964 proof - |
|
965 have True and "?Boolean e \<Longrightarrow> ?Incl e" and True and True |
|
966 proof (induct _ and e and _ and _ rule: var_expr_stmt.induct) |
|
967 case (Cast T e) |
|
968 have "E\<turnstile>e\<Colon>- (PrimT Boolean)" |
|
969 proof - |
|
970 have "E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)" . |
|
971 then obtain Te where "E\<turnstile>e\<Colon>-Te" |
|
972 "prg E\<turnstile>Te\<preceq>? PrimT Boolean" |
|
973 by cases simp |
|
974 thus ?thesis |
|
975 by - (drule cast_Boolean2,simp) |
|
976 qed |
|
977 with Cast.hyps |
|
978 show ?case |
|
979 by simp |
|
980 next |
|
981 case (Lit val) |
|
982 thus ?case |
|
983 by - (erule wt_elim_cases, cases "val", auto simp add: empty_dt_def) |
|
984 next |
|
985 case (UnOp unop e) |
|
986 thus ?case |
|
987 by - (erule wt_elim_cases,cases unop, |
|
988 (fastsimp simp add: assignsE_const_simp)+) |
|
989 next |
|
990 case (BinOp binop e1 e2) |
|
991 from BinOp.prems obtain e1T e2T |
|
992 where "E\<turnstile>e1\<Colon>-e1T" and "E\<turnstile>e2\<Colon>-e2T" and "wt_binop (prg E) binop e1T e2T" |
|
993 and "(binop_type binop) = Boolean" |
|
994 by (elim wt_elim_cases) simp |
|
995 with BinOp.hyps |
|
996 show ?case |
|
997 by - (cases binop, auto simp add: assignsE_const_simp) |
|
998 next |
|
999 case (Cond c e1 e2) |
|
1000 have hyp_c: "?Boolean c \<Longrightarrow> ?Incl c" . |
|
1001 have hyp_e1: "?Boolean e1 \<Longrightarrow> ?Incl e1" . |
|
1002 have hyp_e2: "?Boolean e2 \<Longrightarrow> ?Incl e2" . |
|
1003 have wt: "E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean" . |
|
1004 then obtain |
|
1005 boolean_c: "E\<turnstile>c\<Colon>-PrimT Boolean" and |
|
1006 boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and |
|
1007 boolean_e2: "E\<turnstile>e2\<Colon>-PrimT Boolean" |
|
1008 by (elim wt_elim_cases) (auto dest: widen_Boolean2) |
|
1009 show ?case |
|
1010 proof (cases "constVal c") |
|
1011 case None |
|
1012 with boolean_e1 boolean_e2 |
|
1013 show ?thesis |
|
1014 using hyp_e1 hyp_e2 |
|
1015 by (auto) |
|
1016 next |
|
1017 case (Some bv) |
|
1018 show ?thesis |
|
1019 proof (cases "the_Bool bv") |
|
1020 case True |
|
1021 with Some show ?thesis using hyp_e1 boolean_e1 by auto |
|
1022 next |
|
1023 case False |
|
1024 with Some show ?thesis using hyp_e2 boolean_e2 by auto |
|
1025 qed |
|
1026 qed |
|
1027 qed simp_all |
|
1028 with boolEx |
|
1029 show ?thesis |
|
1030 by blast |
|
1031 qed |
|
1032 |
|
1033 |
|
1034 (* Trick: |
|
1035 If you have a rule with the abstract term injections: |
|
1036 e.g: da.Skip "B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" |
|
1037 and the current goal state as an concrete injection: |
|
1038 e.g: "B \<guillemotright>In1r Skip\<guillemotright> A" |
|
1039 you can convert the rule by: da.Skip [simplified] |
|
1040 if inj_term_simps is in the simpset |
|
1041 |
|
1042 *) |
|
1043 |
|
1044 lemma rmlab_same_label [simp]: "(rmlab l A) l = UNIV" |
|
1045 by (simp add: rmlab_def) |
|
1046 |
|
1047 lemma rmlab_same_label1 [simp]: "l=l' \<Longrightarrow> (rmlab l A) l' = UNIV" |
|
1048 by (simp add: rmlab_def) |
|
1049 |
|
1050 lemma rmlab_other_label [simp]: "l\<noteq>l'\<Longrightarrow> (rmlab l A) l' = A l'" |
|
1051 by (auto simp add: rmlab_def) |
|
1052 |
|
1053 lemma range_inter_ts_subseteq [intro]: "\<forall> k. A k \<subseteq> B k \<Longrightarrow> \<Rightarrow>\<Inter>A \<subseteq> \<Rightarrow>\<Inter>B" |
|
1054 by (auto simp add: range_inter_ts_def) |
|
1055 |
|
1056 lemma range_inter_ts_subseteq': |
|
1057 "\<lbrakk>\<forall> k. A k \<subseteq> B k; x \<in> \<Rightarrow>\<Inter>A\<rbrakk> \<Longrightarrow> x \<in> \<Rightarrow>\<Inter>B" |
|
1058 by (auto simp add: range_inter_ts_def) |
|
1059 |
|
1060 lemma da_monotone: |
|
1061 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and |
|
1062 subseteq_B_B': "B \<subseteq> B'" and |
|
1063 da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" |
|
1064 shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))" |
|
1065 proof - |
|
1066 from da |
|
1067 show "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> |
|
1068 \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))" |
|
1069 (is "PROP ?Hyp Env B t A") |
|
1070 proof (induct) |
|
1071 case Skip |
|
1072 from Skip.prems Skip.hyps |
|
1073 show ?case by cases simp |
|
1074 next |
|
1075 case Expr |
|
1076 from Expr.prems Expr.hyps |
|
1077 show ?case by cases simp |
|
1078 next |
|
1079 case (Lab A B C Env c l B' A') |
|
1080 have A: "nrm A = nrm C \<inter> brk C l" "brk A = rmlab l (brk C)" . |
|
1081 have "PROP ?Hyp Env B \<langle>c\<rangle> C" . |
|
1082 moreover |
|
1083 have "B \<subseteq> B'" . |
|
1084 moreover |
|
1085 obtain C' |
|
1086 where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
|
1087 and A': "nrm A' = nrm C' \<inter> brk C' l" "brk A' = rmlab l (brk C')" |
|
1088 using Lab.prems |
|
1089 by - (erule da_elim_cases,simp) |
|
1090 ultimately |
|
1091 have "nrm C \<subseteq> nrm C'" and hyp_brk: "(\<forall>l. brk C l \<subseteq> brk C' l)" by auto |
|
1092 then |
|
1093 have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto |
|
1094 moreover |
|
1095 { |
|
1096 fix l' |
|
1097 from hyp_brk |
|
1098 have "rmlab l (brk C) l' \<subseteq> rmlab l (brk C') l'" |
|
1099 by (cases "l=l'") simp_all |
|
1100 } |
|
1101 moreover note A A' |
|
1102 ultimately show ?case |
|
1103 by simp |
|
1104 next |
|
1105 case (Comp A B C1 C2 Env c1 c2 B' A') |
|
1106 have A: "nrm A = nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2" . |
|
1107 have "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'" . |
|
1108 then obtain C1' C2' |
|
1109 where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
|
1110 da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
|
1111 A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
|
1112 by (rule da_elim_cases) auto |
|
1113 have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" . |
|
1114 moreover have "B \<subseteq> B'" . |
|
1115 moreover note da_c1 |
|
1116 ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
|
1117 by (auto) |
|
1118 have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2" . |
|
1119 with da_c2 C1' |
|
1120 have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)" |
|
1121 by (auto) |
|
1122 with A A' C1' |
|
1123 show ?case |
|
1124 by auto |
|
1125 next |
|
1126 case (If A B C1 C2 E Env c1 c2 e B' A') |
|
1127 have A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2" . |
|
1128 have "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'" . |
|
1129 then obtain C1' C2' |
|
1130 where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
|
1131 da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
|
1132 A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
|
1133 by (rule da_elim_cases) auto |
|
1134 have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1" . |
|
1135 moreover have B': "B \<subseteq> B'" . |
|
1136 moreover note da_c1 |
|
1137 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
|
1138 by blast |
|
1139 have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2" . |
|
1140 with da_c2 B' |
|
1141 obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)" |
|
1142 by blast |
|
1143 with A A' C1' |
|
1144 show ?case |
|
1145 by auto |
|
1146 next |
|
1147 case (Loop A B C E Env c e l B' A') |
|
1148 have A: "nrm A = nrm C \<inter> (B \<union> assigns_if False e)" |
|
1149 "brk A = brk C" . |
|
1150 have "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" . |
|
1151 then obtain C' |
|
1152 where |
|
1153 da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and |
|
1154 A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)" |
|
1155 "brk A' = brk C'" |
|
1156 by (rule da_elim_cases) auto |
|
1157 have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C" . |
|
1158 moreover have B': "B \<subseteq> B'" . |
|
1159 moreover note da_c' |
|
1160 ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)" |
|
1161 by blast |
|
1162 with A A' B' |
|
1163 have "nrm A \<subseteq> nrm A'" |
|
1164 by blast |
|
1165 moreover |
|
1166 { fix l' |
|
1167 have "brk A l' \<subseteq> brk A' l'" |
|
1168 proof (cases "constVal e") |
|
1169 case None |
|
1170 with A A' C' |
|
1171 show ?thesis |
|
1172 by (cases "l=l'") auto |
|
1173 next |
|
1174 case (Some bv) |
|
1175 with A A' C' |
|
1176 show ?thesis |
|
1177 by (cases "the_Bool bv", cases "l=l'") auto |
|
1178 qed |
|
1179 } |
|
1180 ultimately show ?case |
|
1181 by auto |
|
1182 next |
|
1183 case (Jmp A B Env jump B' A') |
|
1184 thus ?case by (elim da_elim_cases) (auto split: jump.splits) |
|
1185 next |
|
1186 case Throw thus ?case by - (erule da_elim_cases, auto) |
|
1187 next |
|
1188 case (Try A B C C1 C2 Env c1 c2 vn B' A') |
|
1189 have A: "nrm A = nrm C1 \<inter> nrm C2" |
|
1190 "brk A = brk C1 \<Rightarrow>\<inter> brk C2" . |
|
1191 have "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'" . |
|
1192 then obtain C1' C2' |
|
1193 where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
|
1194 da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} |
|
1195 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
|
1196 A': "nrm A' = nrm C1' \<inter> nrm C2'" |
|
1197 "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'" |
|
1198 by (rule da_elim_cases) auto |
|
1199 have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" . |
|
1200 moreover have B': "B \<subseteq> B'" . |
|
1201 moreover note da_c1' |
|
1202 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
|
1203 by blast |
|
1204 have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) |
|
1205 (B \<union> {VName vn}) \<langle>c2\<rangle> C2" . |
|
1206 with B' da_c2' |
|
1207 obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)" |
|
1208 by blast |
|
1209 with C1' A A' |
|
1210 show ?case |
|
1211 by auto |
|
1212 next |
|
1213 case (Fin A B C1 C2 Env c1 c2 B' A') |
|
1214 have A: "nrm A = nrm C1 \<union> nrm C2" |
|
1215 "brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)" . |
|
1216 have "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'" . |
|
1217 then obtain C1' C2' |
|
1218 where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and |
|
1219 da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and |
|
1220 A': "nrm A' = nrm C1' \<union> nrm C2'" |
|
1221 "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')" |
|
1222 by (rule da_elim_cases) auto |
|
1223 have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" . |
|
1224 moreover have B': "B \<subseteq> B'" . |
|
1225 moreover note da_c1' |
|
1226 ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)" |
|
1227 by blast |
|
1228 have hyp_c2: "PROP ?Hyp Env B \<langle>c2\<rangle> C2" . |
|
1229 from da_c2' B' |
|
1230 obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)" |
|
1231 by - (drule hyp_c2,auto) |
|
1232 with A A' C1' |
|
1233 show ?case |
|
1234 by auto |
|
1235 next |
|
1236 case Init thus ?case by - (erule da_elim_cases, auto) |
|
1237 next |
|
1238 case NewC thus ?case by - (erule da_elim_cases, auto) |
|
1239 next |
|
1240 case NewA thus ?case by - (erule da_elim_cases, auto) |
|
1241 next |
|
1242 case Cast thus ?case by - (erule da_elim_cases, auto) |
|
1243 next |
|
1244 case Inst thus ?case by - (erule da_elim_cases, auto) |
|
1245 next |
|
1246 case Lit thus ?case by - (erule da_elim_cases, auto) |
|
1247 next |
|
1248 case UnOp thus ?case by - (erule da_elim_cases, auto) |
|
1249 next |
|
1250 case (CondAnd A B E1 E2 Env e1 e2 B' A') |
|
1251 have A: "nrm A = B \<union> |
|
1252 assigns_if True (BinOp CondAnd e1 e2) \<inter> |
|
1253 assigns_if False (BinOp CondAnd e1 e2)" |
|
1254 "brk A = (\<lambda>l. UNIV)" . |
|
1255 have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'" . |
|
1256 then obtain A': "nrm A' = B' \<union> |
|
1257 assigns_if True (BinOp CondAnd e1 e2) \<inter> |
|
1258 assigns_if False (BinOp CondAnd e1 e2)" |
|
1259 "brk A' = (\<lambda>l. UNIV)" |
|
1260 by (rule da_elim_cases) auto |
|
1261 have B': "B \<subseteq> B'" . |
|
1262 with A A' show ?case |
|
1263 by auto |
|
1264 next |
|
1265 case CondOr thus ?case by - (erule da_elim_cases, auto) |
|
1266 next |
|
1267 case BinOp thus ?case by - (erule da_elim_cases, auto) |
|
1268 next |
|
1269 case Super thus ?case by - (erule da_elim_cases, auto) |
|
1270 next |
|
1271 case AccLVar thus ?case by - (erule da_elim_cases, auto) |
|
1272 next |
|
1273 case Acc thus ?case by - (erule da_elim_cases, auto) |
|
1274 next |
|
1275 case AssLVar thus ?case by - (erule da_elim_cases, auto) |
|
1276 next |
|
1277 case Ass thus ?case by - (erule da_elim_cases, auto) |
|
1278 next |
|
1279 case (CondBool A B C E1 E2 Env c e1 e2 B' A') |
|
1280 have A: "nrm A = B \<union> |
|
1281 assigns_if True (c ? e1 : e2) \<inter> |
|
1282 assigns_if False (c ? e1 : e2)" |
|
1283 "brk A = (\<lambda>l. UNIV)" . |
|
1284 have "Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" . |
|
1285 moreover |
|
1286 have "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" . |
|
1287 ultimately |
|
1288 obtain A': "nrm A' = B' \<union> |
|
1289 assigns_if True (c ? e1 : e2) \<inter> |
|
1290 assigns_if False (c ? e1 : e2)" |
|
1291 "brk A' = (\<lambda>l. UNIV)" |
|
1292 by - (erule da_elim_cases,auto simp add: inj_term_simps) |
|
1293 (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *) |
|
1294 have B': "B \<subseteq> B'" . |
|
1295 with A A' show ?case |
|
1296 by auto |
|
1297 next |
|
1298 case (Cond A B C E1 E2 Env c e1 e2 B' A') |
|
1299 have A: "nrm A = nrm E1 \<inter> nrm E2" |
|
1300 "brk A = (\<lambda>l. UNIV)" . |
|
1301 have not_bool: "\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" . |
|
1302 have "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" . |
|
1303 then obtain E1' E2' |
|
1304 where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and |
|
1305 da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and |
|
1306 A': "nrm A' = nrm E1' \<inter> nrm E2'" |
|
1307 "brk A' = (\<lambda>l. UNIV)" |
|
1308 using not_bool |
|
1309 by - (erule da_elim_cases, auto simp add: inj_term_simps) |
|
1310 (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *) |
|
1311 have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1" . |
|
1312 moreover have B': "B \<subseteq> B'" . |
|
1313 moreover note da_e1' |
|
1314 ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)" |
|
1315 by blast |
|
1316 have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2" . |
|
1317 with B' da_e2' |
|
1318 obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)" |
|
1319 by blast |
|
1320 with E1' A A' |
|
1321 show ?case |
|
1322 by auto |
|
1323 next |
|
1324 case Call |
|
1325 from Call.prems and Call.hyps |
|
1326 show ?case by cases auto |
|
1327 next |
|
1328 case Methd thus ?case by - (erule da_elim_cases, auto) |
|
1329 next |
|
1330 case Body thus ?case by - (erule da_elim_cases, auto) |
|
1331 next |
|
1332 case LVar thus ?case by - (erule da_elim_cases, auto) |
|
1333 next |
|
1334 case FVar thus ?case by - (erule da_elim_cases, auto) |
|
1335 next |
|
1336 case AVar thus ?case by - (erule da_elim_cases, auto) |
|
1337 next |
|
1338 case Nil thus ?case by - (erule da_elim_cases, auto) |
|
1339 next |
|
1340 case Cons thus ?case by - (erule da_elim_cases, auto) |
|
1341 qed |
|
1342 qed |
|
1343 |
|
1344 lemma da_weaken: |
|
1345 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and |
|
1346 subseteq_B_B': "B \<subseteq> B'" |
|
1347 shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'" |
|
1348 proof - |
|
1349 note assigned.select_convs [CPure.intro] |
|
1350 from da |
|
1351 show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t") |
|
1352 proof (induct) |
|
1353 case Skip thus ?case by (rules intro: da.Skip) |
|
1354 next |
|
1355 case Expr thus ?case by (rules intro: da.Expr) |
|
1356 next |
|
1357 case (Lab A B C Env c l B') |
|
1358 have "PROP ?Hyp Env B \<langle>c\<rangle>" . |
|
1359 moreover |
|
1360 have B': "B \<subseteq> B'" . |
|
1361 ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
|
1362 by rules |
|
1363 then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'" |
|
1364 by (rules intro: da.Lab) |
|
1365 thus ?case .. |
|
1366 next |
|
1367 case (Comp A B C1 C2 Env c1 c2 B') |
|
1368 have da_c1: "Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" . |
|
1369 have "PROP ?Hyp Env B \<langle>c1\<rangle>" . |
|
1370 moreover |
|
1371 have B': "B \<subseteq> B'" . |
|
1372 ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" |
|
1373 by rules |
|
1374 with da_c1 B' |
|
1375 have |
|
1376 "nrm C1 \<subseteq> nrm C1'" |
|
1377 by (rule da_monotone [elim_format]) simp |
|
1378 moreover |
|
1379 have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>" . |
|
1380 ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" |
|
1381 by rules |
|
1382 with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'" |
|
1383 by (rules intro: da.Comp) |
|
1384 thus ?case .. |
|
1385 next |
|
1386 case (If A B C1 C2 E Env c1 c2 e B') |
|
1387 have B': "B \<subseteq> B'" . |
|
1388 obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
|
1389 proof - |
|
1390 have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps) |
|
1391 with B' |
|
1392 show ?thesis using that by rules |
|
1393 qed |
|
1394 moreover |
|
1395 obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" |
|
1396 proof - |
|
1397 from B' |
|
1398 have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)" |
|
1399 by blast |
|
1400 moreover |
|
1401 have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps) |
|
1402 ultimately |
|
1403 show ?thesis using that by rules |
|
1404 qed |
|
1405 moreover |
|
1406 obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" |
|
1407 proof - |
|
1408 from B' have "(B \<union> assigns_if False e) \<subseteq> (B' \<union> assigns_if False e)" |
|
1409 by blast |
|
1410 moreover |
|
1411 have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps) |
|
1412 ultimately |
|
1413 show ?thesis using that by rules |
|
1414 qed |
|
1415 ultimately |
|
1416 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'" |
|
1417 by (rules intro: da.If) |
|
1418 thus ?case .. |
|
1419 next |
|
1420 case (Loop A B C E Env c e l B') |
|
1421 have B': "B \<subseteq> B'" . |
|
1422 obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
|
1423 proof - |
|
1424 have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps) |
|
1425 with B' |
|
1426 show ?thesis using that by rules |
|
1427 qed |
|
1428 moreover |
|
1429 obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
|
1430 proof - |
|
1431 from B' |
|
1432 have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)" |
|
1433 by blast |
|
1434 moreover |
|
1435 have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps) |
|
1436 ultimately |
|
1437 show ?thesis using that by rules |
|
1438 qed |
|
1439 ultimately |
|
1440 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" |
|
1441 by (rules intro: da.Loop ) |
|
1442 thus ?case .. |
|
1443 next |
|
1444 case (Jmp A B Env jump B') |
|
1445 have B': "B \<subseteq> B'" . |
|
1446 with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' " |
|
1447 by auto |
|
1448 moreover |
|
1449 obtain A'::assigned |
|
1450 where "nrm A' = UNIV" |
|
1451 "brk A' = (case jump of |
|
1452 Break l \<Rightarrow> \<lambda>k. if k = l then B' else UNIV |
|
1453 | Cont l \<Rightarrow> \<lambda>k. UNIV |
|
1454 | Ret \<Rightarrow> \<lambda>k. UNIV)" |
|
1455 |
|
1456 by rules |
|
1457 ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'" |
|
1458 by (rule da.Jmp) |
|
1459 thus ?case .. |
|
1460 next |
|
1461 case Throw thus ?case by (rules intro: da.Throw ) |
|
1462 next |
|
1463 case (Try A B C C1 C2 Env c1 c2 vn B') |
|
1464 have B': "B \<subseteq> B'" . |
|
1465 obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" |
|
1466 proof - |
|
1467 have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps) |
|
1468 with B' |
|
1469 show ?thesis using that by rules |
|
1470 qed |
|
1471 moreover |
|
1472 obtain C2' where |
|
1473 "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" |
|
1474 proof - |
|
1475 from B' have "B \<union> {VName vn} \<subseteq> B' \<union> {VName vn}" by blast |
|
1476 moreover |
|
1477 have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) |
|
1478 (B \<union> {VName vn}) \<langle>c2\<rangle>" |
|
1479 by (rule Try.hyps) |
|
1480 ultimately |
|
1481 show ?thesis using that by rules |
|
1482 qed |
|
1483 ultimately |
|
1484 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'" |
|
1485 by (rules intro: da.Try ) |
|
1486 thus ?case .. |
|
1487 next |
|
1488 case (Fin A B C1 C2 Env c1 c2 B') |
|
1489 have B': "B \<subseteq> B'" . |
|
1490 obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" |
|
1491 proof - |
|
1492 have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps) |
|
1493 with B' |
|
1494 show ?thesis using that by rules |
|
1495 qed |
|
1496 moreover |
|
1497 obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" |
|
1498 proof - |
|
1499 have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps) |
|
1500 with B' |
|
1501 show ?thesis using that by rules |
|
1502 qed |
|
1503 ultimately |
|
1504 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'" |
|
1505 by (rules intro: da.Fin ) |
|
1506 thus ?case .. |
|
1507 next |
|
1508 case Init thus ?case by (rules intro: da.Init) |
|
1509 next |
|
1510 case NewC thus ?case by (rules intro: da.NewC) |
|
1511 next |
|
1512 case NewA thus ?case by (rules intro: da.NewA) |
|
1513 next |
|
1514 case Cast thus ?case by (rules intro: da.Cast) |
|
1515 next |
|
1516 case Inst thus ?case by (rules intro: da.Inst) |
|
1517 next |
|
1518 case Lit thus ?case by (rules intro: da.Lit) |
|
1519 next |
|
1520 case UnOp thus ?case by (rules intro: da.UnOp) |
|
1521 next |
|
1522 case (CondAnd A B E1 E2 Env e1 e2 B') |
|
1523 have B': "B \<subseteq> B'" . |
|
1524 obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" |
|
1525 proof - |
|
1526 have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps) |
|
1527 with B' |
|
1528 show ?thesis using that by rules |
|
1529 qed |
|
1530 moreover |
|
1531 obtain E2' where "Env\<turnstile> B' \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" |
|
1532 proof - |
|
1533 from B' have "B \<union> assigns_if True e1 \<subseteq> B' \<union> assigns_if True e1" |
|
1534 by blast |
|
1535 moreover |
|
1536 have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps) |
|
1537 ultimately show ?thesis using that by rules |
|
1538 qed |
|
1539 ultimately |
|
1540 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'" |
|
1541 by (rules intro: da.CondAnd) |
|
1542 thus ?case .. |
|
1543 next |
|
1544 case (CondOr A B E1 E2 Env e1 e2 B') |
|
1545 have B': "B \<subseteq> B'" . |
|
1546 obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" |
|
1547 proof - |
|
1548 have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps) |
|
1549 with B' |
|
1550 show ?thesis using that by rules |
|
1551 qed |
|
1552 moreover |
|
1553 obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" |
|
1554 proof - |
|
1555 from B' have "B \<union> assigns_if False e1 \<subseteq> B' \<union> assigns_if False e1" |
|
1556 by blast |
|
1557 moreover |
|
1558 have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps) |
|
1559 ultimately show ?thesis using that by rules |
|
1560 qed |
|
1561 ultimately |
|
1562 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'" |
|
1563 by (rules intro: da.CondOr) |
|
1564 thus ?case .. |
|
1565 next |
|
1566 case (BinOp A B E1 Env binop e1 e2 B') |
|
1567 have B': "B \<subseteq> B'" . |
|
1568 obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" |
|
1569 proof - |
|
1570 have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps) |
|
1571 with B' |
|
1572 show ?thesis using that by rules |
|
1573 qed |
|
1574 moreover |
|
1575 obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" |
|
1576 proof - |
|
1577 have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule BinOp.hyps) |
|
1578 from this B' E1' |
|
1579 have "nrm E1 \<subseteq> nrm E1'" |
|
1580 by (rule da_monotone [THEN conjE]) |
|
1581 moreover |
|
1582 have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps) |
|
1583 ultimately show ?thesis using that by rules |
|
1584 qed |
|
1585 ultimately |
|
1586 have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'" |
|
1587 using BinOp.hyps by (rules intro: da.BinOp) |
|
1588 thus ?case .. |
|
1589 next |
|
1590 case (Super B Env B') |
|
1591 have B': "B \<subseteq> B'" . |
|
1592 with Super.hyps have "This \<in> B' " |
|
1593 by auto |
|
1594 thus ?case by (rules intro: da.Super) |
|
1595 next |
|
1596 case (AccLVar A B Env vn B') |
|
1597 have "vn \<in> B" . |
|
1598 moreover |
|
1599 have "B \<subseteq> B'" . |
|
1600 ultimately have "vn \<in> B'" by auto |
|
1601 thus ?case by (rules intro: da.AccLVar) |
|
1602 next |
|
1603 case Acc thus ?case by (rules intro: da.Acc) |
|
1604 next |
|
1605 case (AssLVar A B E Env e vn B') |
|
1606 have B': "B \<subseteq> B'" . |
|
1607 then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
|
1608 by (rule AssLVar.hyps [elim_format]) rules |
|
1609 then obtain A' where |
|
1610 "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'" |
|
1611 by (rules intro: da.AssLVar) |
|
1612 thus ?case .. |
|
1613 next |
|
1614 case (Ass A B Env V e v B') |
|
1615 have B': "B \<subseteq> B'" . |
|
1616 have "\<forall>vn. v \<noteq> LVar vn". |
|
1617 moreover |
|
1618 obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'" |
|
1619 proof - |
|
1620 have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps) |
|
1621 with B' |
|
1622 show ?thesis using that by rules |
|
1623 qed |
|
1624 moreover |
|
1625 obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" |
|
1626 proof - |
|
1627 have "Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V" by (rule Ass.hyps) |
|
1628 from this B' V' |
|
1629 have "nrm V \<subseteq> nrm V'" |
|
1630 by (rule da_monotone [THEN conjE]) |
|
1631 moreover |
|
1632 have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps) |
|
1633 ultimately show ?thesis using that by rules |
|
1634 qed |
|
1635 ultimately |
|
1636 have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'" |
|
1637 by (rules intro: da.Ass) |
|
1638 thus ?case .. |
|
1639 next |
|
1640 case (CondBool A B C E1 E2 Env c e1 e2 B') |
|
1641 have B': "B \<subseteq> B'" . |
|
1642 have "Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" . |
|
1643 moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
|
1644 proof - |
|
1645 have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps) |
|
1646 with B' |
|
1647 show ?thesis using that by rules |
|
1648 qed |
|
1649 moreover |
|
1650 obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" |
|
1651 proof - |
|
1652 from B' |
|
1653 have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)" |
|
1654 by blast |
|
1655 moreover |
|
1656 have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps) |
|
1657 ultimately |
|
1658 show ?thesis using that by rules |
|
1659 qed |
|
1660 moreover |
|
1661 obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" |
|
1662 proof - |
|
1663 from B' |
|
1664 have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)" |
|
1665 by blast |
|
1666 moreover |
|
1667 have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps) |
|
1668 ultimately |
|
1669 show ?thesis using that by rules |
|
1670 qed |
|
1671 ultimately |
|
1672 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" |
|
1673 by (rules intro: da.CondBool) |
|
1674 thus ?case .. |
|
1675 next |
|
1676 case (Cond A B C E1 E2 Env c e1 e2 B') |
|
1677 have B': "B \<subseteq> B'" . |
|
1678 have "\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" . |
|
1679 moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
|
1680 proof - |
|
1681 have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps) |
|
1682 with B' |
|
1683 show ?thesis using that by rules |
|
1684 qed |
|
1685 moreover |
|
1686 obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" |
|
1687 proof - |
|
1688 from B' |
|
1689 have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)" |
|
1690 by blast |
|
1691 moreover |
|
1692 have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps) |
|
1693 ultimately |
|
1694 show ?thesis using that by rules |
|
1695 qed |
|
1696 moreover |
|
1697 obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" |
|
1698 proof - |
|
1699 from B' |
|
1700 have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)" |
|
1701 by blast |
|
1702 moreover |
|
1703 have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps) |
|
1704 ultimately |
|
1705 show ?thesis using that by rules |
|
1706 qed |
|
1707 ultimately |
|
1708 obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" |
|
1709 by (rules intro: da.Cond) |
|
1710 thus ?case .. |
|
1711 next |
|
1712 case (Call A B E Env accC args e mn mode pTs statT B') |
|
1713 have B': "B \<subseteq> B'" . |
|
1714 obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
|
1715 proof - |
|
1716 have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps) |
|
1717 with B' |
|
1718 show ?thesis using that by rules |
|
1719 qed |
|
1720 moreover |
|
1721 obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" |
|
1722 proof - |
|
1723 have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Call.hyps) |
|
1724 from this B' E' |
|
1725 have "nrm E \<subseteq> nrm E'" |
|
1726 by (rule da_monotone [THEN conjE]) |
|
1727 moreover |
|
1728 have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps) |
|
1729 ultimately show ?thesis using that by rules |
|
1730 qed |
|
1731 ultimately |
|
1732 have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'" |
|
1733 by (rules intro: da.Call) |
|
1734 thus ?case .. |
|
1735 next |
|
1736 case Methd thus ?case by (rules intro: da.Methd) |
|
1737 next |
|
1738 case (Body A B C D Env c B') |
|
1739 have B': "B \<subseteq> B'" . |
|
1740 obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'" |
|
1741 proof - |
|
1742 have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps) |
|
1743 moreover note B' |
|
1744 moreover |
|
1745 from B' obtain C' where da_c: "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" |
|
1746 by (rule Body.hyps [elim_format]) blast |
|
1747 ultimately |
|
1748 have "nrm C \<subseteq> nrm C'" |
|
1749 by (rule da_monotone [THEN conjE]) |
|
1750 with da_c that show ?thesis by rules |
|
1751 qed |
|
1752 moreover |
|
1753 have "Result \<in> nrm C" . |
|
1754 with nrm_C' have "Result \<in> nrm C'" |
|
1755 by blast |
|
1756 moreover have "jumpNestingOkS {Ret} c" . |
|
1757 ultimately obtain A' where |
|
1758 "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'" |
|
1759 by (rules intro: da.Body) |
|
1760 thus ?case .. |
|
1761 next |
|
1762 case LVar thus ?case by (rules intro: da.LVar) |
|
1763 next |
|
1764 case FVar thus ?case by (rules intro: da.FVar) |
|
1765 next |
|
1766 case (AVar A B E1 Env e1 e2 B') |
|
1767 have B': "B \<subseteq> B'" . |
|
1768 obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" |
|
1769 proof - |
|
1770 have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps) |
|
1771 with B' |
|
1772 show ?thesis using that by rules |
|
1773 qed |
|
1774 moreover |
|
1775 obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" |
|
1776 proof - |
|
1777 have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule AVar.hyps) |
|
1778 from this B' E1' |
|
1779 have "nrm E1 \<subseteq> nrm E1'" |
|
1780 by (rule da_monotone [THEN conjE]) |
|
1781 moreover |
|
1782 have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps) |
|
1783 ultimately show ?thesis using that by rules |
|
1784 qed |
|
1785 ultimately |
|
1786 have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'" |
|
1787 by (rules intro: da.AVar) |
|
1788 thus ?case .. |
|
1789 next |
|
1790 case Nil thus ?case by (rules intro: da.Nil) |
|
1791 next |
|
1792 case (Cons A B E Env e es B') |
|
1793 have B': "B \<subseteq> B'" . |
|
1794 obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" |
|
1795 proof - |
|
1796 have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps) |
|
1797 with B' |
|
1798 show ?thesis using that by rules |
|
1799 qed |
|
1800 moreover |
|
1801 obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" |
|
1802 proof - |
|
1803 have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Cons.hyps) |
|
1804 from this B' E' |
|
1805 have "nrm E \<subseteq> nrm E'" |
|
1806 by (rule da_monotone [THEN conjE]) |
|
1807 moreover |
|
1808 have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps) |
|
1809 ultimately show ?thesis using that by rules |
|
1810 qed |
|
1811 ultimately |
|
1812 have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'" |
|
1813 by (rules intro: da.Cons) |
|
1814 thus ?case .. |
|
1815 qed |
|
1816 qed |
|
1817 |
|
1818 (* Remarks about the proof style: |
|
1819 |
|
1820 "by (rule <Case>.hyps)" vs "." |
|
1821 -------------------------- |
|
1822 |
|
1823 with <Case>.hyps you state more precise were the rule comes from |
|
1824 |
|
1825 . takes all assumptions into account, but looks more "light" |
|
1826 and is more resistent for cut and paste proof in different |
|
1827 cases. |
|
1828 |
|
1829 "intro: da.intros" vs "da.<Case>" |
|
1830 --------------------------------- |
|
1831 The first ist more convinient for cut and paste between cases, |
|
1832 the second is more informativ for the reader |
|
1833 *) |
|
1834 |
|
1835 corollary da_weakenE [consumes 2]: |
|
1836 assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and |
|
1837 B': "B \<subseteq> B'" and |
|
1838 ex_mono: "\<And> A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; nrm A \<subseteq> nrm A'; |
|
1839 \<And> l. brk A l \<subseteq> brk A' l\<rbrakk> \<Longrightarrow> P" |
|
1840 shows "P" |
|
1841 proof - |
|
1842 from da B' |
|
1843 obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" |
|
1844 by (rule da_weaken [elim_format]) rules |
|
1845 with da B' |
|
1846 have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)" |
|
1847 by (rule da_monotone) |
|
1848 with A' ex_mono |
|
1849 show ?thesis |
|
1850 by rules |
|
1851 qed |
|
1852 |
|
1853 end |