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