author | nipkow |
Wed, 08 May 2013 06:14:11 +0200 | |
changeset 51914 | df962fe09a37 |
parent 51890 | 93a976fcb01f |
child 51924 | e398ab28eaa7 |
permissions | -rw-r--r-- |
47613 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_Int3 |
|
4 |
imports Abs_Int2_ivl |
|
5 |
begin |
|
6 |
||
7 |
||
8 |
subsection "Widening and Narrowing" |
|
9 |
||
10 |
class widen = |
|
11 |
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65) |
|
12 |
||
13 |
class narrow = |
|
14 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65) |
|
15 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
16 |
class WN = widen + narrow + order + |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
17 |
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
|
18 |
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
|
19 |
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
|
20 |
assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
21 |
begin |
47613 | 22 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
23 |
lemma narrowid[simp]: "x \<triangle> x = x" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
24 |
by (metis eq_iff narrow1 narrow2) |
47613 | 25 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
26 |
end |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
27 |
|
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
28 |
lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{WN,top})" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
29 |
by (metis eq_iff top_greatest widen2) |
47613 | 30 |
|
31 |
instantiation ivl :: WN |
|
32 |
begin |
|
33 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
34 |
definition "widen_rep p1 p2 = |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
35 |
(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
|
36 |
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
|
37 |
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
|
38 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
39 |
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
|
40 |
by(auto simp: widen_rep_def eq_ivl_iff) |
47613 | 41 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
42 |
definition "narrow_rep p1 p2 = |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
43 |
(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
|
44 |
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
|
45 |
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
|
46 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
47 |
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
|
48 |
by(auto simp: narrow_rep_def eq_ivl_iff) |
47613 | 49 |
|
50 |
instance |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
51 |
proof |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
52 |
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 eq_ivl_def split: if_splits extended.splits)+ |
47613 | 53 |
|
54 |
end |
|
55 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
56 |
instantiation st :: ("{top,WN}")WN |
47613 | 57 |
begin |
58 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
59 |
lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
60 |
by(auto simp: eq_st_def) |
47613 | 61 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
62 |
lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
63 |
by(auto simp: eq_st_def) |
47613 | 64 |
|
65 |
instance |
|
66 |
proof |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
67 |
case goal1 thus ?case |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
68 |
by transfer (simp add: less_eq_st_rep_iff widen1) |
47613 | 69 |
next |
70 |
case goal2 thus ?case |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
71 |
by transfer (simp add: less_eq_st_rep_iff widen2) |
47613 | 72 |
next |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
73 |
case goal3 thus ?case |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
74 |
by transfer (simp add: less_eq_st_rep_iff narrow1) |
47613 | 75 |
next |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
76 |
case goal4 thus ?case |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
77 |
by transfer (simp add: less_eq_st_rep_iff narrow2) |
47613 | 78 |
qed |
79 |
||
80 |
end |
|
81 |
||
82 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
83 |
instantiation option :: (WN)WN |
47613 | 84 |
begin |
85 |
||
86 |
fun widen_option where |
|
87 |
"None \<nabla> x = x" | |
|
88 |
"x \<nabla> None = x" | |
|
89 |
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" |
|
90 |
||
91 |
fun narrow_option where |
|
92 |
"None \<triangle> x = None" | |
|
93 |
"x \<triangle> None = None" | |
|
94 |
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" |
|
95 |
||
96 |
instance |
|
97 |
proof |
|
98 |
case goal1 thus ?case |
|
99 |
by(induct x y rule: widen_option.induct)(simp_all add: widen1) |
|
100 |
next |
|
101 |
case goal2 thus ?case |
|
102 |
by(induct x y rule: widen_option.induct)(simp_all add: widen2) |
|
103 |
next |
|
104 |
case goal3 thus ?case |
|
105 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) |
|
106 |
next |
|
107 |
case goal4 thus ?case |
|
108 |
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) |
|
109 |
qed |
|
110 |
||
111 |
end |
|
112 |
||
51914 | 113 |
text_raw{*\snip{maptwoacomdef}{2}{2}{% *} |
114 |
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" |
|
115 |
where |
|
116 |
"map2_acom f (SKIP {a\<^isub>1}) (SKIP {a\<^isub>2}) = (SKIP {f a\<^isub>1 a\<^isub>2})" | |
|
117 |
"map2_acom f (x ::= e {a\<^isub>1}) (x' ::= e' {a\<^isub>2}) = (x ::= e {f a\<^isub>1 a\<^isub>2})" | |
|
118 |
"map2_acom f (C\<^isub>1;C\<^isub>2) (D\<^isub>1;D\<^isub>2) |
|
119 |
= (map2_acom f C\<^isub>1 D\<^isub>1; map2_acom f C\<^isub>2 D\<^isub>2)" | |
|
120 |
"map2_acom f (IF b THEN {p\<^isub>1} C\<^isub>1 ELSE {p\<^isub>2} C\<^isub>2 {a\<^isub>1}) |
|
121 |
(IF b' THEN {q\<^isub>1} D\<^isub>1 ELSE {q\<^isub>2} D\<^isub>2 {a\<^isub>2}) |
|
122 |
= (IF b THEN {f p\<^isub>1 q\<^isub>1} map2_acom f C\<^isub>1 D\<^isub>1 |
|
123 |
ELSE {f p\<^isub>2 q\<^isub>2} map2_acom f C\<^isub>2 D\<^isub>2 {f a\<^isub>1 a\<^isub>2})" | |
|
124 |
"map2_acom f ({a\<^isub>1} WHILE b DO {p} C {a\<^isub>2}) |
|
125 |
({a\<^isub>3} WHILE b' DO {q} D {a\<^isub>4}) |
|
126 |
= ({f a\<^isub>1 a\<^isub>3} WHILE b DO {f p q} map2_acom f C D {f a\<^isub>2 a\<^isub>4})" |
|
127 |
text_raw{*}%endsnip*} |
|
47613 | 128 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
129 |
lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow> |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
130 |
annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
131 |
by(induction f C1 C2 rule: map2_acom.induct)(simp_all add: size_annos_same2) |
49548 | 132 |
|
133 |
instantiation acom :: (widen)widen |
|
134 |
begin |
|
135 |
definition "widen_acom = map2_acom (op \<nabla>)" |
|
136 |
instance .. |
|
137 |
end |
|
138 |
||
139 |
instantiation acom :: (narrow)narrow |
|
140 |
begin |
|
141 |
definition "narrow_acom = map2_acom (op \<triangle>)" |
|
142 |
instance .. |
|
143 |
end |
|
144 |
||
47613 | 145 |
lemma strip_map2_acom[simp]: |
146 |
"strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1" |
|
147 |
by(induct f C1 C2 rule: map2_acom.induct) simp_all |
|
148 |
||
149 |
lemma strip_widen_acom[simp]: |
|
150 |
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1" |
|
49548 | 151 |
by(simp add: widen_acom_def) |
47613 | 152 |
|
153 |
lemma strip_narrow_acom[simp]: |
|
154 |
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1" |
|
49548 | 155 |
by(simp add: narrow_acom_def) |
47613 | 156 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
157 |
lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::WN acom)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
158 |
by(induct C1 C2 rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1) |
47613 | 159 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
160 |
lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::WN acom) \<le> C1" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
161 |
by(induct C1 C2 rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2) |
47613 | 162 |
|
163 |
||
164 |
subsubsection "Post-fixed point computation" |
|
165 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
166 |
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
|
167 |
where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)" |
47613 | 168 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
169 |
definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option" |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
170 |
where "iter_narrow f = while_option (\<lambda>x. x \<triangle> f x < x) (\<lambda>x. x \<triangle> f x)" |
47613 | 171 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
172 |
definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" |
49548 | 173 |
where "pfp_wn f x = |
49576 | 174 |
(case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)" |
47613 | 175 |
|
176 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
177 |
lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p" |
47613 | 178 |
by(auto simp add: iter_widen_def dest: while_option_stop) |
179 |
||
180 |
lemma iter_widen_inv: |
|
181 |
assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x" |
|
182 |
and "iter_widen f x = Some y" shows "P y" |
|
183 |
using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]] |
|
184 |
by (blast intro: assms(1-3)) |
|
185 |
||
186 |
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom" |
|
187 |
assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'" |
|
188 |
shows "strip C' = strip C" |
|
189 |
using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)] |
|
190 |
by (metis assms(1)) |
|
191 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
192 |
lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom" |
47613 | 193 |
assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'" |
194 |
shows "strip C' = strip C" |
|
195 |
proof- |
|
196 |
have "\<forall>C. strip(C \<nabla> f C) = strip C" |
|
197 |
by (metis assms(1) strip_map2_acom widen_acom_def) |
|
198 |
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) |
|
199 |
qed |
|
200 |
||
201 |
lemma iter_narrow_pfp: |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
202 |
assumes mono: "!!x1 x2::_::WN acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2" |
49576 | 203 |
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
|
204 |
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
|
205 |
shows "P p \<and> f p \<le> p" |
47613 | 206 |
proof- |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
207 |
let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0" |
49576 | 208 |
{ fix p assume "?Q p" |
47613 | 209 |
note P = conjunct1[OF this] and 12 = conjunct2[OF this] |
210 |
note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12] |
|
49576 | 211 |
let ?p' = "p \<triangle> f p" |
212 |
have "?Q ?p'" |
|
47613 | 213 |
proof auto |
49576 | 214 |
show "P ?p'" by (blast intro: P Pinv) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
215 |
have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)` P narrow2_acom[OF 1]]) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
216 |
also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1]) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
217 |
finally show "f ?p' \<le> ?p'" . |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
218 |
have "?p' \<le> p" by (rule narrow2_acom[OF 1]) |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
219 |
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
|
220 |
finally show "?p' \<le> p0" . |
47613 | 221 |
qed |
222 |
} |
|
223 |
thus ?thesis |
|
224 |
using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]] |
|
225 |
by (blast intro: assms(4,5) le_refl) |
|
226 |
qed |
|
227 |
||
228 |
lemma pfp_wn_pfp: |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
229 |
assumes mono: "!!x1 x2::_::WN acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2" |
49548 | 230 |
and Pinv: "P x" "!!x. P x \<Longrightarrow> P(f x)" |
231 |
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" |
|
232 |
"!!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
|
233 |
and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p" |
47613 | 234 |
proof- |
49576 | 235 |
from pfp_wn obtain p0 |
236 |
where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p" |
|
47613 | 237 |
by(auto simp: pfp_wn_def split: option.splits) |
49576 | 238 |
have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3)) |
47613 | 239 |
thus ?thesis |
240 |
by - (assumption | |
|
241 |
rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+ |
|
242 |
qed |
|
243 |
||
244 |
lemma strip_pfp_wn: |
|
49548 | 245 |
"\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C" |
47613 | 246 |
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) |
51390 | 247 |
(metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while) |
47613 | 248 |
|
249 |
||
51826 | 250 |
locale Abs_Int2 = Abs_Int1_mono where \<gamma>=\<gamma> |
251 |
for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set" |
|
47613 | 252 |
begin |
253 |
||
254 |
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
255 |
"AI_wn c = pfp_wn (step' \<top>) (bot c)" |
47613 | 256 |
|
257 |
lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C" |
|
258 |
proof(simp add: CS_def AI_wn_def) |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
259 |
assume 1: "pfp_wn (step' \<top>) (bot c) = Some C" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
260 |
have 2: "strip C = c \<and> step' \<top> C \<le> C" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
261 |
by(rule pfp_wn_pfp[where x="bot c"]) (simp_all add: 1 mono_step'_top) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
262 |
have pfp: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C" |
50986 | 263 |
proof(rule order_trans) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
264 |
show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
265 |
by(rule step_step') |
50986 | 266 |
show "... \<le> \<gamma>\<^isub>c C" |
267 |
by(rule mono_gamma_c[OF conjunct2[OF 2]]) |
|
47613 | 268 |
qed |
50986 | 269 |
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1]) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
270 |
have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
271 |
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 pfp]) |
50986 | 272 |
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp |
47613 | 273 |
qed |
274 |
||
275 |
end |
|
276 |
||
277 |
interpretation Abs_Int2 |
|
51245 | 278 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 279 |
and test_num' = in_ivl |
51890
93a976fcb01f
tuned name: filter -> constrain (longer but more intuitive)
nipkow
parents:
51826
diff
changeset
|
280 |
and constrain_plus' = constrain_plus_ivl and constrain_less' = constrain_less_ivl |
47613 | 281 |
defines AI_ivl' is AI_wn |
282 |
.. |
|
283 |
||
284 |
||
285 |
subsubsection "Tests" |
|
286 |
||
51791 | 287 |
definition "step_up_ivl n = ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)" |
288 |
definition "step_down_ivl n = ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)" |
|
47613 | 289 |
|
290 |
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as |
|
291 |
the loop took to execute. In contrast, @{const AI_ivl'} converges in a |
|
292 |
constant number of steps: *} |
|
293 |
||
294 |
value "show_acom (step_up_ivl 1 (bot test3_ivl))" |
|
295 |
value "show_acom (step_up_ivl 2 (bot test3_ivl))" |
|
296 |
value "show_acom (step_up_ivl 3 (bot test3_ivl))" |
|
297 |
value "show_acom (step_up_ivl 4 (bot test3_ivl))" |
|
298 |
value "show_acom (step_up_ivl 5 (bot test3_ivl))" |
|
49188 | 299 |
value "show_acom (step_up_ivl 6 (bot test3_ivl))" |
300 |
value "show_acom (step_up_ivl 7 (bot test3_ivl))" |
|
301 |
value "show_acom (step_up_ivl 8 (bot test3_ivl))" |
|
302 |
value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))" |
|
303 |
value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))" |
|
304 |
value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))" |
|
305 |
value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))" |
|
51036 | 306 |
value "show_acom_opt (AI_ivl' test3_ivl)" |
47613 | 307 |
|
308 |
||
309 |
text{* Now all the analyses terminate: *} |
|
310 |
||
51036 | 311 |
value "show_acom_opt (AI_ivl' test4_ivl)" |
312 |
value "show_acom_opt (AI_ivl' test5_ivl)" |
|
313 |
value "show_acom_opt (AI_ivl' test6_ivl)" |
|
47613 | 314 |
|
315 |
||
316 |
subsubsection "Generic Termination Proof" |
|
317 |
||
51722 | 318 |
lemma top_on_opt_widen: |
51785 | 319 |
"top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<nabla> o2 :: _ st option) X" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
320 |
apply(induct o1 o2 rule: widen_option.induct) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
321 |
apply (auto) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
322 |
by transfer simp |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
323 |
|
51722 | 324 |
lemma top_on_opt_narrow: |
51785 | 325 |
"top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<triangle> o2 :: _ st option) X" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
326 |
apply(induct o1 o2 rule: narrow_option.induct) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
327 |
apply (auto) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
328 |
by transfer simp |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
329 |
|
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
330 |
lemma top_on_acom_widen: |
51785 | 331 |
"\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk> |
332 |
\<Longrightarrow> top_on_acom (C1 \<nabla> C2 :: _ st option acom) X" |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
333 |
by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
334 |
|
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
335 |
lemma top_on_acom_narrow: |
51785 | 336 |
"\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk> |
337 |
\<Longrightarrow> top_on_acom (C1 \<triangle> C2 :: _ st option acom) X" |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
338 |
by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
339 |
|
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
340 |
text{* The assumptions for widening and narrowing differ because during |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
341 |
narrowing we have the invariant @{prop"y \<le> x"} (where @{text y} is the next |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
342 |
iterate), but during widening there is no such invariant, there we only have |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
343 |
that not yet @{prop"y \<le> x"}. This complicates the termination proof for |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
344 |
widening. *} |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
345 |
|
51826 | 346 |
locale Measure_WN = Measure1 where m=m |
347 |
for m :: "'av::{top,WN} \<Rightarrow> nat" + |
|
47613 | 348 |
fixes n :: "'av \<Rightarrow> nat" |
51372 | 349 |
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
350 |
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x" |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
351 |
assumes n_narrow: "y \<le> x \<Longrightarrow> x \<triangle> y < x \<Longrightarrow> n(x \<triangle> y) < n x" |
47613 | 352 |
|
353 |
begin |
|
354 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
355 |
lemma m_s_anti_mono_rep: assumes "\<forall>x. S1 x \<le> S2 x" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
356 |
shows "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
357 |
proof- |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
358 |
from assms have "\<forall>x. m(S1 x) \<ge> m(S2 x)" by (metis m_anti_mono) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
359 |
thus "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" by (metis setsum_mono) |
51372 | 360 |
qed |
361 |
||
51791 | 362 |
lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 X \<ge> m_s S2 X" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
363 |
unfolding m_s_def |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
364 |
apply (transfer fixing: m) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
365 |
apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
366 |
done |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
367 |
|
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
368 |
lemma m_s_widen_rep: assumes "finite X" "S1 = S2 on -X" "\<not> S2 x \<le> S1 x" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
369 |
shows "(\<Sum>x\<in>X. m (S1 x \<nabla> S2 x)) < (\<Sum>x\<in>X. m (S1 x))" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
370 |
proof- |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
371 |
have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S1 x \<nabla> S2 x)" |
51372 | 372 |
by (metis m_anti_mono WN_class.widen1) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
373 |
have "x \<in> X" using assms(2,3) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
374 |
by(auto simp add: Ball_def) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
375 |
hence 2: "\<exists>x\<in>X. m(S1 x) > m(S1 x \<nabla> S2 x)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
376 |
using assms(3) m_widen by blast |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
377 |
from setsum_strict_mono_ex1[OF `finite X` 1 2] |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
378 |
show ?thesis . |
47613 | 379 |
qed |
380 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
381 |
lemma m_s_widen: "finite X \<Longrightarrow> fun S1 = fun S2 on -X ==> |
51791 | 382 |
~ S2 \<le> S1 \<Longrightarrow> m_s (S1 \<nabla> S2) X < m_s S1 X" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
383 |
apply(auto simp add: less_st_def m_s_def) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
384 |
apply (transfer fixing: m) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
385 |
apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
386 |
done |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
387 |
|
51785 | 388 |
lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow> |
51791 | 389 |
o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X" |
51372 | 390 |
proof(induction o1 o2 rule: less_eq_option.induct) |
391 |
case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono) |
|
392 |
next |
|
393 |
case 2 thus ?case |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
394 |
by(simp add: m_o_def le_SucI m_s_h split: option.splits) |
51372 | 395 |
next |
396 |
case 3 thus ?case by simp |
|
397 |
qed |
|
398 |
||
51785 | 399 |
lemma m_o_widen: "\<lbrakk> finite X; top_on_opt S1 (-X); top_on_opt S2 (-X); \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow> |
51791 | 400 |
m_o (S1 \<nabla> S2) X < m_o S1 X" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
401 |
by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split) |
47613 | 402 |
|
49547 | 403 |
lemma m_c_widen: |
51785 | 404 |
"strip C1 = strip C2 \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
405 |
\<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1" |
51792 | 406 |
apply(auto simp: m_c_def widen_acom_def listsum_setsum_nth) |
49547 | 407 |
apply(subgoal_tac "length(annos C2) = length(annos C1)") |
51390 | 408 |
prefer 2 apply (simp add: size_annos_same2) |
49547 | 409 |
apply (auto) |
410 |
apply(rule setsum_strict_mono_ex1) |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
411 |
apply(auto simp add: m_o_anti_mono vars_acom_def top_on_acom_def top_on_opt_widen widen1 le_iff_le_annos listrel_iff_nth) |
49547 | 412 |
apply(rule_tac x=i in bexI) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
413 |
apply (auto simp: vars_acom_def m_o_widen top_on_acom_def) |
49547 | 414 |
done |
415 |
||
416 |
||
51791 | 417 |
definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^isub>s") where |
418 |
"n\<^isub>s S X = (\<Sum>x\<in>X. n(fun S x))" |
|
49547 | 419 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
420 |
lemma n_s_narrow_rep: |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
421 |
assumes "finite X" "S1 = S2 on -X" "\<forall>x. S2 x \<le> S1 x" "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
422 |
"S1 x \<noteq> S1 x \<triangle> S2 x" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
423 |
shows "(\<Sum>x\<in>X. n (S1 x \<triangle> S2 x)) < (\<Sum>x\<in>X. n (S1 x))" |
47613 | 424 |
proof- |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
425 |
have 1: "\<forall>x. n(S1 x \<triangle> S2 x) \<le> n(S1 x)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
426 |
by (metis assms(3) assms(4) eq_iff less_le_not_le n_narrow) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
427 |
have "x \<in> X" by (metis Compl_iff assms(2) assms(5) narrowid) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
428 |
hence 2: "\<exists>x\<in>X. n(S1 x \<triangle> S2 x) < n(S1 x)" |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
429 |
by (metis assms(3-5) eq_iff less_le_not_le n_narrow) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
430 |
show ?thesis |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
431 |
apply(rule setsum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+ |
47613 | 432 |
qed |
433 |
||
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
434 |
lemma n_s_narrow: "finite X \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 |
51791 | 435 |
\<Longrightarrow> n\<^isub>s (S1 \<triangle> S2) X < n\<^isub>s S1 X" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
436 |
apply(auto simp add: less_st_def n_s_def) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
437 |
apply (transfer fixing: n) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
438 |
apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
439 |
done |
47613 | 440 |
|
51791 | 441 |
definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^isub>o") where |
442 |
"n\<^isub>o opt X = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S X + 1)" |
|
47613 | 443 |
|
444 |
lemma n_o_narrow: |
|
51785 | 445 |
"top_on_opt S1 (-X) \<Longrightarrow> top_on_opt S2 (-X) \<Longrightarrow> finite X |
51791 | 446 |
\<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) X < n\<^isub>o S1 X" |
47613 | 447 |
apply(induction S1 S2 rule: narrow_option.induct) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
448 |
apply(auto simp: n_o_def n_s_narrow) |
47613 | 449 |
done |
450 |
||
49576 | 451 |
|
452 |
definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^isub>c") where |
|
51792 | 453 |
"n\<^isub>c C = listsum (map (\<lambda>a. n\<^isub>o a (vars C)) (annos C))" |
47613 | 454 |
|
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
455 |
lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and> |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
456 |
(\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))" |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
457 |
by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2) |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
458 |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
459 |
lemma n_c_narrow: "strip C1 = strip C2 |
51785 | 460 |
\<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
461 |
\<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1" |
51792 | 462 |
apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth) |
47613 | 463 |
apply(subgoal_tac "length(annos C2) = length(annos C1)") |
464 |
prefer 2 apply (simp add: size_annos_same2) |
|
465 |
apply (auto) |
|
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
466 |
apply(simp add: less_annos_iff le_iff_le_annos) |
47613 | 467 |
apply(rule setsum_strict_mono_ex1) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
468 |
apply (auto simp: vars_acom_def top_on_acom_def) |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
469 |
apply (metis n_o_narrow nth_mem finite_cvars less_imp_le le_less order_refl) |
47613 | 470 |
apply(rule_tac x=i in bexI) |
471 |
prefer 2 apply simp |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
472 |
apply(rule n_o_narrow[where X = "vars(strip C2)"]) |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
473 |
apply (simp_all) |
47613 | 474 |
done |
475 |
||
476 |
end |
|
477 |
||
478 |
||
479 |
lemma iter_widen_termination: |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
480 |
fixes m :: "'a::WN acom \<Rightarrow> nat" |
47613 | 481 |
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)" |
482 |
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
|
483 |
and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1" |
47613 | 484 |
and "P C" shows "EX C'. iter_widen f C = Some C'" |
49547 | 485 |
proof(simp add: iter_widen_def, |
486 |
rule measure_while_option_Some[where P = P and f=m]) |
|
47613 | 487 |
show "P C" by(rule `P C`) |
488 |
next |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
489 |
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 | 490 |
by(simp add: P_f P_widen m_widen) |
47613 | 491 |
qed |
49496 | 492 |
|
47613 | 493 |
lemma iter_narrow_termination: |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
494 |
fixes n :: "'a::WN acom \<Rightarrow> nat" |
47613 | 495 |
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)" |
496 |
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
|
497 |
and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2" |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
498 |
and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n(C1 \<triangle> C2) < n C1" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
499 |
and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'" |
49547 | 500 |
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
|
501 |
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
|
502 |
show "P C \<and> f C \<le> C" using init by blast |
47613 | 503 |
next |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
504 |
fix C assume 1: "P C \<and> f C \<le> C" and 2: "C \<triangle> f C < C" |
47613 | 505 |
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
|
506 |
moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C" |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
507 |
by (metis narrow1_acom narrow2_acom 1 mono order_trans) |
49547 | 508 |
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
|
509 |
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 | 510 |
by blast |
47613 | 511 |
qed |
512 |
||
51826 | 513 |
locale Abs_Int2_measure = Abs_Int2 where \<gamma>=\<gamma> + Measure_WN where m=m |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
514 |
for \<gamma> :: "'av::{WN,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat" |
49547 | 515 |
|
47613 | 516 |
|
517 |
subsubsection "Termination: Intervals" |
|
518 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
519 |
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
|
520 |
"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
|
521 |
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
|
522 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
523 |
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
|
524 |
by(auto simp: m_rep_def eq_ivl_iff) |
47613 | 525 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
526 |
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
|
527 |
(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
|
528 |
unfolding bot_ivl_def |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
529 |
by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split) |
47613 | 530 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
531 |
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
|
532 |
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
|
533 |
|
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
534 |
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
|
535 |
by transfer |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
536 |
(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
|
537 |
split: prod.split extended.splits if_splits) |
47613 | 538 |
|
539 |
lemma m_ivl_widen: |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
540 |
"~ 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
|
541 |
by transfer |
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
542 |
(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
|
543 |
split: prod.split extended.splits if_splits) |
47613 | 544 |
|
545 |
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
|
546 |
"n_ivl ivl = 3 - m_ivl ivl" |
47613 | 547 |
|
548 |
lemma n_ivl_narrow: |
|
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
549 |
"x \<triangle> y < x \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x" |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
550 |
unfolding n_ivl_def |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
551 |
apply(subst (asm) less_le_not_le) |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
552 |
apply transfer |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
553 |
by(auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset |
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
554 |
split: prod.splits if_splits extended.split) |
47613 | 555 |
|
556 |
||
557 |
interpretation Abs_Int2_measure |
|
51245 | 558 |
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" |
47613 | 559 |
and test_num' = in_ivl |
51890
93a976fcb01f
tuned name: filter -> constrain (longer but more intuitive)
nipkow
parents:
51826
diff
changeset
|
560 |
and constrain_plus' = constrain_plus_ivl and constrain_less' = constrain_less_ivl |
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
561 |
and m = m_ivl and n = n_ivl and h = 3 |
47613 | 562 |
proof |
51372 | 563 |
case goal2 thus ?case by(rule m_ivl_anti_mono) |
47613 | 564 |
next |
51372 | 565 |
case goal1 thus ?case by(rule m_ivl_height) |
47613 | 566 |
next |
49547 | 567 |
case goal3 thus ?case by(rule m_ivl_widen) |
47613 | 568 |
next |
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset
|
569 |
case goal4 from goal4(2) show ?case by(rule n_ivl_narrow) |
49576 | 570 |
-- "note that the first assms is unnecessary for intervals" |
47613 | 571 |
qed |
572 |
||
573 |
lemma iter_winden_step_ivl_termination: |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
574 |
"\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C" |
51785 | 575 |
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom C (- vars C)"]) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
576 |
apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def] |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
577 |
vars_acom_def top_on_acom_widen) |
47613 | 578 |
done |
579 |
||
580 |
lemma iter_narrow_step_ivl_termination: |
|
51785 | 581 |
"top_on_acom C0 (- vars C0) \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow> |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
582 |
\<exists>C. iter_narrow (step_ivl \<top>) C0 = Some C" |
51785 | 583 |
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on_acom C (-vars C)"]) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
584 |
apply(auto simp: top_on_step'[simplified comp_def vars_acom_def] |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
585 |
mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow) |
47613 | 586 |
done |
587 |
||
588 |
theorem AI_ivl'_termination: |
|
589 |
"\<exists>C. AI_ivl' c = Some C" |
|
590 |
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination |
|
591 |
split: option.split) |
|
592 |
apply(rule iter_narrow_step_ivl_termination) |
|
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
593 |
apply(rule conjunct2) |
51785 | 594 |
apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom C (- vars C)"]) |
51711
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
595 |
apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def] |
df3426139651
complete revision: finally got rid of annoying L-predicate
nipkow
parents:
51390
diff
changeset
|
596 |
iter_widen_pfp top_on_bot vars_acom_def) |
47613 | 597 |
done |
598 |
||
51390 | 599 |
(*unused_thms Abs_Int_init - *) |
47613 | 600 |
|
49578 | 601 |
subsubsection "Counterexamples" |
602 |
||
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
603 |
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
|
604 |
It can already be lost after the first step: *} |
49578 | 605 |
|
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset
|
606 |
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
|
607 |
and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)" |
49578 | 608 |
nitpick[card = 3, expect = genuine, show_consts] |
609 |
(* |
|
610 |
1 < 2 < 3, |
|
611 |
f x = 2, |
|
612 |
x widen y = 3 -- guarantees termination with top=3 |
|
613 |
x = 1 |
|
614 |
Now f is mono, x <= f x, not f x <= x |
|
615 |
but x widen f x = 3, f 3 = 2, but not 3 <= 2 |
|
616 |
*) |
|
617 |
oops |
|
618 |
||
619 |
text{* Widening terminates but may converge more slowly than Kleene iteration. |
|
620 |
In the following model, Kleene iteration goes from 0 to the least pfp |
|
621 |
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
|
622 |
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
|
623 |
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
|
624 |
shows "f(x \<nabla> f x) \<le> x \<nabla> f x" |
49578 | 625 |
nitpick[card = 4, expect = genuine, show_consts] |
626 |
(* |
|
627 |
||
628 |
0 < 1 < 2 < 3 |
|
629 |
f: 1 1 3 3 |
|
630 |
||
631 |
0 widen 1 = 2 |
|
632 |
2 widen 3 = 3 |
|
633 |
and x widen y arbitrary, eg 3, which guarantees termination |
|
634 |
||
635 |
Kleene: f(f 0) = f 1 = 1 <= 1 = f 1 |
|
636 |
||
637 |
but |
|
638 |
||
639 |
because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2, |
|
640 |
which is again not a pfp: not f 2 = 3 <= 2 |
|
641 |
Another widening step yields 2 widen f 2 = 2 widen 3 = 3 |
|
642 |
*) |
|
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
|
643 |
oops |
49578 | 644 |
|
47613 | 645 |
end |