author | nipkow |
Sun, 27 Nov 2011 13:31:52 +0100 | |
changeset 45655 | a49f9428aba4 |
parent 45623 | f682f3f7b726 |
child 45903 | 02dd9319dcb7 |
permissions | -rw-r--r-- |
45111 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_Int2 |
|
4 |
imports Abs_Int1_ivl |
|
5 |
begin |
|
6 |
||
7 |
||
8 |
subsection "Widening and Narrowing" |
|
9 |
||
10 |
class WN = SL_top + |
|
11 |
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65) |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
12 |
assumes widen1: "x \<sqsubseteq> x \<nabla> y" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
13 |
assumes widen2: "y \<sqsubseteq> x \<nabla> y" |
45111 | 14 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65) |
15 |
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y" |
|
16 |
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x" |
|
17 |
||
18 |
||
19 |
instantiation ivl :: WN |
|
20 |
begin |
|
21 |
||
22 |
definition "widen_ivl ivl1 ivl2 = |
|
23 |
((*if is_empty ivl1 then ivl2 else |
|
24 |
if is_empty ivl2 then ivl1 else*) |
|
25 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow> |
|
26 |
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1) |
|
27 |
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))" |
|
28 |
||
29 |
definition "narrow_ivl ivl1 ivl2 = |
|
30 |
((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*) |
|
31 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow> |
|
32 |
I (if l1 = None then l2 else l1) |
|
33 |
(if h1 = None then h2 else h1))" |
|
34 |
||
35 |
instance |
|
36 |
proof qed |
|
37 |
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits) |
|
38 |
||
39 |
end |
|
40 |
||
41 |
instantiation st :: (WN)WN |
|
42 |
begin |
|
43 |
||
44 |
definition "widen_st F1 F2 = |
|
45 |
FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))" |
|
46 |
||
47 |
definition "narrow_st F1 F2 = |
|
48 |
FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))" |
|
49 |
||
50 |
instance |
|
51 |
proof |
|
52 |
case goal1 thus ?case |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
53 |
by(simp add: widen_st_def le_st_def lookup_def widen1) |
45111 | 54 |
next |
55 |
case goal2 thus ?case |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
56 |
by(simp add: widen_st_def le_st_def lookup_def widen2) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
57 |
next |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
58 |
case goal3 thus ?case |
45111 | 59 |
by(auto simp: narrow_st_def le_st_def lookup_def narrow1) |
60 |
next |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
61 |
case goal4 thus ?case |
45111 | 62 |
by(auto simp: narrow_st_def le_st_def lookup_def narrow2) |
63 |
qed |
|
64 |
||
65 |
end |
|
66 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
67 |
instantiation option :: (WN)WN |
45111 | 68 |
begin |
69 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
70 |
fun widen_option where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
71 |
"None \<nabla> x = x" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
72 |
"x \<nabla> None = x" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
73 |
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" |
45111 | 74 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
75 |
fun narrow_option where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
76 |
"None \<triangle> x = None" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
77 |
"x \<triangle> None = None" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
78 |
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
45111 | 79 |
|
80 |
instance |
|
81 |
proof |
|
82 |
case goal1 show ?case |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
83 |
by(induct x y rule: widen_option.induct) (simp_all add: widen1) |
45111 | 84 |
next |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
85 |
case goal2 show ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
86 |
by(induct x y rule: widen_option.induct) (simp_all add: widen2) |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
87 |
next |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
88 |
case goal3 thus ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
89 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
45111 | 90 |
next |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
91 |
case goal4 thus ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
92 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
45111 | 93 |
qed |
94 |
||
95 |
end |
|
96 |
||
97 |
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
|
98 |
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | |
|
99 |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | |
|
100 |
"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" | |
|
101 |
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) = |
|
102 |
(IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" | |
|
103 |
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) = |
|
104 |
({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})" |
|
105 |
||
106 |
abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65) |
|
107 |
where "widen_acom == map2_acom (op \<nabla>)" |
|
108 |
||
109 |
abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65) |
|
110 |
where "narrow_acom == map2_acom (op \<triangle>)" |
|
111 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
112 |
lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
113 |
by(induct c c' rule: le_acom.induct)(simp_all add: widen1) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
114 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
115 |
lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
116 |
by(induct c c' rule: le_acom.induct)(simp_all add: widen2) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
117 |
|
45111 | 118 |
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y" |
119 |
by(induct y x rule: le_acom.induct) (simp_all add: narrow1) |
|
120 |
||
121 |
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x" |
|
122 |
by(induct y x rule: le_acom.induct) (simp_all add: narrow2) |
|
123 |
||
124 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
125 |
subsubsection "Post-fixed point computation" |
45111 | 126 |
|
127 |
definition |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
128 |
prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
129 |
"prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
130 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
131 |
definition |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
132 |
pfp_WN :: "(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
133 |
where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
134 |
| Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')" |
45111 | 135 |
|
136 |
lemma strip_map2_acom: |
|
137 |
"strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1" |
|
138 |
by(induct f c1 c2 rule: map2_acom.induct) simp_all |
|
139 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
140 |
lemma lpfp_step_up_pfp: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
141 |
"\<lbrakk> \<forall>c. strip(f c) = strip c; lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
142 |
by (metis (no_types) assms lpfpc_pfp le_trans widen2_acom) |
45111 | 143 |
|
144 |
lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
145 |
and "prefp (\<lambda>c. c \<triangle>\<^sub>c f c) x0 = Some x" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
146 |
shows "f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0" (is "?P x") |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
147 |
proof- |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
148 |
{ fix x assume "?P x" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
149 |
note 1 = conjunct1[OF this] and 2 = conjunct2[OF this] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
150 |
let ?x' = "x \<triangle>\<^sub>c f x" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
151 |
have "?P ?x'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
152 |
proof |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
153 |
have "f ?x' \<sqsubseteq> f x" by(rule monoD[OF `mono f` narrow2_acom[OF 1]]) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
154 |
also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1_acom[OF 1]) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
155 |
finally show "f ?x' \<sqsubseteq> ?x'" . |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
156 |
have "?x' \<sqsubseteq> x" by (rule narrow2_acom[OF 1]) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
157 |
also have "x \<sqsubseteq> x0" by(rule 2) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
158 |
finally show "?x' \<sqsubseteq> x0" . |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
159 |
qed |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
160 |
} |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
161 |
with while_option_rule[where P = ?P, OF _ assms(3)[simplified prefp_def]] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
162 |
assms(2) le_refl |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
163 |
show ?thesis by blast |
45111 | 164 |
qed |
165 |
||
166 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
167 |
lemma pfp_WN_pfp: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
168 |
"\<lbrakk> \<forall>c. strip (f c) = strip c; mono f; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
169 |
unfolding pfp_WN_def |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
170 |
by (auto dest: iter_down_pfp lpfp_step_up_pfp split: option.splits) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
171 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
172 |
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
173 |
assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
174 |
shows "strip c' = strip c" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
175 |
using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
176 |
by (metis assms(1)) |
45111 | 177 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
178 |
lemma strip_pfp_WN: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
179 |
"\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
180 |
apply(auto simp add: pfp_WN_def prefp_def split: option.splits) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
181 |
by (metis (no_types) strip_lpfpc strip_map2_acom strip_while) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
182 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
183 |
locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
184 |
begin |
45111 | 185 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
186 |
definition AI_WN :: "com \<Rightarrow> 'a st option acom option" where |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
187 |
"AI_WN = pfp_WN (step' \<top>)" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
188 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
189 |
lemma AI_WN_sound: "AI_WN c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
190 |
proof(simp add: CS_def AI_WN_def) |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
191 |
assume 1: "pfp_WN (step' \<top>) c = Some c'" |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
192 |
from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1] |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
193 |
have 2: "step' \<top> c' \<sqsubseteq> c'" . |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
194 |
have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1]) |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
195 |
have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
196 |
proof(rule lfp_lowerbound[OF 3]) |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
197 |
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
198 |
proof(rule step_preserves_le[OF _ _ 3]) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
199 |
show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
200 |
show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2]) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
201 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
202 |
qed |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
203 |
from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
204 |
by (blast intro: mono_rep_c order_trans) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
205 |
qed |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
206 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
207 |
end |
45111 | 208 |
|
209 |
interpretation |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
210 |
Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
211 |
defines AI_ivl' is AI_WN |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
212 |
proof qed |
45111 | 213 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
214 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
215 |
subsubsection "Tests" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
216 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
217 |
definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
218 |
definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)" |
45111 | 219 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
220 |
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
221 |
the loop took to execute. In contrast, @{const AI_ivl} converges in a |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
222 |
constant number of steps: *} |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
223 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
224 |
value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
225 |
value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
226 |
value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
227 |
value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
228 |
value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
229 |
value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
230 |
value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
231 |
value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
45111 | 232 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
233 |
text{* Now all the analyses terminate: *} |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
234 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
235 |
value [code] "show_acom_opt (AI_ivl' test4_ivl)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
236 |
value [code] "show_acom_opt (AI_ivl' test5_ivl)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
237 |
value [code] "show_acom_opt (AI_ivl' test6_ivl)" |
45111 | 238 |
|
239 |
end |