src/HOL/IMP/Abs_Int1_ivl.thy
author nipkow
Wed Oct 12 09:16:30 2011 +0200 (2011-10-12)
changeset 45127 d2eb07a1e01b
parent 45113 2a0d7be998bb
child 45623 f682f3f7b726
permissions -rw-r--r--
separated monotonicity reasoning and defined narrowing with while_option
nipkow@45111
     1
(* Author: Tobias Nipkow *)
nipkow@45111
     2
nipkow@45111
     3
theory Abs_Int1_ivl
nipkow@45111
     4
imports Abs_Int1
nipkow@45111
     5
begin
nipkow@45111
     6
nipkow@45111
     7
subsection "Interval Analysis"
nipkow@45111
     8
nipkow@45111
     9
datatype ivl = I "int option" "int option"
nipkow@45111
    10
nipkow@45111
    11
definition "rep_ivl i = (case i of
nipkow@45111
    12
  I (Some l) (Some h) \<Rightarrow> {l..h} |
nipkow@45111
    13
  I (Some l) None \<Rightarrow> {l..} |
nipkow@45111
    14
  I None (Some h) \<Rightarrow> {..h} |
nipkow@45111
    15
  I None None \<Rightarrow> UNIV)"
nipkow@45111
    16
nipkow@45113
    17
abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
nipkow@45113
    18
"{lo\<dots>hi} == I (Some lo) (Some hi)"
nipkow@45113
    19
abbreviation I_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
nipkow@45113
    20
"{lo\<dots>} == I (Some lo) None"
nipkow@45113
    21
abbreviation I_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
nipkow@45113
    22
"{\<dots>hi} == I None (Some hi)"
nipkow@45113
    23
abbreviation I_None_None :: "ivl"  ("{\<dots>}") where
nipkow@45113
    24
"{\<dots>} == I None None"
nipkow@45113
    25
nipkow@45113
    26
definition "num_ivl n = {n\<dots>n}"
nipkow@45111
    27
nipkow@45111
    28
instantiation option :: (plus)plus
nipkow@45111
    29
begin
nipkow@45111
    30
nipkow@45111
    31
fun plus_option where
nipkow@45111
    32
"Some x + Some y = Some(x+y)" |
nipkow@45111
    33
"_ + _ = None"
nipkow@45111
    34
nipkow@45111
    35
instance proof qed
nipkow@45111
    36
nipkow@45111
    37
end
nipkow@45111
    38
nipkow@45113
    39
definition empty where "empty = {1\<dots>0}"
nipkow@45111
    40
nipkow@45111
    41
fun is_empty where
nipkow@45113
    42
"is_empty {l\<dots>h} = (h<l)" |
nipkow@45111
    43
"is_empty _ = False"
nipkow@45111
    44
nipkow@45111
    45
lemma [simp]: "is_empty(I l h) =
nipkow@45111
    46
  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
nipkow@45111
    47
by(auto split:option.split)
nipkow@45111
    48
nipkow@45111
    49
lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
nipkow@45111
    50
by(auto simp add: rep_ivl_def split: ivl.split option.split)
nipkow@45111
    51
nipkow@45111
    52
definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
nipkow@45111
    53
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
nipkow@45111
    54
nipkow@45111
    55
instantiation ivl :: SL_top
nipkow@45111
    56
begin
nipkow@45111
    57
nipkow@45111
    58
definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
nipkow@45111
    59
"le_option pos x y =
nipkow@45111
    60
 (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
nipkow@45111
    61
  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
nipkow@45111
    62
nipkow@45111
    63
fun le_aux where
nipkow@45111
    64
"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
nipkow@45111
    65
nipkow@45111
    66
definition le_ivl where
nipkow@45111
    67
"i1 \<sqsubseteq> i2 =
nipkow@45111
    68
 (if is_empty i1 then True else
nipkow@45111
    69
  if is_empty i2 then False else le_aux i1 i2)"
nipkow@45111
    70
nipkow@45111
    71
definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
nipkow@45111
    72
"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
nipkow@45111
    73
nipkow@45111
    74
definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
nipkow@45111
    75
"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
nipkow@45111
    76
nipkow@45111
    77
definition "i1 \<squnion> i2 =
nipkow@45111
    78
 (if is_empty i1 then i2 else if is_empty i2 then i1
nipkow@45111
    79
  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
nipkow@45111
    80
          I (min_option False l1 l2) (max_option True h1 h2))"
nipkow@45111
    81
nipkow@45113
    82
definition "\<top> = {\<dots>}"
nipkow@45111
    83
nipkow@45111
    84
instance
nipkow@45111
    85
proof
nipkow@45111
    86
  case goal1 thus ?case
nipkow@45111
    87
    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
nipkow@45111
    88
next
nipkow@45111
    89
  case goal2 thus ?case
nipkow@45111
    90
    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
nipkow@45111
    91
next
nipkow@45111
    92
  case goal3 thus ?case
nipkow@45111
    93
    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)
