src/HOL/IMP/Abs_Int1_ivl.thy
author nipkow
Sun, 05 Feb 2012 16:53:11 +0100
changeset 46430 ead59736792b
parent 46355 42a01315d998
permissions -rw-r--r--
simplified code generation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     2
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     3
theory Abs_Int1_ivl
45990
b7b905b23b2a incorporated More_Set and More_List into the Main body -- to be consolidated later
haftmann
parents: 45978
diff changeset
     4
imports Abs_Int1 Abs_Int_Tests
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     5
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     6
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     7
subsection "Interval Analysis"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     8
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
     9
datatype ivl = I "int option" "int option"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    10
46039
nipkow
parents: 46028
diff changeset
    11
definition "\<gamma>_ivl i = (case i of
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    12
  I (Some l) (Some h) \<Rightarrow> {l..h} |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    13
  I (Some l) None \<Rightarrow> {l..} |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    14
  I None (Some h) \<Rightarrow> {..h} |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    15
  I None None \<Rightarrow> UNIV)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    16
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    17
abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    18
"{lo\<dots>hi} == I (Some lo) (Some hi)"
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    19
abbreviation I_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    20
"{lo\<dots>} == I (Some lo) None"
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    21
abbreviation I_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    22
"{\<dots>hi} == I None (Some hi)"
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    23
abbreviation I_None_None :: "ivl"  ("{\<dots>}") where
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    24
"{\<dots>} == I None None"
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    25
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    26
definition "num_ivl n = {n\<dots>n}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    27
46430
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
    28
fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
    29
"in_ivl k (I (Some l) (Some h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
    30
"in_ivl k (I (Some l) None) \<longleftrightarrow> l \<le> k" |
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
    31
"in_ivl k (I None (Some h)) \<longleftrightarrow> k \<le> h" |
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
    32
"in_ivl k (I None None) \<longleftrightarrow> True"
45978
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    33
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    34
instantiation option :: (plus)plus
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    35
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    36
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    37
fun plus_option where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    38
"Some x + Some y = Some(x+y)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    39
"_ + _ = None"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    40
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
    41
instance ..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    42
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    43
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    44
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    45
definition empty where "empty = {1\<dots>0}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    46
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    47
fun is_empty where
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    48
"is_empty {l\<dots>h} = (h<l)" |
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    49
"is_empty _ = False"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    50
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    51
lemma [simp]: "is_empty(I l h) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    52
  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    53
