author | nipkow |
Sun, 23 Oct 2011 16:03:59 +0200 | |
changeset 45257 | 12063e071d92 |
parent 45212 | e87feee00a4c |
child 45623 | f682f3f7b726 |
permissions | -rw-r--r-- |
45111 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header "Abstract Interpretation" |
|
4 |
||
5 |
theory Abs_Int0_fun |
|
6 |
imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
7 |
"~~/src/HOL/Library/While_Combinator" |
45111 | 8 |
begin |
9 |
||
10 |
subsection "Annotated Commands" |
|
11 |
||
12 |
datatype 'a acom = |
|
13 |
SKIP 'a ("SKIP {_}") | |
|
45212 | 14 |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
15 |
Semi "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) | |
|
16 |
If bexp "('a acom)" "('a acom)" 'a |
|
45113 | 17 |
("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) | |
45212 | 18 |
While 'a bexp "('a acom)" 'a |
45113 | 19 |
("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61) |
45111 | 20 |
|
21 |
fun post :: "'a acom \<Rightarrow>'a" where |
|
22 |
"post (SKIP {P}) = P" | |
|
23 |
"post (x ::= e {P}) = P" | |
|
24 |
"post (c1; c2) = post c2" | |
|
25 |
"post (IF b THEN c1 ELSE c2 {P}) = P" | |
|
26 |
"post ({Inv} WHILE b DO c {P}) = P" |
|
27 |
||
28 |
fun strip :: "'a acom \<Rightarrow> com" where |
|
29 |
"strip (SKIP {a}) = com.SKIP" | |
|
30 |
"strip (x ::= e {a}) = (x ::= e)" | |
|
31 |
"strip (c1;c2) = (strip c1; strip c2)" | |
|
32 |
"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" | |
|
33 |
"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)" |
|
34 |
||
35 |
fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where |
|
36 |
"anno a com.SKIP = SKIP {a}" | |
|
37 |
"anno a (x ::= e) = (x ::= e {a})" | |
|
38 |
"anno a (c1;c2) = (anno a c1; anno a c2)" | |
|
39 |
"anno a (IF b THEN c1 ELSE c2) = |
|
40 |
(IF b THEN anno a c1 ELSE anno a c2 {a})" | |
|
41 |
"anno a (WHILE b DO c) = |
|
42 |
({a} WHILE b DO anno a c {a})" |
|
43 |
||
44 |
lemma strip_anno[simp]: "strip (anno a c) = c" |
|
45 |
by(induct c) simp_all |
|
46 |
||
47 |
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
|
48 |
"map_acom f (SKIP {a}) = SKIP {f a}" | |
|
49 |
"map_acom f (x ::= e {a}) = (x ::= e {f a})" | |
|
50 |
"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" | |
|
51 |
"map_acom f (IF b THEN c1 ELSE c2 {a}) = |
|
52 |
(IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" | |
|
53 |
"map_acom f ({a1} WHILE b DO c {a2}) = |
|
54 |
({f a1} WHILE b DO map_acom f c {f a2})" |
|
55 |
||
56 |
||
57 |
subsection "Orderings" |
|
58 |
||
59 |
class preord = |
|
60 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
|
61 |
assumes le_refl[simp]: "x \<sqsubseteq> x" |
|
62 |
and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" |
|
63 |
begin |
|
64 |
||
65 |
definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)" |
|
66 |
||
67 |
lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def) |
|
68 |
||
69 |
lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)" |
|
70 |
by(simp add: mono_def) |
|
71 |
||
72 |
declare le_trans[trans] |
|
73 |
||
74 |
end |
|
75 |
||
76 |
text{* Note: no antisymmetry. Allows implementations where some abstract |
|
77 |
element is implemented by two different values @{prop "x \<noteq> y"} |
|
78 |
such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not |
|
79 |
needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}. |
|
80 |
*} |
|
81 |
||
82 |
class SL_top = preord + |
|
83 |
fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
|
84 |
fixes Top :: "'a" ("\<top>") |
|
85 |
assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
|
86 |
and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
|
87 |
and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
88 |
and top[simp]: "x \<sqsubseteq> \<top>" |
|
89 |
begin |
|
90 |
||
91 |
lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
92 |
by (metis join_ge1 join_ge2 join_least le_trans) |
|
93 |
||
94 |
lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z" |
|
95 |
by (metis join_ge1 join_ge2 le_trans) |
|
96 |
||
97 |
end |
|
98 |
||
99 |
instantiation "fun" :: (type, SL_top) SL_top |
|
100 |
begin |
|
101 |
||
102 |
definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)" |
|
103 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
|
104 |
definition "\<top> = (\<lambda>x. \<top>)" |
|
105 |
||
106 |
lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x" |
|
107 |
by (simp add: join_fun_def) |
|
108 |
||
109 |
instance |
|
110 |
proof |
|
111 |
case goal2 thus ?case by (metis le_fun_def preord_class.le_trans) |
|
112 |
qed (simp_all add: le_fun_def Top_fun_def) |
|
113 |
||
114 |
end |
|
115 |
||
116 |
||
117 |
instantiation acom :: (preord) preord |
|
118 |
begin |
|
119 |
||
120 |
fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
|
121 |
"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" | |
|
122 |
"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" | |
|
123 |
"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" | |
|
124 |
"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) = |
|
125 |
(b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" | |
|
126 |
"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) = |
|
127 |
(b=b' \<and> le_acom c c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" | |
|
128 |
"le_acom _ _ = False" |
|
129 |
||
130 |
lemma [simp]: "SKIP {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<sqsubseteq> S')" |
|
131 |
by (cases c) auto |
|
132 |
||
133 |
lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')" |
|
134 |
by (cases c) auto |
|
135 |
||
136 |
lemma [simp]: "c1;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')" |
|
137 |
by (cases c) auto |
|
138 |
||
139 |
lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow> |
|
140 |
(\<exists>c1' c2' S'. c = IF b THEN c1' ELSE c2' {S'} \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2' \<and> S \<sqsubseteq> S')" |
|
141 |
by (cases c) auto |
|
142 |
||
143 |
lemma [simp]: "{Inv} WHILE b DO c {P} \<sqsubseteq> w \<longleftrightarrow> |
|
144 |
(\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<sqsubseteq> c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" |
|
145 |
by (cases w) auto |
|
146 |
||
147 |
instance |
|
148 |
proof |
|
149 |
case goal1 thus ?case by (induct x) auto |
|
150 |
next |
|
151 |
case goal2 thus ?case |
|
152 |
apply(induct x y arbitrary: z rule: le_acom.induct) |
|
153 |
apply (auto intro: le_trans) |
|
154 |
done |
|
155 |
qed |
|
156 |
||
157 |
end |
|
158 |
||
159 |
||
160 |
subsubsection "Lifting" |
|
161 |
||
162 |
datatype 'a up = Bot | Up 'a |
|
163 |
||
164 |
instantiation up :: (SL_top)SL_top |
|
165 |
begin |
|
166 |
||
167 |
fun le_up where |
|
168 |
"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" | |
|
169 |
"Bot \<sqsubseteq> y = True" | |
|
170 |
"Up _ \<sqsubseteq> Bot = False" |
|
171 |
||
172 |
lemma [simp]: "(x \<sqsubseteq> Bot) = (x = Bot)" |
|
173 |
by (cases x) simp_all |
|
174 |
||
175 |
lemma [simp]: "(Up x \<sqsubseteq> u) = (\<exists>y. u = Up y & x \<sqsubseteq> y)" |
|
176 |
by (cases u) auto |
|
177 |
||
178 |
fun join_up where |
|
179 |
"Up x \<squnion> Up y = Up(x \<squnion> y)" | |
|
180 |
"Bot \<squnion> y = y" | |
|
181 |
"x \<squnion> Bot = x" |
|
182 |
||
183 |
lemma [simp]: "x \<squnion> Bot = x" |
|
184 |
by (cases x) simp_all |
|
185 |
||
186 |
definition "\<top> = Up \<top>" |
|
187 |
||
188 |
instance proof |
|
189 |
case goal1 show ?case by(cases x, simp_all) |
|
190 |
next |
|
191 |
case goal2 thus ?case |
|
192 |
by(cases z, simp, cases y, simp, cases x, auto intro: le_trans) |
|
193 |
next |
|
194 |
case goal3 thus ?case by(cases x, simp, cases y, simp_all) |
|
195 |
next |
|
196 |
case goal4 thus ?case by(cases y, simp, cases x, simp_all) |
|
197 |
next |
|
198 |
case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all) |
|
199 |
next |
|
200 |
case goal6 thus ?case by(cases x, simp_all add: Top_up_def) |
|
201 |
qed |
|
202 |
||
203 |
end |
|
204 |
||
205 |
definition bot_acom :: "com \<Rightarrow> ('a::SL_top)up acom" ("\<bottom>\<^sub>c") where |
|
206 |
"\<bottom>\<^sub>c = anno Bot" |
|
207 |
||
208 |
lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c" |
|
209 |
by(simp add: bot_acom_def) |
|
210 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
211 |
lemma bot_acom[rule_format]: "strip c' = c \<longrightarrow> \<bottom>\<^sub>c c \<sqsubseteq> c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
212 |
apply(induct c arbitrary: c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
213 |
apply (simp_all add: bot_acom_def) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
214 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
215 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
216 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
217 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
218 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
219 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
220 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
221 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
222 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
223 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
224 |
done |
45111 | 225 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
226 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
227 |
subsubsection "Post-fixed point iteration" |
45111 | 228 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
229 |
definition |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
230 |
pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
231 |
"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
232 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
233 |
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
234 |
using while_option_stop[OF assms[simplified pfp_def]] by simp |
45111 | 235 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
236 |
lemma pfp_least: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
237 |
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
238 |
and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
239 |
proof- |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
240 |
{ fix x assume "x \<sqsubseteq> p" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
241 |
hence "f x \<sqsubseteq> f p" by(rule mono) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
242 |
from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
243 |
} |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
244 |
thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
245 |
unfolding pfp_def by blast |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
246 |
qed |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
247 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
248 |
definition |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
249 |
lpfp\<^isub>c :: "(('a::SL_top)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option" where |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
250 |
"lpfp\<^isub>c f c = pfp f (\<bottom>\<^sub>c c)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
251 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
252 |
lemma lpfpc_pfp: "lpfp\<^isub>c f c0 = Some c \<Longrightarrow> f c \<sqsubseteq> c" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
253 |
by(simp add: pfp_pfp lpfp\<^isub>c_def) |
45111 | 254 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
255 |
lemma strip_pfp: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
256 |
assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
257 |
using assms while_option_rule[where P = "%x. g x = g x0" and c = f] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
258 |
unfolding pfp_def by metis |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
259 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
260 |
lemma strip_lpfpc: assumes "\<And>c. strip(f c) = strip c" and "lpfp\<^isub>c f c = Some c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
261 |
shows "strip c' = c" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
262 |
using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp\<^isub>c_def]] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
263 |
by(metis strip_bot_acom) |
45111 | 264 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
265 |
lemma lpfpc_least: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
266 |
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
267 |
and "strip p = c0" and "f p \<sqsubseteq> p" and lp: "lpfp\<^isub>c f c0 = Some c" shows "c \<sqsubseteq> p" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
268 |
using pfp_least[OF _ _ bot_acom[OF `strip p = c0`] lp[simplified lpfp\<^isub>c_def]] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
269 |
mono `f p \<sqsubseteq> p` |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
270 |
by blast |
45111 | 271 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
272 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
273 |
subsection "Abstract Interpretation" |
45111 | 274 |
|
275 |
definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
|
276 |
"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}" |
|
277 |
||
278 |
fun rep_up :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a up \<Rightarrow> 'b set" where |
|
279 |
"rep_up rep Bot = {}" | |
|
280 |
"rep_up rep (Up a) = rep a" |
|
281 |
||
282 |
text{* The interface for abstract values: *} |
|
283 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
284 |
locale Val_abs = |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
285 |
fixes rep :: "'a::SL_top \<Rightarrow> val set" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
286 |
assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
287 |
and rep_Top: "rep \<top> = UNIV" |
45111 | 288 |
fixes num' :: "val \<Rightarrow> 'a" |
289 |
and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
290 |
assumes rep_num': "n : rep(num' n)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
291 |
and rep_plus': |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
292 |
"n1 : rep a1 \<Longrightarrow> n2 : rep a2 \<Longrightarrow> n1+n2 : rep(plus' a1 a2)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
293 |
begin |
45111 | 294 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
295 |
abbreviation in_rep (infix "<:" 50) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
296 |
where "x <: a == x : rep a" |
45111 | 297 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
298 |
lemma in_rep_Top[simp]: "x <: \<top>" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
299 |
by(simp add: rep_Top) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
300 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
301 |
end |
45111 | 302 |
|
45212 | 303 |
type_synonym 'a st = "(vname \<Rightarrow> 'a)" |
45111 | 304 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
305 |
locale Abs_Int_Fun = Val_abs |
45111 | 306 |
begin |
307 |
||
308 |
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where |
|
309 |
"aval' (N n) _ = num' n" | |
|
310 |
"aval' (V x) S = S x" | |
|
311 |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
312 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
313 |
fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
314 |
where |
45111 | 315 |
"step S (SKIP {P}) = (SKIP {S})" | |
316 |
"step S (x ::= e {P}) = |
|
317 |
x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(S(x := aval' e S))}" | |
|
318 |
"step S (c1; c2) = step S c1; step (post c1) c2" | |
|
319 |
"step S (IF b THEN c1 ELSE c2 {P}) = |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
320 |
IF b THEN step S c1 ELSE step S c2 {post c1 \<squnion> post c2}" | |
45111 | 321 |
"step S ({Inv} WHILE b DO c {P}) = |
322 |
{S \<squnion> post c} WHILE b DO (step Inv c) {Inv}" |
|
323 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
324 |
definition AI :: "com \<Rightarrow> 'a st up acom option" where |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
325 |
"AI = lpfp\<^isub>c (step \<top>)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
326 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
327 |
|
45111 | 328 |
lemma strip_step[simp]: "strip(step S c) = strip c" |
329 |
by(induct c arbitrary: S) (simp_all add: Let_def) |
|
330 |
||
331 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
332 |
text{*Lifting @{text "<:"} to other types: *} |
45111 | 333 |
|
334 |
abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where |
|
335 |
"s <:f S == s \<in> rep_fun rep S" |
|
336 |
||
337 |
notation fun_in_rep (infix "<:\<^sub>f" 50) |
|
338 |
||
339 |
lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T" |
|
340 |
by(auto simp add: rep_fun_def le_fun_def dest: le_rep) |
|
341 |
||
342 |
abbreviation up_in_rep :: "state \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50) where |
|
343 |
"s <:up S == s : rep_up (rep_fun rep) S" |
|
344 |
||
345 |
notation (output) up_in_rep (infix "<:\<^sub>u\<^sub>p" 50) |
|
346 |
||
347 |
lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T" |
|
348 |
by (cases S) (auto intro:fun_in_rep_le) |
|
349 |
||
350 |
lemma in_rep_Top_fun: "s <:f Top" |
|
351 |
by(simp add: Top_fun_def rep_fun_def) |
|
352 |
||
353 |
lemma in_rep_Top_up: "s <:up Top" |
|
354 |
by(simp add: Top_up_def in_rep_Top_fun) |
|
355 |
||
356 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
357 |
text{* Soundness: *} |
45111 | 358 |
|
359 |
lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S" |
|
360 |
by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def) |
|
361 |
||
362 |
lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f S(x := a)" |
|
363 |
by(simp add: rep_fun_def) |
|
364 |
||
365 |
lemma step_sound: |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
366 |
"\<lbrakk> step S c \<sqsubseteq> c; (strip c,s) \<Rightarrow> t; s <:up S \<rbrakk> |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
367 |
\<Longrightarrow> t <:up post c" |
45111 | 368 |
proof(induction c arbitrary: S s t) |
369 |
case SKIP thus ?case |
|
370 |
by simp (metis skipE up_fun_in_rep_le) |
|
371 |
next |
|
372 |
case Assign thus ?case |
|
373 |
apply (auto simp del: fun_upd_apply split: up.splits) |
|
374 |
by (metis aval'_sound fun_in_rep_le in_rep_update) |
|
375 |
next |
|
376 |
case Semi thus ?case by simp blast |
|
377 |
next |
|
378 |
case (If b c1 c2 S0) thus ?case |
|
379 |
apply(auto simp: Let_def) |
|
380 |
apply (metis up_fun_in_rep_le)+ |
|
381 |
done |
|
382 |
next |
|
383 |
case (While Inv b c P) |
|
384 |
from While.prems have inv: "step Inv c \<sqsubseteq> c" |
|
385 |
and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def) |
|
386 |
{ fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv" |
|
387 |
proof(induction "WHILE b DO strip c" s t rule: big_step_induct) |
|
388 |
case WhileFalse thus ?case by simp |
|
389 |
next |
|
390 |
case (WhileTrue s1 s2 s3) |
|
391 |
from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]] |
|
392 |
show ?case . |
|
393 |
qed |
|
394 |
} |
|
395 |
thus ?case using While.prems(2) |
|
396 |
by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le) |
|
397 |
qed |
|
398 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
399 |
lemma AI_sound: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
400 |
"\<lbrakk> AI c = Some c'; (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
401 |
by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
402 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
403 |
end |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
404 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
405 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
406 |
subsubsection "Monotonicity" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
407 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
408 |
locale Abs_Int_Fun_mono = Abs_Int_Fun + |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
409 |
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
410 |
begin |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
411 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
412 |
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
413 |
by(induction e)(auto simp: le_fun_def mono_plus') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
414 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
415 |
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
416 |
by(simp add: le_fun_def) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
417 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
418 |
lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
419 |
apply(induction c arbitrary: S S') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
420 |
apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
421 |
done |
45111 | 422 |
|
423 |
end |
|
424 |
||
425 |
text{* Problem: not executable because of the comparison of abstract states, |
|
426 |
i.e. functions, in the post-fixedpoint computation. *} |
|
427 |
||
428 |
end |