1 (* Title: HOL/MicroJava/BV/BVLCorrect.thy |
1 (* |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Gerwin Klein |
3 Author: Gerwin Klein |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Correctness of the LBV} *} |
7 header {* \isaheader{Correctness of the LBV} *} |
8 |
8 |
9 theory LBVCorrect = LBVSpec + Typing_Framework: |
9 theory LBVCorrect = LBVSpec + Typing_Framework: |
10 |
10 |
11 constdefs |
11 locale lbvc = lbv + |
12 fits :: "'s option list \<Rightarrow> 's certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> |
12 fixes s0 :: 'a |
13 's steptype \<Rightarrow> 's option \<Rightarrow> 'a list \<Rightarrow> bool" |
13 fixes c :: "'a list" |
14 "fits phi cert f r step s0 is \<equiv> |
14 fixes ins :: "'b list" |
15 length phi = length is \<and> |
15 fixes phi :: "'a list" ("\<phi>") |
16 (\<forall>pc s. pc < length is --> |
16 defines phi_def: |
17 (wtl_inst_list (take pc is) cert f r step 0 s0 = OK s \<longrightarrow> |
17 "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) |
18 (case cert!pc of None => phi!pc = s |
18 [0..length ins(]" |
19 | Some t => phi!pc = Some t)))" |
|
20 |
19 |
21 make_phi :: "'s certificate \<Rightarrow> 's ebinop \<Rightarrow> 's ord \<Rightarrow> |
|
22 's steptype \<Rightarrow> 's option \<Rightarrow> 'a list \<Rightarrow> 's option list" |
|
23 "make_phi cert f r step s0 is \<equiv> |
|
24 map (\<lambda>pc. case cert!pc of |
|
25 None => ok_val (wtl_inst_list (take pc is) cert f r step 0 s0) |
|
26 | Some t => Some t) [0..length is(]" |
|
27 |
20 |
28 lemma fitsD_None [intro?]: |
21 lemma (in lbvc) phi_None [intro?]: |
29 "\<lbrakk> fits phi cert f r step s0 is; pc < length is; |
22 "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0" |
30 wtl_inst_list (take pc is) cert f r step 0 s0 = OK s; |
23 by (simp add: phi_def) |
31 cert!pc = None \<rbrakk> \<Longrightarrow> phi!pc = s" |
|
32 by (auto simp add: fits_def) |
|
33 |
24 |
34 lemma fitsD_Some [intro?]: |
25 lemma (in lbvc) phi_Some [intro?]: |
35 "\<lbrakk> fits phi cert f r step s0 is; pc < length is; |
26 "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc" |
36 wtl_inst_list (take pc is) cert f r step 0 s0 = OK s; |
27 by (simp add: phi_def) |
37 cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t" |
|
38 by (auto simp add: fits_def) |
|
39 |
28 |
40 lemma make_phi_Some: |
29 lemma (in lbvc) phi_len [simp]: |
41 "pc < length is \<Longrightarrow> cert!pc = Some t \<Longrightarrow> |
30 "length \<phi> = length ins" |
42 make_phi cert f r step s0 is ! pc = Some t" |
31 by (simp add: phi_def) |
43 by (simp add: make_phi_def) |
|
44 |
32 |
45 lemma make_phi_None: |
|
46 "pc < length is \<Longrightarrow> cert!pc = None \<Longrightarrow> |
|
47 make_phi cert f r step s0 is ! pc = |
|
48 ok_val (wtl_inst_list (take pc is) cert f r step 0 s0)" |
|
49 by (simp add: make_phi_def) |
|
50 |
33 |
51 lemma make_phi_len: |
34 lemma (in lbvc) wtl_suc_pc: |
52 "length (make_phi cert f r step s0 is) = length is" |
35 assumes all: "wtl ins c 0 s0 \<noteq> \<top>" |
53 by (simp add: make_phi_def) |
36 assumes pc: "pc+1 < length ins" |
54 |
37 shows "wtl (take (pc+1) ins) c 0 s0 <=_r \<phi>!(pc+1)" |
55 lemma exists_phi: |
38 proof - |
56 "\<exists>phi. fits phi cert f r step s0 is" |
39 from all pc |
57 proof - |
40 have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all) |
58 have "fits (make_phi cert f r step s0 is) cert f r step s0 is" |
41 with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm) |
59 by (auto simp add: fits_def make_phi_Some make_phi_None make_phi_len |
|
60 split: option.splits) |
|
61 thus ?thesis by fast |
|
62 qed |
|
63 |
|
64 lemma fits_lemma1 [intro?]: |
|
65 "\<lbrakk>wtl_inst_list is cert f r step 0 s \<noteq> Err; fits phi cert f r step s is\<rbrakk> |
|
66 \<Longrightarrow> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t" |
|
67 proof (intro strip) |
|
68 fix pc t |
|
69 assume "wtl_inst_list is cert f r step 0 s \<noteq> Err" |
|
70 then obtain s'' where |
|
71 "wtl_inst_list (take pc is) cert f r step 0 s = OK s''" |
|
72 by (blast dest: wtl_take) |
|
73 moreover |
|
74 assume "fits phi cert f r step s is" |
|
75 "pc < length is" "cert ! pc = Some t" |
|
76 ultimately |
|
77 show "phi!pc = Some t" by (auto dest: fitsD_Some) |
|
78 qed |
42 qed |
79 |
43 |
80 |
44 |
81 lemma wtl_suc_pc: |
45 lemma (in lbvc) wtl_stable: |
82 assumes |
46 assumes |
83 semi: "err_semilat (A,r,f)" and |
47 pres: "pres_type step (length ins) A" and |
84 all: "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" and |
48 s0_in_A: "s0 \<in> A" and |
85 wtl: "wtl_inst_list (take pc is) cert f r step 0 s0 = OK s'" and |
49 cert_ok: "cert_ok c (length ins) \<top> \<bottom> A" and |
86 cert: "wtl_cert cert f r step pc s' = OK s''" and |
50 wtl: "wtl ins c 0 s0 \<noteq> \<top>" and |
87 fits: "fits phi cert f r step s0 is" and |
51 pc: "pc < length ins" and |
88 pc: "pc+1 < length is" |
52 bounded: "bounded step (length ins)" |
89 shows "OK s'' \<le>|r OK (phi!(pc+1))" |
53 shows "stable r step \<phi> pc" |
90 proof - |
|
91 from wtl cert pc |
|
92 have wts: "wtl_inst_list (take (pc+1) is) cert f r step 0 s0 = OK s''" |
|
93 by (rule wtl_Suc) |
|
94 moreover |
|
95 from all pc |
|
96 have "\<exists>s' s''. wtl_inst_list (take (pc+1) is) cert f r step 0 s0 = OK s' \<and> |
|
97 wtl_cert cert f r step (pc+1) s' = OK s''" |
|
98 by (rule wtl_all) |
|
99 ultimately |
|
100 obtain x where "wtl_cert cert f r step (pc+1) s'' = OK x" by auto |
|
101 hence "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> OK s'' \<le>|r OK (cert!(pc+1))" |
|
102 by (simp add: wtl_cert_def split: split_if_asm) |
|
103 also from fits pc wts |
|
104 have "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> cert!(pc+1) = phi!(pc+1)" |
|
105 by (auto dest!: fitsD_Some) |
|
106 finally have "\<And>t. cert!(pc+1) = Some t \<Longrightarrow> OK s'' \<le>|r OK (phi!(pc+1))" . |
|
107 moreover |
|
108 from fits pc wts have "cert!(pc+1) = None \<Longrightarrow> s'' = phi!(pc+1)" |
|
109 by (rule fitsD_None [symmetric]) |
|
110 with semi have "cert!(pc+1) = None \<Longrightarrow> OK s'' \<le>|r OK (phi!(pc+1))" by simp |
|
111 ultimately |
|
112 show "OK s'' \<le>|r OK (phi!(pc+1))" by (cases "cert!(pc+1)", blast+) |
|
113 qed |
|
114 |
|
115 lemma wtl_stable: |
|
116 assumes |
|
117 semi: "err_semilat (A,r,f)" and |
|
118 pres: "pres_type step (length is) (err (opt A))" and |
|
119 s0_in_A: "s0 \<in> opt A" and |
|
120 cert_ok: "cert_ok cert (length is) A" and |
|
121 fits: "fits phi cert f r step s0 is" and |
|
122 wtl: "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" and |
|
123 pc: "pc < length is" and |
|
124 bounded: "bounded step (length is)" |
|
125 shows "stable (Err.le (Opt.le r)) step (map OK phi) pc" |
|
126 proof (unfold stable_def, clarify) |
54 proof (unfold stable_def, clarify) |
127 fix pc' s' assume step: "(pc',s') \<in> set (step pc ((map OK phi) ! pc))" |
55 fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))" |
128 (is "(pc',s') \<in> set (?step pc)") |
56 (is "(pc',s') \<in> set (?step pc)") |
129 |
57 |
130 from step pc bounded have pc': "pc' < length is" |
58 from step pc bounded have pc': "pc' < length ins" |
131 by (unfold bounded_def) blast |
59 by (unfold bounded_def) blast |
|
60 |
|
61 have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take) |
|
62 have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take) |
132 |
63 |
133 from wtl pc obtain s1 s2 where |
64 from wtl pc have cert: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all) |
134 tkpc: "wtl_inst_list (take pc is) cert f r step 0 s0 = OK s1" and |
|
135 cert: "wtl_cert cert f r step pc s1 = OK s2" |
|
136 by - (drule wtl_all, auto) |
|
137 |
65 |
138 have c_Some: "\<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t" .. |
66 have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc" |
139 have c_None: "cert!pc = None \<Longrightarrow> phi!pc = s1" .. |
67 by (simp add: phi_def) |
|
68 have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" .. |
140 |
69 |
141 from cert pc c_None c_Some |
70 from cert pc c_None c_Some |
142 have inst: "wtl_inst cert f r step pc (phi!pc) = OK s2" |
71 have inst: "wtc c pc ?s1 = wti c pc (\<phi>!pc)" |
143 by (simp add: wtl_cert_def split: option.splits split_if_asm) |
72 by (simp add: wtc split: split_if_asm) |
144 |
|
145 from semi have "order (Err.le (Opt.le r))" by simp note order_trans [OF this, trans] |
|
146 |
|
147 from pc fits have [simp]: "map OK phi!pc = OK (phi!pc)" by (simp add: fits_def) |
|
148 from pc' fits have [simp]: "map OK phi!pc' = OK (phi!pc')" by (simp add: fits_def) |
|
149 |
73 |
150 have "s1 \<in> opt A" by (rule wtl_inst_list_pres) |
74 have "?s1 \<in> A" by (rule wtl_pres) |
151 with pc c_Some cert_ok c_None |
75 with pc c_Some cert_ok c_None |
152 have "phi!pc \<in> opt A" by (cases "cert!pc") (auto dest: cert_okD1) |
76 have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1) |
153 with pc pres |
77 with pc pres |
154 have step_in_A: "\<forall>(pc',s') \<in> set (?step pc). s' \<in> err (opt A)" |
78 have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2) |
155 by (auto dest: pres_typeD) |
|
156 |
79 |
157 show "s' \<le>|r (map OK phi) ! pc'" |
80 show "s' <=_r \<phi>!pc'" |
158 proof (cases "pc' = pc+1") |
81 proof (cases "pc' = pc+1") |
159 case True |
82 case True |
160 with pc' cert_ok |
83 with pc' cert_ok |
161 have cert_in_A: "OK (cert!(pc+1)) \<in> err (opt A)" by (auto dest: cert_okD1) |
84 have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1) |
162 from inst |
85 from True pc' have pc1: "pc+1 < length ins" by simp |
163 have ok: "OK s2 = merge cert f r pc (?step pc) (OK (cert!(pc+1)))" |
86 with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc) |
164 by (simp add: wtl_inst_def) |
87 with inst |
|
88 have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti) |
165 also |
89 also |
166 have "\<dots> = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++|f (OK (cert!(pc+1))))" |
90 from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp |
167 using cert_in_A step_in_A semi ok |
91 with cert_in_A step_in_A |
168 by - (drule merge_def, auto split: split_if_asm) |
92 have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))" |
|
93 by (rule merge_not_top_s) |
169 finally |
94 finally |
170 have "s' \<le>|r OK s2" |
95 have "s' <=_r ?s2" using step_in_A cert_in_A True step |
171 using semi step_in_A cert_in_A True step by (auto intro: ub1') |
96 by (auto intro: pp_ub1') |
172 also |
97 also |
173 from True pc' have "pc+1 < length is" by simp |
98 from wtl pc1 have "?s2 <=_r \<phi>!(pc+1)" by (rule wtl_suc_pc) |
174 with semi wtl tkpc cert fits |
|
175 have "OK s2 \<le>|r (OK (phi ! (pc+1)))" by (rule wtl_suc_pc) |
|
176 also note True [symmetric] |
99 also note True [symmetric] |
177 finally show ?thesis by simp |
100 finally show ?thesis by simp |
178 next |
101 next |
179 case False |
102 case False |
180 from inst |
103 from cert inst |
181 have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' \<le>|r OK (cert!pc')" |
104 have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti) |
182 by (unfold wtl_inst_def) (rule merge_ok, simp) |
105 with step_in_A |
|
106 have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" |
|
107 by - (rule merge_not_top) |
183 with step False |
108 with step False |
184 have ok: "s' \<le>|r (OK (cert!pc'))" by blast |
109 have ok: "s' <=_r c!pc'" by blast |
185 moreover |
110 moreover |
186 from ok |
111 from ok |
187 have "cert!pc' = None \<longrightarrow> s' = OK None" by auto |
112 have "c!pc' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp |
188 moreover |
113 moreover |
189 from c_Some pc' |
114 from c_Some pc' |
190 have "cert!pc' \<noteq> None \<longrightarrow> phi!pc' = cert!pc'" by auto |
115 have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto |
191 ultimately |
116 ultimately |
192 show ?thesis by auto |
117 show ?thesis by (cases "c!pc' = \<bottom>") auto |
193 qed |
118 qed |
194 qed |
119 qed |
195 |
120 |
|
121 |
|
122 lemma (in lbvc) phi_not_top: |
|
123 assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" |
|
124 assumes crt: "cert_ok c (length ins) \<top> \<bottom> A" |
|
125 assumes pc: "pc < length ins" |
|
126 shows "\<phi>!pc \<noteq> \<top>" |
|
127 proof (cases "c!pc = \<bottom>") |
|
128 case False with pc |
|
129 have "\<phi>!pc = c!pc" .. |
|
130 also from crt pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4) |
|
131 finally show ?thesis . |
|
132 next |
|
133 case True with pc |
|
134 have "\<phi>!pc = wtl (take pc ins) c 0 s0" .. |
|
135 also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take) |
|
136 finally show ?thesis . |
|
137 qed |
|
138 |
196 |
139 |
197 lemma wtl_fits: |
140 theorem (in lbvc) wtl_sound: |
198 "wtl_inst_list is cert f r step 0 s0 \<noteq> Err \<Longrightarrow> |
141 assumes "wtl ins c 0 s0 \<noteq> \<top>" |
199 fits phi cert f r step s0 is \<Longrightarrow> |
142 assumes "bounded step (length ins)" |
200 err_semilat (A,r,f) \<Longrightarrow> |
143 assumes "s0 \<in> A" and "cert_ok c (length ins) \<top> \<bottom> A" |
201 bounded step (length is) \<Longrightarrow> |
144 assumes "pres_type step (length ins) A" |
202 pres_type step (length is) (err (opt A)) \<Longrightarrow> |
145 shows "\<exists>ts. wt_step r \<top> step ts" |
203 s0 \<in> opt A \<Longrightarrow> |
146 proof - |
204 cert_ok cert (length is) A \<Longrightarrow> |
147 have "wt_step r \<top> step \<phi>" |
205 wt_step (Err.le (Opt.le r)) Err step (map OK phi)" |
148 proof (unfold wt_step_def, intro strip conjI) |
206 apply (unfold wt_step_def) |
149 fix pc assume "pc < length \<phi>" |
207 apply (intro strip) |
150 then obtain "pc < length ins" by simp |
208 apply (rule conjI, simp) |
151 show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top) |
209 apply (rule wtl_stable) |
152 show "stable r step \<phi> pc" by (rule wtl_stable) |
210 apply assumption+ |
153 qed |
211 apply (simp add: fits_def) |
154 thus ?thesis .. |
212 apply assumption |
|
213 done |
|
214 |
|
215 |
|
216 theorem wtl_sound: |
|
217 assumes "wtl_inst_list is cert f r step 0 s0 \<noteq> Err" |
|
218 assumes "err_semilat (A,r,f)" and "bounded step (length is)" |
|
219 assumes "s0 \<in> opt A" and "cert_ok cert (length is) A" |
|
220 assumes "pres_type step (length is) (err (opt A))" |
|
221 shows "\<exists>ts. wt_step (Err.le (Opt.le r)) Err step ts" |
|
222 proof - |
|
223 obtain phi where "fits phi cert f r step s0 is" by (insert exists_phi) fast |
|
224 have "wt_step (Err.le (Opt.le r)) Err step (map OK phi)" by (rule wtl_fits) |
|
225 thus ?thesis .. |
|
226 qed |
155 qed |
227 |
156 |
228 |
|
229 end |
157 end |