Theory Abs_Int2_ivl

(* Author: Tobias Nipkow *)

section "Interval Analysis"

theory Abs_Int2_ivl
imports Abs_Int2 "HOL-IMP.Abs_Int_Tests"
begin

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

definition "γ_ivl i = (case i of
  I (Some l) (Some h) ⇒ {l..h} |
  I (Some l) None ⇒ {l..} |
  I None (Some h) ⇒ {..h} |
  I None None ⇒ UNIV)"

abbreviation I_Some_Some :: "int ⇒ int ⇒ ivl"  (‹{_…_}›) where
"{lo…hi} == I (Some lo) (Some hi)"
abbreviation I_Some_None :: "int ⇒ ivl"  (‹{_…}›) where
"{lo…} == I (Some lo) None"
abbreviation I_None_Some :: "int ⇒ ivl"  (‹{…_}›) where
"{…hi} == I None (Some hi)"
abbreviation I_None_None :: "ivl"  (‹{…}›) where
"{…} == I None None"

definition "num_ivl n = {n…n}"

fun in_ivl :: "int ⇒ ivl ⇒ bool" where
"in_ivl k (I (Some l) (Some h)) ⟷ l ≤ k ∧ k ≤ h" |
"in_ivl k (I (Some l) None) ⟷ l ≤ k" |
"in_ivl k (I None (Some h)) ⟷ k ≤ h" |
"in_ivl k (I None None) ⟷ True"

instantiation option :: (plus)plus
begin

fun plus_option where
"Some x + Some y = Some(x+y)" |
"_ + _ = None"

instance ..

end

definition empty where "empty = {1…0}"

fun is_empty where
"is_empty {l…h} = (h<l)" |
"is_empty _ = False"

lemma [simp]: "is_empty(I l h) =
  (case l of Some l ⇒ (case h of Some h ⇒ h<l | None ⇒ False) | None ⇒ False)"
by(auto split:option.split)

lemma [simp]: "is_empty i ⟹ γ_ivl i = {}"
by(auto simp add: γ_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) ⇒ I (l1+l2) (h1+h2))"

instantiation ivl :: SL_top
begin

definition le_option :: "bool ⇒ int option ⇒ int option ⇒ bool" where
"le_option pos x y =
 (case x of (Some i) ⇒ (case y of Some j ⇒ i≤j | None ⇒ pos)
  | None ⇒ (case y of Some j ⇒ ¬pos | None ⇒ 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 ⊑ i2 =
 (if is_empty i1 then True else
  if is_empty i2 then False else le_aux i1 i2)"

definition min_option :: "bool ⇒ int option ⇒ int option ⇒ int option" where
"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"

definition max_option :: "bool ⇒ int option ⇒ int option ⇒ int option" where
"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"

definition "i1 ⊔ 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) ⇒
          I (min_option False l1 l2) (max_option True h1 h2))"

definition "⊤ = {…}"

instance
proof (standard, goal_cases)
  case (1 x) thus ?case
    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
next
  case (2 x y z) thus ?case
    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
next
  case (3 x y) 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 (4 x y) 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 (5 x y z) 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 (6 x) 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 ⊓ i2 = (if is_empty i1 ∨ is_empty i2 then empty else
  case (i1,i2) of (I l1 h1, I l2 h2) ⇒
    I (max_option False l1 l2) (min_option True h1 h2))"

definition "⊥ = empty"

instance
proof (standard, goal_cases)
  case 1 thus ?case
    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)
next
  case 2 thus ?case
    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)
next
  case (3 x y z) 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 (4 x) 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 ..

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) ⇒ I (l1-h2) (h1-l2))"

lemma gamma_minus_ivl:
  "n1 : γ_ivl i1 ⟹ n2 : γ_ivl i2 ⟹ n1-n2 : γ_ivl(minus_ivl i1 i2)"
by(auto simp add: minus_ivl_def γ_ivl_def split: ivl.splits option.splits)

definition "filter_plus_ivl i i1 i2 = (⌦‹if is_empty i then empty else›
  i1 ⊓ minus_ivl i i2, i2 ⊓ minus_ivl i i1)"

