author | nipkow |
Wed, 06 Mar 2013 16:10:56 +0100 | |
changeset 51359 | 00b45c7e831f |
parent 51245 | 311fe56541ea |
child 51372 | d315e9a9ee72 |
permissions | -rw-r--r-- |
47613 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_Int3 |
|
4 |
imports Abs_Int2_ivl |
|
5 |
begin |
|
6 |
||
7 |
subsubsection "Welltypedness" |
|
8 |
||
49396 | 9 |
class Lc = |
10 |
fixes Lc :: "com \<Rightarrow> 'a set" |
|
47613 | 11 |
|
49396 | 12 |
instantiation st :: (type)Lc |
47613 | 13 |
begin |
14 |
||
49396 | 15 |
definition Lc_st :: "com \<Rightarrow> 'a st set" where |
16 |
"Lc_st c = L (vars c)" |
|
47613 | 17 |
|
18 |
instance .. |
|
19 |
||
20 |
end |
|
21 |
||
49396 | 22 |
instantiation acom :: (Lc)Lc |
47613 | 23 |
begin |
24 |
||
49396 | 25 |
definition Lc_acom :: "com \<Rightarrow> 'a acom set" where |
26 |
"Lc c = {C. strip C = c \<and> (\<forall>a\<in>set(annos C). a \<in> Lc c)}" |
|
47613 | 27 |
|
28 |
instance .. |
|
29 |
||
30 |
end |
|
31 |
||
49396 | 32 |
instantiation option :: (Lc)Lc |
47613 | 33 |
begin |
34 |
||
49396 | 35 |
definition Lc_option :: "com \<Rightarrow> 'a option set" where |
36 |
"Lc c = {None} \<union> Some ` Lc c" |
|
37 |
||
38 |
lemma Lc_option_simps[simp]: "None \<in> Lc c" "(Some x \<in> Lc c) = (x \<in> Lc c)" |
|
39 |
by(auto simp: Lc_option_def) |
|
47613 | 40 |
|
41 |
instance .. |
|
42 |
||
43 |
end |
|
44 |
||
49396 | 45 |
lemma Lc_option_iff_wt[simp]: fixes a :: "_ st option" |
46 |
shows "(a \<in> Lc c) = (a \<in> L (vars c))" |
|
47 |
by(auto simp add: L_option_def Lc_st_def split: option.splits) |
|
47613 | 48 |
|
49 |
||
50 |
context Abs_Int1 |
|
51 |
begin |
|
52 |
||
49396 | 53 |
lemma step'_in_Lc: "C \<in> Lc c \<Longrightarrow> S \<in> Lc c \<Longrightarrow> step' S C \<in> Lc c" |
54 |
apply(auto simp add: Lc_acom_def) |
|
55 |
by(metis step'_in_L[simplified L_acom_def mem_Collect_eq] order_refl) |
|
47613 | 56 |
|
57 |
end |
|
58 |
||
59 |
||
60 |
subsection "Widening and Narrowing" |
|
61 |
||
62 |
class widen = |
|
63 |
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65) |
|
64 |
||
65 |
class narrow = |
|
66 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65) |
|
67 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
68 |
class WN = widen + narrow + order + |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
69 |
assumes widen1: "x \<le> x \<nabla> y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
70 |
assumes widen2: "y \<le> x \<nabla> y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
71 |
assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
72 |
assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x" |
47613 | 73 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
74 |
class WN_Lc = widen + narrow + order + Lc + |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
75 |
assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<le> x \<nabla> y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
76 |
assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<le> x \<nabla> y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
77 |
assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
78 |
assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x" |
49396 | 79 |
assumes Lc_widen[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<nabla> y \<in> Lc c" |
80 |
assumes Lc_narrow[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<triangle> y \<in> Lc c" |
|
47613 | 81 |
|
82 |
||
83 |
instantiation ivl :: WN |
|
84 |
begin |
|
85 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
86 |
definition "widen_rep p1 p2 = |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
87 |
(if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
88 |
let (l1,h1) = p1; (l2,h2) = p2 |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
89 |
in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
90 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
91 |
lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
92 |
by(auto simp: widen_rep_def eq_ivl_iff) |
47613 | 93 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
94 |
definition "narrow_rep p1 p2 = |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
95 |
(if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
96 |
let (l1,h1) = p1; (l2,h2) = p2 |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
97 |
in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
98 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
99 |
lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
100 |
by(auto simp: narrow_rep_def eq_ivl_iff) |
47613 | 101 |
|
102 |
instance |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
103 |
proof |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
104 |
qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def split: if_splits extended.splits)+ |
47613 | 105 |
|
106 |
end |
|
107 |
||
108 |
||
49396 | 109 |
instantiation st :: (WN)WN_Lc |
47613 | 110 |
begin |
111 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
112 |
definition "widen_st F1 F2 = St (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)" |
47613 | 113 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
114 |
definition "narrow_st F1 F2 = St (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)" |
47613 | 115 |
|
116 |
instance |
|
117 |
proof |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
118 |
case goal1 thus ?case by(simp add: widen_st_def less_eq_st_def WN_class.widen1) |
47613 | 119 |
next |
120 |
case goal2 thus ?case |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
121 |
by(simp add: widen_st_def less_eq_st_def WN_class.widen2 Lc_st_def L_st_def) |
47613 | 122 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
123 |
case goal3 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow1) |
47613 | 124 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
125 |
case goal4 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow2) |
47613 | 126 |
next |
49396 | 127 |
case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def) |
47613 | 128 |
next |
49396 | 129 |
case goal6 thus ?case by(auto simp: narrow_st_def Lc_st_def L_st_def) |
47613 | 130 |
qed |
131 |
||
132 |
end |
|
133 |
||
134 |
||
49396 | 135 |
instantiation option :: (WN_Lc)WN_Lc |
47613 | 136 |
begin |
137 |
||
138 |
fun widen_option where |
|
139 |
"None \<nabla> x = x" | |
|
140 |
"x \<nabla> None = x" | |
|
141 |
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" |
|
142 |
||
143 |
fun narrow_option where |
|
144 |
"None \<triangle> x = None" | |
|
145 |
"x \<triangle> None = None" | |
|
146 |
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
|
147 |
||
148 |
instance |
|
149 |
proof |
|
150 |
case goal1 thus ?case |
|
151 |
by(induct x y rule: widen_option.induct)(simp_all add: widen1) |
|
152 |
next |
|
153 |
case goal2 thus ?case |
|
154 |
by(induct x y rule: widen_option.induct)(simp_all add: widen2) |
|
155 |
next |
|
156 |
case goal3 thus ?case |
|
157 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
|
158 |
next |
|
159 |
case goal4 thus ?case |
|
160 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
|
161 |
next |
|
162 |
case goal5 thus ?case |
|
49396 | 163 |
by(induction x y rule: widen_option.induct)(auto simp: Lc_st_def) |
47613 | 164 |
next |
165 |
case goal6 thus ?case |
|
49396 | 166 |
by(induction x y rule: narrow_option.induct)(auto simp: Lc_st_def) |
47613 | 167 |
qed |
168 |
||
169 |
end |
|
170 |
||
171 |
||
172 |
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
|
173 |
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" | |
|
174 |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" | |
|
175 |
"map2_acom f (C1;C2) (D1;D2) = (map2_acom f C1 D1; map2_acom f C2 D2)" | |
|
49095 | 176 |
"map2_acom f (IF b THEN {p1} C1 ELSE {p2} C2 {a1}) (IF b' THEN {q1} D1 ELSE {q2} D2 {a2}) = |
177 |
(IF b THEN {f p1 q1} map2_acom f C1 D1 ELSE {f p2 q2} map2_acom f C2 D2 {f a1 a2})" | |
|
178 |
"map2_acom f ({a1} WHILE b DO {p} C {a2}) ({a3} WHILE b' DO {p'} C' {a4}) = |
|
179 |
({f a1 a3} WHILE b DO {f p p'} map2_acom f C C' {f a2 a4})" |
|
47613 | 180 |
|
49548 | 181 |
|
182 |
instantiation acom :: (widen)widen |
|
183 |
begin |
|
184 |
definition "widen_acom = map2_acom (op \<nabla>)" |
|
185 |
instance .. |
|
186 |
end |
|
187 |
||
188 |
instantiation acom :: (narrow)narrow |
|
189 |
begin |
|
190 |
definition "narrow_acom = map2_acom (op \<triangle>)" |
|
191 |
instance .. |
|
192 |
end |
|
193 |
||
49396 | 194 |
instantiation acom :: (WN_Lc)WN_Lc |
47613 | 195 |
begin |
196 |
||
49548 | 197 |
lemma widen_acom1: fixes C1 :: "'a acom" shows |
198 |
"\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk> |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
199 |
\<Longrightarrow> C1 \<le> C1 \<nabla> C2" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
200 |
by(induct C1 C2 rule: less_eq_acom.induct) |
49396 | 201 |
(auto simp: widen_acom_def widen1 Lc_acom_def) |
47613 | 202 |
|
49548 | 203 |
lemma widen_acom2: fixes C1 :: "'a acom" shows |
204 |
"\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk> |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
205 |
\<Longrightarrow> C2 \<le> C1 \<nabla> C2" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
206 |
by(induct C1 C2 rule: less_eq_acom.induct) |
49396 | 207 |
(auto simp: widen_acom_def widen2 Lc_acom_def) |
47613 | 208 |
|
209 |
lemma strip_map2_acom[simp]: |
|
210 |
"strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1" |
|
211 |
by(induct f C1 C2 rule: map2_acom.induct) simp_all |
|
212 |
||
213 |
lemma strip_widen_acom[simp]: |
|
214 |
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1" |
|
49548 | 215 |
by(simp add: widen_acom_def) |
47613 | 216 |
|
217 |
lemma strip_narrow_acom[simp]: |
|
218 |
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1" |
|
49548 | 219 |
by(simp add: narrow_acom_def) |
47613 | 220 |
|
221 |
lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow> |
|
222 |
annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))" |
|
223 |
by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2) |
|
224 |
||
225 |
instance |
|
226 |
proof |
|
49396 | 227 |
case goal1 thus ?case by(auto simp: Lc_acom_def widen_acom1) |
47613 | 228 |
next |
49396 | 229 |
case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2) |
47613 | 230 |
next |
231 |
case goal3 thus ?case |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
232 |
by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1) |
47613 | 233 |
next |
234 |
case goal4 thus ?case |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
235 |
by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2) |
47613 | 236 |
next |
237 |
case goal5 thus ?case |
|
49396 | 238 |
by(auto simp: Lc_acom_def widen_acom_def split_conv elim!: in_set_zipE) |
47613 | 239 |
next |
240 |
case goal6 thus ?case |
|
49396 | 241 |
by(auto simp: Lc_acom_def narrow_acom_def split_conv elim!: in_set_zipE) |
47613 | 242 |
qed |
243 |
||
244 |
end |
|
245 |
||
49396 | 246 |
lemma widen_o_in_L[simp]: fixes x1 x2 :: "_ st option" |
247 |
shows "x1 \<in> L X \<Longrightarrow> x2 \<in> L X \<Longrightarrow> x1 \<nabla> x2 \<in> L X" |
|
47613 | 248 |
by(induction x1 x2 rule: widen_option.induct) |
49396 | 249 |
(simp_all add: widen_st_def L_st_def) |
47613 | 250 |
|
49396 | 251 |
lemma narrow_o_in_L[simp]: fixes x1 x2 :: "_ st option" |
252 |
shows "x1 \<in> L X \<Longrightarrow> x2 \<in> L X \<Longrightarrow> x1 \<triangle> x2 \<in> L X" |
|
47613 | 253 |
by(induction x1 x2 rule: narrow_option.induct) |
49396 | 254 |
(simp_all add: narrow_st_def L_st_def) |
47613 | 255 |
|
49396 | 256 |
lemma widen_c_in_L: fixes C1 C2 :: "_ st option acom" |
257 |
shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<nabla> C2 \<in> L X" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
258 |
by(induction C1 C2 rule: less_eq_acom.induct) |
47613 | 259 |
(auto simp: widen_acom_def) |
260 |
||
49396 | 261 |
lemma narrow_c_in_L: fixes C1 C2 :: "_ st option acom" |
262 |
shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<triangle> C2 \<in> L X" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
263 |
by(induction C1 C2 rule: less_eq_acom.induct) |
47613 | 264 |
(auto simp: narrow_acom_def) |
265 |
||
49396 | 266 |
lemma bot_in_Lc[simp]: "bot c \<in> Lc c" |
267 |
by(simp add: Lc_acom_def bot_def) |
|
47613 | 268 |
|
269 |
||
270 |
subsubsection "Post-fixed point computation" |
|
271 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
272 |
definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
273 |
where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)" |
47613 | 274 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
275 |
definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
276 |
where "iter_narrow f = while_option (\<lambda>x. \<not> x \<le> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)" |
47613 | 277 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
278 |
definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" |
49548 | 279 |
where "pfp_wn f x = |
49576 | 280 |
(case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)" |
47613 | 281 |
|
282 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
283 |
lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p" |
47613 | 284 |
by(auto simp add: iter_widen_def dest: while_option_stop) |
285 |
||
286 |
lemma iter_widen_inv: |
|
287 |
assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x" |
|
288 |
and "iter_widen f x = Some y" shows "P y" |
|
289 |
using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]] |
|
290 |
by (blast intro: assms(1-3)) |
|
291 |
||
292 |
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom" |
|
293 |
assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'" |
|
294 |
shows "strip C' = strip C" |
|
295 |
using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)] |
|
296 |
by (metis assms(1)) |
|
297 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
298 |
lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom" |
47613 | 299 |
assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'" |
300 |
shows "strip C' = strip C" |
|
301 |
proof- |
|
302 |
have "\<forall>C. strip(C \<nabla> f C) = strip C" |
|
303 |
by (metis assms(1) strip_map2_acom widen_acom_def) |
|
304 |
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) |
|
305 |
qed |
|
306 |
||
307 |
lemma iter_narrow_pfp: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
308 |
assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2" |
49576 | 309 |
and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
310 |
and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
311 |
shows "P p \<and> f p \<le> p" |
47613 | 312 |
proof- |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
313 |
let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0" |
49576 | 314 |
{ fix p assume "?Q p" |
47613 | 315 |
note P = conjunct1[OF this] and 12 = conjunct2[OF this] |
316 |
note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12] |
|
49576 | 317 |
let ?p' = "p \<triangle> f p" |
318 |
have "?Q ?p'" |
|
47613 | 319 |
proof auto |
49576 | 320 |
show "P ?p'" by (blast intro: P Pinv) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
321 |
have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)` P narrow2[OF 1]]) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
322 |
also have "\<dots> \<le> ?p'" by(rule narrow1[OF 1]) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
323 |
finally show "f ?p' \<le> ?p'" . |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
324 |
have "?p' \<le> p" by (rule narrow2[OF 1]) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
325 |
also have "p \<le> p0" by(rule 2) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
326 |
finally show "?p' \<le> p0" . |
47613 | 327 |
qed |
328 |
} |
|
329 |
thus ?thesis |
|
330 |
using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]] |
|
331 |
by (blast intro: assms(4,5) le_refl) |
|
332 |
qed |
|
333 |
||
334 |
lemma pfp_wn_pfp: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
335 |
assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2" |
49548 | 336 |
and Pinv: "P x" "!!x. P x \<Longrightarrow> P(f x)" |
337 |
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" |
|
338 |
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
339 |
and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p" |
47613 | 340 |
proof- |
49576 | 341 |
from pfp_wn obtain p0 |
342 |
where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p" |
|
47613 | 343 |
by(auto simp: pfp_wn_def split: option.splits) |
49576 | 344 |
have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3)) |
47613 | 345 |
thus ?thesis |
346 |
by - (assumption | |
|
347 |
rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+ |
|
348 |
qed |
|
349 |
||
350 |
lemma strip_pfp_wn: |
|
49548 | 351 |
"\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C" |
47613 | 352 |
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) |
49548 | 353 |
(metis (no_types) narrow_acom_def strip_iter_widen strip_map2_acom strip_while) |
47613 | 354 |
|
355 |
||
356 |
locale Abs_Int2 = Abs_Int1_mono |
|
49396 | 357 |
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set" |
47613 | 358 |
begin |
359 |
||
360 |
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
361 |
"AI_wn c = pfp_wn (step' (Top(vars c))) (bot c)" |
47613 | 362 |
|
363 |
lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C" |
|
364 |
proof(simp add: CS_def AI_wn_def) |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
365 |
assume 1: "pfp_wn (step' (Top(vars c))) (bot c) = Some C" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
366 |
have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<le> C" |
49548 | 367 |
by(rule pfp_wn_pfp[where x="bot c"]) |
49396 | 368 |
(simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
369 |
have pfp: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C" |
50986 | 370 |
proof(rule order_trans) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
371 |
show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (Top(vars c)) C)" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
372 |
by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] Top_in_L]) |
50986 | 373 |
show "... \<le> \<gamma>\<^isub>c C" |
374 |
by(rule mono_gamma_c[OF conjunct2[OF 2]]) |
|
47613 | 375 |
qed |
50986 | 376 |
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1]) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
377 |
have "lfp c (step (\<gamma>\<^isub>o (Top(vars c)))) \<le> \<gamma>\<^isub>c C" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
378 |
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 pfp]) |
50986 | 379 |
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp |
47613 | 380 |
qed |
381 |
||
382 |
end |
|
383 |
||
384 |
interpretation Abs_Int2 |
|
51245 | 385 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 386 |
and test_num' = in_ivl |
387 |
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
|
388 |
defines AI_ivl' is AI_wn |
|
389 |
.. |
|
390 |
||
391 |
||
392 |
subsubsection "Tests" |
|
393 |
||
394 |
definition "step_up_ivl n = |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
395 |
((\<lambda>C. C \<nabla> step_ivl (Top(vars(strip C))) C)^^n)" |
47613 | 396 |
definition "step_down_ivl n = |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
397 |
((\<lambda>C. C \<triangle> step_ivl (Top(vars(strip C))) C)^^n)" |
47613 | 398 |
|
399 |
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as |
|
400 |
the loop took to execute. In contrast, @{const AI_ivl'} converges in a |
|
401 |
constant number of steps: *} |
|
402 |
||
403 |
value "show_acom (step_up_ivl 1 (bot test3_ivl))" |
|
404 |
value "show_acom (step_up_ivl 2 (bot test3_ivl))" |
|
405 |
value "show_acom (step_up_ivl 3 (bot test3_ivl))" |
|
406 |
value "show_acom (step_up_ivl 4 (bot test3_ivl))" |
|
407 |
value "show_acom (step_up_ivl 5 (bot test3_ivl))" |
|
49188 | 408 |
value "show_acom (step_up_ivl 6 (bot test3_ivl))" |
409 |
value "show_acom (step_up_ivl 7 (bot test3_ivl))" |
|
410 |
value "show_acom (step_up_ivl 8 (bot test3_ivl))" |
|
411 |
value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))" |
|
412 |
value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))" |
|
413 |
value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))" |
|
414 |
value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))" |
|
51036 | 415 |
value "show_acom_opt (AI_ivl' test3_ivl)" |
47613 | 416 |
|
417 |
||
418 |
text{* Now all the analyses terminate: *} |
|
419 |
||
51036 | 420 |
value "show_acom_opt (AI_ivl' test4_ivl)" |
421 |
value "show_acom_opt (AI_ivl' test5_ivl)" |
|
422 |
value "show_acom_opt (AI_ivl' test6_ivl)" |
|
47613 | 423 |
|
424 |
||
425 |
subsubsection "Generic Termination Proof" |
|
426 |
||
49547 | 427 |
locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" + |
47613 | 428 |
fixes n :: "'av \<Rightarrow> nat" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
429 |
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
430 |
assumes n_mono: "x \<le> y \<Longrightarrow> n x \<le> n y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
431 |
assumes n_narrow: "y \<le> x \<Longrightarrow> ~ x \<le> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x" |
47613 | 432 |
|
433 |
begin |
|
434 |
||
49547 | 435 |
lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow> |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
436 |
~ S2 \<le> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
437 |
proof(auto simp add: less_eq_st_def m_s_def L_st_def widen_st_def) |
47613 | 438 |
assume "finite(dom S1)" |
439 |
have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)" |
|
49547 | 440 |
by (metis m1 WN_class.widen1) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
441 |
fix x assume "x \<in> dom S1" "\<not> fun S2 x \<le> fun S1 x" |
47613 | 442 |
hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)" |
443 |
using m_widen by blast |
|
444 |
from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2] |
|
445 |
show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" . |
|
446 |
qed |
|
447 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
448 |
lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow> |
49547 | 449 |
m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
450 |
by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen split: option.split) |
47613 | 451 |
|
49547 | 452 |
lemma m_c_widen: |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
453 |
"C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1" |
49547 | 454 |
apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def) |
455 |
apply(subgoal_tac "length(annos C2) = length(annos C1)") |
|
456 |
prefer 2 apply (simp add: size_annos_same2) |
|
457 |
apply (auto) |
|
458 |
apply(rule setsum_strict_mono_ex1) |
|
459 |
apply simp |
|
460 |
apply (clarsimp) |
|
461 |
apply(simp add: m_o1 finite_cvars widen1[where c = "strip C2"]) |
|
462 |
apply(auto simp: le_iff_le_annos listrel_iff_nth) |
|
463 |
apply(rule_tac x=i in bexI) |
|
464 |
prefer 2 apply simp |
|
465 |
apply(rule m_o_widen) |
|
466 |
apply (simp add: finite_cvars)+ |
|
467 |
done |
|
468 |
||
469 |
||
49576 | 470 |
definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where |
471 |
"n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))" |
|
49547 | 472 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
473 |
lemma n_s_mono: assumes "S1 \<le> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2" |
47613 | 474 |
proof- |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
475 |
from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<le> fun S2 x" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
476 |
by(simp_all add: less_eq_st_def) |
47613 | 477 |
have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
478 |
by(rule setsum_mono)(simp add: less_eq_st_def n_mono) |
49547 | 479 |
thus ?thesis by(simp add: n_s_def) |
47613 | 480 |
qed |
481 |
||
49547 | 482 |
lemma n_s_narrow: |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
483 |
assumes "finite(dom S1)" and "S2 \<le> S1" "\<not> S1 \<le> S1 \<triangle> S2" |
49576 | 484 |
shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1" |
47613 | 485 |
proof- |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
486 |
from `S2\<le>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<le> fun S1 x" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
487 |
by(simp_all add: less_eq_st_def) |
47613 | 488 |
have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
489 |
by(auto simp: less_eq_st_def narrow_st_def n_mono WN_class.narrow2) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
490 |
have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<le> S1 \<triangle> S2` |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
491 |
by(force simp: less_eq_st_def narrow_st_def intro: n_narrow) |
47613 | 492 |
have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))" |
493 |
apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+ |
|
494 |
moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def) |
|
49547 | 495 |
ultimately show ?thesis by(simp add: n_s_def) |
47613 | 496 |
qed |
497 |
||
498 |
||
49576 | 499 |
definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where |
500 |
"n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)" |
|
47613 | 501 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
502 |
lemma n_o_mono: "S1 \<le> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
503 |
by(induction S1 S2 rule: less_eq_option.induct)(auto simp: n_o_def n_s_mono) |
47613 | 504 |
|
505 |
lemma n_o_narrow: |
|
49396 | 506 |
"S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
507 |
\<Longrightarrow> S2 \<le> S1 \<Longrightarrow> \<not> S1 \<le> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1" |
47613 | 508 |
apply(induction S1 S2 rule: narrow_option.induct) |
49547 | 509 |
apply(auto simp: n_o_def L_st_def n_s_narrow) |
47613 | 510 |
done |
511 |
||
49576 | 512 |
|
513 |
definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^isub>c") where |
|
514 |
"n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))" |
|
47613 | 515 |
|
49396 | 516 |
lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
517 |
C2 \<le> C1 \<Longrightarrow> \<not> C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1" |
49396 | 518 |
apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def) |
47613 | 519 |
apply(subgoal_tac "length(annos C2) = length(annos C1)") |
520 |
prefer 2 apply (simp add: size_annos_same2) |
|
521 |
apply (auto) |
|
522 |
apply(rule setsum_strict_mono_ex1) |
|
523 |
apply simp |
|
524 |
apply (clarsimp) |
|
525 |
apply(rule n_o_mono) |
|
526 |
apply(rule narrow2) |
|
527 |
apply(fastforce simp: le_iff_le_annos listrel_iff_nth) |
|
49496 | 528 |
apply(auto simp: le_iff_le_annos listrel_iff_nth) |
47613 | 529 |
apply(rule_tac x=i in bexI) |
530 |
prefer 2 apply simp |
|
531 |
apply(rule n_o_narrow[where X = "vars(strip C1)"]) |
|
532 |
apply (simp add: finite_cvars)+ |
|
533 |
done |
|
534 |
||
535 |
end |
|
536 |
||
537 |
||
538 |
lemma iter_widen_termination: |
|
49396 | 539 |
fixes m :: "'a::WN_Lc \<Rightarrow> nat" |
47613 | 540 |
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)" |
541 |
and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
542 |
and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1" |
47613 | 543 |
and "P C" shows "EX C'. iter_widen f C = Some C'" |
49547 | 544 |
proof(simp add: iter_widen_def, |
545 |
rule measure_while_option_Some[where P = P and f=m]) |
|
47613 | 546 |
show "P C" by(rule `P C`) |
547 |
next |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
548 |
fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C" |
49547 | 549 |
by(simp add: P_f P_widen m_widen) |
47613 | 550 |
qed |
49496 | 551 |
|
47613 | 552 |
lemma iter_narrow_termination: |
49396 | 553 |
fixes n :: "'a::WN_Lc \<Rightarrow> nat" |
47613 | 554 |
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)" |
555 |
and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)" |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
556 |
and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
557 |
and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> ~ C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
558 |
and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'" |
49547 | 559 |
proof(simp add: iter_narrow_def, |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
560 |
rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"]) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
561 |
show "P C \<and> f C \<le> C" using init by blast |
47613 | 562 |
next |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
563 |
fix C assume 1: "P C \<and> f C \<le> C" and 2: "\<not> C \<le> C \<triangle> f C" |
47613 | 564 |
hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
565 |
moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
566 |
by (metis narrow1 narrow2 1 mono order_trans) |
49547 | 567 |
moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
568 |
ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<le> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C" |
49547 | 569 |
by blast |
47613 | 570 |
qed |
571 |
||
49547 | 572 |
locale Abs_Int2_measure = |
573 |
Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m |
|
574 |
for \<gamma> :: "'av::{WN,lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat" |
|
575 |
||
47613 | 576 |
|
577 |
subsubsection "Termination: Intervals" |
|
578 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
579 |
definition m_rep :: "eint2 \<Rightarrow> nat" where |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
580 |
"m_rep p = (if is_empty_rep p then 3 else |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
581 |
let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
582 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
583 |
lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
584 |
by(auto simp: m_rep_def eq_ivl_iff) |
47613 | 585 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
586 |
lemma m_ivl_nice: "m_ivl[l\<dots>h] = (if [l\<dots>h] = \<bottom> then 3 else |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
587 |
(if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
588 |
unfolding bot_ivl_def |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
589 |
by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split) |
47613 | 590 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
591 |
lemma m_ivl_height: "m_ivl iv \<le> 3" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
592 |
by transfer (simp add: m_rep_def split: prod.split extended.split) |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
593 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
594 |
lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
595 |
by transfer |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
596 |
(auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
597 |
split: prod.split extended.splits if_splits) |
47613 | 598 |
|
599 |
lemma m_ivl_widen: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
600 |
"~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
601 |
by transfer |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
602 |
(auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
603 |
split: prod.split extended.splits if_splits) |
47613 | 604 |
|
605 |
definition n_ivl :: "ivl \<Rightarrow> nat" where |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
606 |
"n_ivl ivl = 3 - m_ivl ivl" |
47613 | 607 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
608 |
lemma n_ivl_mono: "x \<le> y \<Longrightarrow> n_ivl x \<le> n_ivl y" |
47613 | 609 |
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono) |
610 |
||
611 |
lemma n_ivl_narrow: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
612 |
"~ x \<le> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
613 |
unfolding n_ivl_def |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
614 |
by transfer |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
615 |
(auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
616 |
split: prod.splits if_splits extended.splits) |
47613 | 617 |
|
618 |
||
619 |
interpretation Abs_Int2_measure |
|
51245 | 620 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 621 |
and test_num' = in_ivl |
622 |
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
623 |
and m = m_ivl and n = n_ivl and h = 3 |
47613 | 624 |
proof |
625 |
case goal1 thus ?case by(rule m_ivl_anti_mono) |
|
626 |
next |
|
49547 | 627 |
case goal2 thus ?case by(rule m_ivl_height) |
47613 | 628 |
next |
49547 | 629 |
case goal3 thus ?case by(rule m_ivl_widen) |
47613 | 630 |
next |
631 |
case goal4 thus ?case by(rule n_ivl_mono) |
|
632 |
next |
|
49576 | 633 |
case goal5 from goal5(2) show ?case by(rule n_ivl_narrow) |
634 |
-- "note that the first assms is unnecessary for intervals" |
|
47613 | 635 |
qed |
636 |
||
637 |
||
638 |
lemma iter_winden_step_ivl_termination: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
639 |
"\<exists>C. iter_widen (step_ivl (Top(vars c))) (bot c) = Some C" |
49396 | 640 |
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"]) |
641 |
apply (simp_all add: step'_in_Lc m_c_widen) |
|
47613 | 642 |
done |
643 |
||
644 |
lemma iter_narrow_step_ivl_termination: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
645 |
"C0 \<in> Lc c \<Longrightarrow> step_ivl (Top(vars c)) C0 \<le> C0 \<Longrightarrow> |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
646 |
\<exists>C. iter_narrow (step_ivl (Top(vars c))) C0 = Some C" |
49396 | 647 |
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"]) |
648 |
apply (simp add: step'_in_Lc) |
|
47613 | 649 |
apply (simp) |
650 |
apply(rule mono_step'_top) |
|
49396 | 651 |
apply(simp add: Lc_acom_def L_acom_def) |
652 |
apply(simp add: Lc_acom_def L_acom_def) |
|
47613 | 653 |
apply assumption |
654 |
apply(erule (3) n_c_narrow) |
|
655 |
apply assumption |
|
656 |
apply assumption |
|
657 |
done |
|
658 |
||
659 |
theorem AI_ivl'_termination: |
|
660 |
"\<exists>C. AI_ivl' c = Some C" |
|
661 |
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination |
|
662 |
split: option.split) |
|
663 |
apply(rule iter_narrow_step_ivl_termination) |
|
51036 | 664 |
apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified]) |
47613 | 665 |
apply(erule iter_widen_pfp) |
666 |
done |
|
667 |
||
668 |
(*unused_thms Abs_Int_init -*) |
|
669 |
||
49578 | 670 |
subsubsection "Counterexamples" |
671 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
672 |
text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening. |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
673 |
It can already be lost after the first step: *} |
49578 | 674 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
675 |
lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
676 |
and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)" |
49578 | 677 |
nitpick[card = 3, expect = genuine, show_consts] |
678 |
(* |
|
679 |
1 < 2 < 3, |
|
680 |
f x = 2, |
|
681 |
x widen y = 3 -- guarantees termination with top=3 |
|
682 |
x = 1 |
|
683 |
Now f is mono, x <= f x, not f x <= x |
|
684 |
but x widen f x = 3, f 3 = 2, but not 3 <= 2 |
|
685 |
*) |
|
686 |
oops |
|
687 |
||
688 |
text{* Widening terminates but may converge more slowly than Kleene iteration. |
|
689 |
In the following model, Kleene iteration goes from 0 to the least pfp |
|
690 |
in one step but widening takes 2 steps to reach a strictly larger pfp: *} |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
691 |
lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
692 |
and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x" |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
693 |
shows "f(x \<nabla> f x) \<le> x \<nabla> f x" |
49578 | 694 |
nitpick[card = 4, expect = genuine, show_consts] |
695 |
(* |
|
696 |
||
697 |
0 < 1 < 2 < 3 |
|
698 |
f: 1 1 3 3 |
|
699 |
||
700 |
0 widen 1 = 2 |
|
701 |
2 widen 3 = 3 |
|
702 |
and x widen y arbitrary, eg 3, which guarantees termination |
|
703 |
||
704 |
Kleene: f(f 0) = f 1 = 1 <= 1 = f 1 |
|
705 |
||
706 |
but |
|
707 |
||
708 |
because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2, |
|
709 |
which is again not a pfp: not f 2 = 3 <= 2 |
|
710 |
Another widening step yields 2 widen f 2 = 2 widen 3 = 3 |
|
711 |
*) |
|
49892
09956f7a00af
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
wenzelm
parents:
49579
diff
changeset
|
712 |
oops |
49578 | 713 |
|
47613 | 714 |
end |