Theory Complete_Lattice

(* Author: Tobias Nipkow *)

section "Abstract Interpretation"

subsection "Complete Lattice"

theory Complete_Lattice
imports Main

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  aA. b  a  b  Glb A"
and Glb_in_L: "A  L  Glb A  L"

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)"
  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)