nipkow@45111
    94
next
nipkow@45111
    95
  case goal4 thus ?case
nipkow@45111
    96
    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)
nipkow@45111
    97
next
nipkow@45111
    98
  case goal5 thus ?case
nipkow@45111
    99
    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)
nipkow@45111
   100
next
nipkow@45111
   101
  case goal6 thus ?case
nipkow@45111
   102
    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
nipkow@45111
   103
qed
nipkow@45111
   104
nipkow@45111
   105
end
nipkow@45111
   106
nipkow@45111
   107
nipkow@45111
   108
instantiation ivl :: L_top_bot
nipkow@45111
   109
begin
nipkow@45111
   110
nipkow@45111
   111
definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
nipkow@45111
   112
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
nipkow@45111
   113
    I (max_option False l1 l2) (min_option True h1 h2))"
nipkow@45111
   114
nipkow@45111
   115
definition "\<bottom> = empty"
nipkow@45111
   116
nipkow@45111
   117
instance
nipkow@45111
   118
proof
nipkow@45111
   119
  case goal1 thus ?case
nipkow@45111
   120
    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)
nipkow@45111
   121
next
nipkow@45111
   122
  case goal2 thus ?case
nipkow@45111
   123
    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)
nipkow@45111
   124
next
nipkow@45111
   125
  case goal3 thus ?case
nipkow@45111
   126
    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)
nipkow@45111
   127
next
nipkow@45111
   128
  case goal4 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
nipkow@45111
   129
qed
nipkow@45111
   130
nipkow@45111
   131
end
nipkow@45111
   132
nipkow@45111
   133
instantiation option :: (minus)minus
nipkow@45111
   134
begin
nipkow@45111
   135
nipkow@45111
   136
fun minus_option where
nipkow@45111
   137
"Some x - Some y = Some(x-y)" |
nipkow@45111
   138
"_ - _ = None"
nipkow@45111
   139
nipkow@45111
   140
instance proof qed
nipkow@45111
   141
nipkow@45111
   142
end
nipkow@45111
   143
nipkow@45111
   144
definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
nipkow@45111
   145
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
nipkow@45111
   146
nipkow@45111
   147
lemma rep_minus_ivl:
nipkow@45111
   148
  "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
nipkow@45111
   149
by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
nipkow@45111
   150
nipkow@45111
   151
nipkow@45111
   152
definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
nipkow@45111
   153
  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
nipkow@45111
   154
nipkow@45111
   155
fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
nipkow@45111
   156
"filter_less_ivl res (I l1 h1) (I l2 h2) =
nipkow@45111
   157
  (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else
nipkow@45111
   158
   if res
nipkow@45111
   159
   then (I l1 (min_option True h1 (h2 - Some 1)),
nipkow@45111
   160
         I (max_option False (l1 + Some 1) l2) h2)
nipkow@45111
   161
   else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
nipkow@45111
   162
nipkow@45127
   163
interpretation Val_abs rep_ivl num_ivl plus_ivl
nipkow@45111
   164
proof
nipkow@45111
   165
  case goal1 thus ?case
nipkow@45111
   166
    by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
nipkow@45111
   167
next
nipkow@45111
   168
  case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
nipkow@45127
   169
next
nipkow@45127
   170
  case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def)
nipkow@45127
   171
next
nipkow@45127
   172
  case goal4 thus ?case
nipkow@45127
   173
    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
nipkow@45111
   174
qed
nipkow@45111
   175
nipkow@45127
   176
interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl
nipkow@45111
   177
proof
nipkow@45111
   178
  case goal1 thus ?case
nipkow@45111
   179
    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
nipkow@45111
   180
next
nipkow@45111
   181
  case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def)
nipkow@45111
   182
qed
nipkow@45111
   183
nipkow@45111
   184
lemma mono_minus_ivl:
nipkow@45111
   185
  "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'"
nipkow@45111
   186
apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits)
nipkow@45111
   187
  apply(simp split: option.splits)
nipkow@45111
   188
 apply(simp split: option.splits)
nipkow@45111
   189
apply(simp split: option.splits)
nipkow@45111
   190
done
nipkow@45111
   191
nipkow@45111
   192
nipkow@45111
   193
interpretation
nipkow@45111
   194
  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
nipkow@45111
   195
proof
nipkow@45111
   196
  case goal1 thus ?case
nipkow@45111
   197
    by(auto simp add: filter_plus_ivl_def)
nipkow@45111
   198
      (metis rep_minus_ivl add_diff_cancel add_commute)+
nipkow@45111
   199
next
nipkow@45111
   200
  case goal2 thus ?case
