src/HOL/IMP/Abs_Int2_ivl.thy
changeset 51359 00b45c7e831f
parent 51261 d301ba7da9b6
child 51389 8a9f0503b1c0
     1.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Mar 06 14:10:07 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Mar 06 16:10:56 2013 +0100
     1.3 @@ -1,297 +1,341 @@
     1.4  (* Author: Tobias Nipkow *)
     1.5  
     1.6  theory Abs_Int2_ivl
     1.7 -imports Abs_Int2
     1.8 +imports "~~/src/HOL/Library/Quotient_List"
     1.9 +        "~~/src/HOL/Library/Extended"
    1.10 +        Abs_Int2
    1.11  begin
    1.12  
    1.13  subsection "Interval Analysis"
    1.14  
    1.15 -datatype lb = Minf | Lb int
    1.16 -datatype ub = Pinf | Ub int
    1.17 +type_synonym eint = "int extended"
    1.18 +type_synonym eint2 = "eint * eint"
    1.19  
    1.20 -datatype ivl = Ivl lb ub
    1.21 +definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where
    1.22 +"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})"
    1.23  
    1.24 -definition "\<gamma>_ivl i = (case i of
    1.25 -  Ivl (Lb l) (Ub h) \<Rightarrow> {l..h} |
    1.26 -  Ivl (Lb l) Pinf \<Rightarrow> {l..} |
    1.27 -  Ivl Minf (Ub h) \<Rightarrow> {..h} |
    1.28 -  Ivl Minf Pinf \<Rightarrow> UNIV)"
    1.29 +definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
    1.30 +"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)"
    1.31  
    1.32 -abbreviation Ivl_Lb_Ub :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
    1.33 -"{lo\<dots>hi} == Ivl (Lb lo) (Ub hi)"
    1.34 -abbreviation Ivl_Lb_Pinf :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
    1.35 -"{lo\<dots>} == Ivl (Lb lo) Pinf"
    1.36 -abbreviation Ivl_Minf_Ub :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
    1.37 -"{\<dots>hi} == Ivl Minf (Ub hi)"
    1.38 -abbreviation Ivl_Minf_Pinf :: "ivl"  ("{\<dots>}") where
    1.39 -"{\<dots>} == Ivl Minf Pinf"
    1.40 +lemma refl_eq_ivl[simp]: "eq_ivl p p"
    1.41 +by(auto simp: eq_ivl_def)
    1.42  
    1.43 -lemmas lub_splits = lb.splits ub.splits
    1.44 -
    1.45 -definition "num_ivl n = {n\<dots>n}"
    1.46 +quotient_type ivl = eint2 / eq_ivl
    1.47 +by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
    1.48  
    1.49 -fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
    1.50 -"in_ivl k (Ivl (Lb l) (Ub h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
    1.51 -"in_ivl k (Ivl (Lb l) Pinf) \<longleftrightarrow> l \<le> k" |
    1.52 -"in_ivl k (Ivl Minf (Ub h)) \<longleftrightarrow> k \<le> h" |
    1.53 -"in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True"
    1.54 +lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
    1.55 +by(simp add: eq_ivl_def)
    1.56  
    1.57 -
    1.58 -instantiation lb :: linorder
    1.59 -begin
    1.60 +abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where
    1.61 +"[l\<dots>h] == abs_ivl(l,h)"
    1.62  
    1.63 -definition less_eq_lb where
    1.64 -"l1 \<le> l2 = (case l1 of Minf \<Rightarrow> True | Lb i1 \<Rightarrow> (case l2 of Minf \<Rightarrow> False | Lb i2 \<Rightarrow> i1 \<le> i2))"
    1.65 +lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
    1.66 +by(auto simp: eq_ivl_def)
    1.67  
    1.68 -definition less_lb :: "lb \<Rightarrow> lb \<Rightarrow> bool" where
    1.69 -"((l1::lb) < l2) = (l1 \<le> l2 & ~ l1 \<ge> l2)"
    1.70 +fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where
    1.71 +"in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h"
    1.72  
    1.73 -instance
    1.74 -proof
    1.75 -  case goal1 show ?case by(rule less_lb_def)
    1.76 -next
    1.77 -  case goal2 show ?case by(auto simp: less_eq_lb_def split:lub_splits)
    1.78 -next
    1.79 -  case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
    1.80 -next
    1.81 -  case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
    1.82 -next
    1.83 -  case goal5 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
    1.84 -qed
    1.85 +lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep
    1.86 +by(auto simp: eq_ivl_def \<gamma>_rep_def)
    1.87 +
    1.88 +definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
    1.89 +"is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"
    1.90  
    1.91 -end
    1.92 -
    1.93 -instantiation ub :: linorder
    1.94 -begin
    1.95 +lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} |
    1.96 +  (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})"
    1.97 +by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits)
    1.98  
    1.99 -definition less_eq_ub where
   1.100 -"u1 \<le> u2 = (case u2 of Pinf \<Rightarrow> True | Ub i2 \<Rightarrow> (case u1 of Pinf \<Rightarrow> False | Ub i1 \<Rightarrow> i1 \<le> i2))"
   1.101 -
   1.102 -definition less_ub :: "ub \<Rightarrow> ub \<Rightarrow> bool" where
   1.103 -"((u1::ub) < u2) = (u1 \<le> u2 & ~ u1 \<ge> u2)"
   1.104 +lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
   1.105 +apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
   1.106 +apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
   1.107 +done
   1.108  
   1.109 -instance
   1.110 -proof
   1.111 -  case goal1 show ?case by(rule less_ub_def)
   1.112 -next
   1.113 -  case goal2 show ?case by(auto simp: less_eq_ub_def split:lub_splits)
   1.114 -next
   1.115 -  case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
   1.116 -next
   1.117 -  case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
   1.118 -next
   1.119 -  case goal5 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
   1.120 -qed
   1.121 +lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
   1.122 +by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits)
   1.123  
   1.124 -end
   1.125 +definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
   1.126  
   1.127 -lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def
   1.128 +lift_definition empty_ivl :: ivl is empty_rep
   1.129 +by simp
   1.130  
   1.131 -lemma le_lub_simps[simp]:
   1.132 -  "Minf \<le> l" "Lb i \<le> Lb j = (i \<le> j)" "~ Lb i \<le> Minf"
   1.133 -  "h \<le> Pinf" "Ub i \<le> Ub j = (i \<le> j)" "~ Pinf \<le> Ub j"
   1.134 -by(auto simp: le_lub_defs split: lub_splits)
   1.135 -
   1.136 -definition empty where "empty = {1\<dots>0}"
   1.137 +lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
   1.138 +by(auto simp add: is_empty_rep_def empty_rep_def)
   1.139  
   1.140 -fun is_empty where
   1.141 -"is_empty {l\<dots>h} = (h<l)" |
   1.142 -"is_empty _ = False"
   1.143 +lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})"
   1.144 +by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits)
   1.145  
   1.146 -lemma [simp]: "is_empty(Ivl l h) =
   1.147 -  (case l of Lb l \<Rightarrow> (case h of Ub h \<Rightarrow> h<l | Pinf \<Rightarrow> False) | Minf \<Rightarrow> False)"
   1.148 -by(auto split: lub_splits)
   1.149 -
   1.150 -lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
   1.151 -by(auto simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
   1.152 +declare is_empty_rep_iff[THEN iffD1, simp]
   1.153  
   1.154  
   1.155  instantiation ivl :: semilattice
   1.156  begin
   1.157  
   1.158 -fun le_aux where
   1.159 -"le_aux (Ivl l1 h1) (Ivl l2 h2) = (l2 \<le> l1 & h1 \<le> h2)"
   1.160 +definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
   1.161 +"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in
   1.162 +  if is_empty_rep(l1,h1) then True else
   1.163 +  if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)"
   1.164 +
   1.165 +lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2"
   1.166 +apply rule
   1.167 +apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1]
   1.168 +apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def)
   1.169 +apply(auto simp: not_less split: extended.splits)
   1.170 +done
   1.171 +
   1.172 +lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep
   1.173 +by(auto simp: eq_ivl_def le_iff_subset)
   1.174  
   1.175 -definition le_ivl where
   1.176 -"i1 \<sqsubseteq> i2 =
   1.177 - (if is_empty i1 then True else
   1.178 -  if is_empty i2 then False else le_aux i1 i2)"
   1.179 +definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
   1.180 +
   1.181 +definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   1.182 +"join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
   1.183 +  else let (l1,h1) = p1; (l2,h2) = p2 in  (min l1 l2, max h1 h2))"
   1.184  
   1.185 -definition "i1 \<squnion> i2 =
   1.186 - (if is_empty i1 then i2 else if is_empty i2 then i1
   1.187 -  else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (min l1 l2) (max h1 h2))"
   1.188 +lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep
   1.189 +by(auto simp: eq_ivl_iff join_rep_def)
   1.190  
   1.191 -definition "\<top> = {\<dots>}"
   1.192 +lift_definition top_ivl :: ivl is "(Minf,Pinf)"
   1.193 +by(auto simp: eq_ivl_def)
   1.194 +
   1.195 +lemma is_empty_min_max:
   1.196 +  "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
   1.197 +by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
   1.198  
   1.199  instance
   1.200  proof
   1.201 -  case goal1 thus ?case
   1.202 -    by(cases x, simp add: le_ivl_def)
   1.203 +  case goal1 show ?case by (rule less_ivl_def)
   1.204 +next
   1.205 +  case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
   1.206  next
   1.207 -  case goal2 thus ?case
   1.208 -    by(cases x, cases y, cases z, auto simp: le_ivl_def split: if_splits)
   1.209 +  case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
   1.210  next
   1.211 -  case goal3 thus ?case
   1.212 -    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
   1.213 +  case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
   1.214  next
   1.215 -  case goal4 thus ?case
   1.216 -    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
   1.217 +  case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
   1.218 +next
   1.219 +  case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
   1.220  next
   1.221 -  case goal5 thus ?case
   1.222 -    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits if_splits)
   1.223 +  case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def)
   1.224  next
   1.225 -  case goal6 thus ?case
   1.226 -    by(cases x, simp add: Top_ivl_def le_ivl_def le_lub_defs split: lub_splits)
   1.227 +  case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
   1.228  qed
   1.229  
   1.230  end
   1.231  
   1.232 +text{* Implement (naive) executable equality: *}
   1.233 +instantiation ivl :: equal
   1.234 +begin
   1.235 +
   1.236 +definition equal_ivl where
   1.237 +"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
   1.238 +
   1.239 +instance
   1.240 +proof
   1.241 +  case goal1 show ?case by(simp add: equal_ivl_def eq_iff)
   1.242 +qed
   1.243 +
   1.244 +end
   1.245 +
   1.246 +lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)"
   1.247 +by(simp add: not_less)
   1.248 +lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
   1.249 +by(simp add: not_less)
   1.250  
   1.251  instantiation ivl :: lattice
   1.252  begin
   1.253  
   1.254 -definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
   1.255 -  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (max l1 l2) (min h1 h2))"
   1.256 +definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   1.257 +"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
   1.258  
   1.259 -definition "\<bottom> = empty"
   1.260 +lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
   1.261 +by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
   1.262 +
   1.263 +lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep
   1.264 +by(auto simp: \<gamma>_meet_rep eq_ivl_def)
   1.265 +
   1.266 +definition "\<bottom> = empty_ivl"
   1.267  
   1.268  instance
   1.269  proof
   1.270    case goal2 thus ?case
   1.271 -    by (simp add:meet_ivl_def empty_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
   1.272 +    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
   1.273  next
   1.274    case goal3 thus ?case
   1.275 -    by (simp add: empty_def meet_ivl_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
   1.276 +    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
   1.277  next
   1.278    case goal4 thus ?case
   1.279 -    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_lub_defs max_def min_def split: lub_splits if_splits)
   1.280 +    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
   1.281  next
   1.282 -  case goal1 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
   1.283 +  case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
   1.284  qed
   1.285  
   1.286  end
   1.287  
   1.288  
   1.289 -instantiation lb :: plus
   1.290 +lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p"
   1.291 +by (metis eq_ivl_iff is_empty_empty_rep)
   1.292 +
   1.293 +lemma le_ivl_nice: "[l1\<dots>h1] \<le> [l2\<dots>h2] \<longleftrightarrow>
   1.294 +  (if [l1\<dots>h1] = \<bottom> then True else
   1.295 +   if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
   1.296 +unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
   1.297 +
   1.298 +lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] =
   1.299 +  (if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else
   1.300 +   if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
   1.301 +unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty)
   1.302 +
   1.303 +lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
   1.304 +by transfer (simp add: meet_rep_def)
   1.305 +
   1.306 +
   1.307 +instantiation ivl :: plus
   1.308  begin
   1.309  
   1.310 -fun plus_lb where
   1.311 -"Lb x + Lb y = Lb(x+y)" |
   1.312 -"_ + _ = Minf"
   1.313 +definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   1.314 +"plus_rep p1 p2 =
   1.315 +  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
   1.316 +   let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))"
   1.317 +
   1.318 +lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep
   1.319 +by(auto simp: plus_rep_def eq_ivl_iff)
   1.320  
   1.321  instance ..
   1.322  end
   1.323  
   1.324 -instantiation ub :: plus
   1.325 -begin
   1.326 -
   1.327 -fun plus_ub where
   1.328 -"Ub x + Ub y = Ub(x+y)" |
   1.329 -"_ + _ = Pinf"
   1.330 -
   1.331 -instance ..
   1.332 -end
   1.333 -
   1.334 -instantiation ivl :: plus
   1.335 -begin
   1.336 +lemma plus_ivl_nice: "[l1\<dots>h1] + [l2\<dots>h2] =
   1.337 +  (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then \<bottom> else [l1+l2 \<dots> h1+h2])"
   1.338 +unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty)
   1.339  
   1.340 -definition "i1+i2 = (if is_empty i1 | is_empty i2 then empty else
   1.341 -  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
   1.342 -
   1.343 -instance ..
   1.344 -end
   1.345 +lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf"
   1.346 +by(cases x) auto
   1.347 +lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf"
   1.348 +by(cases x) auto
   1.349  
   1.350 -fun uminus_ub :: "ub \<Rightarrow> lb" where
   1.351 -"uminus_ub(Ub( x)) = Lb(-x)" |
   1.352 -"uminus_ub Pinf = Minf"
   1.353 -
   1.354 -fun uminus_lb :: "lb \<Rightarrow> ub" where
   1.355 -"uminus_lb(Lb( x)) = Ub(-x)" |
   1.356 -"uminus_lb Minf = Pinf"
   1.357 +lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)"
   1.358 +by(cases x) auto
   1.359 +lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)"
   1.360 +by(cases x) auto
   1.361  
   1.362  instantiation ivl :: uminus
   1.363  begin
   1.364  
   1.365 -fun uminus_ivl where
   1.366 -"-(Ivl l h) = Ivl (uminus_ub h) (uminus_lb l)"
   1.367 -
   1.368 -instance ..
   1.369 -end
   1.370 +definition uminus_rep :: "eint2 \<Rightarrow> eint2" where
   1.371 +"uminus_rep p = (let (l,h) = p in (-h, -l))"
   1.372  
   1.373 -instantiation ivl :: minus
   1.374 -begin
   1.375 +lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)"
   1.376 +by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff
   1.377 +        split: prod.split)
   1.378  
   1.379 -definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
   1.380 -"(i1::ivl) - i2 = i1 + -i2"
   1.381 +lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep
   1.382 +by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases)
   1.383 +   (auto simp: Icc_eq_Icc split: extended.splits)
   1.384  
   1.385  instance ..
   1.386  end
   1.387  
   1.388 -lemma minus_ivl_cases: "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
   1.389 -  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
   1.390 -by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits)
   1.391 +lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]"
   1.392 +by transfer (simp add: uminus_rep_def)
   1.393 +
   1.394 +instantiation ivl :: minus
   1.395 +begin
   1.396 +definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl) - iv2 = iv1 + -iv2"
   1.397 +instance ..
   1.398 +end
   1.399 +
   1.400  
   1.401 -lemma gamma_minus_ivl:
   1.402 -  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)"
   1.403 -by(auto simp add: minus_ivl_def plus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
   1.404 +definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where
   1.405 +"filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))"
   1.406 +
   1.407 +definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where
   1.408 +"filter_less_rep res p1 p2 =
   1.409 +  (if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else
   1.410 +   let (l1,h1) = p1; (l2,h2) = p2 in
   1.411 +   if res
   1.412 +   then ((l1, min h1 (h2 + Fin -1)), (max (l1 + Fin 1) l2, h2))
   1.413 +   else ((max l1 l2, h1), (l2, min h1 h2)))"
   1.414  
   1.415 -definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
   1.416 -  i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))"
   1.417 +lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep
   1.418 +by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff)
   1.419 +declare filter_less_ivl.abs_eq[code] (* bug in lifting *)
   1.420 +
   1.421 +lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] =
   1.422 +  (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else
   1.423 +   if b
   1.424 +   then ([l1 \<dots> min h1 (h2 + Fin -1)], [max (l1 + Fin 1) l2 \<dots> h2])
   1.425 +   else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))"
   1.426 +unfolding prod_rel_eq[symmetric] bot_ivl_def
   1.427 +by transfer (auto simp: filter_less_rep_def eq_ivl_empty)
   1.428  
   1.429 -fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
   1.430 -"filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) =
   1.431 -  (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else
   1.432 -   if res
   1.433 -   then (Ivl l1 (min h1 (h2 + Ub -1)), Ivl (max (l1 + Lb 1) l2) h2)
   1.434 -   else (Ivl (max l1 l2) h1, Ivl l2 (min h1 h2)))"
   1.435 +lemma add_mono_le_Fin:
   1.436 +  "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))"
   1.437 +by(drule (1) add_mono) simp
   1.438 +
   1.439 +lemma add_mono_Fin_le:
   1.440 +  "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
   1.441 +by(drule (1) add_mono) simp
   1.442 +
   1.443 +lemma plus_rep_plus:
   1.444 +  "\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)"
   1.445 +by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin)
   1.446  
   1.447  interpretation Val_abs
   1.448  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   1.449  proof
   1.450 -  case goal1 thus ?case
   1.451 -    by(auto simp: \<gamma>_ivl_def le_ivl_def le_lub_defs split: ivl.split lub_splits if_splits)
   1.452 +  case goal1 thus ?case by transfer (simp add: le_iff_subset)
   1.453  next
   1.454 -  case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
   1.455 +  case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)
   1.456  next
   1.457 -  case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
   1.458 +  case goal3 show ?case by transfer (simp add: \<gamma>_rep_def)
   1.459  next
   1.460    case goal4 thus ?case
   1.461 -    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split lub_splits)
   1.462 +    apply transfer
   1.463 +    apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
   1.464 +    by(auto simp: empty_rep_def is_empty_rep_def)
   1.465  qed
   1.466  
   1.467 +
   1.468  interpretation Val_abs1_gamma
   1.469  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   1.470  defines aval_ivl is aval'
   1.471  proof
   1.472 -  case goal1 thus ?case
   1.473 -    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_def max_def split: ivl.split lub_splits)
   1.474 +  case goal1 show ?case
   1.475 +    by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split)
   1.476  next
   1.477 -  case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
   1.478 +  case goal2 show ?case unfolding bot_ivl_def by transfer simp
   1.479  qed
   1.480  
   1.481 -lemma mono_minus_ivl: fixes i1 :: ivl
   1.482 -shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'"
   1.483 -apply(auto simp add: minus_ivl_cases empty_def le_ivl_def le_lub_defs split: ivl.splits)
   1.484 -  apply(simp split: lub_splits)
   1.485 - apply(simp split: lub_splits)
   1.486 -apply(simp split: lub_splits)
   1.487 -done
   1.488 +lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)"
   1.489 +by(auto simp: plus_rep_def plus_rep_plus split: prod.splits)
   1.490  
   1.491 +lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow>
   1.492 +     \<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))"
   1.493 +by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv)
   1.494 +   (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus)
   1.495 +
   1.496 +lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and>
   1.497 +       eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2;
   1.498 +        n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk>
   1.499 +       \<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2"
   1.500 +by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac)
   1.501 +   (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+
   1.502  
   1.503  interpretation Val_abs1
   1.504  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   1.505  and test_num' = in_ivl
   1.506  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   1.507  proof
   1.508 -  case goal1 thus ?case
   1.509 -    by (simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
   1.510 +  case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
   1.511  next
   1.512 -  case goal2 thus ?case
   1.513 -    by(auto simp add: filter_plus_ivl_def)
   1.514 -      (metis gamma_minus_ivl add_diff_cancel add_commute)+
   1.515 +  case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric]
   1.516 +    by transfer (simp add: filter_plus)
   1.517  next
   1.518    case goal3 thus ?case
   1.519 -    by(cases a1, cases a2, auto simp: \<gamma>_ivl_def min_def max_def split: if_splits lub_splits)
   1.520 +    unfolding prod_rel_eq[symmetric]
   1.521 +    apply transfer
   1.522 +    apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits)
   1.523 +    apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits)
   1.524 +    done
   1.525  qed
   1.526  
   1.527  interpretation Abs_Int1
   1.528 @@ -308,25 +352,41 @@
   1.529  
   1.530  text{* Monotonicity: *}
   1.531  
   1.532 +lemma mono_meet_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (meet_rep p1 q1) (meet_rep p2 q2)"
   1.533 +by(auto simp add: le_iff_subset \<gamma>_meet_rep)
   1.534 +
   1.535 +lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)"
   1.536 +apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
   1.537 +by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   1.538 +
   1.539 +lemma mono_minus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep (uminus_rep p1) (uminus_rep p2)"
   1.540 +apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split)
   1.541 +by(auto simp: \<gamma>_rep_cases split: extended.splits)
   1.542 +
   1.543  interpretation Abs_Int1_mono
   1.544  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   1.545  and test_num' = in_ivl
   1.546  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   1.547  proof
   1.548 -  case goal1 thus ?case
   1.549 -    by(auto simp: plus_ivl_def le_ivl_def le_lub_defs empty_def split: if_splits ivl.splits lub_splits)
   1.550 +  case goal1 thus ?case by transfer (rule mono_plus_rep)
   1.551 +next
   1.552 +  case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def
   1.553 +    by transfer (auto simp: mono_meet_rep mono_plus_rep mono_minus_rep)
   1.554  next
   1.555 -  case goal2 thus ?case
   1.556 -    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
   1.557 -next
   1.558 -  case goal3 thus ?case
   1.559 -    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
   1.560 -    by(auto simp add: empty_def le_ivl_def le_lub_defs min_def max_def split: lub_splits)
   1.561 +  case goal3 thus ?case unfolding less_eq_prod_def
   1.562 +    apply transfer
   1.563 +    apply(auto simp:filter_less_rep_def le_iff_subset min_def max_def split: if_splits)
   1.564 +    by(auto simp:is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   1.565  qed
   1.566  
   1.567  
   1.568  subsubsection "Tests"
   1.569  
   1.570 +(* Hide Fin in numerals on output *)
   1.571 +declare
   1.572 +Fin_numeral [code_post] Fin_neg_numeral [code_post]
   1.573 +zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
   1.574 +
   1.575  value "show_acom_opt (AI_ivl test1_ivl)"
   1.576  
   1.577  text{* Better than @{text AI_const}: *}
   1.578 @@ -334,7 +394,7 @@
   1.579  value "show_acom_opt (AI_ivl test4_const)"
   1.580  value "show_acom_opt (AI_ivl test6_const)"
   1.581  
   1.582 -definition "steps c i = (step_ivl(top(vars c)) ^^ i) (bot c)"
   1.583 +definition "steps c i = (step_ivl(Top(vars c)) ^^ i) (bot c)"
   1.584  
   1.585  value "show_acom_opt (AI_ivl test2_ivl)"
   1.586  value "show_acom (steps test2_ivl 0)"