fun filter_less_ivl :: "bool ⇒ ivl ⇒ ivl ⇒ ivl * ivl" where
"filter_less_ivl res (I l1 h1) (I l2 h2) =
  (if is_empty(I l1 h1) ∨ 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)))"

global_interpretation Val_abs
where γ = γ_ivl and num' = num_ivl and plus' = plus_ivl
proof (standard, goal_cases)
  case 1 thus ?case
    by(auto simp: γ_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
next
  case 2 show ?case by(simp add: γ_ivl_def Top_ivl_def)
next
  case 3 thus ?case by(simp add: γ_ivl_def num_ivl_def)
next
  case 4 thus ?case
    by(auto simp add: γ_ivl_def plus_ivl_def split: ivl.split option.splits)
qed

global_interpretation Val_abs1_gamma
where γ = γ_ivl and num' = num_ivl and plus' = plus_ivl
defines aval_ivl = aval'
proof (standard, goal_cases)
  case 1 thus ?case
    by(auto simp add: γ_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
next
  case 2 show ?case by(auto simp add: bot_ivl_def γ_ivl_def empty_def)
qed

lemma mono_minus_ivl:
  "i1 ⊑ i1' ⟹ i2 ⊑ i2' ⟹ minus_ivl i1 i2 ⊑ 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


global_interpretation Val_abs1
where γ = γ_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof (standard, goal_cases)
  case 1 thus ?case
    by (simp add: γ_ivl_def split: ivl.split option.split)
next
  case 2 thus ?case
    by(auto simp add: filter_plus_ivl_def)
      (metis gamma_minus_ivl add_diff_cancel add.commute)+
next
  case (3 _ _ a1 a2) thus ?case
    by(cases a1, cases a2,
      auto simp: γ_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed

global_interpretation Abs_Int1
where γ = γ_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
defines afilter_ivl = afilter
and bfilter_ivl = bfilter
and step_ivl = step'
and AI_ivl = AI
and aval_ivl' = aval''
..


text‹Monotonicity:›

global_interpretation Abs_Int1_mono
where γ = γ_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
proof (standard, goal_cases)
  case 1 thus ?case
    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
next
  case 2 thus ?case
    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
next
  case (3 a1 b1 a2 b2) 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


subsection "Tests"

value "show_acom_opt (AI_ivl test1_ivl)"

text‹Better than ‹AI_const›:›
value "show_acom_opt (AI_ivl test3_const)"
value "show_acom_opt (AI_ivl test4_const)"
value "show_acom_opt (AI_ivl test6_const)"

value "show_acom_opt (AI_ivl test2_ivl)"
value "show_acom (((step_ivl ⊤)^^0) (⊥⇩c test2_ivl))"
value "show_acom (((step_ivl ⊤)^^1) (⊥⇩c test2_ivl))"
value "show_acom (((step_ivl ⊤)^^2) (⊥⇩c test2_ivl))"

text‹Fixed point reached in 2 steps. Not so if the start value of x is known:›

value "show_acom_opt (AI_ivl test3_ivl)"
value "show_acom (((step_ivl ⊤)^^0) (⊥⇩c test3_ivl))"
value "show_acom (((step_ivl ⊤)^^1) (⊥⇩c test3_ivl))"
value "show_acom (((step_ivl ⊤)^^2) (⊥⇩c test3_ivl))"
value "show_acom (((step_ivl ⊤)^^3) (⊥⇩c test3_ivl))"
value "show_acom (((step_ivl ⊤)^^4) (⊥⇩c test3_ivl))"

text‹Takes as many iterations as the actual execution. Would diverge if
loop did not terminate. Worse still, as the following example shows: even if
the actual execution terminates, the analysis may not. The value of y keeps
decreasing as the analysis is iterated, no matter how long:›

value "show_acom (((step_ivl ⊤)^^50) (⊥⇩c test4_ivl))"

text‹Relationships between variables are NOT captured:›
value "show_acom_opt (AI_ivl test5_ivl)"

text‹Again, the analysis would not terminate:›
value "show_acom (((step_ivl ⊤)^^50) (⊥⇩c test6_ivl))"

end