47613

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(xy)" 


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 (l1h2) (h1l2))"


152 


153 
lemma gamma_minus_ivl:


154 
"n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1n2 : \<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
