|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Abs_Int2_ivl |
|
4 imports Abs_Int2 |
|
5 begin |
|
6 |
|
7 subsection "Interval Analysis" |
|
8 |
|
9 datatype ivl = I "int option" "int option" |
|
10 |
|
11 definition "\<gamma>_ivl i = (case i of |
|
12 I (Some l) (Some h) \<Rightarrow> {l..h} | |
|
13 I (Some l) None \<Rightarrow> {l..} | |
|
14 I None (Some h) \<Rightarrow> {..h} | |
|
15 I None None \<Rightarrow> UNIV)" |
|
16 |
|
17 abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl" ("{_\<dots>_}") where |
|
18 "{lo\<dots>hi} == I (Some lo) (Some hi)" |
|
19 abbreviation I_Some_None :: "int \<Rightarrow> ivl" ("{_\<dots>}") where |
|
20 "{lo\<dots>} == I (Some lo) None" |
|
21 abbreviation I_None_Some :: "int \<Rightarrow> ivl" ("{\<dots>_}") where |
|
22 "{\<dots>hi} == I None (Some hi)" |
|
23 abbreviation I_None_None :: "ivl" ("{\<dots>}") where |
|
24 "{\<dots>} == I None None" |
|
25 |
|
26 definition "num_ivl n = {n\<dots>n}" |
|
27 |
|
28 fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where |
|
29 "in_ivl k (I (Some l) (Some h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" | |
|
30 "in_ivl k (I (Some l) None) \<longleftrightarrow> l \<le> k" | |
|
31 "in_ivl k (I None (Some h)) \<longleftrightarrow> k \<le> h" | |
|
32 "in_ivl k (I None None) \<longleftrightarrow> True" |
|
33 |
|
34 instantiation option :: (plus)plus |
|
35 begin |
|
36 |
|
37 fun plus_option where |
|
38 "Some x + Some y = Some(x+y)" | |
|
39 "_ + _ = None" |
|
40 |
|
41 instance .. |
|
42 |
|
43 end |
|
44 |
|
45 definition empty where "empty = {1\<dots>0}" |
|
46 |
|
47 fun is_empty where |
|
48 "is_empty {l\<dots>h} = (h<l)" | |
|
49 "is_empty _ = False" |
|
50 |
|
51 lemma [simp]: "is_empty(I l h) = |
|
52 (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)" |
|
53 by(auto split:option.split) |
|
54 |
|
55 lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}" |
|
56 by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split) |
|
57 |
|
58 definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else |
|
59 case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))" |
|
60 |
|
61 instantiation ivl :: SL_top |
|
62 begin |
|
63 |
|
64 definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where |
|
65 "le_option pos x y = |
|
66 (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos) |
|
67 | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))" |
|
68 |
|
69 fun le_aux where |
|
70 "le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)" |
|
71 |
|
72 definition le_ivl where |
|
73 "i1 \<sqsubseteq> i2 = |
|
74 (if is_empty i1 then True else |
|
75 if is_empty i2 then False else le_aux i1 i2)" |
|
76 |
|
77 definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where |
|
78 "min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)" |
|
79 |
|
80 definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where |
|
81 "max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)" |
|
82 |
|
83 definition "i1 \<squnion> i2 = |
|
84 (if is_empty i1 then i2 else if is_empty i2 then i1 |
|
85 else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> |
|
86 I (min_option False l1 l2) (max_option True h1 h2))" |
|
87 |
|
88 definition "\<top> = {\<dots>}" |
|
89 |
|
90 instance |
|
91 proof |
|
92 case goal1 thus ?case |
|
93 by(cases x, simp add: le_ivl_def le_option_def split: option.split) |
|
94 next |
|
95 case goal2 thus ?case |
|
96 by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits) |
|
97 next |
|
98 case goal3 thus ?case |
|
99 by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits) |
|
100 next |
|
101 case goal4 thus ?case |
|
102 by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits) |
|
103 next |
|
104 case goal5 thus ?case |
|
105 by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits) |
|
106 next |
|
107 case goal6 thus ?case |
|
108 by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split) |
|
109 qed |
|
110 |
|
111 end |
|
112 |
|
113 |
|
114 instantiation ivl :: L_top_bot |
|
115 begin |
|
116 |
|
117 definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else |
|
118 case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> |
|
119 I (max_option False l1 l2) (min_option True h1 h2))" |
|
120 |
|
121 definition "\<bottom> = empty" |
|
122 |
|
123 instance |
|
124 proof |
|
125 case goal2 thus ?case |
|
126 by (simp add:meet_ivl_def empty_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits) |
|
127 next |
|
128 case goal3 thus ?case |
|
129 by (simp add: empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits) |
|
130 next |
|
131 case goal4 thus ?case |
|
132 by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits) |
|
133 next |
|
134 case goal1 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def) |
|
135 qed |
|
136 |
|
137 end |
|
138 |
|
139 instantiation option :: (minus)minus |
|
140 begin |
|
141 |
|
142 fun minus_option where |
|
143 "Some x - Some y = Some(x-y)" | |
|
144 "_ - _ = None" |
|
145 |
|
146 instance .. |
|
147 |
|
148 end |
|
149 |
|
150 definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else |
|
151 case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))" |
|
152 |
|
153 lemma gamma_minus_ivl: |
|
154 "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)" |
|
155 by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits option.splits) |
|
156 |
|
157 definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*) |
|
158 i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)" |
|
159 |
|
160 fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where |
|
161 "filter_less_ivl res (I l1 h1) (I l2 h2) = |
|
162 (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else |
|
163 if res |
|
164 then (I l1 (min_option True h1 (h2 - Some 1)), |
|
165 I (max_option False (l1 + Some 1) l2) h2) |
|
166 else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" |
|
167 |
|
168 interpretation Val_abs |
|
169 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl |
|
170 proof |
|
171 case goal1 thus ?case |
|
172 by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits) |
|
173 next |
|
174 case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def) |
|
175 next |
|
176 case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def) |
|
177 next |
|
178 case goal4 thus ?case |
|
179 by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits) |
|
180 qed |
|
181 |
|
182 interpretation Val_abs1_gamma |
|
183 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl |
|
184 defines aval_ivl is aval' |
|
185 proof |
|
186 case goal1 thus ?case |
|
187 by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) |
|
188 next |
|
189 case goal2 show ?case by(auto simp add: Bot_ivl_def \<gamma>_ivl_def empty_def) |
|
190 qed |
|
191 |
|
192 lemma mono_minus_ivl: |
|
193 "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'" |
|
194 apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits) |
|
195 apply(simp split: option.splits) |
|
196 apply(simp split: option.splits) |
|
197 apply(simp split: option.splits) |
|
198 done |
|
199 |
|
200 |
|
201 interpretation Val_abs1 |
|
202 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl |
|
203 and test_num' = in_ivl |
|
204 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
|
205 proof |
|
206 case goal1 thus ?case |
|
207 by (simp add: \<gamma>_ivl_def split: ivl.split option.split) |
|
208 next |
|
209 case goal2 thus ?case |
|
210 by(auto simp add: filter_plus_ivl_def) |
|
211 (metis gamma_minus_ivl add_diff_cancel add_commute)+ |
|
212 next |
|
213 case goal3 thus ?case |
|
214 by(cases a1, cases a2, |
|
215 auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) |
|
216 qed |
|
217 |
|
218 interpretation Abs_Int1 |
|
219 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl |
|
220 and test_num' = in_ivl |
|
221 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
|
222 defines afilter_ivl is afilter |
|
223 and bfilter_ivl is bfilter |
|
224 and step_ivl is step' |
|
225 and AI_ivl is AI |
|
226 and aval_ivl' is aval'' |
|
227 .. |
|
228 |
|
229 |
|
230 text{* Monotonicity: *} |
|
231 |
|
232 interpretation Abs_Int1_mono |
|
233 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl |
|
234 and test_num' = in_ivl |
|
235 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
|
236 proof |
|
237 case goal1 thus ?case |
|
238 by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits) |
|
239 next |
|
240 case goal2 thus ?case |
|
241 by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl) |
|
242 next |
|
243 case goal3 thus ?case |
|
244 apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def) |
|
245 by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits) |
|
246 qed |
|
247 |
|
248 |
|
249 subsubsection "Tests" |
|
250 |
|
251 value "show_acom_opt (AI_ivl test1_ivl)" |
|
252 |
|
253 text{* Better than @{text AI_const}: *} |
|
254 value "show_acom_opt (AI_ivl test3_const)" |
|
255 value "show_acom_opt (AI_ivl test4_const)" |
|
256 value "show_acom_opt (AI_ivl test6_const)" |
|
257 |
|
258 definition "steps c i = (step_ivl(top c) ^^ i) (bot c)" |
|
259 |
|
260 value "show_acom_opt (AI_ivl test2_ivl)" |
|
261 value "show_acom (steps test2_ivl 0)" |
|
262 value "show_acom (steps test2_ivl 1)" |
|
263 value "show_acom (steps test2_ivl 2)" |
|
264 |
|
265 text{* Fixed point reached in 2 steps. |
|
266 Not so if the start value of x is known: *} |
|
267 |
|
268 value "show_acom_opt (AI_ivl test3_ivl)" |
|
269 value "show_acom (steps test3_ivl 0)" |
|
270 value "show_acom (steps test3_ivl 1)" |
|
271 value "show_acom (steps test3_ivl 2)" |
|
272 value "show_acom (steps test3_ivl 3)" |
|
273 value "show_acom (steps test3_ivl 4)" |
|
274 |
|
275 text{* Takes as many iterations as the actual execution. Would diverge if |
|
276 loop did not terminate. Worse still, as the following example shows: even if |
|
277 the actual execution terminates, the analysis may not. The value of y keeps |
|
278 decreasing as the analysis is iterated, no matter how long: *} |
|
279 |
|
280 value "show_acom (steps test4_ivl 50)" |
|
281 |
|
282 text{* Relationships between variables are NOT captured: *} |
|
283 value "show_acom_opt (AI_ivl test5_ivl)" |
|
284 |
|
285 text{* Again, the analysis would not terminate: *} |
|
286 value "show_acom (steps test6_ivl 50)" |
|
287 |
|
288 end |