src/HOL/IMP/Complete_Lattice_ix.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46225 d0a2c4a80a00
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46225
nipkow
parents: 46066
diff changeset
     1
(* Author: Tobias Nipkow *)
nipkow
parents: 46066
diff changeset
     2
nipkow
parents: 46066
diff changeset
     3
header "Abstract Interpretation"
nipkow
parents: 46066
diff changeset
     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
nipkow
parents: 46066
diff changeset
     9
subsection "Complete Lattice (indexed)"
nipkow
parents: 46066
diff changeset
    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
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    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
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    27
assumes Glb_lower: "A \<subseteq> L i \<Longrightarrow> a \<in> A \<Longrightarrow> (Glb i A) \<le> a"
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    28
and Glb_greatest: "b : L i \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> (Glb i A)"
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    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
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    32
definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'i \<Rightarrow> 'a" where
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    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
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    35
lemma index_lfp: "lfp f i : L i"
45903
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    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
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    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
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    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
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    46
lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i"
46066
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    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
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    49
  note assms(1)[simp] index_lfp[simp]
46066
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    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
02dd9319dcb7 improved indexed complete lattice
nipkow
parents: 45623
diff changeset
    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
e81411bfa7ef tuned argument order
nipkow
parents: 45903
diff changeset
    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