248 lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]" |
248 lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]" |
249 by transfer (simp add: uminus_rep_def) |
249 by transfer (simp add: uminus_rep_def) |
250 |
250 |
251 instantiation ivl :: minus |
251 instantiation ivl :: minus |
252 begin |
252 begin |
253 definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl) - iv2 = iv1 + -iv2" |
253 |
|
254 definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where |
|
255 "(iv1::ivl) - iv2 = iv1 + -iv2" |
|
256 |
254 instance .. |
257 instance .. |
255 end |
258 end |
256 |
259 |
257 |
260 |
258 definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where |
261 definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where |
259 "filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))" |
262 "filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))" |
260 |
263 |
261 definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where |
264 definition above_rep :: "eint2 \<Rightarrow> eint2" where |
262 "filter_less_rep res p1 p2 = |
265 "above_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (l,\<infinity>))" |
263 (if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else |
266 |
264 let (l1,h1) = p1; (l2,h2) = p2 in |
267 definition below_rep :: "eint2 \<Rightarrow> eint2" where |
265 if res |
268 "below_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (-\<infinity>,h))" |
266 then ((l1, min h1 (h2 + Fin -1)), (max (l1 + Fin 1) l2, h2)) |
269 |
267 else ((max l1 l2, h1), (l2, min h1 h2)))" |
270 lift_definition above :: "ivl \<Rightarrow> ivl" is above_rep |
268 |
271 by(auto simp: above_rep_def eq_ivl_iff) |
269 lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep |
272 |
270 by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff) |
273 lift_definition below :: "ivl \<Rightarrow> ivl" is below_rep |
271 declare filter_less_ivl.abs_eq[code] (* bug in lifting *) |
274 by(auto simp: below_rep_def eq_ivl_iff) |
272 |
275 |
273 lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] = |
276 lemma \<gamma>_aboveI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> i \<le> j \<Longrightarrow> j \<in> \<gamma>_ivl(above iv)" |
274 (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else |
277 by transfer |
275 if b |
278 (auto simp add: above_rep_def \<gamma>_rep_cases is_empty_rep_def |
276 then ([l1 \<dots> min h1 (h2 + Fin -1)], [max (l1 + Fin 1) l2 \<dots> h2]) |
279 split: extended.splits) |
277 else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))" |
280 |
278 unfolding prod_rel_eq[symmetric] bot_ivl_def |
281 lemma \<gamma>_belowI: "i : \<gamma>_ivl iv \<Longrightarrow> j \<le> i \<Longrightarrow> j : \<gamma>_ivl(below iv)" |
279 by transfer (auto simp: filter_less_rep_def eq_ivl_empty) |
282 by transfer |
|
283 (auto simp add: below_rep_def \<gamma>_rep_cases is_empty_rep_def |
|
284 split: extended.splits) |
|
285 |
|
286 definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where |
|
287 "filter_less_ivl res iv1 iv2 = |
|
288 (if res |
|
289 then (iv1 \<sqinter> (below iv2 - [Fin 1\<dots>Fin 1]), |
|
290 iv2 \<sqinter> (above iv1 + [Fin 1\<dots>Fin 1])) |
|
291 else (iv1 \<sqinter> above iv2, iv2 \<sqinter> below iv1))" |
|
292 |
|
293 lemma above_nice: "above[l\<dots>h] = (if [l\<dots>h] = \<bottom> then \<bottom> else [l\<dots>\<infinity>])" |
|
294 unfolding bot_ivl_def by transfer (simp add: above_rep_def eq_ivl_empty) |
|
295 |
|
296 lemma below_nice: "below[l\<dots>h] = (if [l\<dots>h] = \<bottom> then \<bottom> else [-\<infinity>\<dots>h])" |
|
297 unfolding bot_ivl_def by transfer (simp add: below_rep_def eq_ivl_empty) |
280 |
298 |
281 lemma add_mono_le_Fin: |
299 lemma add_mono_le_Fin: |
282 "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))" |
300 "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))" |
283 by(drule (1) add_mono) simp |
301 by(drule (1) add_mono) simp |
284 |
302 |
285 lemma add_mono_Fin_le: |
303 lemma add_mono_Fin_le: |
286 "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2" |
304 "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2" |
287 by(drule (1) add_mono) simp |
305 by(drule (1) add_mono) simp |
288 |
|
289 lemma plus_rep_plus: |
|
290 "\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)" |
|
291 by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin) |
|
292 |
306 |
293 interpretation Val_abs |
307 interpretation Val_abs |
294 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
308 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
295 proof |
309 proof |
296 case goal1 thus ?case by transfer (simp add: le_iff_subset) |
310 case goal1 thus ?case by transfer (simp add: le_iff_subset) |
321 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
335 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
322 proof |
336 proof |
323 case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def) |
337 case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def) |
324 next |
338 next |
325 case goal2 thus ?case |
339 case goal2 thus ?case |
326 unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric] |
340 unfolding filter_plus_ivl_def minus_ivl_def |
327 apply(clarsimp simp add: \<gamma>_inf) |
341 apply(clarsimp simp add: \<gamma>_inf) |
328 using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"] |
342 using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"] |
329 by(simp add: \<gamma>_uminus) |
343 by(simp add: \<gamma>_uminus) |
330 next |
344 next |
331 case goal3 thus ?case |
345 case goal3 thus ?case |
332 unfolding prod_rel_eq[symmetric] |
346 unfolding filter_less_ivl_def minus_ivl_def |
333 apply transfer |
347 apply(clarsimp simp add: \<gamma>_inf split: if_splits) |
334 apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits) |
348 using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"] |
335 apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits) |
349 apply(simp add: \<gamma>_belowI[of i2] \<gamma>_aboveI[of i1] |
|
350 uminus_ivl.abs_eq uminus_rep_def \<gamma>_ivl_nice) |
|
351 apply(simp add: \<gamma>_aboveI[of i2] \<gamma>_belowI[of i1]) |
336 done |
352 done |
337 qed |
353 qed |
338 |
354 |
339 interpretation Abs_Int1 |
355 interpretation Abs_Int1 |
340 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
356 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
348 .. |
364 .. |
349 |
365 |
350 |
366 |
351 text{* Monotonicity: *} |
367 text{* Monotonicity: *} |
352 |
368 |
353 lemma mono_inf_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (inf_rep p1 q1) (inf_rep p2 q2)" |
369 lemma mono_plus_ivl: "iv1 \<le> iv2 \<Longrightarrow> iv3 \<le> iv4 \<Longrightarrow> iv1+iv3 \<le> iv2+(iv4::ivl)" |
354 by(auto simp add: le_iff_subset \<gamma>_inf_rep) |
370 apply transfer |
355 |
|
356 lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)" |
|
357 apply(auto simp: plus_rep_def le_iff_subset split: if_splits) |
371 apply(auto simp: plus_rep_def le_iff_subset split: if_splits) |
358 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
372 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
359 |
373 |
360 lemma mono_minus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep (uminus_rep p1) (uminus_rep p2)" |
374 lemma mono_minus_ivl: "iv1 \<le> iv2 \<Longrightarrow> -iv1 \<le> -(iv2::ivl)" |
|
375 apply transfer |
361 apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split) |
376 apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split) |
362 by(auto simp: \<gamma>_rep_cases split: extended.splits) |
377 by(auto simp: \<gamma>_rep_cases split: extended.splits) |
|
378 |
|
379 lemma mono_above: "iv1 \<le> iv2 \<Longrightarrow> above iv1 \<le> above iv2" |
|
380 apply transfer |
|
381 apply(auto simp: above_rep_def le_iff_subset split: if_splits prod.split) |
|
382 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
|
383 |
|
384 lemma mono_below: "iv1 \<le> iv2 \<Longrightarrow> below iv1 \<le> below iv2" |
|
385 apply transfer |
|
386 apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split) |
|
387 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
363 |
388 |
364 interpretation Abs_Int1_mono |
389 interpretation Abs_Int1_mono |
365 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
390 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
366 and test_num' = in_ivl |
391 and test_num' = in_ivl |
367 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
392 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
368 proof |
393 proof |
369 case goal1 thus ?case by transfer (rule mono_plus_rep) |
394 case goal1 thus ?case by (rule mono_plus_ivl) |
370 next |
395 next |
371 case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def |
396 case goal2 thus ?case |
372 by transfer (auto simp: mono_inf_rep mono_plus_rep mono_minus_rep) |
397 unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def |
373 next |
398 by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_minus_ivl) |
374 case goal3 thus ?case unfolding less_eq_prod_def |
399 next |
375 apply transfer |
400 case goal3 thus ?case |
376 apply(auto simp:filter_less_rep_def le_iff_subset min_def max_def split: if_splits) |
401 unfolding less_eq_prod_def filter_less_ivl_def minus_ivl_def |
377 by(auto simp:is_empty_rep_iff \<gamma>_rep_cases split: extended.splits) |
402 by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_above mono_below) |
378 qed |
403 qed |
379 |
404 |
380 |
405 |
381 subsubsection "Tests" |
406 subsubsection "Tests" |
382 |
407 |