author | nipkow |
Thu, 15 Sep 2011 09:44:08 +0200 | |
changeset 44932 | 7c93ee993cae |
parent 44923 | b80108b346a9 |
child 44944 | f136409c2cef |
permissions | -rw-r--r-- |
44656 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header "Abstract Interpretation" |
|
4 |
||
5 |
theory AbsInt0_fun |
|
6 |
imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step |
|
7 |
begin |
|
8 |
||
9 |
subsection "Orderings" |
|
10 |
||
11 |
class preord = |
|
12 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
|
13 |
assumes le_refl[simp]: "x \<sqsubseteq> x" |
|
14 |
and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" |
|
15 |
||
16 |
text{* Note: no antisymmetry. Allows implementations where some abstract |
|
17 |
element is implemented by two different values @{prop "x \<noteq> y"} |
|
18 |
such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not |
|
19 |
needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}. |
|
20 |
*} |
|
21 |
||
22 |
class SL_top = preord + |
|
23 |
fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
|
24 |
fixes Top :: "'a" |
|
25 |
assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
|
26 |
and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
|
27 |
and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
28 |
and top[simp]: "x \<sqsubseteq> Top" |
|
29 |
begin |
|
30 |
||
31 |
lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
32 |
by (metis join_ge1 join_ge2 join_least le_trans) |
|
33 |
||
44932 | 34 |
fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where |
35 |
"iter 0 f _ = Top" | |
|
36 |
"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))" |
|
44656 | 37 |
|
44932 | 38 |
lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x" |
44656 | 39 |
apply (induct n arbitrary: x) |
40 |
apply (simp) |
|
41 |
apply (simp) |
|
42 |
done |
|
43 |
||
44932 | 44 |
definition iter_above :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where |
45 |
"iter_above n f x0 = iter n (\<lambda>x. x0 \<squnion> f x) x0" |
|
44923 | 46 |
|
47 |
lemma iter_above_pfp: |
|
44932 | 48 |
shows "f(iter_above n f x0) \<sqsubseteq> iter_above n f x0" and "x0 \<sqsubseteq> iter_above n f x0" |
44923 | 49 |
using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] |
50 |
by(auto simp add: iter_above_def) |
|
51 |
||
52 |
text{* So much for soundness. But how good an approximation of the post-fixed |
|
53 |
point does @{const iter_above} yield? *} |
|
54 |
||
44932 | 55 |
lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x" |
44656 | 56 |
apply(induct n arbitrary: x) |
44923 | 57 |
apply simp |
44656 | 58 |
apply (auto) |
44932 | 59 |
apply(metis funpow.simps(1) id_def) |
44656 | 60 |
by (metis funpow.simps(2) funpow_swap1 o_apply) |
61 |
||
44923 | 62 |
text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least |
63 |
post-fixed point above @{text x0}, unless it yields @{text Top}. *} |
|
44656 | 64 |
|
44923 | 65 |
lemma iter_least_pfp: |
44932 | 66 |
assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top" |
67 |
and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above n f x0 \<sqsubseteq> p" |
|
44656 | 68 |
proof- |
44923 | 69 |
let ?F = "\<lambda>x. x0 \<squnion> f x" |
44932 | 70 |
obtain k where "iter_above n f x0 = (?F^^k) x0" |
71 |
using iter_funpow `iter_above n f x0 \<noteq> Top` |
|
44923 | 72 |
by(fastforce simp add: iter_above_def) |
44656 | 73 |
moreover |
74 |
{ fix n have "(?F^^n) x0 \<sqsubseteq> p" |
|
75 |
proof(induct n) |
|
76 |
case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`) |
|
77 |
next |
|
78 |
case (Suc n) thus ?case |
|
79 |
by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono) |
|
80 |
qed |
|
81 |
} ultimately show ?thesis by simp |
|
82 |
qed |
|
83 |
||
84 |
lemma chain: assumes "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
|
44923 | 85 |
shows "((\<lambda>x. x0 \<squnion> f x)^^i) x0 \<sqsubseteq> ((\<lambda>x. x0 \<squnion> f x)^^(i+1)) x0" |
44656 | 86 |
apply(induct i) |
87 |
apply simp |
|
88 |
apply simp |
|
89 |
by (metis assms join_ge2 le_trans) |
|
90 |
||
44923 | 91 |
lemma iter_above_almost_fp: |
44932 | 92 |
assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top" |
93 |
shows "iter_above n f x0 \<sqsubseteq> x0 \<squnion> f(iter_above n f x0)" |
|
44656 | 94 |
proof- |
44932 | 95 |
let ?p = "iter_above n f x0" |
44923 | 96 |
obtain k where 1: "?p = ((\<lambda>x. x0 \<squnion> f x)^^k) x0" |
97 |
using iter_funpow `?p \<noteq> Top` |
|
98 |
by(fastforce simp add: iter_above_def) |
|
44656 | 99 |
thus ?thesis using chain mono by simp |
100 |
qed |
|
101 |
||
102 |
end |
|
103 |
||
104 |
text{* The interface of abstract values: *} |
|
105 |
||
106 |
locale Rep = |
|
107 |
fixes rep :: "'a::SL_top \<Rightarrow> 'b set" |
|
108 |
assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b" |
|
109 |
begin |
|
110 |
||
111 |
abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a" |
|
112 |
||
113 |
lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2" |
|
114 |
by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD) |
|
115 |
||
116 |
end |
|
117 |
||
118 |
locale Val_abs = Rep rep |
|
119 |
for rep :: "'a::SL_top \<Rightarrow> val set" + |
|
44932 | 120 |
fixes num' :: "val \<Rightarrow> 'a" |
121 |
and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
44656 | 122 |
assumes rep_num': "rep(num' n) = {n}" |
123 |
and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2" |
|
124 |
||
125 |
||
126 |
instantiation "fun" :: (type, SL_top) SL_top |
|
127 |
begin |
|
128 |
||
129 |
definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)" |
|
130 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
|
131 |
definition "Top = (\<lambda>x. Top)" |
|
132 |
||
133 |
lemma join_apply[simp]: |
|
134 |
"(f \<squnion> g) x = f x \<squnion> g x" |
|
135 |
by (simp add: join_fun_def) |
|
136 |
||
137 |
instance |
|
138 |
proof |
|
139 |
case goal2 thus ?case by (metis le_fun_def preord_class.le_trans) |
|
140 |
qed (simp_all add: le_fun_def Top_fun_def) |
|
141 |
||
142 |
end |
|
143 |
||
144 |
subsection "Abstract Interpretation Abstractly" |
|
145 |
||
44932 | 146 |
text{* Abstract interpretation over abstract values. Abstract states are |
147 |
simply functions. The post-fixed point finder is parameterized over. *} |
|
148 |
||
149 |
type_synonym 'a st = "name \<Rightarrow> 'a" |
|
44656 | 150 |
|
44932 | 151 |
locale Abs_Int_Fun = Val_abs + |
152 |
fixes pfp_above :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st" |
|
153 |
assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0" |
|
154 |
assumes above: "x0 \<sqsubseteq> pfp_above f x0" |
|
44656 | 155 |
begin |
156 |
||
44932 | 157 |
fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where |
44656 | 158 |
"aval' (N n) _ = num' n" | |
159 |
"aval' (V x) S = S x" | |
|
160 |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
161 |
||
162 |
abbreviation fun_in_rep (infix "<:" 50) where |
|
44923 | 163 |
"f <: F == \<forall>x. f x <: F x" |
44656 | 164 |
|
165 |
lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T" |
|
166 |
by (metis le_fun_def le_rep subsetD) |
|
167 |
||
168 |
lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S" |
|
169 |
by (induct a) (auto simp: rep_num' rep_plus') |
|
170 |
||
171 |
fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where |
|
172 |
"AI SKIP S = S" | |
|
173 |
"AI (x ::= a) S = S(x := aval' a S)" | |
|
174 |
"AI (c1;c2) S = AI c2 (AI c1 S)" | |
|
175 |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" | |
|
44932 | 176 |
"AI (WHILE b DO c) S = pfp_above (AI c) S" |
44656 | 177 |
|
178 |
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0" |
|
179 |
proof(induct c arbitrary: s t S0) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44656
diff
changeset
|
180 |
case SKIP thus ?case by fastforce |
44656 | 181 |
next |
182 |
case Assign thus ?case by (auto simp: aval'_sound) |
|
183 |
next |
|
184 |
case Semi thus ?case by auto |
|
185 |
next |
|
186 |
case If thus ?case by(auto simp: in_rep_join) |
|
187 |
next |
|
188 |
case (While b c) |
|
44932 | 189 |
let ?P = "pfp_above (AI c) S0" |
44656 | 190 |
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P" |
191 |
proof(induct "WHILE b DO c" s t rule: big_step_induct) |
|
192 |
case WhileFalse thus ?case by simp |
|
193 |
next |
|
44923 | 194 |
case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le) |
44656 | 195 |
qed |
196 |
} |
|
44932 | 197 |
with fun_in_rep_le[OF `s <: S0` above] |
44656 | 198 |
show ?case by (metis While(2) AI.simps(5)) |
199 |
qed |
|
200 |
||
201 |
end |
|
202 |
||
203 |
||
204 |
text{* Problem: not executable because of the comparison of abstract states, |
|
205 |
i.e. functions, in the post-fixedpoint computation. Need to implement |
|
206 |
abstract states concretely. *} |
|
207 |
||
208 |
end |