src/HOL/IMP/Abs_Int2_ivl.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61890 f6ded81f5690
child 67399 eab6ce8368fa
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@47613
     1
(* Author: Tobias Nipkow *)
nipkow@47613
     2
nipkow@47613
     3
theory Abs_Int2_ivl
nipkow@51390
     4
imports Abs_Int2
nipkow@47613
     5
begin
nipkow@47613
     6
nipkow@47613
     7
subsection "Interval Analysis"
nipkow@47613
     8
nipkow@51359
     9
type_synonym eint = "int extended"
nipkow@51359
    10
type_synonym eint2 = "eint * eint"
nipkow@51245
    11
nipkow@51359
    12
definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where
nipkow@51359
    13
"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})"
nipkow@47613
    14
nipkow@51359
    15
definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
nipkow@51359
    16
"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)"
nipkow@47613
    17
nipkow@51359
    18
lemma refl_eq_ivl[simp]: "eq_ivl p p"
nipkow@51359
    19
by(auto simp: eq_ivl_def)
nipkow@51245
    20
nipkow@51359
    21
quotient_type ivl = eint2 / eq_ivl
nipkow@51359
    22
by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
nipkow@47613
    23
nipkow@51924
    24
abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_, _]") where
nipkow@51924
    25
"[l,h] == abs_ivl(l,h)"
nipkow@51871
    26
nipkow@51359
    27
lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
nipkow@51359
    28
by(simp add: eq_ivl_def)
nipkow@47613
    29
nipkow@51924
    30
lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l,h] = {i. l \<le> Fin i \<and> Fin i \<le> h}"
nipkow@51871
    31
by transfer (simp add: \<gamma>_rep_def)
nipkow@47613
    32
kuncar@55565
    33
lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)" .
nipkow@51245
    34
nipkow@51887
    35
lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool"
nipkow@51887
    36
  is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h"
nipkow@51887
    37
by(auto simp: eq_ivl_def \<gamma>_rep_def)
nipkow@47613
    38
nipkow@51924
    39
lemma in_ivl_nice: "in_ivl i [l,h] = (l \<le> Fin i \<and> Fin i \<le> h)"
nipkow@51887
    40
by transfer simp
nipkow@51359
    41
nipkow@51359
    42
definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
nipkow@51359
    43
"is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"
nipkow@47613
    44
nipkow@51359
    45
lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} |
nipkow@51359
    46
  (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})"
nipkow@51359
    47
by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits)
nipkow@51245
    48
nipkow@51359
    49
lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
nipkow@51359
    50
apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
noschinl@53427
    51
apply(auto simp: not_less less_eq_extended_case split: extended.splits)
nipkow@51359
    52
done
nipkow@51245
    53
nipkow@51359
    54
lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
nipkow@51359
    55
by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits)
nipkow@51245
    56
nipkow@51359
    57
definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
nipkow@51245
    58
kuncar@51994
    59
lift_definition empty_ivl :: ivl is empty_rep .
nipkow@51245
    60
nipkow@51359
    61
lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
nipkow@51359
    62
by(auto simp add: is_empty_rep_def empty_rep_def)
nipkow@47613
    63
nipkow@51359
    64
lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})"
nipkow@51359
    65
by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits)
nipkow@47613
    66
nipkow@51359
    67
declare is_empty_rep_iff[THEN iffD1, simp]
nipkow@47613
    68
nipkow@47613
    69
nipkow@51826
    70
instantiation ivl :: semilattice_sup_top
nipkow@47613
    71
begin
nipkow@47613
    72
nipkow@51359
    73
definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
nipkow@51359
    74
"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in
nipkow@51359
    75
  if is_empty_rep(l1,h1) then True else
nipkow@51359
    76
  if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)"
nipkow@51359
    77
nipkow@51359
    78
lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2"
nipkow@51359
    79
apply rule
nipkow@51359
    80
apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1]
nipkow@51359
    81
apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def)
nipkow@51359
    82
apply(auto simp: not_less split: extended.splits)
nipkow@51359
    83
done
nipkow@51359
    84
nipkow@51359
    85
lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep
nipkow@51359
    86
by(auto simp: eq_ivl_def le_iff_subset)
nipkow@47613
    87
