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