Theory Complete_Lattice

theory Complete_Lattice
imports Main
header "Abstract Interpretation"

theory Complete_Lattice
imports Main
begin

locale Complete_Lattice =
fixes L :: "'a::order set" and Glb :: "'a set => 'a"
assumes Glb_lower: "A ⊆ L ==> a ∈ A ==> Glb A ≤ a"
and Glb_greatest: "b : L ==> ∀a∈A. b ≤ a ==> b ≤ Glb A"
and Glb_in_L: "A ⊆ L ==> Glb A : L"
begin

definition lfp :: "('a => 'a) => 'a" where
"lfp f = Glb {a : L. f a ≤ a}"

lemma index_lfp: "lfp f : L"
by(auto simp: lfp_def intro: Glb_in_L)

lemma lfp_lowerbound:
"[| a : L; f a ≤ a |] ==> lfp f ≤ a"
by (auto simp add: lfp_def intro: Glb_lower)

lemma lfp_greatest:
"[| a : L; !!u. [| u : L; f u ≤ u|] ==> a ≤ u |] ==> a ≤ lfp f"
by (auto simp add: lfp_def intro: Glb_greatest)

lemma lfp_unfold: assumes "!!x. f x : L <-> x : L"
and mono: "mono f" shows "lfp f = f (lfp f)"
proof-
note assms(1)[simp] index_lfp[simp]
have 1: "f (lfp f) ≤ lfp f"
apply(rule lfp_greatest)
apply simp
by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
have "lfp f ≤ f (lfp f)"
by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
with 1 show ?thesis by(blast intro: order_antisym)
qed

end

end