nipkow@51359
    88
definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
nipkow@51359
    89
nipkow@51874
    90
lemma le_ivl_iff_subset: "iv1 \<le> iv2 \<longleftrightarrow> \<gamma>_ivl iv1 \<subseteq> \<gamma>_ivl iv2"
nipkow@51874
    91
by transfer (rule le_iff_subset)
nipkow@51874
    92
nipkow@51389
    93
definition sup_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
nipkow@51389
    94
"sup_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
nipkow@51359
    95
  else let (l1,h1) = p1; (l2,h2) = p2 in  (min l1 l2, max h1 h2))"
nipkow@47613
    96
nipkow@51389
    97
lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep
nipkow@51389
    98
by(auto simp: eq_ivl_iff sup_rep_def)
nipkow@47613
    99
kuncar@51994
   100
lift_definition top_ivl :: ivl is "(Minf,Pinf)" .
nipkow@51359
   101
nipkow@51359
   102
lemma is_empty_min_max:
nipkow@51359
   103
  "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
nipkow@51359
   104
by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
nipkow@47613
   105
nipkow@47613
   106
instance
nipkow@61179
   107
proof (standard, goal_cases)
nipkow@61179
   108
  case 1 show ?case by (rule less_ivl_def)
nipkow@51359
   109
next
nipkow@61179
   110
  case 2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
nipkow@47613
   111
next
nipkow@61179
   112
  case 3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
nipkow@47613
   113
next
nipkow@61179
   114
  case 4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
nipkow@47613
   115
next
nipkow@61179
   116
  case 5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
nipkow@51359
   117
next
nipkow@61179
   118
  case 6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
nipkow@47613
   119
next
nipkow@61179
   120
  case 7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
nipkow@47613
   121
next
nipkow@61179
   122
  case 8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
nipkow@47613
   123
qed
nipkow@47613
   124
nipkow@47613
   125
end
nipkow@47613
   126
nipkow@51359
   127
text{* Implement (naive) executable equality: *}
nipkow@51359
   128
instantiation ivl :: equal
nipkow@51359
   129
begin
nipkow@51359
   130
nipkow@51359
   131
definition equal_ivl where
nipkow@51359
   132
"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
nipkow@51359
   133
nipkow@51359
   134
instance
nipkow@61179
   135
proof (standard, goal_cases)
nipkow@61179
   136
  case 1 show ?case by(simp add: equal_ivl_def eq_iff)
nipkow@51359
   137
qed
nipkow@51359
   138
nipkow@51359
   139
end
nipkow@51359
   140
nipkow@51359
   141
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)"
nipkow@51359
   142
by(simp add: not_less)
nipkow@51359
   143
lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
nipkow@51359
   144
by(simp add: not_less)
nipkow@47613
   145
nipkow@51711
   146
instantiation ivl :: bounded_lattice
nipkow@47613
   147
begin
nipkow@47613
   148
nipkow@51389
   149
definition inf_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
nipkow@51389
   150
"inf_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
nipkow@47613
   151
nipkow@51389
   152
lemma \<gamma>_inf_rep: "\<gamma>_rep(inf_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
nipkow@51389
   153
