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