47613
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory Abs_Int3
|
|
4 |
imports Abs_Int2_ivl
|
|
5 |
begin
|
|
6 |
|
|
7 |
subsubsection "Welltypedness"
|
|
8 |
|
|
9 |
class Wt =
|
|
10 |
fixes Wt :: "'a \<Rightarrow> com \<Rightarrow> bool"
|
|
11 |
|
|
12 |
instantiation st :: (type)Wt
|
|
13 |
begin
|
|
14 |
|
|
15 |
definition Wt_st :: "'a st \<Rightarrow> com \<Rightarrow> bool" where
|
|
16 |
"Wt_st S c = wt S (vars c)"
|
|
17 |
|
|
18 |
instance ..
|
|
19 |
|
|
20 |
end
|
|
21 |
|
|
22 |
instantiation acom :: (Wt)Wt
|
|
23 |
begin
|
|
24 |
|
|
25 |
definition Wt_acom :: "'a acom \<Rightarrow> com \<Rightarrow> bool" where
|
|
26 |
"Wt C c = (strip C = c \<and> (\<forall>a\<in>set(annos C). Wt a c))"
|
|
27 |
|
|
28 |
instance ..
|
|
29 |
|
|
30 |
end
|
|
31 |
|
|
32 |
instantiation option :: (Wt)Wt
|
|
33 |
begin
|
|
34 |
|
|
35 |
fun Wt_option :: "'a option \<Rightarrow> com \<Rightarrow> bool" where
|
|
36 |
"Wt None c = True" |
|
|
37 |
"Wt (Some x) c = Wt x c"
|
|
38 |
|
|
39 |
instance ..
|
|
40 |
|
|
41 |
end
|
|
42 |
|
|
43 |
lemma Wt_option_iff_wt[simp]: fixes a :: "_ st option"
|
|
44 |
shows "Wt a c = wt a (vars c)"
|
|
45 |
by(auto simp add: wt_option_def Wt_st_def split: option.splits)
|
|
46 |
|
|
47 |
|
|
48 |
context Abs_Int1
|
|
49 |
begin
|
|
50 |
|
|
51 |
lemma Wt_step': "Wt C c \<Longrightarrow> Wt S c \<Longrightarrow> Wt (step' S C) c"
|
|
52 |
apply(auto simp add: Wt_acom_def)
|
|
53 |
by (metis wt_acom_def wt_step' order_refl)
|
|
54 |
|
|
55 |
end
|
|
56 |
|
|
57 |
|
|
58 |
subsection "Widening and Narrowing"
|
|
59 |
|
|
60 |
class widen =
|
|
61 |
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
|
|
62 |
|
|
63 |
class narrow =
|
|
64 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
|
|
65 |
|
|
66 |
class WN = widen + narrow + preord +
|
|
67 |
assumes widen1: "x \<sqsubseteq> x \<nabla> y"
|
|
68 |
assumes widen2: "y \<sqsubseteq> x \<nabla> y"
|
|
69 |
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
|
|
70 |
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
|
|
71 |
|
|
72 |
class WN_Wt = widen + narrow + preord + Wt +
|
|
73 |
assumes widen1: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
|
|
74 |
assumes widen2: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
|
|
75 |
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
|
|
76 |
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
|
|
77 |
assumes Wt_widen[simp]: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> Wt (x \<nabla> y) c"
|
|
78 |
assumes Wt_narrow[simp]: "Wt x c \<Longrightarrow> Wt y c \<Longrightarrow> Wt (x \<triangle> y) c"
|
|
79 |
|
|
80 |
|
|
81 |
instantiation ivl :: WN
|
|
82 |
begin
|
|
83 |
|
|
84 |
definition "widen_ivl ivl1 ivl2 =
|
|
85 |
((*if is_empty ivl1 then ivl2 else
|
|
86 |
if is_empty ivl2 then ivl1 else*)
|
|
87 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
|
|
88 |
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
|
|
89 |
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
|
|
90 |
|
|
91 |
definition "narrow_ivl ivl1 ivl2 =
|
|
92 |
((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
|
|
93 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
|
|
94 |
I (if l1 = None then l2 else l1)
|
|
95 |
(if h1 = None then h2 else h1))"
|
|
96 |
|
|
97 |
instance
|
|
98 |
proof qed
|
|
99 |
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
|
|
100 |
|
|
101 |
end
|
|
102 |
|
|
103 |
|
|
104 |
instantiation st :: (WN)WN_Wt
|
|
105 |
begin
|
|
106 |
|
|
107 |
definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
|
|
108 |
|
|
109 |
definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
|
|
110 |
|
|
111 |
instance
|
|
112 |
proof
|
|
113 |
case goal1 thus ?case
|
|
114 |
by(simp add: widen_st_def le_st_def WN_class.widen1)
|
|
115 |
next
|
|
116 |
case goal2 thus ?case
|
|
117 |
by(simp add: widen_st_def le_st_def WN_class.widen2 Wt_st_def wt_st_def)
|
|
118 |
next
|
|
119 |
case goal3 thus ?case
|
|
120 |
by(auto simp: narrow_st_def le_st_def WN_class.narrow1)
|
|
121 |
next
|
|
122 |
case goal4 thus ?case
|
|
123 |
by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
|
|
124 |
next
|
|
125 |
case goal5 thus ?case by(auto simp: widen_st_def Wt_st_def wt_st_def)
|
|
126 |
next
|
|
127 |
case goal6 thus ?case by(auto simp: narrow_st_def Wt_st_def wt_st_def)
|
|
128 |
qed
|
|
129 |
|
|
130 |
end
|
|
131 |
|
|
132 |
|
|
133 |
instantiation option :: (WN_Wt)WN_Wt
|
|
134 |
begin
|
|
135 |
|
|
136 |
fun widen_option where
|
|
137 |
"None \<nabla> x = x" |
|
|
138 |
"x \<nabla> None = x" |
|
|
139 |
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
|
|
140 |
|
|
141 |
fun narrow_option where
|
|
142 |
"None \<triangle> x = None" |
|
|
143 |
"x \<triangle> None = None" |
|
|
144 |
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
|
|
145 |
|
|
146 |
instance
|
|
147 |
proof
|
|
148 |
case goal1 thus ?case
|
|
149 |
by(induct x y rule: widen_option.induct)(simp_all add: widen1)
|
|
150 |
next
|
|
151 |
case goal2 thus ?case
|
|
152 |
by(induct x y rule: widen_option.induct)(simp_all add: widen2)
|
|
153 |
next
|
|
154 |
case goal3 thus ?case
|
|
155 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
|
|
156 |
next
|
|
157 |
case goal4 thus ?case
|
|
158 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
|
|
159 |
next
|
|
160 |
case goal5 thus ?case
|
|
161 |
by(induction x y rule: widen_option.induct)(auto simp: Wt_st_def)
|
|
162 |
next
|
|
163 |
case goal6 thus ?case
|
|
164 |
by(induction x y rule: narrow_option.induct)(auto simp: Wt_st_def)
|
|
165 |
qed
|
|
166 |
|
|
167 |
end
|
|
168 |
|
|
169 |
|
|
170 |
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
|
|
171 |
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
|
|
172 |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
|
|
173 |
"map2_acom f (C1;C2) (D1;D2) = (map2_acom f C1 D1; map2_acom f C2 D2)" |
|
|
174 |
"map2_acom f (IF b THEN C1 ELSE C2 {a1}) (IF b' THEN D1 ELSE D2 {a2}) =
|
|
175 |
(IF b THEN map2_acom f C1 D1 ELSE map2_acom f C2 D2 {f a1 a2})" |
|
|
176 |
"map2_acom f ({a1} WHILE b DO C {a2}) ({a3} WHILE b' DO C' {a4}) =
|
|
177 |
({f a1 a3} WHILE b DO map2_acom f C C' {f a2 a4})"
|
|
178 |
|
|
179 |
instantiation acom :: (WN_Wt)WN_Wt
|
|
180 |
begin
|
|
181 |
|
|
182 |
definition "widen_acom = map2_acom (op \<nabla>)"
|
|
183 |
|
|
184 |
definition "narrow_acom = map2_acom (op \<triangle>)"
|
|
185 |
|
|
186 |
lemma widen_acom1:
|
|
187 |
"\<lbrakk>\<forall>a\<in>set(annos x). Wt a c; \<forall>a\<in>set (annos y). Wt a c; strip x = strip y\<rbrakk>
|
|
188 |
\<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
|
|
189 |
by(induct x y rule: le_acom.induct)
|
|
190 |
(auto simp: widen_acom_def widen1 Wt_acom_def)
|
|
191 |
|
|
192 |
lemma widen_acom2:
|
|
193 |
"\<lbrakk>\<forall>a\<in>set(annos x). Wt a c; \<forall>a\<in>set (annos y). Wt a c; strip x = strip y\<rbrakk>
|
|
194 |
\<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
|
|
195 |
by(induct x y rule: le_acom.induct)
|
|
196 |
(auto simp: widen_acom_def widen2 Wt_acom_def)
|
|
197 |
|
|
198 |
lemma strip_map2_acom[simp]:
|
|
199 |
"strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1"
|
|
200 |
by(induct f C1 C2 rule: map2_acom.induct) simp_all
|
|
201 |
|
|
202 |
lemma strip_widen_acom[simp]:
|
|
203 |
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1"
|
|
204 |
by(simp add: widen_acom_def strip_map2_acom)
|
|
205 |
|
|
206 |
lemma strip_narrow_acom[simp]:
|
|
207 |
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
|
|
208 |
by(simp add: narrow_acom_def strip_map2_acom)
|
|
209 |
|
|
210 |
lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
|
|
211 |
annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
|
|
212 |
by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2)
|
|
213 |
|
|
214 |
instance
|
|
215 |
proof
|
|
216 |
case goal1 thus ?case by(auto simp: Wt_acom_def widen_acom1)
|
|
217 |
next
|
|
218 |
case goal2 thus ?case by(auto simp: Wt_acom_def widen_acom2)
|
|
219 |
next
|
|
220 |
case goal3 thus ?case
|
|
221 |
by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
|
|
222 |
next
|
|
223 |
case goal4 thus ?case
|
|
224 |
by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
|
|
225 |
next
|
|
226 |
case goal5 thus ?case
|
|
227 |
by(auto simp: Wt_acom_def widen_acom_def split_conv elim!: in_set_zipE)
|
|
228 |
next
|
|
229 |
case goal6 thus ?case
|
|
230 |
by(auto simp: Wt_acom_def narrow_acom_def split_conv elim!: in_set_zipE)
|
|
231 |
qed
|
|
232 |
|
|
233 |
end
|
|
234 |
|
|
235 |
lemma wt_widen_o[simp]: fixes x1 x2 :: "_ st option"
|
|
236 |
shows "wt x1 X \<Longrightarrow> wt x2 X \<Longrightarrow> wt (x1 \<nabla> x2) X"
|
|
237 |
by(induction x1 x2 rule: widen_option.induct)
|
|
238 |
(simp_all add: widen_st_def wt_st_def)
|
|
239 |
|
|
240 |
lemma wt_narrow_o[simp]: fixes x1 x2 :: "_ st option"
|
|
241 |
shows "wt x1 X \<Longrightarrow> wt x2 X \<Longrightarrow> wt (x1 \<triangle> x2) X"
|
|
242 |
by(induction x1 x2 rule: narrow_option.induct)
|
|
243 |
(simp_all add: narrow_st_def wt_st_def)
|
|
244 |
|
|
245 |
lemma wt_widen_c: fixes C1 C2 :: "_ st option acom"
|
|
246 |
shows "strip C1 = strip C2 \<Longrightarrow> wt C1 X \<Longrightarrow> wt C2 X \<Longrightarrow> wt (C1 \<nabla> C2) X"
|
|
247 |
by(induction C1 C2 rule: le_acom.induct)
|
|
248 |
(auto simp: widen_acom_def)
|
|
249 |
|
|
250 |
lemma wt_narrow_c: fixes C1 C2 :: "_ st option acom"
|
|
251 |
shows "strip C1 = strip C2 \<Longrightarrow> wt C1 X \<Longrightarrow> wt C2 X \<Longrightarrow> wt (C1 \<triangle> C2) X"
|
|
252 |
by(induction C1 C2 rule: le_acom.induct)
|
|
253 |
(auto simp: narrow_acom_def)
|
|
254 |
|
|
255 |
lemma Wt_bot[simp]: "Wt (bot c) c"
|
|
256 |
by(simp add: Wt_acom_def bot_def)
|
|
257 |
|
|
258 |
|
|
259 |
subsubsection "Post-fixed point computation"
|
|
260 |
|
|
261 |
definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
|
|
262 |
where "iter_widen f = while_option (\<lambda>c. \<not> f c \<sqsubseteq> c) (\<lambda>c. c \<nabla> f c)"
|
|
263 |
|
|
264 |
definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
|
|
265 |
where "iter_narrow f = while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle> f c) (\<lambda>c. c \<triangle> f c)"
|
|
266 |
|
|
267 |
definition pfp_wn :: "(('a::WN_Wt option acom) \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option"
|
|
268 |
where "pfp_wn f c =
|
|
269 |
(case iter_widen f (bot c) of None \<Rightarrow> None | Some c' \<Rightarrow> iter_narrow f c')"
|
|
270 |
|
|
271 |
|
|
272 |
lemma iter_widen_pfp: "iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'"
|
|
273 |
by(auto simp add: iter_widen_def dest: while_option_stop)
|
|
274 |
|
|
275 |
lemma iter_widen_inv:
|
|
276 |
assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x"
|
|
277 |
and "iter_widen f x = Some y" shows "P y"
|
|
278 |
using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]]
|
|
279 |
by (blast intro: assms(1-3))
|
|
280 |
|
|
281 |
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
|
|
282 |
assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'"
|
|
283 |
shows "strip C' = strip C"
|
|
284 |
using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
|
|
285 |
by (metis assms(1))
|
|
286 |
|
|
287 |
lemma strip_iter_widen: fixes f :: "'a::WN_Wt acom \<Rightarrow> 'a acom"
|
|
288 |
assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
|
|
289 |
shows "strip C' = strip C"
|
|
290 |
proof-
|
|
291 |
have "\<forall>C. strip(C \<nabla> f C) = strip C"
|
|
292 |
by (metis assms(1) strip_map2_acom widen_acom_def)
|
|
293 |
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
|
|
294 |
qed
|
|
295 |
|
|
296 |
lemma iter_narrow_pfp:
|
|
297 |
assumes mono: "!!c1 c2::_::WN_Wt. P c1 \<Longrightarrow> P c2 \<Longrightarrow> c1 \<sqsubseteq> c2 \<Longrightarrow> f c1 \<sqsubseteq> f c2"
|
|
298 |
and Pinv: "!!c. P c \<Longrightarrow> P(f c)" "!!c1 c2. P c1 \<Longrightarrow> P c2 \<Longrightarrow> P(c1 \<triangle> c2)" and "P c0"
|
|
299 |
and "f c0 \<sqsubseteq> c0" and "iter_narrow f c0 = Some c"
|
|
300 |
shows "P c \<and> f c \<sqsubseteq> c"
|
|
301 |
proof-
|
|
302 |
let ?Q = "%c. P c \<and> f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0"
|
|
303 |
{ fix c assume "?Q c"
|
|
304 |
note P = conjunct1[OF this] and 12 = conjunct2[OF this]
|
|
305 |
note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
|
|
306 |
let ?c' = "c \<triangle> f c"
|
|
307 |
have "?Q ?c'"
|
|
308 |
proof auto
|
|
309 |
show "P ?c'" by (blast intro: P Pinv)
|
|
310 |
have "f ?c' \<sqsubseteq> f c" by(rule mono[OF `P (c \<triangle> f c)` P narrow2[OF 1]])
|
|
311 |
also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1[OF 1])
|
|
312 |
finally show "f ?c' \<sqsubseteq> ?c'" .
|
|
313 |
have "?c' \<sqsubseteq> c" by (rule narrow2[OF 1])
|
|
314 |
also have "c \<sqsubseteq> c0" by(rule 2)
|
|
315 |
finally show "?c' \<sqsubseteq> c0" .
|
|
316 |
qed
|
|
317 |
}
|
|
318 |
thus ?thesis
|
|
319 |
using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
|
|
320 |
by (blast intro: assms(4,5) le_refl)
|
|
321 |
qed
|
|
322 |
|
|
323 |
lemma pfp_wn_pfp:
|
|
324 |
assumes mono: "!!c1 c2::_::WN_Wt option acom. P c1 \<Longrightarrow> P c2 \<Longrightarrow> c1 \<sqsubseteq> c2 \<Longrightarrow> f c1 \<sqsubseteq> f c2"
|
|
325 |
and Pinv: "P (bot c)" "!!c. P c \<Longrightarrow> P(f c)"
|
|
326 |
"!!c1 c2. P c1 \<Longrightarrow> P c2 \<Longrightarrow> P(c1 \<nabla> c2)"
|
|
327 |
"!!c1 c2. P c1 \<Longrightarrow> P c2 \<Longrightarrow> P(c1 \<triangle> c2)"
|
|
328 |
and pfp_wn: "pfp_wn f c = Some c'" shows "P c' \<and> f c' \<sqsubseteq> c'"
|
|
329 |
proof-
|
|
330 |
from pfp_wn obtain p
|
|
331 |
where its: "iter_widen f (bot c) = Some p" "iter_narrow f p = Some c'"
|
|
332 |
by(auto simp: pfp_wn_def split: option.splits)
|
|
333 |
have "P p" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
|
|
334 |
thus ?thesis
|
|
335 |
by - (assumption |
|
|
336 |
rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
|
|
337 |
qed
|
|
338 |
|
|
339 |
lemma strip_pfp_wn:
|
|
340 |
"\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
|
|
341 |
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
|
|
342 |
(metis (no_types) narrow_acom_def strip_bot strip_iter_widen strip_map2_acom strip_while)
|
|
343 |
|
|
344 |
|
|
345 |
locale Abs_Int2 = Abs_Int1_mono
|
|
346 |
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"
|
|
347 |
begin
|
|
348 |
|
|
349 |
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
|
|
350 |
"AI_wn c = pfp_wn (step' (top c)) c"
|
|
351 |
|
|
352 |
lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
|
|
353 |
proof(simp add: CS_def AI_wn_def)
|
|
354 |
assume 1: "pfp_wn (step' (top c)) c = Some C"
|
|
355 |
have 2: "(strip C = c & wt C (vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
|
|
356 |
by(rule pfp_wn_pfp[where c=c])
|
|
357 |
(simp_all add: 1 mono_step'_top wt_widen_c wt_narrow_c)
|
|
358 |
have 3: "strip (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) = c" by(simp add: strip_pfp_wn[OF _ 1])
|
|
359 |
have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
|
|
360 |
proof(rule lfp_lowerbound[simplified,OF 3])
|
|
361 |
show "step UNIV (\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)) \<le> \<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C)"
|
|
362 |
proof(rule step_preserves_le[OF _ _ _ wt_top])
|
|
363 |
show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>\<^bsub>c\<^esub>" by simp
|
|
364 |
show "\<gamma>\<^isub>c (step' \<top>\<^bsub>c\<^esub> C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF conjunct2[OF 2]])
|
|
365 |
show "wt C (vars c)" using 2 by blast
|
|
366 |
qed
|
|
367 |
qed
|
|
368 |
from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
|
|
369 |
by (blast intro: mono_gamma_c order_trans)
|
|
370 |
qed
|
|
371 |
|
|
372 |
end
|
|
373 |
|
|
374 |
interpretation Abs_Int2
|
|
375 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
|
|
376 |
and test_num' = in_ivl
|
|
377 |
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
|
|
378 |
defines AI_ivl' is AI_wn
|
|
379 |
..
|
|
380 |
|
|
381 |
|
|
382 |
subsubsection "Tests"
|
|
383 |
|
|
384 |
definition "step_up_ivl n =
|
|
385 |
((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
|
|
386 |
definition "step_down_ivl n =
|
|
387 |
((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
|
|
388 |
|
|
389 |
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
|
|
390 |
the loop took to execute. In contrast, @{const AI_ivl'} converges in a
|
|
391 |
constant number of steps: *}
|
|
392 |
|
|
393 |
value "show_acom (step_up_ivl 1 (bot test3_ivl))"
|
|
394 |
value "show_acom (step_up_ivl 2 (bot test3_ivl))"
|
|
395 |
value "show_acom (step_up_ivl 3 (bot test3_ivl))"
|
|
396 |
value "show_acom (step_up_ivl 4 (bot test3_ivl))"
|
|
397 |
value "show_acom (step_up_ivl 5 (bot test3_ivl))"
|
|
398 |
value "show_acom (step_down_ivl 1 (step_up_ivl 5 (bot test3_ivl)))"
|
|
399 |
value "show_acom (step_down_ivl 2 (step_up_ivl 5 (bot test3_ivl)))"
|
|
400 |
value "show_acom (step_down_ivl 3 (step_up_ivl 5 (bot test3_ivl)))"
|
|
401 |
value "show_acom_opt (AI_ivl' test3_ivl)"
|
|
402 |
|
|
403 |
|
|
404 |
text{* Now all the analyses terminate: *}
|
|
405 |
|
|
406 |
value "show_acom_opt (AI_ivl' test4_ivl)"
|
|
407 |
value "show_acom_opt (AI_ivl' test5_ivl)"
|
|
408 |
value "show_acom_opt (AI_ivl' test6_ivl)"
|
|
409 |
|
|
410 |
|
|
411 |
subsubsection "Generic Termination Proof"
|
|
412 |
|
|
413 |
locale Abs_Int2_measure = Abs_Int2
|
|
414 |
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set" +
|
|
415 |
fixes m :: "'av \<Rightarrow> nat"
|
|
416 |
fixes n :: "'av \<Rightarrow> nat"
|
|
417 |
fixes h :: "nat"
|
|
418 |
assumes m_anti_mono: "x \<sqsubseteq> y \<Longrightarrow> m x \<ge> m y"
|
|
419 |
assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
|
|
420 |
assumes m_height: "m x \<le> h"
|
|
421 |
assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
|
|
422 |
assumes n_narrow: "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
|
|
423 |
|
|
424 |
begin
|
|
425 |
|
|
426 |
definition "m_st S = (SUM x:dom S. m(fun S x))"
|
|
427 |
|
|
428 |
lemma h_st: assumes "finite X" and "dom S \<subseteq> X"
|
|
429 |
shows "m_st S \<le> h * card X"
|
|
430 |
proof(auto simp: m_st_def)
|
|
431 |
have "(\<Sum>x\<in>dom S. m (fun S x)) \<le> (\<Sum>x\<in>dom S. h)" (is "?L \<le> _")
|
|
432 |
by(rule setsum_mono)(simp add: m_height)
|
|
433 |
also have "\<dots> \<le> (\<Sum>x\<in>X. h)"
|
|
434 |
by(rule setsum_mono3[OF assms]) simp
|
|
435 |
also have "\<dots> = h * card X" by simp
|
|
436 |
finally show "?L \<le> \<dots>" .
|
|
437 |
qed
|
|
438 |
|
|
439 |
|
|
440 |
(* FIXME identical *)
|
|
441 |
lemma m_st_anti_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st S1 \<ge> m_st S2"
|
|
442 |
proof(auto simp add: le_st_def m_st_def)
|
|
443 |
assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
|
|
444 |
hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m_anti_mono)
|
|
445 |
thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
|
|
446 |
by (metis setsum_mono)
|
|
447 |
qed
|
|
448 |
|
|
449 |
lemma m_st_widen: "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> finite X \<Longrightarrow>
|
|
450 |
~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_st(S1 \<nabla> S2) < m_st S1"
|
|
451 |
proof(auto simp add: le_st_def m_st_def wt_st_def widen_st_def)
|
|
452 |
assume "finite(dom S1)"
|
|
453 |
have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
|
|
454 |
by (metis m_anti_mono WN_class.widen1)
|
|
455 |
fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
|
|
456 |
hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
|
|
457 |
using m_widen by blast
|
|
458 |
from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
|
|
459 |
show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
|
|
460 |
qed
|
|
461 |
|
|
462 |
definition "n_st S = (\<Sum>x\<in>dom S. n(fun S x))"
|
|
463 |
|
|
464 |
lemma n_st_mono: assumes "S1 \<sqsubseteq> S2" shows "n_st S1 \<le> n_st S2"
|
|
465 |
proof-
|
|
466 |
from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
|
|
467 |
by(simp_all add: le_st_def)
|
|
468 |
have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
|
|
469 |
by(rule setsum_mono)(simp add: le_st_def n_mono)
|
|
470 |
thus ?thesis by(simp add: n_st_def)
|
|
471 |
qed
|
|
472 |
|
|
473 |
lemma n_st_narrow:
|
|
474 |
assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
|
|
475 |
shows "n_st (S1 \<triangle> S2) < n_st S1"
|
|
476 |
proof-
|
|
477 |
from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
|
|
478 |
by(simp_all add: le_st_def)
|
|
479 |
have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
|
|
480 |
by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
|
|
481 |
have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
|
|
482 |
by(auto simp: le_st_def narrow_st_def intro: n_narrow)
|
|
483 |
have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
|
|
484 |
apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
|
|
485 |
moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
|
|
486 |
ultimately show ?thesis by(simp add: n_st_def)
|
|
487 |
qed
|
|
488 |
|
|
489 |
|
|
490 |
definition "m_o k opt = (case opt of None \<Rightarrow> k+1 | Some x \<Rightarrow> m_st x)"
|
|
491 |
|
|
492 |
lemma m_o_anti_mono: "wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> finite X \<Longrightarrow>
|
|
493 |
S1 \<sqsubseteq> S2 \<Longrightarrow> m_o (h * card X) S2 \<le> m_o (h * card X) S1"
|
|
494 |
apply(induction S1 S2 rule: le_option.induct)
|
|
495 |
apply(auto simp: m_o_def m_st_anti_mono le_SucI h_st wt_st_def
|
|
496 |
split: option.splits)
|
|
497 |
done
|
|
498 |
|
|
499 |
lemma m_o_widen: "\<lbrakk> wt S1 X; wt S2 X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
|
|
500 |
m_o (h * card X) (S1 \<nabla> S2) < m_o (h * card X) S1"
|
|
501 |
by(auto simp: m_o_def wt_st_def h_st less_Suc_eq_le m_st_widen
|
|
502 |
split: option.split)
|
|
503 |
|
|
504 |
definition "n_o opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n_st x + 1)"
|
|
505 |
|
|
506 |
lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n_o S1 \<le> n_o S2"
|
|
507 |
by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_st_mono)
|
|
508 |
|
|
509 |
lemma n_o_narrow:
|
|
510 |
"wt S1 X \<Longrightarrow> wt S2 X \<Longrightarrow> finite X
|
|
511 |
\<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n_o (S1 \<triangle> S2) < n_o S1"
|
|
512 |
apply(induction S1 S2 rule: narrow_option.induct)
|
|
513 |
apply(auto simp: n_o_def wt_st_def n_st_narrow)
|
|
514 |
done
|
|
515 |
|
|
516 |
|
|
517 |
lemma annos_narrow_acom[simp]: "strip C2 = strip (C1::'a::WN_Wt acom) \<Longrightarrow>
|
|
518 |
annos(C1 \<triangle> C2) = map (%(x,y).x\<triangle>y) (zip (annos C1) (annos C2))"
|
|
519 |
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" C1 C2 rule: map2_acom.induct)
|
|
520 |
(simp_all add: narrow_acom_def size_annos_same2)
|
|
521 |
|
|
522 |
|
|
523 |
definition "m_c C = (let as = annos C in
|
|
524 |
\<Sum>i=0..<size as. m_o (h * card(vars(strip C))) (as!i))"
|
|
525 |
|
|
526 |
lemma m_c_widen:
|
|
527 |
"Wt C1 c \<Longrightarrow> Wt C2 c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
|
|
528 |
apply(auto simp: Wt_acom_def m_c_def Let_def widen_acom_def)
|
|
529 |
apply(subgoal_tac "length(annos C2) = length(annos C1)")
|
|
530 |
prefer 2 apply (simp add: size_annos_same2)
|
|
531 |
apply (auto)
|
|
532 |
apply(rule setsum_strict_mono_ex1)
|
|
533 |
apply simp
|
|
534 |
apply (clarsimp)
|
|
535 |
apply(simp add: m_o_anti_mono finite_cvars widen1[where c = "strip C2"])
|
|
536 |
apply(auto simp: le_iff_le_annos listrel_iff_nth)
|
|
537 |
apply(rule_tac x=i in bexI)
|
|
538 |
prefer 2 apply simp
|
|
539 |
apply(rule m_o_widen)
|
|
540 |
apply (simp add: finite_cvars)+(*FIXME [simp]*)
|
|
541 |
done
|
|
542 |
|
|
543 |
definition "n_c C = (let as = annos C in \<Sum>i=0..<size as. n_o (as!i))"
|
|
544 |
|
|
545 |
lemma n_c_narrow:
|
|
546 |
"Wt C1 c \<Longrightarrow> Wt C2 c \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n_c (C1 \<triangle> C2) < n_c C1"
|
|
547 |
apply(auto simp: n_c_def Let_def Wt_acom_def narrow_acom_def)
|
|
548 |
apply(subgoal_tac "length(annos C2) = length(annos C1)")
|
|
549 |
prefer 2 apply (simp add: size_annos_same2)
|
|
550 |
apply (auto)
|
|
551 |
apply(rule setsum_strict_mono_ex1)
|
|
552 |
apply simp
|
|
553 |
apply (clarsimp)
|
|
554 |
apply(rule n_o_mono)
|
|
555 |
apply(rule narrow2)
|
|
556 |
apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
|
|
557 |
apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom)
|
|
558 |
apply(rule_tac x=i in bexI)
|
|
559 |
prefer 2 apply simp
|
|
560 |
apply(rule n_o_narrow[where X = "vars(strip C1)"])
|
|
561 |
apply (simp add: finite_cvars)+
|
|
562 |
done
|
|
563 |
|
|
564 |
end
|
|
565 |
|
|
566 |
|
|
567 |
lemma iter_widen_termination:
|
|
568 |
fixes m :: "'a::WN_Wt \<Rightarrow> nat"
|
|
569 |
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
|
|
570 |
and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
|
|
571 |
and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
|
|
572 |
and "P C" shows "EX C'. iter_widen f C = Some C'"
|
|
573 |
proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = P])
|
|
574 |
show "wf {(cc, c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc = c \<nabla> f c}"
|
|
575 |
by(rule wf_subset[OF wf_measure[of "m"]])(auto simp: m_widen P_f)
|
|
576 |
next
|
|
577 |
show "P C" by(rule `P C`)
|
|
578 |
next
|
|
579 |
fix C assume "P C" thus "P (C \<nabla> f C)" by(simp add: P_f P_widen)
|
|
580 |
qed
|
|
581 |
thm mono_step'(*FIXME does not need wt assms*)
|
|
582 |
lemma iter_narrow_termination:
|
|
583 |
fixes n :: "'a::WN_Wt \<Rightarrow> nat"
|
|
584 |
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
|
|
585 |
and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
|
|
586 |
and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
|
|
587 |
and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> ~ C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
|
|
588 |
and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
|
|
589 |
proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "%C. P C \<and> f C \<sqsubseteq> C"])
|
|
590 |
show "wf {(c', c). ((P c \<and> f c \<sqsubseteq> c) \<and> \<not> c \<sqsubseteq> c \<triangle> f c) \<and> c' = c \<triangle> f c}"
|
|
591 |
by(rule wf_subset[OF wf_measure[of "n"]])(auto simp: n_narrow P_f)
|
|
592 |
next
|
|
593 |
show "P C \<and> f C \<sqsubseteq> C" using init by blast
|
|
594 |
next
|
|
595 |
fix C assume 1: "P C \<and> f C \<sqsubseteq> C"
|
|
596 |
hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
|
|
597 |
moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
|
|
598 |
by (metis narrow1 narrow2 1 mono preord_class.le_trans)
|
|
599 |
ultimately show "P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C" ..
|
|
600 |
qed
|
|
601 |
|
|
602 |
|
|
603 |
subsubsection "Termination: Intervals"
|
|
604 |
|
|
605 |
definition m_ivl :: "ivl \<Rightarrow> nat" where
|
|
606 |
"m_ivl ivl = (case ivl of I l h \<Rightarrow>
|
|
607 |
(case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
|
|
608 |
|
|
609 |
lemma m_ivl_height: "m_ivl ivl \<le> 2"
|
|
610 |
by(simp add: m_ivl_def split: ivl.split option.split)
|
|
611 |
|
|
612 |
lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
|
|
613 |
by(auto simp: m_ivl_def le_option_def le_ivl_def
|
|
614 |
split: ivl.split option.split if_splits)
|
|
615 |
|
|
616 |
lemma m_ivl_widen:
|
|
617 |
"~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
|
|
618 |
by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
|
|
619 |
split: ivl.splits option.splits if_splits)
|
|
620 |
|
|
621 |
definition n_ivl :: "ivl \<Rightarrow> nat" where
|
|
622 |
"n_ivl ivl = 2 - m_ivl ivl"
|
|
623 |
|
|
624 |
lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
|
|
625 |
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
|
|
626 |
|
|
627 |
lemma n_ivl_narrow:
|
|
628 |
"~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
|
|
629 |
by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
|
|
630 |
split: ivl.splits option.splits if_splits)
|
|
631 |
|
|
632 |
|
|
633 |
interpretation Abs_Int2_measure
|
|
634 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
|
|
635 |
and test_num' = in_ivl
|
|
636 |
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
|
|
637 |
and m = m_ivl and n = n_ivl and h = 2
|
|
638 |
proof
|
|
639 |
case goal1 thus ?case by(rule m_ivl_anti_mono)
|
|
640 |
next
|
|
641 |
case goal2 thus ?case by(rule m_ivl_widen)
|
|
642 |
next
|
|
643 |
case goal3 thus ?case by(rule m_ivl_height)
|
|
644 |
next
|
|
645 |
case goal4 thus ?case by(rule n_ivl_mono)
|
|
646 |
next
|
|
647 |
case goal5 thus ?case by(rule n_ivl_narrow)
|
|
648 |
qed
|
|
649 |
|
|
650 |
|
|
651 |
lemma iter_winden_step_ivl_termination:
|
|
652 |
"\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
|
|
653 |
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. Wt C c"])
|
|
654 |
apply (simp_all add: Wt_step' m_c_widen)
|
|
655 |
done
|
|
656 |
|
|
657 |
lemma iter_narrow_step_ivl_termination:
|
|
658 |
"Wt C0 c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
|
|
659 |
\<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
|
|
660 |
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. Wt C c"])
|
|
661 |
apply (simp add: Wt_step')
|
|
662 |
apply (simp)
|
|
663 |
apply(rule mono_step'_top)
|
|
664 |
apply(simp add: Wt_acom_def wt_acom_def)
|
|
665 |
apply(simp add: Wt_acom_def wt_acom_def)
|
|
666 |
apply assumption
|
|
667 |
apply(erule (3) n_c_narrow)
|
|
668 |
apply assumption
|
|
669 |
apply assumption
|
|
670 |
done
|
|
671 |
|
|
672 |
theorem AI_ivl'_termination:
|
|
673 |
"\<exists>C. AI_ivl' c = Some C"
|
|
674 |
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
|
|
675 |
split: option.split)
|
|
676 |
apply(rule iter_narrow_step_ivl_termination)
|
|
677 |
apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>c\<^esub>" and P = "%C. Wt C c"] Wt_bot Wt_widen Wt_step'[where S = "\<top>\<^bsub>c\<^esub>" and c=c, simplified])
|
|
678 |
apply(erule iter_widen_pfp)
|
|
679 |
done
|
|
680 |
|
|
681 |
(*unused_thms Abs_Int_init -*)
|
|
682 |
|
|
683 |
end
|