src/HOL/IMP/Abs_Int1_ivl.thy
author nipkow
Sun, 29 Jan 2012 15:16:27 +0100
changeset 46355 42a01315d998
parent 46346 10c18630612a
child 46430 ead59736792b
permissions -rw-r--r--
removed accidental dependance of abstract interpreter on gamma
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
45978
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    28
definition
46039
nipkow
parents: 46028
diff changeset
    29
  [code_abbrev]: "contained_in i k \<longleftrightarrow> k \<in> \<gamma>_ivl i"
45978
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    30
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    31
lemma contained_in_simps [code]:
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    32
  "contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    33
  "contained_in (I (Some l) None) k \<longleftrightarrow> l \<le> k"
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    34
  "contained_in (I None (Some h)) k \<longleftrightarrow> k \<le> h"
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    35
  "contained_in (I None None) k \<longleftrightarrow> True"
46039
nipkow
parents: 46028
diff changeset
    36
  by (simp_all add: contained_in_def \<gamma>_ivl_def)
45978
d3325de5f299 executable intervals
haftmann
parents: 45655
diff changeset
    37
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    38
instantiation option :: (plus)plus
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    39
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    40
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    41
fun plus_option where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    42
"Some x + Some y = Some(x+y)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    43
"_ + _ = None"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    44
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
    45
