author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46225  d0a2c4a80a00 
permissions  rwrr 
46225  1 
(* Author: Tobias Nipkow *) 
2 

3 
header "Abstract Interpretation" 

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 