1 (* Title: HOL/MicroJava/BV/LBVComplete.thy |
|
2 ID: $Id$ |
|
3 Author: Gerwin Klein |
|
4 Copyright 2000 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 header {* \isaheader{Completeness of the LBV} *} |
|
8 |
|
9 theory LBVComplete |
|
10 imports LBVSpec Typing_Framework |
|
11 begin |
|
12 |
|
13 constdefs |
|
14 is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" |
|
15 "is_target step phi pc' \<equiv> |
|
16 \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))" |
|
17 |
|
18 make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" |
|
19 "make_cert step phi B \<equiv> |
|
20 map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]" |
|
21 |
|
22 lemma [code]: |
|
23 "is_target step phi pc' = |
|
24 list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]" |
|
25 by (force simp: list_ex_iff is_target_def mem_iff) |
|
26 |
|
27 |
|
28 locale lbvc = lbv + |
|
29 fixes phi :: "'a list" ("\<phi>") |
|
30 fixes c :: "'a list" |
|
31 defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>" |
|
32 |
|
33 assumes mono: "mono r step (length \<phi>) A" |
|
34 assumes pres: "pres_type step (length \<phi>) A" |
|
35 assumes phi: "\<forall>pc < length \<phi>. \<phi>!pc \<in> A \<and> \<phi>!pc \<noteq> \<top>" |
|
36 assumes bounded: "bounded step (length \<phi>)" |
|
37 |
|
38 assumes B_neq_T: "\<bottom> \<noteq> \<top>" |
|
39 |
|
40 |
|
41 lemma (in lbvc) cert: "cert_ok c (length \<phi>) \<top> \<bottom> A" |
|
42 proof (unfold cert_ok_def, intro strip conjI) |
|
43 note [simp] = make_cert_def cert_def nth_append |
|
44 |
|
45 show "c!length \<phi> = \<bottom>" by simp |
|
46 |
|
47 fix pc assume pc: "pc < length \<phi>" |
|
48 from pc phi B_A show "c!pc \<in> A" by simp |
|
49 from pc phi B_neq_T show "c!pc \<noteq> \<top>" by simp |
|
50 qed |
|
51 |
|
52 lemmas [simp del] = split_paired_Ex |
|
53 |
|
54 |
|
55 lemma (in lbvc) cert_target [intro?]: |
|
56 "\<lbrakk> (pc',s') \<in> set (step pc (\<phi>!pc)); |
|
57 pc' \<noteq> pc+1; pc < length \<phi>; pc' < length \<phi> \<rbrakk> |
|
58 \<Longrightarrow> c!pc' = \<phi>!pc'" |
|
59 by (auto simp add: cert_def make_cert_def nth_append is_target_def) |
|
60 |
|
61 |
|
62 lemma (in lbvc) cert_approx [intro?]: |
|
63 "\<lbrakk> pc < length \<phi>; c!pc \<noteq> \<bottom> \<rbrakk> |
|
64 \<Longrightarrow> c!pc = \<phi>!pc" |
|
65 by (auto simp add: cert_def make_cert_def nth_append) |
|
66 |
|
67 |
|
68 lemma (in lbv) le_top [simp, intro]: |
|
69 "x <=_r \<top>" |
|
70 by (insert top) simp |
|
71 |
|
72 |
|
73 lemma (in lbv) merge_mono: |
|
74 assumes less: "ss2 <=|r| ss1" |
|
75 assumes x: "x \<in> A" |
|
76 assumes ss1: "snd`set ss1 \<subseteq> A" |
|
77 assumes ss2: "snd`set ss2 \<subseteq> A" |
|
78 shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1") |
|
79 proof- |
|
80 have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp |
|
81 moreover { |
|
82 assume merge: "?s1 \<noteq> T" |
|
83 from x ss1 have "?s1 = |
|
84 (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc' |
|
85 then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x |
|
86 else \<top>)" |
|
87 by (rule merge_def) |
|
88 with merge obtain |
|
89 app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" |
|
90 (is "?app ss1") and |
|
91 sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1" |
|
92 (is "?map ss1 ++_f x = _" is "?sum ss1 = _") |
|
93 by (simp split: split_if_asm) |
|
94 from app less |
|
95 have "?app ss2" by (blast dest: trans_r lesub_step_typeD) |
|
96 moreover { |
|
97 from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto |
|
98 with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed semilat) |
|
99 with sum have "?s1 \<in> A" by simp |
|
100 moreover |
|
101 have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto |
|
102 from x map1 |
|
103 have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1" |
|
104 by clarify (rule pp_ub1) |
|
105 with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp |
|
106 with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1" |
|
107 by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r) |
|
108 moreover |
|
109 from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2) |
|
110 with sum have "x <=_r ?s1" by simp |
|
111 moreover |
|
112 from ss2 have "set (?map ss2) \<subseteq> A" by auto |
|
113 ultimately |
|
114 have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub) |
|
115 } |
|
116 moreover |
|
117 from x ss2 have |
|
118 "?s2 = |
|
119 (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc' |
|
120 then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x |
|
121 else \<top>)" |
|
122 by (rule merge_def) |
|
123 ultimately have ?thesis by simp |
|
124 } |
|
125 ultimately show ?thesis by (cases "?s1 = \<top>") auto |
|
126 qed |
|
127 |
|
128 |
|
129 lemma (in lbvc) wti_mono: |
|
130 assumes less: "s2 <=_r s1" |
|
131 assumes pc: "pc < length \<phi>" |
|
132 assumes s1: "s1 \<in> A" |
|
133 assumes s2: "s2 \<in> A" |
|
134 shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'") |
|
135 proof - |
|
136 from mono pc s2 less have "step pc s2 <=|r| step pc s1" by (rule monoD) |
|
137 moreover |
|
138 from cert B_A pc have "c!Suc pc \<in> A" by (rule cert_okD3) |
|
139 moreover |
|
140 from pres s1 pc |
|
141 have "snd`set (step pc s1) \<subseteq> A" by (rule pres_typeD2) |
|
142 moreover |
|
143 from pres s2 pc |
|
144 have "snd`set (step pc s2) \<subseteq> A" by (rule pres_typeD2) |
|
145 ultimately |
|
146 show ?thesis by (simp add: wti merge_mono) |
|
147 qed |
|
148 |
|
149 lemma (in lbvc) wtc_mono: |
|
150 assumes less: "s2 <=_r s1" |
|
151 assumes pc: "pc < length \<phi>" |
|
152 assumes s1: "s1 \<in> A" |
|
153 assumes s2: "s2 \<in> A" |
|
154 shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'") |
|
155 proof (cases "c!pc = \<bottom>") |
|
156 case True |
|
157 moreover from less pc s1 s2 have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono) |
|
158 ultimately show ?thesis by (simp add: wtc) |
|
159 next |
|
160 case False |
|
161 have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp |
|
162 moreover { |
|
163 assume "?s1' \<noteq> \<top>" |
|
164 with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm) |
|
165 with less have "s2 <=_r c!pc" .. |
|
166 with False c have ?thesis by (simp add: wtc) |
|
167 } |
|
168 ultimately show ?thesis by (cases "?s1' = \<top>") auto |
|
169 qed |
|
170 |
|
171 |
|
172 lemma (in lbv) top_le_conv [simp]: |
|
173 "\<top> <=_r x = (x = \<top>)" |
|
174 by (insert semilat) (simp add: top top_le_conv) |
|
175 |
|
176 lemma (in lbv) neq_top [simp, elim]: |
|
177 "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>" |
|
178 by (cases "x = T") auto |
|
179 |
|
180 |
|
181 lemma (in lbvc) stable_wti: |
|
182 assumes stable: "stable r step \<phi> pc" |
|
183 assumes pc: "pc < length \<phi>" |
|
184 shows "wti c pc (\<phi>!pc) \<noteq> \<top>" |
|
185 proof - |
|
186 let ?step = "step pc (\<phi>!pc)" |
|
187 from stable |
|
188 have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def) |
|
189 |
|
190 from cert B_A pc |
|
191 have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3) |
|
192 moreover |
|
193 from phi pc have "\<phi>!pc \<in> A" by simp |
|
194 from pres this pc |
|
195 have stepA: "snd`set ?step \<subseteq> A" by (rule pres_typeD2) |
|
196 ultimately |
|
197 have "merge c pc ?step (c!Suc pc) = |
|
198 (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc' |
|
199 then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc |
|
200 else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms]) |
|
201 moreover { |
|
202 fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1" |
|
203 with less have "s' <=_r \<phi>!pc'" by auto |
|
204 also |
|
205 from bounded pc s' have "pc' < length \<phi>" by (rule boundedD) |
|
206 with s' suc_pc pc have "c!pc' = \<phi>!pc'" .. |
|
207 hence "\<phi>!pc' = c!pc'" .. |
|
208 finally have "s' <=_r c!pc'" . |
|
209 } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto |
|
210 moreover |
|
211 from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto |
|
212 hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" |
|
213 (is "?map ++_f _ \<noteq> _") |
|
214 proof (rule disjE) |
|
215 assume pc': "Suc pc = length \<phi>" |
|
216 with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2) |
|
217 moreover |
|
218 from pc' bounded pc |
|
219 have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto) |
|
220 hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False) |
|
221 hence "?map = []" by simp |
|
222 ultimately show ?thesis by (simp add: B_neq_T) |
|
223 next |
|
224 assume pc': "Suc pc < length \<phi>" |
|
225 from pc' phi have "\<phi>!Suc pc \<in> A" by simp |
|
226 moreover note cert_suc |
|
227 moreover from stepA |
|
228 have "set ?map \<subseteq> A" by auto |
|
229 moreover |
|
230 have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto |
|
231 with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto |
|
232 moreover |
|
233 from pc' have "c!Suc pc <=_r \<phi>!Suc pc" |
|
234 by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx) |
|
235 ultimately |
|
236 have "?map ++_f c!Suc pc <=_r \<phi>!Suc pc" by (rule pp_lub) |
|
237 moreover |
|
238 from pc' phi have "\<phi>!Suc pc \<noteq> \<top>" by simp |
|
239 ultimately |
|
240 show ?thesis by auto |
|
241 qed |
|
242 ultimately |
|
243 have "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by simp |
|
244 thus ?thesis by (simp add: wti) |
|
245 qed |
|
246 |
|
247 lemma (in lbvc) wti_less: |
|
248 assumes stable: "stable r step \<phi> pc" |
|
249 assumes suc_pc: "Suc pc < length \<phi>" |
|
250 shows "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wti <=_r _") |
|
251 proof - |
|
252 let ?step = "step pc (\<phi>!pc)" |
|
253 |
|
254 from stable |
|
255 have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def) |
|
256 |
|
257 from suc_pc have pc: "pc < length \<phi>" by simp |
|
258 with cert B_A have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3) |
|
259 moreover |
|
260 from phi pc have "\<phi>!pc \<in> A" by simp |
|
261 with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2) |
|
262 moreover |
|
263 from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti) |
|
264 hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti) |
|
265 ultimately |
|
266 have "merge c pc ?step (c!Suc pc) = |
|
267 map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) |
|
268 hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti) |
|
269 also { |
|
270 from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp |
|
271 moreover note cert_suc |
|
272 moreover from stepA have "set ?map \<subseteq> A" by auto |
|
273 moreover |
|
274 have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto |
|
275 with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto |
|
276 moreover |
|
277 from suc_pc have "c!Suc pc <=_r \<phi>!Suc pc" |
|
278 by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx) |
|
279 ultimately |
|
280 have "?sum <=_r \<phi>!Suc pc" by (rule pp_lub) |
|
281 } |
|
282 finally show ?thesis . |
|
283 qed |
|
284 |
|
285 lemma (in lbvc) stable_wtc: |
|
286 assumes stable: "stable r step phi pc" |
|
287 assumes pc: "pc < length \<phi>" |
|
288 shows "wtc c pc (\<phi>!pc) \<noteq> \<top>" |
|
289 proof - |
|
290 from stable pc have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti) |
|
291 show ?thesis |
|
292 proof (cases "c!pc = \<bottom>") |
|
293 case True with wti show ?thesis by (simp add: wtc) |
|
294 next |
|
295 case False |
|
296 with pc have "c!pc = \<phi>!pc" .. |
|
297 with False wti show ?thesis by (simp add: wtc) |
|
298 qed |
|
299 qed |
|
300 |
|
301 lemma (in lbvc) wtc_less: |
|
302 assumes stable: "stable r step \<phi> pc" |
|
303 assumes suc_pc: "Suc pc < length \<phi>" |
|
304 shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _") |
|
305 proof (cases "c!pc = \<bottom>") |
|
306 case True |
|
307 moreover from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" |
|
308 by (rule wti_less) |
|
309 ultimately show ?thesis by (simp add: wtc) |
|
310 next |
|
311 case False |
|
312 from suc_pc have pc: "pc < length \<phi>" by simp |
|
313 with stable have "?wtc \<noteq> \<top>" by (rule stable_wtc) |
|
314 with False have "?wtc = wti c pc (c!pc)" |
|
315 by (unfold wtc) (simp split: split_if_asm) |
|
316 also from pc False have "c!pc = \<phi>!pc" .. |
|
317 finally have "?wtc = wti c pc (\<phi>!pc)" . |
|
318 also from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less) |
|
319 finally show ?thesis . |
|
320 qed |
|
321 |
|
322 |
|
323 lemma (in lbvc) wt_step_wtl_lemma: |
|
324 assumes wt_step: "wt_step r \<top> step \<phi>" |
|
325 shows "\<And>pc s. pc+length ls = length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> |
|
326 wtl ls c pc s \<noteq> \<top>" |
|
327 (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ls pc s \<noteq> _") |
|
328 proof (induct ls) |
|
329 fix pc s assume "s\<noteq>\<top>" thus "?wtl [] pc s \<noteq> \<top>" by simp |
|
330 next |
|
331 fix pc s i ls |
|
332 assume "\<And>pc s. pc+length ls=length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> |
|
333 ?wtl ls pc s \<noteq> \<top>" |
|
334 moreover |
|
335 assume pc_l: "pc + length (i#ls) = length \<phi>" |
|
336 hence suc_pc_l: "Suc pc + length ls = length \<phi>" by simp |
|
337 ultimately |
|
338 have IH: "\<And>s. s <=_r \<phi>!Suc pc \<Longrightarrow> s \<in> A \<Longrightarrow> s \<noteq> \<top> \<Longrightarrow> ?wtl ls (Suc pc) s \<noteq> \<top>" . |
|
339 |
|
340 from pc_l obtain pc: "pc < length \<phi>" by simp |
|
341 with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def) |
|
342 from this pc have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wtc) |
|
343 assume s_phi: "s <=_r \<phi>!pc" |
|
344 from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp |
|
345 assume s: "s \<in> A" |
|
346 with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" by (rule wtc_mono) |
|
347 with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp |
|
348 moreover |
|
349 assume s': "s \<noteq> \<top>" |
|
350 ultimately |
|
351 have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp |
|
352 moreover { |
|
353 assume "ls \<noteq> []" |
|
354 with pc_l have suc_pc: "Suc pc < length \<phi>" by (auto simp add: neq_Nil_conv) |
|
355 with stable have "wtc c pc (phi!pc) <=_r \<phi>!Suc pc" by (rule wtc_less) |
|
356 with wt_s_phi have "wtc c pc s <=_r \<phi>!Suc pc" by (rule trans_r) |
|
357 moreover |
|
358 from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" |
|
359 by (auto simp add: cert_ok_def) |
|
360 from pres this s pc have "wtc c pc s \<in> A" by (rule wtc_pres) |
|
361 ultimately |
|
362 have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast |
|
363 with s' wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp |
|
364 } |
|
365 ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+ |
|
366 qed |
|
367 |
|
368 |
|
369 theorem (in lbvc) wtl_complete: |
|
370 assumes wt: "wt_step r \<top> step \<phi>" |
|
371 and s: "s <=_r \<phi>!0" "s \<in> A" "s \<noteq> \<top>" |
|
372 and len: "length ins = length phi" |
|
373 shows "wtl ins c 0 s \<noteq> \<top>" |
|
374 proof - |
|
375 from len have "0+length ins = length phi" by simp |
|
376 from wt this s show ?thesis by (rule wt_step_wtl_lemma) |
|
377 qed |
|
378 |
|
379 end |
|