by(auto simp:inf_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
nipkow@51359
   154
nipkow@51389
   155
lift_definition inf_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is inf_rep
nipkow@51389
   156
by(auto simp: \<gamma>_inf_rep eq_ivl_def)
nipkow@51359
   157
nipkow@51874
   158
lemma \<gamma>_inf: "\<gamma>_ivl (iv1 \<sqinter> iv2) = \<gamma>_ivl iv1 \<inter> \<gamma>_ivl iv2"
nipkow@51874
   159
by transfer (rule \<gamma>_inf_rep)
nipkow@51874
   160
nipkow@51359
   161
definition "\<bottom> = empty_ivl"
nipkow@47613
   162
nipkow@47613
   163
instance
nipkow@61179
   164
proof (standard, goal_cases)
nipkow@61179
   165
  case 1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
nipkow@51874
   166
next
nipkow@61179
   167
  case 2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
nipkow@51389
   168
next
nipkow@61179
   169
  case 3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
nipkow@47613
   170
next
nipkow@61179
   171
  case 4 show ?case
nipkow@51874
   172
    unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
nipkow@47613
   173
qed
nipkow@47613
   174
nipkow@47613
   175
end
nipkow@47613
   176
nipkow@51245
   177
nipkow@51359
   178
lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p"
nipkow@51359
   179
by (metis eq_ivl_iff is_empty_empty_rep)
nipkow@51359
   180
nipkow@51924
   181
lemma le_ivl_nice: "[l1,h1] \<le> [l2,h2] \<longleftrightarrow>
nipkow@51924
   182
  (if [l1,h1] = \<bottom> then True else
nipkow@51924
   183
   if [l2,h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
nipkow@51359
   184
unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
nipkow@51359
   185
nipkow@51924
   186
lemma sup_ivl_nice: "[l1,h1] \<squnion> [l2,h2] =
nipkow@51924
   187
  (if [l1,h1] = \<bottom> then [l2,h2] else
nipkow@51924
   188
   if [l2,h2] = \<bottom> then [l1,h1] else [min l1 l2,max h1 h2])"
nipkow@51389
   189
unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty)
nipkow@51359
   190
nipkow@51924
   191
lemma inf_ivl_nice: "[l1,h1] \<sqinter> [l2,h2] = [max l1 l2,min h1 h2]"
nipkow@51389
   192
by transfer (simp add: inf_rep_def)
nipkow@51359
   193
nipkow@51924
   194
lemma top_ivl_nice: "\<top> = [-\<infinity>,\<infinity>]"
nipkow@51870
   195
by (simp add: top_ivl_def)
nipkow@51870
   196
nipkow@51359
   197
nipkow@51359
   198
instantiation ivl :: plus
nipkow@47613
   199
begin
nipkow@47613
   200
nipkow@51359
   201
definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
nipkow@51359
   202
"plus_rep p1 p2 =
nipkow@51359
   203
  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
nipkow@51359
   204
   let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))"
nipkow@51359
   205
nipkow@51359
   206
lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep
nipkow@51359
   207
by(auto simp: plus_rep_def eq_ivl_iff)
nipkow@51245
   208
nipkow@51245
   209
instance ..
nipkow@51245
   210
end
nipkow@51245
   211
nipkow@51924
   212
lemma plus_ivl_nice: "[l1,h1] + [l2,h2] =
nipkow@51924
   213
  (if [l1,h1] = \<bottom> \<or> [l2,h2] = \<bottom> then \<bottom> else [l1+l2 , h1+h2])"
nipkow@51359
   214
unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty)
nipkow@51245
   215
nipkow@51359
   216
lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf"
nipkow@51359
   217
by(cases x) auto
nipkow@51359
   218
lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf"
nipkow@51359
   219
by(cases x) auto
nipkow@47613
   220
nipkow@51359
   221
lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)"
nipkow@51359
   222
by(cases x) auto
nipkow@51359
   223
lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)"
nipkow@51359
   224
by(cases x) auto
nipkow@51245
   225
nipkow@51245
   226
instantiation ivl :: uminus
nipkow@51245
   227
begin
nipkow@51245
   228
nipkow@51359
   229
definition uminus_rep :: "eint2 \<Rightarrow> eint2" where
nipkow@51359
   230
"uminus_rep p = (let (l,h) = p in (-h, -l))"
nipkow@51245
   231
nipkow@51359
   232
lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)"
nipkow@51359
   233
by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff
nipkow@51359
   234
        split: prod.split)
nipkow@51261
   235
nipkow@51359
   236
lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep
nipkow@51359
   237
by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases)
nipkow@51359
   238
   (auto simp: Icc_eq_Icc split: extended.splits)
nipkow@51261
   239
nipkow@51261
   240
instance ..
nipkow@51261
   241
end
nipkow@51261
   242
nipkow@51874
   243
lemma \<gamma>_uminus: "i : \<gamma>_ivl iv \<Longrightarrow> -i \<in> \<gamma>_ivl(- iv)"
nipkow@51874
   244
by transfer (rule \<gamma>_uminus_rep)
nipkow@51874
   245
nipkow@51924
   246
lemma uminus_nice: "-[l,h] = [-h,-l]"
nipkow@51359
   247
by transfer (simp add: uminus_rep_def)
nipkow@51359
   248