nipkow@45111
   201
    by(cases a1, cases a2,
nipkow@45111
   202
      auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
nipkow@45111
   203
qed
nipkow@45111
   204
nipkow@45111
   205
interpretation
nipkow@45127
   206
  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
nipkow@45111
   207
defines afilter_ivl is afilter
nipkow@45111
   208
and bfilter_ivl is bfilter
nipkow@45111
   209
and step_ivl is step
nipkow@45111
   210
and AI_ivl is AI
nipkow@45111
   211
and aval_ivl is aval'
nipkow@45127
   212
proof qed
nipkow@45111
   213
nipkow@45111
   214
definition "test1_ivl =
nipkow@45111
   215
 ''y'' ::= N 7;
nipkow@45111
   216
 IF Less (V ''x'') (V ''y'')
nipkow@45111
   217
 THEN ''y'' ::= Plus (V ''y'') (V ''x'')
nipkow@45111
   218
 ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
nipkow@45111
   219
nipkow@45127
   220
value [code] "show_acom_opt (AI_ivl test1_ivl)"
nipkow@45111
   221
nipkow@45127
   222
value [code] "show_acom_opt (AI_const test3_const)"
nipkow@45127
   223
value [code] "show_acom_opt (AI_ivl test3_const)"
nipkow@45111
   224
nipkow@45127
   225
value [code] "show_acom_opt (AI_const test4_const)"
nipkow@45127
   226
value [code] "show_acom_opt (AI_ivl test4_const)"
nipkow@45111
   227
nipkow@45127
   228
value [code] "show_acom_opt (AI_ivl test6_const)"
nipkow@45111
   229
nipkow@45111
   230
definition "test2_ivl =
nipkow@45111
   231
 WHILE Less (V ''x'') (N 100)
nipkow@45111
   232
 DO ''x'' ::= Plus (V ''x'') (N 1)"
nipkow@45111
   233
nipkow@45127
   234
value [code] "show_acom_opt (AI_ivl test2_ivl)"
nipkow@45127
   235
value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
nipkow@45127
   236
value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
nipkow@45127
   237
value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
nipkow@45127
   238
nipkow@45127
   239
text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
nipkow@45111
   240
nipkow@45111
   241
definition "test3_ivl =
nipkow@45111
   242
 ''x'' ::= N 7;
nipkow@45111
   243
 WHILE Less (V ''x'') (N 100)
nipkow@45111
   244
 DO ''x'' ::= Plus (V ''x'') (N 1)"
nipkow@45111
   245
nipkow@45127
   246
value [code] "show_acom_opt (AI_ivl test3_ivl)"
nipkow@45111
   247
value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
nipkow@45111
   248
value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
nipkow@45111
   249
value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
nipkow@45111
   250
value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
nipkow@45111
   251
value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
nipkow@45111
   252
nipkow@45127
   253
text{* Takes as many iterations as the actual execution. Would diverge if
nipkow@45127
   254
loop did not terminate. Worse still, as the following example shows: even if
nipkow@45127
   255
the actual execution terminates, the analysis may not: *}
nipkow@45127
   256
nipkow@45111
   257
definition "test4_ivl =
nipkow@45111
   258
 ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
nipkow@45111
   259
 WHILE Less (V ''x'') (N 11)
nipkow@45111
   260
 DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
nipkow@45127
   261
nipkow@45127
   262
text{* The value of y keeps decreasing as the analysis is iterated, no matter
nipkow@45127
   263
how long: *}
nipkow@45127
   264
nipkow@45127
   265
value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
nipkow@45111
   266
nipkow@45111
   267
definition "test5_ivl =
nipkow@45111
   268
 ''x'' ::= N 0; ''y'' ::= N 0;
nipkow@45127
   269
 WHILE Less (V ''x'') (N 1000)
nipkow@45111
   270
 DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
nipkow@45127
   271
value [code] "show_acom_opt (AI_ivl test5_ivl)"
nipkow@45111
   272
nipkow@45127
   273
text{* Again, the analysis would not terminate: *}
nipkow@45111
   274
definition "test6_ivl =
nipkow@45111
   275
 ''x'' ::= N 0;
nipkow@45111
   276
 WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
nipkow@45127
   277
nipkow@45127
   278
text{* Monotonicity: *}
nipkow@45127
   279
nipkow@45127
   280
interpretation
nipkow@45127
   281
  Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
nipkow@45127
   282
proof
nipkow@45127
   283
  case goal1 thus ?case
nipkow@45127
   284
    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
nipkow@45127
   285
next
nipkow@45127
   286
  case goal2 thus ?case
nipkow@45127
   287
    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
nipkow@45127
   288
next
nipkow@45127
   289
  case goal3 thus ?case
nipkow@45127
   290
    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
nipkow@45127
   291
    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
nipkow@45127
   292
qed
nipkow@45111
   293
nipkow@45111
   294
end