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