nipkow@51359
   249
instantiation ivl :: minus
nipkow@51359
   250
begin
nipkow@51882
   251
nipkow@51882
   252
definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
nipkow@51882
   253
"(iv1::ivl) - iv2 = iv1 + -iv2"
nipkow@51882
   254
nipkow@51359
   255
instance ..
nipkow@51359
   256
end
nipkow@51359
   257
nipkow@47613
   258
nipkow@51974
   259
definition inv_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where
nipkow@51974
   260
"inv_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))"
nipkow@51359
   261
nipkow@51882
   262
definition above_rep :: "eint2 \<Rightarrow> eint2" where
nipkow@51882
   263
"above_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (l,\<infinity>))"
nipkow@51882
   264
nipkow@51882
   265
definition below_rep :: "eint2 \<Rightarrow> eint2" where
nipkow@51882
   266
"below_rep p = (if is_empty_rep p then empty_rep else let (l,h) = p in (-\<infinity>,h))"
nipkow@51882
   267
nipkow@51882
   268
lift_definition above :: "ivl \<Rightarrow> ivl" is above_rep
nipkow@51882
   269
by(auto simp: above_rep_def eq_ivl_iff)
nipkow@51882
   270
nipkow@51882
   271
lift_definition below :: "ivl \<Rightarrow> ivl" is below_rep
nipkow@51882
   272
by(auto simp: below_rep_def eq_ivl_iff)
nipkow@51882
   273
nipkow@51882
   274
lemma \<gamma>_aboveI: "i \<in> \<gamma>_ivl iv \<Longrightarrow> i \<le> j \<Longrightarrow> j \<in> \<gamma>_ivl(above iv)"
nipkow@51882
   275
by transfer 
nipkow@51882
   276
   (auto simp add: above_rep_def \<gamma>_rep_cases is_empty_rep_def
nipkow@51882
   277
         split: extended.splits)
nipkow@47613
   278
nipkow@51882
   279
lemma \<gamma>_belowI: "i : \<gamma>_ivl iv \<Longrightarrow> j \<le> i \<Longrightarrow> j : \<gamma>_ivl(below iv)"
nipkow@51882
   280
by transfer 
nipkow@51882
   281
   (auto simp add: below_rep_def \<gamma>_rep_cases is_empty_rep_def
nipkow@51882
   282
         split: extended.splits)
nipkow@51359
   283
nipkow@51974
   284
definition inv_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
nipkow@51974
   285
"inv_less_ivl res iv1 iv2 =
nipkow@51882
   286
  (if res
nipkow@55125
   287
   then (iv1 \<sqinter> (below iv2 - [1,1]),
nipkow@55125
   288
         iv2 \<sqinter> (above iv1 + [1,1]))
nipkow@51882
   289
   else (iv1 \<sqinter> above iv2, iv2 \<sqinter> below iv1))"
nipkow@51882
   290
nipkow@51924
   291
lemma above_nice: "above[l,h] = (if [l,h] = \<bottom> then \<bottom> else [l,\<infinity>])"
nipkow@51882
   292
unfolding bot_ivl_def by transfer (simp add: above_rep_def eq_ivl_empty)
nipkow@51882
   293
nipkow@51924
   294
lemma below_nice: "below[l,h] = (if [l,h] = \<bottom> then \<bottom> else [-\<infinity>,h])"
nipkow@51882
   295
unfolding bot_ivl_def by transfer (simp add: below_rep_def eq_ivl_empty)
nipkow@47613
   296
nipkow@51359
   297
lemma add_mono_le_Fin:
nipkow@51359
   298
  "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))"
nipkow@51359
   299
by(drule (1) add_mono) simp
nipkow@51359
   300
nipkow@51359
   301
lemma add_mono_Fin_le:
nipkow@51359
   302
  "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
nipkow@51359
   303
by(drule (1) add_mono) simp
nipkow@51359
   304
haftmann@61890
   305
global_interpretation Val_semilattice
nipkow@51245
   306
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
nipkow@61179
   307
proof (standard, goal_cases)
nipkow@61179
   308
  case 1 thus ?case by transfer (simp add: le_iff_subset)
nipkow@47613
   309