by(auto split:option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    54
46039
nipkow
parents: 46028
diff changeset
    55
lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
nipkow
parents: 46028
diff changeset
    56
by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    57
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    58
definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    59
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    60
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    61
instantiation ivl :: SL_top
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    62
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    63
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    64
definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    65
"le_option pos x y =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    66
 (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    67
  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    68
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    69
fun le_aux where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    70
"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    71
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    72
definition le_ivl where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    73
"i1 \<sqsubseteq> i2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    74
 (if is_empty i1 then True else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    75
  if is_empty i2 then False else le_aux i1 i2)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    76
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    77
definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    78
"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    79
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    80
definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    81
"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    82
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    83
definition "i1 \<squnion> i2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    84
 (if is_empty i1 then i2 else if is_empty i2 then i1
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    85
  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    86
          I (min_option False l1 l2) (max_option True h1 h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    87
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    88
definition "\<top> = {\<dots>}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    89
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    90
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    91
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    92
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    93
    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    94
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    95
  case goal2 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    96
    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    97
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    98
  case goal3 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   100
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   101
  case goal4 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   103
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   104
  case goal5 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   106
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   107
  case goal6 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   108
    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   109
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   110
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   111
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   112
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   113
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   114
instantiation ivl :: L_top_bot
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   115
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   116
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   117
definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   118
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   119
    I (max_option False l1 l2) (min_option True h1 h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   120
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   121
definition "\<bottom> = empty"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   122
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   123
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   124
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   125
  case goal1 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   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)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   127
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   128
  case goal2 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   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)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   130
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   131
  case goal3 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   133
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   134
  case goal4 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   135
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   136
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   137
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   138
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   139
instantiation option :: (minus)minus
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   140
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   141
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   142
fun minus_option where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   143
"Some x - Some y = Some(x-y)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   144
"_ - _ = None"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   145
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   146
instance ..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   147
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   148
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   149
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   150
definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   151
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   152
46039
nipkow
parents: 46028
diff changeset
   153
lemma gamma_minus_ivl:
nipkow
parents: 46028
diff changeset
   154
  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
nipkow
parents: 46028
diff changeset
   155
by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits option.splits)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   156
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   157
definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   158
  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   159
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   160
fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   161
"filter_less_ivl res (I l1 h1) (I l2 h2) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   162
  (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   163
   if res
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   164
   then (I l1 (min_option True h1 (h2 - Some 1)),
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   165
         I (max_option False (l1 + Some 1) l2) h2)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   166
   else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   167
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   168
interpretation Val_abs
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   169
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   170
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   171
  case goal1 thus ?case
46039
nipkow
parents: 46028
diff changeset
   172
    by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   173
next
46039
nipkow
parents: 46028
diff changeset
   174
  case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   175
next
46039
nipkow
parents: 46028
diff changeset
   176
  case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   177
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   178
  case goal4 thus ?case
46039
nipkow
parents: 46028
diff changeset
   179
    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   180
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   181
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   182
interpretation Val_abs1_gamma
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   183
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46346
10c18630612a removed duplicate definitions that made locale inconsistent
nipkow
parents: 46063
diff changeset
   184
defines aval_ivl is aval'
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   185
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   186
  case goal1 thus ?case
46039
nipkow
parents: 46028
diff changeset
   187
    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   188
next
46039
nipkow
parents: 46028
diff changeset
   189
  case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   190
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   191
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   192
lemma mono_minus_ivl:
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   193
  "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   194
apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   195
  apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   196
 apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   197
apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   198
done
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   199
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   200
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   201
interpretation Val_abs1
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   202
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46430
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
   203
and test_num' = in_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   204
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   205
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   206
  case goal1 thus ?case
46430
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
   207
    by (simp add: \<gamma>_ivl_def split: ivl.split option.split)
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   208
next
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   209
  case goal2 thus ?case
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   210
    by(auto simp add: filter_plus_ivl_def)
46039
nipkow
parents: 46028
diff changeset
   211
      (metis gamma_minus_ivl add_diff_cancel add_commute)+
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   212
next
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   213
  case goal3 thus ?case
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   214
    by(cases a1, cases a2,
46039
nipkow
parents: 46028
diff changeset
   215
      auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   216
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   217
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   218
interpretation Abs_Int1
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   219
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46430
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
   220
and test_num' = in_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   221
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   222
defines afilter_ivl is afilter
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   223
and bfilter_ivl is bfilter
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   224
and step_ivl is step'
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   225
and AI_ivl is AI
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   226
and aval_ivl' is aval''
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   227
..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   228
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   229
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   230
text{* Monotonicity: *}
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   231
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   232
interpretation Abs_Int1_mono
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   233
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46430
ead59736792b simplified code generation
nipkow
parents: 46355
diff changeset
   234
and test_num' = in_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   235
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   236
proof
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   237
  case goal1 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   238
    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   239
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   240
  case goal2 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   241
    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   242
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   243
  case goal3 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   244
    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   245
    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   246
qed
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   247
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   248
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   249
subsubsection "Tests"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   250
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   251
value "show_acom_opt (AI_ivl test1_ivl)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   252
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   253
text{* Better than @{text AI_const}: *}
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   254
value "show_acom_opt (AI_ivl test3_const)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   255
value "show_acom_opt (AI_ivl test4_const)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   256
value "show_acom_opt (AI_ivl test6_const)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   257
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   258
value "show_acom_opt (AI_ivl test2_ivl)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   259
value "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   260
value "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   261
value "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   262
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   263
text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   264
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   265
value "show_acom_opt (AI_ivl test3_ivl)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   266
value "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   267
value "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   268
value "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   269
value "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   270
value "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   271
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   272
text{* Takes as many iterations as the actual execution. Would diverge if
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   273
loop did not terminate. Worse still, as the following example shows: even if
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   274
the actual execution terminates, the analysis may not. The value of y keeps
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   275
decreasing as the analysis is iterated, no matter how long: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   276
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   277
value "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   278
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   279
text{* Relationships between variables are NOT captured: *}
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   280
value "show_acom_opt (AI_ivl test5_ivl)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   281
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   282
text{* Again, the analysis would not terminate: *}
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   283
value "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test6_ivl))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   284
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   285
end