author | traytel |
Wed, 12 Feb 2014 16:35:58 +0100 | |
changeset 55441 | b445c39cc7e9 |
parent 53015 | a1119cf551e8 |
child 55599 | 6535c537b243 |
permissions | -rw-r--r-- |
45111 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
47602 | 3 |
theory Abs_Int3_ITP |
4 |
imports Abs_Int2_ivl_ITP |
|
45111 | 5 |
begin |
6 |
||
7 |
subsection "Widening and Narrowing" |
|
8 |
||
9 |
class WN = SL_top + |
|
10 |
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
|
11 |
assumes widen1: "x \<sqsubseteq> x \<nabla> y" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
12 |
assumes widen2: "y \<sqsubseteq> x \<nabla> y" |
45111 | 13 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65) |
14 |
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y" |
|
15 |
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x" |
|
16 |
||
17 |
||
46249 | 18 |
subsubsection "Intervals" |
19 |
||
45111 | 20 |
instantiation ivl :: WN |
21 |
begin |
|
22 |
||
23 |
definition "widen_ivl ivl1 ivl2 = |
|
24 |
((*if is_empty ivl1 then ivl2 else |
|
25 |
if is_empty ivl2 then ivl1 else*) |
|
26 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow> |
|
27 |
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1) |
|
28 |
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))" |
|
29 |
||
30 |
definition "narrow_ivl ivl1 ivl2 = |
|
31 |
((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*) |
|
32 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow> |
|
33 |
I (if l1 = None then l2 else l1) |
|
34 |
(if h1 = None then h2 else h1))" |
|
35 |
||
36 |
instance |
|
37 |
proof qed |
|
38 |
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits) |
|
39 |
||
40 |
end |
|
41 |
||
46249 | 42 |
|
43 |
subsubsection "Abstract State" |
|
44 |
||
45111 | 45 |
instantiation st :: (WN)WN |
46 |
begin |
|
47 |
||
48 |
definition "widen_st F1 F2 = |
|
49 |
FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))" |
|
50 |
||
51 |
definition "narrow_st F1 F2 = |
|
52 |
FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))" |
|
53 |
||
54 |
instance |
|
55 |
proof |
|
56 |
case goal1 thus ?case |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
57 |
by(simp add: widen_st_def le_st_def lookup_def widen1) |
45111 | 58 |
next |
59 |
case goal2 thus ?case |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
60 |
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
|
61 |
next |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
62 |
case goal3 thus ?case |
45111 | 63 |
by(auto simp: narrow_st_def le_st_def lookup_def narrow1) |
64 |
next |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
65 |
case goal4 thus ?case |
45111 | 66 |
by(auto simp: narrow_st_def le_st_def lookup_def narrow2) |
67 |
qed |
|
68 |
||
69 |
end |
|
70 |
||
46249 | 71 |
|
72 |
subsubsection "Option" |
|
73 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
74 |
instantiation option :: (WN)WN |
45111 | 75 |
begin |
76 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
77 |
fun widen_option where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
78 |
"None \<nabla> x = x" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
79 |
"x \<nabla> None = x" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
80 |
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" |
45111 | 81 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
82 |
fun narrow_option where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
83 |
"None \<triangle> x = None" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
84 |
"x \<triangle> None = None" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
85 |
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
45111 | 86 |
|
87 |
instance |
|
88 |
proof |
|
89 |
case goal1 show ?case |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
90 |
by(induct x y rule: widen_option.induct) (simp_all add: widen1) |
45111 | 91 |
next |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
92 |
case goal2 show ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
93 |
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
|
94 |
next |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
95 |
case goal3 thus ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
96 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
45111 | 97 |
next |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
98 |
case goal4 thus ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
99 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
45111 | 100 |
qed |
101 |
||
102 |
end |
|
103 |
||
46249 | 104 |
|
105 |
subsubsection "Annotated commands" |
|
106 |
||
45111 | 107 |
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
108 |
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | |
|
109 |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
47602
diff
changeset
|
110 |
"map2_acom f (c1;;c2) (c1';;c2') = (map2_acom f c1 c1';; map2_acom f c2 c2')" | |
45111 | 111 |
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) = |
112 |
(IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" | |
|
113 |
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) = |
|
114 |
({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})" |
|
115 |
||
116 |
abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65) |
|
117 |
where "widen_acom == map2_acom (op \<nabla>)" |
|
118 |
||
119 |
abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65) |
|
120 |
where "narrow_acom == map2_acom (op \<triangle>)" |
|
121 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
125 |
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
|
126 |
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
|
127 |
|
45111 | 128 |
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y" |
129 |
by(induct y x rule: le_acom.induct) (simp_all add: narrow1) |
|
130 |
||
131 |
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x" |
|
132 |
by(induct y x rule: le_acom.induct) (simp_all add: narrow2) |
|
133 |
||
134 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
135 |
subsubsection "Post-fixed point computation" |
45111 | 136 |
|
46249 | 137 |
definition iter_widen :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> ('a::WN)acom option" |
138 |
where "iter_widen f = while_option (\<lambda>c. \<not> f c \<sqsubseteq> c) (\<lambda>c. c \<nabla>\<^sub>c f c)" |
|
139 |
||
46251 | 140 |
definition iter_narrow :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a::WN acom option" |
141 |
where "iter_narrow f = while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) (\<lambda>c. c \<triangle>\<^sub>c f c)" |
|
46249 | 142 |
|
46251 | 143 |
definition pfp_wn :: |
144 |
"(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" |
|
145 |
where "pfp_wn f c = (case iter_widen f (\<bottom>\<^sub>c c) of None \<Rightarrow> None |
|
146 |
| Some c' \<Rightarrow> iter_narrow f c')" |
|
45111 | 147 |
|
148 |
lemma strip_map2_acom: |
|
149 |
"strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1" |
|
150 |
by(induct f c1 c2 rule: map2_acom.induct) simp_all |
|
151 |
||
46249 | 152 |
lemma iter_widen_pfp: "iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'" |
153 |
by(auto simp add: iter_widen_def dest: while_option_stop) |
|
154 |
||
155 |
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom" |
|
156 |
assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'" |
|
157 |
shows "strip c' = strip c" |
|
158 |
using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)] |
|
159 |
by (metis assms(1)) |
|
160 |
||
161 |
lemma strip_iter_widen: fixes f :: "'a::WN acom \<Rightarrow> 'a acom" |
|
162 |
assumes "\<forall>c. strip (f c) = strip c" and "iter_widen f c = Some c'" |
|
163 |
shows "strip c' = strip c" |
|
164 |
proof- |
|
165 |
have "\<forall>c. strip(c \<nabla>\<^sub>c f c) = strip c" by (metis assms(1) strip_map2_acom) |
|
166 |
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) |
|
167 |
qed |
|
45111 | 168 |
|
46251 | 169 |
lemma iter_narrow_pfp: assumes "mono f" and "f c0 \<sqsubseteq> c0" |
170 |
and "iter_narrow f c0 = Some c" |
|
171 |
shows "f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0" (is "?P c") |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
172 |
proof- |
46251 | 173 |
{ fix c assume "?P c" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
174 |
note 1 = conjunct1[OF this] and 2 = conjunct2[OF this] |
46251 | 175 |
let ?c' = "c \<triangle>\<^sub>c f c" |
176 |
have "?P ?c'" |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
177 |
proof |
46251 | 178 |
have "f ?c' \<sqsubseteq> f c" by(rule monoD[OF `mono f` narrow2_acom[OF 1]]) |
179 |
also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1_acom[OF 1]) |
|
180 |
finally show "f ?c' \<sqsubseteq> ?c'" . |
|
181 |
have "?c' \<sqsubseteq> c" by (rule narrow2_acom[OF 1]) |
|
182 |
also have "c \<sqsubseteq> c0" by(rule 2) |
|
183 |
finally show "?c' \<sqsubseteq> c0" . |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
184 |
qed |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
185 |
} |
46251 | 186 |
with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]] |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
187 |
assms(2) le_refl |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
188 |
show ?thesis by blast |
45111 | 189 |
qed |
190 |
||
46251 | 191 |
lemma pfp_wn_pfp: |
192 |
"\<lbrakk> mono f; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'" |
|
193 |
unfolding pfp_wn_def |
|
194 |
by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits) |
|
45111 | 195 |
|
46251 | 196 |
lemma strip_pfp_wn: |
197 |
"\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c" |
|
198 |
apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) |
|
55441 | 199 |
by (metis (mono_tags) strip_map2_acom strip_while strip_bot_acom strip_iter_widen) |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
200 |
|
46063 | 201 |
locale Abs_Int2 = Abs_Int1_mono |
202 |
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set" |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
203 |
begin |
45111 | 204 |
|
46251 | 205 |
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where |
206 |
"AI_wn = pfp_wn (step' \<top>)" |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
207 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
208 |
lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c c'" |
46251 | 209 |
proof(simp add: CS_def AI_wn_def) |
210 |
assume 1: "pfp_wn (step' \<top>) c = Some c'" |
|
211 |
from pfp_wn_pfp[OF mono_step'2 1] |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
212 |
have 2: "step' \<top> c' \<sqsubseteq> c'" . |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
213 |
have 3: "strip (\<gamma>\<^sub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1]) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
214 |
have "lfp (step UNIV) c \<le> \<gamma>\<^sub>c (step' \<top> c')" |
45903 | 215 |
proof(rule lfp_lowerbound[simplified,OF 3]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
216 |
show "step UNIV (\<gamma>\<^sub>c (step' \<top> c')) \<le> \<gamma>\<^sub>c (step' \<top> c')" |
46068 | 217 |
proof(rule step_preserves_le[OF _ _]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
218 |
show "UNIV \<subseteq> \<gamma>\<^sub>o \<top>" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
219 |
show "\<gamma>\<^sub>c (step' \<top> c') \<le> \<gamma>\<^sub>c c'" by(rule mono_gamma_c[OF 2]) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
220 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
221 |
qed |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
222 |
from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^sub>c c'" |
46039 | 223 |
by (blast intro: mono_gamma_c order_trans) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
224 |
qed |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
225 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
226 |
end |
45111 | 227 |
|
46063 | 228 |
interpretation Abs_Int2 |
229 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl |
|
46430 | 230 |
and test_num' = in_ivl |
46063 | 231 |
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
46251 | 232 |
defines AI_ivl' is AI_wn |
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46303
diff
changeset
|
233 |
.. |
45111 | 234 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
235 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
236 |
subsubsection "Tests" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
237 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
238 |
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
|
239 |
definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)" |
45111 | 240 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
241 |
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as |
46303 | 242 |
the loop took to execute. In contrast, @{const AI_ivl'} converges in a |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
243 |
constant number of steps: *} |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
244 |
|
46303 | 245 |
value "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))" |
246 |
value "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))" |
|
247 |
value "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))" |
|
248 |
value "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))" |
|
249 |
value "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))" |
|
250 |
value "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
|
251 |
value "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
|
252 |
value "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" |
|
45111 | 253 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
254 |
text{* Now all the analyses terminate: *} |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
255 |
|
46303 | 256 |
value "show_acom_opt (AI_ivl' test4_ivl)" |
257 |
value "show_acom_opt (AI_ivl' test5_ivl)" |
|
258 |
value "show_acom_opt (AI_ivl' test6_ivl)" |
|
45111 | 259 |
|
46249 | 260 |
|
261 |
subsubsection "Termination: Intervals" |
|
262 |
||
263 |
definition m_ivl :: "ivl \<Rightarrow> nat" where |
|
264 |
"m_ivl ivl = (case ivl of I l h \<Rightarrow> |
|
265 |
(case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))" |
|
266 |
||
267 |
lemma m_ivl_height: "m_ivl ivl \<le> 2" |
|
268 |
by(simp add: m_ivl_def split: ivl.split option.split) |
|
269 |
||
270 |
lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y" |
|
271 |
by(auto simp: m_ivl_def le_option_def le_ivl_def |
|
272 |
split: ivl.split option.split if_splits) |
|
273 |
||
46251 | 274 |
lemma m_ivl_widen: |
46249 | 275 |
"~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x" |
276 |
by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def |
|
277 |
split: ivl.splits option.splits if_splits) |
|
278 |
||
279 |
lemma Top_less_ivl: "\<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0" |
|
280 |
by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def |
|
281 |
split: ivl.split option.split if_splits) |
|
282 |
||
283 |
||
46251 | 284 |
definition n_ivl :: "ivl \<Rightarrow> nat" where |
285 |
"n_ivl ivl = 2 - m_ivl ivl" |
|
286 |
||
287 |
lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y" |
|
288 |
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono) |
|
289 |
||
290 |
lemma n_ivl_narrow: |
|
291 |
"~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x" |
|
292 |
by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def |
|
293 |
split: ivl.splits option.splits if_splits) |
|
294 |
||
295 |
||
46249 | 296 |
subsubsection "Termination: Abstract State" |
297 |
||
298 |
definition "m_st m st = (\<Sum>x\<in>set(dom st). m(fun st x))" |
|
299 |
||
300 |
lemma m_st_height: assumes "finite X" and "set (dom S) \<subseteq> X" |
|
301 |
shows "m_st m_ivl S \<le> 2 * card X" |
|
302 |
proof(auto simp: m_st_def) |
|
303 |
have "(\<Sum>x\<in>set(dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set(dom S). 2)" (is "?L \<le> _") |
|
304 |
by(rule setsum_mono)(simp add:m_ivl_height) |
|
305 |
also have "\<dots> \<le> (\<Sum>x\<in>X. 2)" |
|
306 |
by(rule setsum_mono3[OF assms]) simp |
|
307 |
also have "\<dots> = 2 * card X" by(simp add: setsum_constant) |
|
308 |
finally show "?L \<le> \<dots>" . |
|
309 |
qed |
|
310 |
||
311 |
lemma m_st_anti_mono: |
|
312 |
"S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1" |
|
313 |
proof(auto simp: m_st_def le_st_def lookup_def split: if_splits) |
|
314 |
let ?X = "set(dom S1)" let ?Y = "set(dom S2)" |
|
315 |
let ?f = "fun S1" let ?g = "fun S2" |
|
316 |
assume asm: "\<forall>x\<in>?Y. (x \<in> ?X \<longrightarrow> ?f x \<sqsubseteq> ?g x) \<and> (x \<in> ?X \<or> \<top> \<sqsubseteq> ?g x)" |
|
317 |
hence 1: "\<forall>y\<in>?Y\<inter>?X. m_ivl(?g y) \<le> m_ivl(?f y)" by(simp add: m_ivl_anti_mono) |
|
318 |
have 0: "\<forall>x\<in>?Y-?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl) |
|
319 |
have "(\<Sum>y\<in>?Y. m_ivl(?g y)) = (\<Sum>y\<in>(?Y-?X) \<union> (?Y\<inter>?X). m_ivl(?g y))" |
|
320 |
by (metis Un_Diff_Int) |
|
321 |
also have "\<dots> = (\<Sum>y\<in>?Y-?X. m_ivl(?g y)) + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" |
|
322 |
by(subst setsum_Un_disjoint) auto |
|
323 |
also have "(\<Sum>y\<in>?Y-?X. m_ivl(?g y)) = 0" using 0 by simp |
|
324 |
also have "0 + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y)) = (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" by simp |
|
325 |
also have "\<dots> \<le> (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?f y))" |
|
326 |
by(rule setsum_mono)(simp add: 1) |
|
327 |
also have "\<dots> \<le> (\<Sum>y\<in>?X. m_ivl(?f y))" |
|
328 |
by(simp add: setsum_mono3[of "?X" "?Y Int ?X", OF _ Int_lower2]) |
|
329 |
finally show "(\<Sum>y\<in>?Y. m_ivl(?g y)) \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" |
|
330 |
by (metis add_less_cancel_left) |
|
331 |
qed |
|
332 |
||
46251 | 333 |
lemma m_st_widen: |
46249 | 334 |
assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1" |
335 |
proof- |
|
336 |
{ let ?X = "set(dom S1)" let ?Y = "set(dom S2)" |
|
337 |
let ?f = "fun S1" let ?g = "fun S2" |
|
338 |
fix x assume "x \<in> ?X" "\<not> lookup S2 x \<sqsubseteq> ?f x" |
|
339 |
have "(\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x)) < (\<Sum>x\<in>?X. m_ivl(?f x))" (is "?L < ?R") |
|
340 |
proof cases |
|
341 |
assume "x : ?Y" |
|
342 |
have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" |
|
343 |
proof(rule setsum_strict_mono1, simp) |
|
344 |
show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" |
|
345 |
by (metis m_ivl_anti_mono widen1) |
|
346 |
next |
|
347 |
show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)" |
|
348 |
using `x:?X` `x:?Y` `\<not> lookup S2 x \<sqsubseteq> ?f x` |
|
46251 | 349 |
by (metis IntI m_ivl_widen lookup_def) |
46249 | 350 |
qed |
351 |
also have "\<dots> \<le> ?R" by(simp add: setsum_mono3[OF _ Int_lower1]) |
|
352 |
finally show ?thesis . |
|
353 |
next |
|
354 |
assume "x ~: ?Y" |
|
355 |
have "?L \<le> (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" |
|
356 |
proof(rule setsum_mono, simp) |
|
357 |
fix x assume "x:?X \<and> x:?Y" show "m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" |
|
358 |
by (metis m_ivl_anti_mono widen1) |
|
359 |
qed |
|
360 |
also have "\<dots> < m_ivl(?f x) + \<dots>" |
|
46251 | 361 |
using m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`] |
46249 | 362 |
by (metis Nat.le_refl add_strict_increasing gr0I not_less0) |
363 |
also have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))" |
|
364 |
using `x ~: ?Y` by simp |
|
365 |
also have "\<dots> \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" |
|
366 |
by(rule setsum_mono3)(insert `x:?X`, auto) |
|
367 |
finally show ?thesis . |
|
368 |
qed |
|
369 |
} with assms show ?thesis |
|
370 |
by(auto simp: le_st_def widen_st_def m_st_def Int_def) |
|
371 |
qed |
|
372 |
||
46251 | 373 |
definition "n_st m X st = (\<Sum>x\<in>X. m(lookup st x))" |
374 |
||
375 |
lemma n_st_mono: assumes "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" "S1 \<sqsubseteq> S2" |
|
376 |
shows "n_st n_ivl X S1 \<le> n_st n_ivl X S2" |
|
377 |
proof- |
|
378 |
have "(\<Sum>x\<in>X. n_ivl(lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl(lookup S2 x))" |
|
379 |
apply(rule setsum_mono) using assms |
|
380 |
by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits) |
|
381 |
thus ?thesis by(simp add: n_st_def) |
|
382 |
qed |
|
383 |
||
384 |
lemma n_st_narrow: |
|
385 |
assumes "finite X" and "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" |
|
386 |
and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2" |
|
387 |
shows "n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1" |
|
388 |
proof- |
|
389 |
have 1: "\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)" |
|
390 |
using assms(2-4) |
|
391 |
by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2 |
|
392 |
split: if_splits) |
|
393 |
have 2: "\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)" |
|
394 |
using assms(2-5) |
|
395 |
by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow |
|
396 |
split: if_splits) |
|
397 |
have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))" |
|
398 |
apply(rule setsum_strict_mono1[OF `finite X`]) using 1 2 by blast+ |
|
399 |
thus ?thesis by(simp add: n_st_def) |
|
400 |
qed |
|
401 |
||
46249 | 402 |
|
403 |
subsubsection "Termination: Option" |
|
404 |
||
405 |
definition "m_o m n opt = (case opt of None \<Rightarrow> n+1 | Some x \<Rightarrow> m x)" |
|
406 |
||
407 |
lemma m_o_anti_mono: "finite X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> |
|
408 |
m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1" |
|
409 |
apply(induction S1 S2 rule: le_option.induct) |
|
410 |
apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height |
|
411 |
split: option.splits) |
|
412 |
done |
|
413 |
||
46251 | 414 |
lemma m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow> |
46249 | 415 |
m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1" |
46251 | 416 |
by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen |
46249 | 417 |
split: option.split) |
418 |
||
46251 | 419 |
definition "n_o n opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n x + 1)" |
420 |
||
421 |
lemma n_o_mono: "domo S1 \<subseteq> X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> |
|
422 |
n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2" |
|
423 |
apply(induction S1 S2 rule: le_option.induct) |
|
424 |
apply(auto simp: domo_def n_o_def n_st_mono |
|
425 |
split: option.splits) |
|
426 |
done |
|
427 |
||
428 |
lemma n_o_narrow: |
|
429 |
"\<lbrakk> finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<rbrakk> |
|
430 |
\<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1" |
|
431 |
apply(induction S1 S2 rule: narrow_option.induct) |
|
432 |
apply(auto simp: n_o_def domo_def n_st_narrow) |
|
433 |
done |
|
46249 | 434 |
|
435 |
lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2" |
|
436 |
apply(induction S1 S2 rule: widen_option.induct) |
|
437 |
apply (auto simp: domo_def widen_st_def) |
|
438 |
done |
|
439 |
||
46251 | 440 |
lemma domo_narrow_subset: "domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2" |
441 |
apply(induction S1 S2 rule: narrow_option.induct) |
|
442 |
apply (auto simp: domo_def narrow_st_def) |
|
443 |
done |
|
444 |
||
46249 | 445 |
subsubsection "Termination: Commands" |
446 |
||
46251 | 447 |
lemma strip_widen_acom[simp]: |
46249 | 448 |
"strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<nabla>\<^sub>c c') = strip c" |
449 |
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all |
|
450 |
||
46251 | 451 |
lemma strip_narrow_acom[simp]: |
452 |
"strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<triangle>\<^sub>c c') = strip c" |
|
453 |
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all |
|
454 |
||
46249 | 455 |
lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> |
456 |
annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))" |
|
457 |
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) |
|
458 |
(simp_all add: size_annos_same2) |
|
459 |
||
46251 | 460 |
lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> |
461 |
annos(c1 \<triangle>\<^sub>c c2) = map (%(x,y).x\<triangle>y) (zip (annos c1) (annos(c2::'a::WN acom)))" |
|
462 |
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) |
|
463 |
(simp_all add: size_annos_same2) |
|
464 |
||
465 |
lemma widen_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow> |
|
46249 | 466 |
c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X" |
46251 | 467 |
apply(auto simp add: Com_def) |
46249 | 468 |
apply(rename_tac S S' x) |
469 |
apply(erule in_set_zipE) |
|
46251 | 470 |
apply(auto simp: domo_def split: option.splits) |
46249 | 471 |
apply(case_tac S) |
472 |
apply(case_tac S') |
|
473 |
apply simp |
|
474 |
apply fastforce |
|
475 |
apply(case_tac S') |
|
476 |
apply fastforce |
|
477 |
apply (fastforce simp: widen_st_def) |
|
478 |
done |
|
479 |
||
46251 | 480 |
lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow> |
481 |
c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<triangle>\<^sub>c c2) : Com X" |
|
482 |
apply(auto simp add: Com_def) |
|
483 |
apply(rename_tac S S' x) |
|
484 |
apply(erule in_set_zipE) |
|
485 |
apply(auto simp: domo_def split: option.splits) |
|
486 |
apply(case_tac S) |
|
487 |
apply(case_tac S') |
|
488 |
apply simp |
|
489 |
apply fastforce |
|
490 |
apply(case_tac S') |
|
491 |
apply fastforce |
|
492 |
apply (fastforce simp: narrow_st_def) |
|
493 |
done |
|
494 |
||
46249 | 495 |
definition "m_c m c = (let as = annos c in \<Sum>i=0..<size as. m(as!i))" |
496 |
||
497 |
lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'\<Colon>ivl st option acom. |
|
498 |
strip c' = strip c \<and> c : Com X \<and> c' : Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse> |
|
499 |
\<subseteq> measure(m_c(m_o (m_st m_ivl) (2*card(X))))" |
|
500 |
apply(auto simp: m_c_def Let_def Com_def) |
|
501 |
apply(subgoal_tac "length(annos c') = length(annos c)") |
|
502 |
prefer 2 apply (simp add: size_annos_same2) |
|
503 |
apply (auto) |
|
504 |
apply(rule setsum_strict_mono1) |
|
505 |
apply simp |
|
506 |
apply (clarsimp) |
|
507 |
apply(erule m_o_anti_mono) |
|
508 |
apply(rule subset_trans[OF domo_widen_subset]) |
|
46251 | 509 |
apply fastforce |
46249 | 510 |
apply(rule widen1) |
511 |
apply(auto simp: le_iff_le_annos listrel_iff_nth) |
|
512 |
apply(rule_tac x=n in bexI) |
|
513 |
prefer 2 apply simp |
|
46251 | 514 |
apply(erule m_o_widen) |
515 |
apply (simp)+ |
|
516 |
done |
|
517 |
||
518 |
lemma measure_n_c: "finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') |c c'. |
|
519 |
strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse> |
|
520 |
\<subseteq> measure(m_c(n_o (n_st n_ivl X)))" |
|
521 |
apply(auto simp: m_c_def Let_def Com_def) |
|
522 |
apply(subgoal_tac "length(annos c') = length(annos c)") |
|
523 |
prefer 2 apply (simp add: size_annos_same2) |
|
524 |
apply (auto) |
|
525 |
apply(rule setsum_strict_mono1) |
|
526 |
apply simp |
|
527 |
apply (clarsimp) |
|
528 |
apply(rule n_o_mono) |
|
529 |
using domo_narrow_subset apply fastforce |
|
530 |
apply fastforce |
|
531 |
apply(rule narrow2) |
|
532 |
apply(fastforce simp: le_iff_le_annos listrel_iff_nth) |
|
533 |
apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom) |
|
534 |
apply(rule_tac x=n in bexI) |
|
535 |
prefer 2 apply simp |
|
536 |
apply(erule n_o_narrow) |
|
46249 | 537 |
apply (simp)+ |
538 |
done |
|
539 |
||
540 |
||
541 |
subsubsection "Termination: Post-Fixed Point Iterations" |
|
542 |
||
543 |
lemma iter_widen_termination: |
|
544 |
fixes c0 :: "'a::WN acom" |
|
545 |
assumes P_f: "\<And>c. P c \<Longrightarrow> P(f c)" |
|
546 |
assumes P_widen: "\<And>c c'. P c \<Longrightarrow> P c' \<Longrightarrow> P(c \<nabla>\<^sub>c c')" |
|
547 |
and "wf({(c::'a acom,c \<nabla>\<^sub>c c')|c c'. P c \<and> P c' \<and> ~ c' \<sqsubseteq> c}^-1)" |
|
548 |
and "P c0" and "c0 \<sqsubseteq> f c0" shows "EX c. iter_widen f c0 = Some c" |
|
549 |
proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"]) |
|
550 |
show "wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}" |
|
551 |
apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f) |
|
552 |
next |
|
553 |
show "P c0" by(rule `P c0`) |
|
554 |
next |
|
555 |
fix c assume "P c" thus "P (c \<nabla>\<^sub>c f c)" by(simp add: P_f P_widen) |
|
556 |
qed |
|
557 |
||
46251 | 558 |
lemma iter_narrow_termination: |
559 |
assumes P_f: "\<And>c. P c \<Longrightarrow> P(c \<triangle>\<^sub>c f c)" |
|
560 |
and wf: "wf({(c, c \<triangle>\<^sub>c f c)|c c'. P c \<and> ~ c \<sqsubseteq> c \<triangle>\<^sub>c f c}^-1)" |
|
561 |
and "P c0" shows "EX c. iter_narrow f c0 = Some c" |
|
562 |
proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"]) |
|
563 |
show "wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}" |
|
564 |
apply(rule wf_subset[OF wf]) by(blast intro: P_f) |
|
565 |
next |
|
566 |
show "P c0" by(rule `P c0`) |
|
567 |
next |
|
568 |
fix c assume "P c" thus "P (c \<triangle>\<^sub>c f c)" by(simp add: P_f) |
|
569 |
qed |
|
570 |
||
571 |
lemma iter_winden_step_ivl_termination: |
|
572 |
"EX c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c" |
|
46249 | 573 |
apply(rule iter_widen_termination[where |
574 |
P = "%c. strip c = c0 \<and> c : Com(vars c0)"]) |
|
46251 | 575 |
apply (simp_all add: step'_Com bot_acom) |
46249 | 576 |
apply(rule wf_subset) |
577 |
apply(rule wf_measure) |
|
578 |
apply(rule subset_trans) |
|
579 |
prefer 2 |
|
580 |
apply(rule measure_m_c[where X = "vars c0", OF finite_cvars]) |
|
581 |
apply blast |
|
582 |
done |
|
583 |
||
46251 | 584 |
lemma iter_narrow_step_ivl_termination: |
585 |
"c0 \<in> Com (vars(strip c0)) \<Longrightarrow> step_ivl \<top> c0 \<sqsubseteq> c0 \<Longrightarrow> |
|
586 |
EX c. iter_narrow (step_ivl \<top>) c0 = Some c" |
|
587 |
apply(rule iter_narrow_termination[where |
|
588 |
P = "%c. strip c = strip c0 \<and> c : Com(vars(strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c"]) |
|
589 |
apply (simp_all add: step'_Com) |
|
590 |
apply(clarify) |
|
591 |
apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom]) |
|
592 |
apply assumption |
|
593 |
apply(rule wf_subset) |
|
594 |
apply(rule wf_measure) |
|
595 |
apply(rule subset_trans) |
|
596 |
prefer 2 |
|
597 |
apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars]) |
|
598 |
apply auto |
|
599 |
by (metis bot_least domo_Top order_refl step'_Com strip_step') |
|
600 |
||
601 |
(* FIXME: simplify type system: Combine Com(X) and vars <= X?? *) |
|
602 |
lemma while_Com: |
|
603 |
fixes c :: "'a st option acom" |
|
604 |
assumes "while_option P f c = Some c'" |
|
605 |
and "!!c. strip(f c) = strip c" |
|
606 |
and "\<forall>c::'a st option acom. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)" |
|
607 |
and "c : Com(X)" and "vars(strip c) \<subseteq> X" shows "c' : Com(X)" |
|
608 |
using while_option_rule[where P = "\<lambda>c'. c' : Com(X) \<and> vars(strip c') \<subseteq> X", OF _ assms(1)] |
|
609 |
by(simp add: assms(2-)) |
|
610 |
||
611 |
lemma iter_widen_Com: fixes f :: "'a::WN st option acom \<Rightarrow> 'a st option acom" |
|
612 |
assumes "iter_widen f c = Some c'" |
|
613 |
and "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)" |
|
614 |
and "!!c. strip(f c) = strip c" |
|
615 |
and "c : Com(X)" and "vars (strip c) \<subseteq> X" shows "c' : Com(X)" |
|
616 |
proof- |
|
617 |
have "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c : Com(X)" |
|
618 |
by (metis (full_types) widen_acom_Com assms(2,3)) |
|
619 |
from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)] |
|
620 |
show ?thesis using assms(3) by(simp) |
|
621 |
qed |
|
622 |
||
46387 | 623 |
|
624 |
context Abs_Int2 |
|
625 |
begin |
|
626 |
||
46251 | 627 |
lemma iter_widen_step'_Com: |
628 |
"iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X) |
|
629 |
\<Longrightarrow> c' : Com(X)" |
|
630 |
apply(subgoal_tac "strip c'= strip c") |
|
631 |
prefer 2 apply (metis strip_iter_widen strip_step') |
|
632 |
apply(drule iter_widen_Com) |
|
633 |
prefer 3 apply assumption |
|
634 |
prefer 3 apply assumption |
|
635 |
apply (auto simp: step'_Com) |
|
636 |
done |
|
637 |
||
46387 | 638 |
end |
639 |
||
640 |
theorem AI_ivl'_termination: |
|
641 |
"EX c'. AI_ivl' c = Some c'" |
|
46251 | 642 |
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split) |
643 |
apply(rule iter_narrow_step_ivl_termination) |
|
644 |
apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step') |
|
645 |
apply(erule iter_widen_pfp) |
|
646 |
done |
|
647 |
||
45111 | 648 |
end |
46251 | 649 |
|
650 |
||
651 |
(* interesting(?) relic |
|
652 |
lemma widen_assoc: |
|
653 |
"~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)" |
|
654 |
apply(cases x) |
|
655 |
apply(cases y) |
|
656 |
apply(cases z) |
|
657 |
apply(rename_tac x1 x2 y1 y2 z1 z2) |
|
658 |
apply(simp add: le_ivl_def) |
|
659 |
apply(case_tac x1) |
|
660 |
apply(case_tac x2) |
|
661 |
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) |
|
662 |
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) |
|
663 |
apply(case_tac x2) |
|
664 |
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) |
|
665 |
apply(case_tac y1) |
|
666 |
apply(case_tac y2) |
|
667 |
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) |
|
668 |
apply(case_tac z1) |
|
669 |
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] |
|
670 |
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] |
|
671 |
apply(case_tac y2) |
|
672 |
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] |
|
673 |
apply(case_tac z1) |
|
674 |
apply(auto simp add:le_option_def widen_ivl_def split: if_splits ivl.splits option.splits)[1] |
|
675 |
apply(case_tac z2) |
|
676 |
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1] |
|
677 |
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1] |
|
678 |
done |
|
679 |
||
680 |
lemma widen_step_trans: |
|
681 |
"~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x" |
|
682 |
by (metis widen_assoc preord_class.le_trans widen1) |
|
683 |
*) |