(* Author: Tobias Nipkow *)

theory Abs_Int1_ivl

imports Abs_Int1

begin

subsection "Interval Analysis"

datatype ivl = I "int option" "int option"

definition "rep_ivl i = (case i of

  I (Some l) (Some h) \<Rightarrow> {l..h} |

  I (Some l) None \<Rightarrow> {l..} |

  I None (Some h) \<Rightarrow> {..h} |

  I None None \<Rightarrow> UNIV)"

definition "num_ivl n = I (Some n) (Some n)"

instantiation option :: (plus)plus

begin

fun plus_option where

"Some x + Some y = Some(x+y)" |

"_ + _ = None"

instance proof qed

end

definition empty where "empty = I (Some 1) (Some 0)"

fun is_empty where

"is_empty(I (Some l) (Some h)) = (h<l)" |

"is_empty _ = False"

lemma [simp]: "is_empty(I l h) =

  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"

by(auto split:option.split)

lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"

by(auto simp add: rep_ivl_def split: ivl.split option.split)

definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else

  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"

instantiation ivl :: SL_top

begin

definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where

"le_option pos x y =

 (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)

  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"

fun le_aux where

"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"

definition le_ivl where

"i1 \<sqsubseteq> i2 =

 (if is_empty i1 then True else

  if is_empty i2 then False else le_aux i1 i2)"

definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where

"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"

definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where

"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"

definition "i1 \<squnion> i2 =

 (if is_empty i1 then i2 else if is_empty i2 then i1

  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>

          I (min_option False l1 l2) (max_option True h1 h2))"

definition "\<top> = I None None"

instance

proof

  case goal1 thus ?case

    by(cases x, simp add: le_ivl_def le_option_def split: option.split)

next

  case goal2 thus ?case

    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)

next

  case goal3 thus ?case

    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)

next

  case goal4 thus ?case

    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)

next

  case goal5 thus ?case

    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)

next

  case goal6 thus ?case

    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)

qed

end

instantiation ivl :: L_top_bot

begin

definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else

  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>

    I (max_option False l1 l2) (min_option True h1 h2))"

definition "\<bottom> = empty"

instance

proof

  case goal1 thus ?case

    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)

next

  case goal2 thus ?case

    by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)

next

  case goal3 thus ?case

    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)

next

  case goal4 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)

qed

end

instantiation option :: (minus)minus

begin

fun minus_option where

"Some x - Some y = Some(x-y)" |

"_ - _ = None"

instance proof qed

end

definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else

  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"

lemma rep_minus_ivl:

  "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"

by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)

definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)

  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"

fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where

"filter_less_ivl res (I l1 h1) (I l2 h2) =

  (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else

   if res

   then (I l1 (min_option True h1 (h2 - Some 1)),

         I (max_option False (l1 + Some 1) l2) h2)

   else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"

interpretation Rep rep_ivl

proof

  case goal1 thus ?case

    by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)

next

  case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)

qed

interpretation Val_abs rep_ivl num_ivl plus_ivl

proof

  case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)

next

  case goal2 thus ?case

    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)

next

  case goal3 thus ?case

    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)

qed

interpretation Rep1 rep_ivl

proof

  case goal1 thus ?case

    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)

next

  case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def)

qed

lemma mono_minus_ivl:

  "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'"

apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits)

  apply(simp split: option.splits)

 apply(simp split: option.splits)

apply(simp split: option.splits)

done

interpretation

  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl

proof

  case goal1 thus ?case

    by(auto simp add: filter_plus_ivl_def)

      (metis rep_minus_ivl add_diff_cancel add_commute)+

next

  case goal2 thus ?case

    by(cases a1, cases a2,

      auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)

next

  case goal3 thus ?case

    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)

next

  case goal4 thus ?case

    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)

    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)

qed

interpretation

  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter 20)"

defines afilter_ivl is afilter

and bfilter_ivl is bfilter

and step_ivl is step

and AI_ivl is AI

and aval_ivl is aval'

proof qed (auto simp: iter_pfp strip_iter)

definition "test1_ivl =

 ''y'' ::= N 7;

 IF Less (V ''x'') (V ''y'')

 THEN ''y'' ::= Plus (V ''y'') (V ''x'')

 ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"

translations

"{i..j}" <= "CONST I (CONST Some i) (CONST Some j)"

"{..j}" <= "CONST I (CONST None) (CONST Some j)"

"{i..}" <= "CONST I (CONST Some i) (CONST None)"

"CONST UNIV" <= "CONST I (CONST None) (CONST None)"

value [code] "show_acom (AI_ivl test1_ivl)"

value [code] "show_acom (AI_const test3_const)"

value [code] "show_acom (AI_ivl test3_const)"

value [code] "show_acom (AI_const test4_const)"

value [code] "show_acom (AI_ivl test4_const)"

value [code] "show_acom (AI_ivl test6_const)"

definition "test2_ivl =

 WHILE Less (V ''x'') (N 100)

 DO ''x'' ::= Plus (V ''x'') (N 1)"

value [code] "show_acom (AI_ivl test2_ivl)"

definition "test3_ivl =

 ''x'' ::= N 7;

 WHILE Less (V ''x'') (N 100)

 DO ''x'' ::= Plus (V ''x'') (N 1)"

value [code] "show_acom (AI_ivl test3_ivl)"

value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"

value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"

value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"

value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"

value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"

definition "test4_ivl =

 ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');

 WHILE Less (V ''x'') (N 11)

 DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"

value [code] "show_acom(AI_ivl test4_ivl)"

definition "test5_ivl =

 ''x'' ::= N 0; ''y'' ::= N 0;

 WHILE Less (V ''x'') (N 1001)

 DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"

value [code] "show_acom(AI_ivl test5_ivl)"

text{* Nontermination not detected: *}

definition "test6_ivl =

 ''x'' ::= N 0;

 WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"

value [code] "show_acom(AI_ivl test6_ivl)"

end