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