45111
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory Abs_Int2
|
|
4 |
imports Abs_Int1_ivl
|
|
5 |
begin
|
|
6 |
|
|
7 |
|
|
8 |
subsection "Widening and Narrowing"
|
|
9 |
|
|
10 |
class WN = SL_top +
|
|
11 |
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
|
|
12 |
assumes widen: "y \<sqsubseteq> x \<nabla> y"
|
|
13 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
|
|
14 |
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
|
|
15 |
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
|
|
16 |
|
|
17 |
|
|
18 |
instantiation ivl :: WN
|
|
19 |
begin
|
|
20 |
|
|
21 |
definition "widen_ivl ivl1 ivl2 =
|
|
22 |
((*if is_empty ivl1 then ivl2 else
|
|
23 |
if is_empty ivl2 then ivl1 else*)
|
|
24 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
|
|
25 |
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
|
|
26 |
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
|
|
27 |
|
|
28 |
definition "narrow_ivl ivl1 ivl2 =
|
|
29 |
((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
|
|
30 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
|
|
31 |
I (if l1 = None then l2 else l1)
|
|
32 |
(if h1 = None then h2 else h1))"
|
|
33 |
|
|
34 |
instance
|
|
35 |
proof qed
|
|
36 |
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
|
|
37 |
|
|
38 |
end
|
|
39 |
|
|
40 |
instantiation st :: (WN)WN
|
|
41 |
begin
|
|
42 |
|
|
43 |
definition "widen_st F1 F2 =
|
|
44 |
FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
|
|
45 |
|
|
46 |
definition "narrow_st F1 F2 =
|
|
47 |
FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
|
|
48 |
|
|
49 |
instance
|
|
50 |
proof
|
|
51 |
case goal1 thus ?case
|
|
52 |
by(simp add: widen_st_def le_st_def lookup_def widen)
|
|
53 |
next
|
|
54 |
case goal2 thus ?case
|
|
55 |
by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
|
|
56 |
next
|
|
57 |
case goal3 thus ?case
|
|
58 |
by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
|
|
59 |
qed
|
|
60 |
|
|
61 |
end
|
|
62 |
|
|
63 |
instantiation up :: (WN)WN
|
|
64 |
begin
|
|
65 |
|
|
66 |
fun widen_up where
|
|
67 |
"widen_up Bot x = x" |
|
|
68 |
"widen_up x Bot = x" |
|
|
69 |
"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
|
|
70 |
|
|
71 |
fun narrow_up where
|
|
72 |
"narrow_up Bot x = Bot" |
|
|
73 |
"narrow_up x Bot = Bot" |
|
|
74 |
"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
|
|
75 |
|
|
76 |
instance
|
|
77 |
proof
|
|
78 |
case goal1 show ?case
|
|
79 |
by(induct x y rule: widen_up.induct) (simp_all add: widen)
|
|
80 |
next
|
|
81 |
case goal2 thus ?case
|
|
82 |
by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
|
|
83 |
next
|
|
84 |
case goal3 thus ?case
|
|
85 |
by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
|
|
86 |
qed
|
|
87 |
|
|
88 |
end
|
|
89 |
|
|
90 |
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
|
|
91 |
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
|
|
92 |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
|
|
93 |
"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
|
|
94 |
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
|
|
95 |
(IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
|
|
96 |
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
|
|
97 |
({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})"
|
|
98 |
|
|
99 |
abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65)
|
|
100 |
where "widen_acom == map2_acom (op \<nabla>)"
|
|
101 |
|
|
102 |
abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
|
|
103 |
where "narrow_acom == map2_acom (op \<triangle>)"
|
|
104 |
|
|
105 |
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
|
|
106 |
by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
|
|
107 |
|
|
108 |
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
|
|
109 |
by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
|
|
110 |
|
|
111 |
fun iter_up :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
|
|
112 |
"iter_up f 0 x = \<top>\<^sub>c (strip x)" |
|
|
113 |
"iter_up f (Suc n) x =
|
|
114 |
(let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla>\<^sub>c fx))"
|
|
115 |
|
|
116 |
abbreviation
|
|
117 |
iter_down :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
|
|
118 |
"iter_down f n x == ((\<lambda>x. x \<triangle>\<^sub>c f x)^^n) x"
|
|
119 |
|
|
120 |
definition
|
|
121 |
iter' :: "nat \<Rightarrow> nat \<Rightarrow> (('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
|
|
122 |
"iter' m n f x = iter_down f n (iter_up f m x)"
|
|
123 |
|
|
124 |
lemma strip_map2_acom:
|
|
125 |
"strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
|
|
126 |
by(induct f c1 c2 rule: map2_acom.induct) simp_all
|
|
127 |
|
|
128 |
lemma strip_iter_up: assumes "\<forall>c. strip(f c) = strip c"
|
|
129 |
shows "strip(iter_up f n c) = strip c"
|
|
130 |
apply (induction n arbitrary: c)
|
|
131 |
apply (metis iter_up.simps(1) strip_Top_acom snd_conv)
|
|
132 |
apply (simp add:Let_def)
|
|
133 |
by (metis assms strip_map2_acom)
|
|
134 |
|
|
135 |
lemma iter_up_pfp: assumes "\<forall>c. strip(f c) = strip c"
|
|
136 |
shows "f(iter_up f n c) \<sqsubseteq> iter_up f n c"
|
|
137 |
apply (induction n arbitrary: c)
|
|
138 |
apply(simp add: assms)
|
|
139 |
apply (simp add:Let_def)
|
|
140 |
done
|
|
141 |
|
|
142 |
lemma strip_iter_down: assumes "\<forall>c. strip(f c) = strip c"
|
|
143 |
shows "strip(iter_down f n c) = strip c"
|
|
144 |
apply (induction n arbitrary: c)
|
|
145 |
apply(simp)
|
|
146 |
apply (simp add: strip_map2_acom assms)
|
|
147 |
done
|
|
148 |
|
|
149 |
lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
|
|
150 |
defines "x n == iter_down f n x0"
|
|
151 |
shows "f(x n) \<sqsubseteq> x n"
|
|
152 |
proof (induction n)
|
|
153 |
case 0 show ?case by (simp add: x_def assms(2))
|
|
154 |
next
|
|
155 |
case (Suc n)
|
|
156 |
have "f (x (Suc n)) = f(x n \<triangle>\<^sub>c f(x n))" by(simp add: x_def)
|
|
157 |
also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2_acom[OF Suc]])
|
|
158 |
also have "\<dots> \<sqsubseteq> x n \<triangle>\<^sub>c f(x n)" by(rule narrow1_acom[OF Suc])
|
|
159 |
also have "\<dots> = x(Suc n)" by(simp add: x_def)
|
|
160 |
finally show ?case .
|
|
161 |
qed
|
|
162 |
|
|
163 |
lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
|
|
164 |
defines "x n == iter_down f n x0"
|
|
165 |
shows "x n \<sqsubseteq> x0"
|
|
166 |
proof (induction n)
|
|
167 |
case 0 show ?case by(simp add: x_def)
|
|
168 |
next
|
|
169 |
case (Suc n)
|
|
170 |
have "x(Suc n) = x n \<triangle>\<^sub>c f(x n)" by(simp add: x_def)
|
|
171 |
also have "\<dots> \<sqsubseteq> x n" unfolding x_def
|
|
172 |
by(rule narrow2_acom[OF iter_down_pfp[OF assms(1), OF assms(2)]])
|
|
173 |
also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
|
|
174 |
finally show ?case .
|
|
175 |
qed
|
|
176 |
|
|
177 |
|
|
178 |
lemma iter'_pfp: assumes "\<forall>c. strip (f c) = strip c" and "mono f"
|
|
179 |
shows "f (iter' m n f c) \<sqsubseteq> iter' m n f c"
|
|
180 |
using iter_up_pfp[of f] iter_down_pfp[of f]
|
|
181 |
by(auto simp add: iter'_def Let_def assms)
|
|
182 |
|
|
183 |
lemma strip_iter': assumes "\<forall>c. strip(f c) = strip c"
|
|
184 |
shows "strip(iter' m n f c) = strip c"
|
|
185 |
by(simp add: iter'_def strip_iter_down strip_iter_up assms)
|
|
186 |
|
|
187 |
|
|
188 |
interpretation
|
|
189 |
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 20 5)"
|
|
190 |
defines afilter_ivl' is afilter
|
|
191 |
and bfilter_ivl' is bfilter
|
|
192 |
and step_ivl' is step
|
|
193 |
and AI_ivl' is AI
|
|
194 |
and aval_ivl' is aval'
|
|
195 |
proof qed (auto simp: iter'_pfp strip_iter')
|
|
196 |
|
|
197 |
value [code] "show_acom (AI_ivl test3_ivl)"
|
|
198 |
value [code] "show_acom (AI_ivl' test3_ivl)"
|
|
199 |
|
|
200 |
definition "step_up n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
|
|
201 |
definition "step_down n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
|
|
202 |
|
|
203 |
value [code] "show_acom (step_up 1 (\<bottom>\<^sub>c test3_ivl))"
|
|
204 |
value [code] "show_acom (step_up 2 (\<bottom>\<^sub>c test3_ivl))"
|
|
205 |
value [code] "show_acom (step_up 3 (\<bottom>\<^sub>c test3_ivl))"
|
|
206 |
value [code] "show_acom (step_up 4 (\<bottom>\<^sub>c test3_ivl))"
|
|
207 |
value [code] "show_acom (step_up 5 (\<bottom>\<^sub>c test3_ivl))"
|
|
208 |
value [code] "show_acom (step_down 1 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
|
|
209 |
value [code] "show_acom (step_down 2 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
|
|
210 |
value [code] "show_acom (step_down 3 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
|
|
211 |
|
|
212 |
value [code] "show_acom (AI_ivl' test4_ivl)"
|
|
213 |
value [code] "show_acom (AI_ivl' test5_ivl)"
|
|
214 |
value [code] "show_acom (AI_ivl' test6_ivl)"
|
|
215 |
|
|
216 |
end
|