author | blanchet |
Wed, 24 Sep 2014 15:45:55 +0200 | |
changeset 58425 | 246985c6b20b |
parent 51625 | bd3358aac5d2 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
46225 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
51625 | 3 |
header "Abstract Interpretation (ITP)" |
46225 | 4 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
5 |
theory Complete_Lattice_ix |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
6 |
imports Main |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
7 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
8 |
|
46225 | 9 |
subsection "Complete Lattice (indexed)" |
10 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
11 |
text{* A complete lattice is an ordered type where every set of elements has |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
12 |
a greatest lower (and thus also a leats upper) bound. Sets are the |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
13 |
prototypical complete lattice where the greatest lower bound is |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
14 |
intersection. Sometimes that set of all elements of a type is not a complete |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
15 |
lattice although all elements of the same shape form a complete lattice, for |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
16 |
example lists of the same length, where the list elements come from a |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
17 |
complete lattice. We will have exactly this situation with annotated |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
18 |
commands. This theory introduces a slightly generalised version of complete |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
19 |
lattices where elements have an ``index'' and only the set of elements with |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
20 |
the same index form a complete lattice; the type as a whole is a disjoint |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
21 |
union of complete lattices. Because sets are not types, this requires a |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
22 |
special treatment. *} |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
23 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
24 |
locale Complete_Lattice_ix = |
45903 | 25 |
fixes L :: "'i \<Rightarrow> 'a::order set" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
26 |
and Glb :: "'i \<Rightarrow> 'a set \<Rightarrow> 'a" |
45903 | 27 |
assumes Glb_lower: "A \<subseteq> L i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a" |
28 |
and Glb_greatest: "b : L i \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> (Glb i A)" |
|
29 |
and Glb_in_L: "A \<subseteq> L i \<Longrightarrow> Glb i A : L i" |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
30 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
31 |
|
46066 | 32 |
definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'i \<Rightarrow> 'a" where |
33 |
"lfp f i = Glb i {a : L i. f a \<le> a}" |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
34 |
|
46066 | 35 |
lemma index_lfp: "lfp f i : L i" |
45903 | 36 |
by(auto simp: lfp_def intro: Glb_in_L) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
37 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
38 |
lemma lfp_lowerbound: |
46066 | 39 |
"\<lbrakk> a : L i; f a \<le> a \<rbrakk> \<Longrightarrow> lfp f i \<le> a" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
40 |
by (auto simp add: lfp_def intro: Glb_lower) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
41 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
42 |
lemma lfp_greatest: |
46066 | 43 |
"\<lbrakk> a : L i; \<And>u. \<lbrakk> u : L i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f i" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
44 |
by (auto simp add: lfp_def intro: Glb_greatest) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
45 |
|
45903 | 46 |
lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i" |
46066 | 47 |
and mono: "mono f" shows "lfp f i = f (lfp f i)" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
48 |
proof- |
45903 | 49 |
note assms(1)[simp] index_lfp[simp] |
46066 | 50 |
have 1: "f (lfp f i) \<le> lfp f i" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
51 |
apply(rule lfp_greatest) |
45903 | 52 |
apply simp |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
53 |
by (blast intro: lfp_lowerbound monoD[OF mono] order_trans) |
46066 | 54 |
have "lfp f i \<le> f (lfp f i)" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
55 |
by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
56 |
with 1 show ?thesis by(blast intro: order_antisym) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
57 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
58 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
59 |
end |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
60 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
61 |
end |