62 by(auto simp: narrow_st_def le_st_def lookup_def narrow2) |
62 by(auto simp: narrow_st_def le_st_def lookup_def narrow2) |
63 qed |
63 qed |
64 |
64 |
65 end |
65 end |
66 |
66 |
67 instantiation up :: (WN)WN |
67 instantiation option :: (WN)WN |
68 begin |
68 begin |
69 |
69 |
70 fun widen_up where |
70 fun widen_option where |
71 "widen_up Bot x = x" | |
71 "None \<nabla> x = x" | |
72 "widen_up x Bot = x" | |
72 "x \<nabla> None = x" | |
73 "widen_up (Up x) (Up y) = Up(x \<nabla> y)" |
73 "(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" |
74 |
74 |
75 fun narrow_up where |
75 fun narrow_option where |
76 "narrow_up Bot x = Bot" | |
76 "None \<triangle> x = None" | |
77 "narrow_up x Bot = Bot" | |
77 "x \<triangle> None = None" | |
78 "narrow_up (Up x) (Up y) = Up(x \<triangle> y)" |
78 "(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
79 |
79 |
80 instance |
80 instance |
81 proof |
81 proof |
82 case goal1 show ?case |
82 case goal1 show ?case |
83 by(induct x y rule: widen_up.induct) (simp_all add: widen1) |
83 by(induct x y rule: widen_option.induct) (simp_all add: widen1) |
84 next |
84 next |
85 case goal2 show ?case |
85 case goal2 show ?case |
86 by(induct x y rule: widen_up.induct) (simp_all add: widen2) |
86 by(induct x y rule: widen_option.induct) (simp_all add: widen2) |
87 next |
87 next |
88 case goal3 thus ?case |
88 case goal3 thus ?case |
89 by(induct x y rule: narrow_up.induct) (simp_all add: narrow1) |
89 by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
90 next |
90 next |
91 case goal4 thus ?case |
91 case goal4 thus ?case |
92 by(induct x y rule: narrow_up.induct) (simp_all add: narrow2) |
92 by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
93 qed |
93 qed |
94 |
94 |
95 end |
95 end |
96 |
96 |
97 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
97 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
127 definition |
127 definition |
128 prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
128 prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
129 "prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f" |
129 "prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f" |
130 |
130 |
131 definition |
131 definition |
132 pfp_WN :: "(('a::WN)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option" |
132 pfp_WN :: "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" |
133 where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None |
133 where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None |
134 | Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')" |
134 | Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')" |
135 |
135 |
136 lemma strip_map2_acom: |
136 lemma strip_map2_acom: |
137 "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1" |
137 "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1" |
181 by (metis (no_types) strip_lpfpc strip_map2_acom strip_while) |
181 by (metis (no_types) strip_lpfpc strip_map2_acom strip_while) |
182 |
182 |
183 locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set" |
183 locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set" |
184 begin |
184 begin |
185 |
185 |
186 definition AI_WN :: "com \<Rightarrow> 'a st up acom option" where |
186 definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where |
187 "AI_WN = pfp_WN (step \<top>)" |
187 "AI_WN = pfp_WN (step \<top>)" |
188 |
188 |
189 lemma AI_sound: "\<lbrakk> AI_WN c = Some c'; (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'" |
189 lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'" |
190 unfolding AI_WN_def |
190 proof(simp add: CS_def AI_WN_def) |
191 by(metis step_sound[of "\<top>" c' s t] strip_pfp_WN strip_step |
191 assume 1: "pfp_WN (step \<top>) c = Some c'" |
192 pfp_WN_pfp mono_def mono_step[OF le_refl] in_rep_Top_up) |
192 from pfp_WN_pfp[OF allI[OF strip_step] mono_step 1] |
|
193 have 2: "step \<top> c' \<sqsubseteq> c'" . |
|
194 have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1]) |
|
195 have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')" |
|
196 proof(rule lfp_lowerbound[OF 3]) |
|
197 show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')" |
|
198 proof(rule step_preserves_le[OF _ _ 3]) |
|
199 show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp |
|
200 show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2]) |
|
201 qed |
|
202 qed |
|
203 from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'" |
|
204 by (blast intro: mono_rep_c order_trans) |
|
205 qed |
193 |
206 |
194 end |
207 end |
195 |
208 |
196 interpretation |
209 interpretation |
197 Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl |
210 Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl |
198 defines AI_ivl' is AI_WN |
211 defines AI_ivl' is AI_WN |
199 proof qed |
212 proof qed |
200 |
213 |
201 value [code] "show_acom_opt (AI_ivl test3_ivl)" |
214 |
202 value [code] "show_acom_opt (AI_ivl' test3_ivl)" |
215 subsubsection "Tests" |
203 |
216 |
204 definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)" |
217 definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)" |
205 definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)" |
218 definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)" |
|
219 |
|
220 text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as |
|
221 the loop took to execute. In contrast, @{const AI_ivl} converges in a |
|
222 constant number of steps: *} |
206 |
223 |
207 value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))" |
224 value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))" |
208 value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))" |
225 value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))" |
209 value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))" |
226 value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))" |
210 value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))" |
227 value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))" |
211 value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))" |
228 value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))" |
212 value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
229 value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
213 value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
230 value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
214 value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
231 value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
215 |
232 |
|
233 text{* Now all the analyses terminate: *} |
|
234 |
216 value [code] "show_acom_opt (AI_ivl' test4_ivl)" |
235 value [code] "show_acom_opt (AI_ivl' test4_ivl)" |
217 value [code] "show_acom_opt (AI_ivl' test5_ivl)" |
236 value [code] "show_acom_opt (AI_ivl' test5_ivl)" |
218 value [code] "show_acom_opt (AI_ivl' test6_ivl)" |
237 value [code] "show_acom_opt (AI_ivl' test6_ivl)" |
219 |
238 |
220 end |
239 end |