instance ..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    46
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    47
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    48
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    49
definition empty where "empty = {1\<dots>0}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    50
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    51
fun is_empty where
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    52
"is_empty {l\<dots>h} = (h<l)" |
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    53
"is_empty _ = False"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    54
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    55
lemma [simp]: "is_empty(I l h) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    56
  (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
    57
by(auto split:option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    58
46039
nipkow
parents: 46028
diff changeset
    59
lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
nipkow
parents: 46028
diff changeset
    60
by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    61
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    62
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
    63
  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
    64
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    65
instantiation ivl :: SL_top
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    66
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    67
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    68
definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    69
"le_option pos x y =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    70
 (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
    71
  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    72
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    73
fun le_aux where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    74
"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
    75
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    76
definition le_ivl where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    77
"i1 \<sqsubseteq> i2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    78
 (if is_empty i1 then True else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    79
  if is_empty i2 then False else le_aux i1 i2)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    80
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    81
definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    82
"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
    83
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    84
definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    85
"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
    86
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    87
definition "i1 \<squnion> i2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    88
 (if is_empty i1 then i2 else if is_empty i2 then i1
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    89
  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    90
          I (min_option False l1 l2) (max_option True h1 h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    91
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    92
definition "\<top> = {\<dots>}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    93
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    94
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    95
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    96
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    97
    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    98
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    99
  case goal2 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   100
    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
   101
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   102
  case goal3 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   103
    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
   104
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   105
  case goal4 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   106
    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
   107
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   108
  case goal5 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   109
    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
   110
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   111
  case goal6 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   112
    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
   113
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   114
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   115
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   116
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   117
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   118
instantiation ivl :: L_top_bot
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   119
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   120
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   121
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
   122
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   123
    I (max_option False l1 l2) (min_option True h1 h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   124
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   125
definition "\<bottom> = empty"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   126
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   127
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   128
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   129
  case goal1 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   130
    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
   131
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   132
  case goal2 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   133
    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
   134
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   135
  case goal3 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   136
    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
   137
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   138
  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
   139
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   140
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   141
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   142
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   143
instantiation option :: (minus)minus
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   144
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   145
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   146
fun minus_option where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   147
"Some x - Some y = Some(x-y)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   148
"_ - _ = None"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   149
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   150
instance ..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   151
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   152
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   153
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   154
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
   155
  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
   156
46039
nipkow
parents: 46028
diff changeset
   157
lemma gamma_minus_ivl:
nipkow
parents: 46028
diff changeset
   158
  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
nipkow
parents: 46028
diff changeset
   159
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
   160
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   161
definition "test_num_ivl n ivl = contained_in ivl n"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   162
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   163
definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   164
  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   165
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   166
fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   167
"filter_less_ivl res (I l1 h1) (I l2 h2) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   168
  (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
   169
   if res
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   170
   then (I l1 (min_option True h1 (h2 - Some 1)),
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   171
         I (max_option False (l1 + Some 1) l2) h2)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   172
   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
   173
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   174
interpretation Val_abs
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   175
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   176
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   177
  case goal1 thus ?case
46039
nipkow
parents: 46028
diff changeset
   178
    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
   179
next
46039
nipkow
parents: 46028
diff changeset
   180
  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
   181
next
46039
nipkow
parents: 46028
diff changeset
   182
  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
   183
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   184
  case goal4 thus ?case
46039
nipkow
parents: 46028
diff changeset
   185
    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
   186
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   187
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   188
interpretation Val_abs1_gamma
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   189
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
   190
defines aval_ivl is aval'
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   191
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   192
  case goal1 thus ?case
46039
nipkow
parents: 46028
diff changeset
   193
    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
   194
next
46039
nipkow
parents: 46028
diff changeset
   195
  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
   196
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   197
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   198
lemma mono_minus_ivl:
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   199
  "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
   200
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
   201
  apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   202
 apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   203
apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   204
done
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   205
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   206
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   207
interpretation Val_abs1
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   208
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   209
and test_num' = test_num_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   210
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   211
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   212
  case goal1 thus ?case
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   213
    by(auto simp add: test_num_ivl_def contained_in_def)
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   214
next
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   215
  case goal2 thus ?case
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   216
    by(auto simp add: filter_plus_ivl_def)
46039
nipkow
parents: 46028
diff changeset
   217
      (metis gamma_minus_ivl add_diff_cancel add_commute)+
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   218
next
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   219
  case goal3 thus ?case
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   220
    by(cases a1, cases a2,
46039
nipkow
parents: 46028
diff changeset
   221
      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
   222
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   223
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   224
interpretation Abs_Int1
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   225
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   226
and test_num' = test_num_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   227
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   228
defines afilter_ivl is afilter
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   229
and bfilter_ivl is bfilter
45655
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents: 45623
diff changeset
   230
and step_ivl is step'
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   231
and AI_ivl is AI
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   232
and aval_ivl' is aval''
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   233
..
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   234
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   235
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   236
text{* Monotonicity: *}
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   237
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   238
interpretation Abs_Int1_mono
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   239
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   240
and test_num' = test_num_ivl
46063
81ebd0cdb300 tuned types
nipkow
parents: 46039
diff changeset
   241
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
   242
proof
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   243
  case goal1 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   244
    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
   245
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   246
  case goal2 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   247
    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
   248
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   249
  case goal3 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   250
    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
   251
    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
   252
qed
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   253
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   254
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   255
subsubsection "Tests"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   256
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   257
value "show_acom_opt (AI_ivl test1_ivl)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   258
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   259
text{* Better than @{text AI_const}: *}
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   260
value "show_acom_opt (AI_ivl test3_const)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   261
value "show_acom_opt (AI_ivl test4_const)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   262
value "show_acom_opt (AI_ivl test6_const)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   263
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   264
value "show_acom_opt (AI_ivl test2_ivl)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   265
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
   266
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
   267
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
   268
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   269
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
   270
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   271
value "show_acom_opt (AI_ivl test3_ivl)"
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   272
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
   273
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
   274
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
   275
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
   276
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
   277
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   278
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
   279
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
   280
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
   281
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
   282
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 test4_ivl))"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   284
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   285
text{* Relationships between variables are NOT captured: *}
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   286
value "show_acom_opt (AI_ivl test5_ivl)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   287
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   288
text{* Again, the analysis would not terminate: *}
46355
42a01315d998 removed accidental dependance of abstract interpreter on gamma
nipkow
parents: 46346
diff changeset
   289
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
   290
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   291
end