next
nipkow@61179
   310
  case 2 show ?case by transfer (simp add: \<gamma>_rep_def)
nipkow@47613
   311
next
nipkow@61179
   312
  case 3 show ?case by transfer (simp add: \<gamma>_rep_def)
nipkow@47613
   313
next
nipkow@61179
   314
  case 4 thus ?case
nipkow@51359
   315
    apply transfer
nipkow@51359
   316
    apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
nipkow@51359
   317
    by(auto simp: empty_rep_def is_empty_rep_def)
nipkow@47613
   318
qed
nipkow@47613
   319
nipkow@51359
   320
haftmann@61890
   321
global_interpretation Val_lattice_gamma
nipkow@51245
   322
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
haftmann@61671
   323
defines aval_ivl = aval'
nipkow@61179
   324
proof (standard, goal_cases)
nipkow@61179
   325
  case 1 show ?case by(simp add: \<gamma>_inf)
nipkow@47613
   326
next
nipkow@61179
   327
  case 2 show ?case unfolding bot_ivl_def by transfer simp
nipkow@47613
   328
qed
nipkow@47613
   329
haftmann@61890
   330
global_interpretation Val_inv
nipkow@51245
   331
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
nipkow@47613
   332
and test_num' = in_ivl
nipkow@51974
   333
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
nipkow@61179
   334
proof (standard, goal_cases)
nipkow@61179
   335
  case 1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
nipkow@47613
   336
next
nipkow@61179
   337
  case (2 _ _ _ _ _ i1 i2) thus ?case
nipkow@51974
   338
    unfolding inv_plus_ivl_def minus_ivl_def
nipkow@51874
   339
    apply(clarsimp simp add: \<gamma>_inf)
nipkow@51874
   340
    using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"]
nipkow@51874
   341
    by(simp add:  \<gamma>_uminus)
nipkow@47613
   342
next
nipkow@61179
   343
  case (3 i1 i2) thus ?case
nipkow@55125
   344
    unfolding inv_less_ivl_def minus_ivl_def one_extended_def
nipkow@51882
   345
    apply(clarsimp simp add: \<gamma>_inf split: if_splits)
nipkow@51882
   346
    using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"]
nipkow@51882
   347
    apply(simp add: \<gamma>_belowI[of i2] \<gamma>_aboveI[of i1]
nipkow@51882
   348
      uminus_ivl.abs_eq uminus_rep_def \<gamma>_ivl_nice)
nipkow@51882
   349
    apply(simp add: \<gamma>_aboveI[of i2] \<gamma>_belowI[of i1])
nipkow@51359
   350
    done
nipkow@47613
   351
qed
nipkow@47613
   352
haftmann@61890
   353
global_interpretation Abs_Int_inv
nipkow@51245
   354
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
nipkow@47613
   355
and test_num' = in_ivl
nipkow@51974
   356
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
haftmann@61671
   357
defines inv_aval_ivl = inv_aval'
haftmann@55600
   358
and inv_bval_ivl = inv_bval'
haftmann@55600
   359
and step_ivl = step'
haftmann@55600
   360
and AI_ivl = AI
haftmann@55600
   361
and aval_ivl' = aval''
nipkow@47613
   362
..
nipkow@47613
   363
nipkow@47613
   364
nipkow@47613
   365
text{* Monotonicity: *}
nipkow@47613
   366
nipkow@51882
   367
lemma mono_plus_ivl: "iv1 \<le> iv2 \<Longrightarrow> iv3 \<le> iv4 \<Longrightarrow> iv1+iv3 \<le> iv2+(iv4::ivl)"
nipkow@51882
   368
apply transfer
nipkow@51359
   369
apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
nipkow@51359
   370
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
nipkow@51359
   371
nipkow@51882
   372
lemma mono_minus_ivl: "iv1 \<le> iv2 \<Longrightarrow> -iv1 \<le> -(iv2::ivl)"
nipkow@51882
   373
apply transfer
nipkow@51359
   374
apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split)
nipkow@51359
   375
by(auto simp: \<gamma>_rep_cases split: extended.splits)
nipkow@51359
   376
nipkow@51882
   377
lemma mono_above: "iv1 \<le> iv2 \<Longrightarrow> above iv1 \<le> above iv2"
nipkow@51882
   378
