section "Abstract Interpretation (ITP)"
theory Complete_Lattice_ix
imports Main
begin
subsection "Complete Lattice (indexed)"
text{* A complete lattice is an ordered type where every set of elements has
a greatest lower (and thus also a leats upper) bound. Sets are the
prototypical complete lattice where the greatest lower bound is
intersection. Sometimes that set of all elements of a type is not a complete
lattice although all elements of the same shape form a complete lattice, for
example lists of the same length, where the list elements come from a
complete lattice. We will have exactly this situation with annotated
commands. This theory introduces a slightly generalised version of complete
lattices where elements have an ``index'' and only the set of elements with
the same index form a complete lattice; the type as a whole is a disjoint
union of complete lattices. Because sets are not types, this requires a
special treatment. *}
locale Complete_Lattice_ix =
fixes L :: "'i ⇒ 'a::order set"
and Glb :: "'i ⇒ 'a set ⇒ 'a"
assumes Glb_lower: "A ⊆ L i ⟹ a ∈ A ⟹ (Glb i A) ≤ a"
and Glb_greatest: "b : L i ⟹ ∀a∈A. b ≤ a ⟹ b ≤ (Glb i A)"
and Glb_in_L: "A ⊆ L i ⟹ Glb i A : L i"
begin
definition lfp :: "('a ⇒ 'a) ⇒ 'i ⇒ 'a" where
"lfp f i = Glb i {a : L i. f a ≤ a}"
lemma index_lfp: "lfp f i : L i"
by(auto simp: lfp_def intro: Glb_in_L)
lemma lfp_lowerbound:
"⟦ a : L i; f a ≤ a ⟧ ⟹ lfp f i ≤ a"
by (auto simp add: lfp_def intro: Glb_lower)
lemma lfp_greatest:
"⟦ a : L i; ⋀u. ⟦ u : L i; f u ≤ u⟧ ⟹ a ≤ u ⟧ ⟹ a ≤ lfp f i"
by (auto simp add: lfp_def intro: Glb_greatest)
lemma lfp_unfold: assumes "⋀x i. f x : L i ⟷ x : L i"
and mono: "mono f" shows "lfp f i = f (lfp f i)"
proof-
note assms(1)[simp] index_lfp[simp]
have 1: "f (lfp f i) ≤ lfp f i"
apply(rule lfp_greatest)
apply simp
by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
have "lfp f i ≤ f (lfp f i)"
by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
with 1 show ?thesis by(blast intro: order_antisym)
qed
end
end