src/HOL/IMP/Abs_Int1_ivl.thy
author nipkow
Thu, 24 Nov 2011 19:58:37 +0100
changeset 45623 f682f3f7b726
parent 45127 d2eb07a1e01b
child 45655 a49f9428aba4
permissions -rw-r--r--
Abstract interpretation is now based uniformly on annotated programs, including a collecting and a small step semantics
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
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
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
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    11
definition "rep_ivl i = (case i of
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
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    28
instantiation option :: (plus)plus
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    29
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    30
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    31
fun plus_option where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    32
"Some x + Some y = Some(x+y)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    33
"_ + _ = None"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    34
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    35
instance proof qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    36
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    37
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    38
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    39
definition empty where "empty = {1\<dots>0}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    40
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    41
fun is_empty where
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    42
"is_empty {l\<dots>h} = (h<l)" |
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    43
"is_empty _ = False"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    44
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    45
lemma [simp]: "is_empty(I l h) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    46
  (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
    47
by(auto split:option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    48
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    49
lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    50
by(auto simp add: rep_ivl_def split: ivl.split option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    51
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    52
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
    53
  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
    54
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    55
instantiation ivl :: SL_top
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    56
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    57
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    58
definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    59
"le_option pos x y =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    60
 (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
    61
  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    62
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    63
fun le_aux where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    64
"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
    65
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    66
definition le_ivl where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    67
"i1 \<sqsubseteq> i2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    68
 (if is_empty i1 then True else
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    69
  if is_empty i2 then False else le_aux i1 i2)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    70
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    71
definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    72
"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
    73
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    74
definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    75
"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
    76
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    77
definition "i1 \<squnion> i2 =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    78
 (if is_empty i1 then i2 else if is_empty i2 then i1
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    79
  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    80
          I (min_option False l1 l2) (max_option True h1 h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    81
45113
2a0d7be998bb added nice interval syntax
nipkow
parents: 45111
diff changeset
    82
definition "\<top> = {\<dots>}"
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    83
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    84
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    85
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    86
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    87
    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    88
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    89
  case goal2 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    90
    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
    91
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    92
  case goal3 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    94
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    95
  case goal4 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    97
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    98
  case goal5 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
    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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   100
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   101
  case goal6 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   102
    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
   103
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   104
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   105
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   106
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   107
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   108
instantiation ivl :: L_top_bot
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   109
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   110
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   111
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
   112
  case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   113
    I (max_option False l1 l2) (min_option True h1 h2))"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   114
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   115
definition "\<bottom> = empty"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   116
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   117
instance
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   118
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   119
  case goal1 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   120
    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
   121
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   122
  case goal2 thus ?case
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   123
    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
   124
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   125
  case goal3 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   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)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   127
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   128
  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
   129
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   130
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   131
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   132
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   133
instantiation option :: (minus)minus
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   134
begin
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   135
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   136
fun minus_option where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   137
"Some x - Some y = Some(x-y)" |
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   138
"_ - _ = None"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   139
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   140
instance proof qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   141
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   142
end
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   143
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   144
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
   145
  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
   146
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   147
lemma rep_minus_ivl:
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   148
  "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   149
by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   150
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   151
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   152
definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   153
  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   154
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   155
fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   156
"filter_less_ivl res (I l1 h1) (I l2 h2) =
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   157
  (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
   158
   if res
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   159
   then (I l1 (min_option True h1 (h2 - Some 1)),
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   160
         I (max_option False (l1 + Some 1) l2) h2)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   161
   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
   162
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   163
interpretation Val_abs rep_ivl num_ivl plus_ivl
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   164
defines aval_ivl is aval'
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   165
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   166
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   167
    by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   168
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   169
  case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   170
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   171
  case goal3 thus ?case by(simp add: rep_ivl_def num_ivl_def)
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   172
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   173
  case goal4 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   174
    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   175
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   176
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   177
interpretation Val_abs1_rep rep_ivl num_ivl plus_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   178
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   179
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   180
    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   181
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   182
  case goal2 show ?case by(auto simp add: bot_ivl_def rep_ivl_def empty_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   183
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   184
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   185
lemma mono_minus_ivl:
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   186
  "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
   187
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
   188
  apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   189
 apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   190
apply(simp split: option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   191
done
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   192
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   193
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   194
interpretation
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   195
  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   196
proof
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   197
  case goal1 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   198
    by(auto simp add: filter_plus_ivl_def)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   199
      (metis rep_minus_ivl add_diff_cancel add_commute)+
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   200
next
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   201
  case goal2 thus ?case
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   202
    by(cases a1, cases a2,
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   203
      auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   204
qed
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   205
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   206
interpretation
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   207
  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   208
defines afilter_ivl is afilter
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   209
and bfilter_ivl is bfilter
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   210
and step_ivl is step
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   211
and AI_ivl is AI
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   212
and aval_ivl' is aval''
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   213
proof qed
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   214
45127
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   215
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   216
text{* Monotonicity: *}
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   217
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   218
interpretation
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   219
  Abs_Int1_mono rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   220
proof
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   221
  case goal1 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   222
    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
   223
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   224
  case goal2 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   225
    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
   226
next
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   227
  case goal3 thus ?case
d2eb07a1e01b separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents: 45113
diff changeset
   228
    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
   229
    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
   230
qed
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   231
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   232
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   233
subsubsection "Tests"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   234
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   235
value [code] "show_acom_opt (AI_ivl test1_ivl)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   236
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   237
text{* Better than @{text AI_const}: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   238
value [code] "show_acom_opt (AI_ivl test3_const)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   239
value [code] "show_acom_opt (AI_ivl test4_const)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   240
value [code] "show_acom_opt (AI_ivl test6_const)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   241
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   242
value [code] "show_acom_opt (AI_ivl test2_ivl)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   243
value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   244
value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   245
value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   246
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   247
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
   248
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   249
value [code] "show_acom_opt (AI_ivl test3_ivl)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   250
value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   251
value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   252
value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   253
value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   254
value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   255
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   256
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
   257
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
   258
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
   259
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
   260
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   261
value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
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{* Relationships between variables are NOT captured: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   264
value [code] "show_acom_opt (AI_ivl test5_ivl)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   265
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   266
text{* Again, the analysis would not terminate: *}
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   267
value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test6_ivl))"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents: 45127
diff changeset
   268
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents:
diff changeset
   269
end