apply transfer
nipkow@51882
   379
apply(auto simp: above_rep_def le_iff_subset split: if_splits prod.split)
nipkow@51882
   380
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
nipkow@51882
   381
nipkow@51882
   382
lemma mono_below: "iv1 \<le> iv2 \<Longrightarrow> below iv1 \<le> below iv2"
nipkow@51882
   383
apply transfer
nipkow@51882
   384
apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
nipkow@51882
   385
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
nipkow@51882
   386
haftmann@61890
   387
global_interpretation Abs_Int_inv_mono
nipkow@51245
   388
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
nipkow@47613
   389
and test_num' = in_ivl
nipkow@51974
   390
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
nipkow@61179
   391
proof (standard, goal_cases)
nipkow@61179
   392
  case 1 thus ?case by (rule mono_plus_ivl)
nipkow@47613
   393
next
nipkow@61179
   394
  case 2 thus ?case
nipkow@51974
   395
    unfolding inv_plus_ivl_def minus_ivl_def less_eq_prod_def
nipkow@51882
   396
    by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_minus_ivl)
nipkow@51882
   397
next
nipkow@61179
   398
  case 3 thus ?case
nipkow@51974
   399
    unfolding less_eq_prod_def inv_less_ivl_def minus_ivl_def
nipkow@51882
   400
    by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_above mono_below)
nipkow@47613
   401
qed
nipkow@47613
   402
nipkow@47613
   403
nipkow@47613
   404
subsubsection "Tests"
nipkow@47613
   405
nipkow@51036
   406
value "show_acom_opt (AI_ivl test1_ivl)"
nipkow@47613
   407
nipkow@47613
   408
text{* Better than @{text AI_const}: *}
nipkow@51036
   409
value "show_acom_opt (AI_ivl test3_const)"
nipkow@51036
   410
value "show_acom_opt (AI_ivl test4_const)"
nipkow@51036
   411
value "show_acom_opt (AI_ivl test6_const)"
nipkow@47613
   412
nipkow@51711
   413
definition "steps c i = (step_ivl \<top> ^^ i) (bot c)"
nipkow@47613
   414
nipkow@51036
   415
value "show_acom_opt (AI_ivl test2_ivl)"
nipkow@47613
   416
value "show_acom (steps test2_ivl 0)"
nipkow@47613
   417
value "show_acom (steps test2_ivl 1)"
nipkow@47613
   418
value "show_acom (steps test2_ivl 2)"
nipkow@49188
   419
value "show_acom (steps test2_ivl 3)"
nipkow@47613
   420
nipkow@51036
   421
text{* Fixed point reached in 2 steps.
nipkow@47613
   422
 Not so if the start value of x is known: *}
nipkow@47613
   423
nipkow@51036
   424
value "show_acom_opt (AI_ivl test3_ivl)"
nipkow@47613
   425
value "show_acom (steps test3_ivl 0)"
nipkow@47613
   426
value "show_acom (steps test3_ivl 1)"
nipkow@47613
   427
value "show_acom (steps test3_ivl 2)"
nipkow@47613
   428
value "show_acom (steps test3_ivl 3)"
nipkow@47613
   429
value "show_acom (steps test3_ivl 4)"
nipkow@49188
   430
value "show_acom (steps test3_ivl 5)"
nipkow@47613
   431
nipkow@47613
   432
text{* Takes as many iterations as the actual execution. Would diverge if
nipkow@47613
   433
loop did not terminate. Worse still, as the following example shows: even if
nipkow@47613
   434
the actual execution terminates, the analysis may not. The value of y keeps
nipkow@47613
   435
decreasing as the analysis is iterated, no matter how long: *}
nipkow@47613
   436
nipkow@47613
   437
value "show_acom (steps test4_ivl 50)"
nipkow@47613
   438
nipkow@47613
   439
text{* Relationships between variables are NOT captured: *}
nipkow@51036
   440
value "show_acom_opt (AI_ivl test5_ivl)"
nipkow@47613
   441
nipkow@47613
   442
text{* Again, the analysis would not terminate: *}
nipkow@47613
   443
value "show_acom (steps test6_ivl 50)"
nipkow@47613
   444
nipkow@47613
   445
end