(* Title: HOL/Lattice/Bounds.thy

Author: Markus Wenzel, TU Muenchen

*)

header {* Bounds *}

theory Bounds imports Orders begin

hide_const (open) inf sup

subsection {* Infimum and supremum *}

text {*

Given a partial order, we define infimum (greatest lower bound) and

supremum (least upper bound) wrt.\ @{text \<sqsubseteq>} for two and for any

number of elements.

*}

definition

is_inf :: "'a::partial_order => 'a => 'a => bool" where

"is_inf x y inf = (inf \<sqsubseteq> x ∧ inf \<sqsubseteq> y ∧ (∀z. z \<sqsubseteq> x ∧ z \<sqsubseteq> y --> z \<sqsubseteq> inf))"

definition

is_sup :: "'a::partial_order => 'a => 'a => bool" where

"is_sup x y sup = (x \<sqsubseteq> sup ∧ y \<sqsubseteq> sup ∧ (∀z. x \<sqsubseteq> z ∧ y \<sqsubseteq> z --> sup \<sqsubseteq> z))"

definition

is_Inf :: "'a::partial_order set => 'a => bool" where

"is_Inf A inf = ((∀x ∈ A. inf \<sqsubseteq> x) ∧ (∀z. (∀x ∈ A. z \<sqsubseteq> x) --> z \<sqsubseteq> inf))"

definition

is_Sup :: "'a::partial_order set => 'a => bool" where

"is_Sup A sup = ((∀x ∈ A. x \<sqsubseteq> sup) ∧ (∀z. (∀x ∈ A. x \<sqsubseteq> z) --> sup \<sqsubseteq> z))"

text {*

These definitions entail the following basic properties of boundary

elements.

*}

lemma is_infI [intro?]: "inf \<sqsubseteq> x ==> inf \<sqsubseteq> y ==>

(!!z. z \<sqsubseteq> x ==> z \<sqsubseteq> y ==> z \<sqsubseteq> inf) ==> is_inf x y inf"

by (unfold is_inf_def) blast

lemma is_inf_greatest [elim?]:

"is_inf x y inf ==> z \<sqsubseteq> x ==> z \<sqsubseteq> y ==> z \<sqsubseteq> inf"

by (unfold is_inf_def) blast

lemma is_inf_lower [elim?]:

"is_inf x y inf ==> (inf \<sqsubseteq> x ==> inf \<sqsubseteq> y ==> C) ==> C"

by (unfold is_inf_def) blast

lemma is_supI [intro?]: "x \<sqsubseteq> sup ==> y \<sqsubseteq> sup ==>

(!!z. x \<sqsubseteq> z ==> y \<sqsubseteq> z ==> sup \<sqsubseteq> z) ==> is_sup x y sup"

by (unfold is_sup_def) blast

lemma is_sup_least [elim?]:

"is_sup x y sup ==> x \<sqsubseteq> z ==> y \<sqsubseteq> z ==> sup \<sqsubseteq> z"

by (unfold is_sup_def) blast

lemma is_sup_upper [elim?]:

"is_sup x y sup ==> (x \<sqsubseteq> sup ==> y \<sqsubseteq> sup ==> C) ==> C"

by (unfold is_sup_def) blast

lemma is_InfI [intro?]: "(!!x. x ∈ A ==> inf \<sqsubseteq> x) ==>

(!!z. (∀x ∈ A. z \<sqsubseteq> x) ==> z \<sqsubseteq> inf) ==> is_Inf A inf"

by (unfold is_Inf_def) blast

lemma is_Inf_greatest [elim?]:

"is_Inf A inf ==> (!!x. x ∈ A ==> z \<sqsubseteq> x) ==> z \<sqsubseteq> inf"

by (unfold is_Inf_def) blast

lemma is_Inf_lower [dest?]:

"is_Inf A inf ==> x ∈ A ==> inf \<sqsubseteq> x"

by (unfold is_Inf_def) blast

lemma is_SupI [intro?]: "(!!x. x ∈ A ==> x \<sqsubseteq> sup) ==>

(!!z. (∀x ∈ A. x \<sqsubseteq> z) ==> sup \<sqsubseteq> z) ==> is_Sup A sup"

by (unfold is_Sup_def) blast

lemma is_Sup_least [elim?]:

"is_Sup A sup ==> (!!x. x ∈ A ==> x \<sqsubseteq> z) ==> sup \<sqsubseteq> z"

by (unfold is_Sup_def) blast

lemma is_Sup_upper [dest?]:

"is_Sup A sup ==> x ∈ A ==> x \<sqsubseteq> sup"

by (unfold is_Sup_def) blast

subsection {* Duality *}

text {*

Infimum and supremum are dual to each other.

*}

theorem dual_inf [iff?]:

"is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"

by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)

theorem dual_sup [iff?]:

"is_sup (dual x) (dual y) (dual inf) = is_inf x y inf"

by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)

theorem dual_Inf [iff?]:

"is_Inf (dual ` A) (dual sup) = is_Sup A sup"

by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)

theorem dual_Sup [iff?]:

"is_Sup (dual ` A) (dual inf) = is_Inf A inf"

by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)

subsection {* Uniqueness *}

text {*

Infima and suprema on partial orders are unique; this is mainly due

to anti-symmetry of the underlying relation.

*}

theorem is_inf_uniq: "is_inf x y inf ==> is_inf x y inf' ==> inf = inf'"

proof -

assume inf: "is_inf x y inf"

assume inf': "is_inf x y inf'"

show ?thesis

proof (rule leq_antisym)

from inf' show "inf \<sqsubseteq> inf'"

proof (rule is_inf_greatest)

from inf show "inf \<sqsubseteq> x" ..

from inf show "inf \<sqsubseteq> y" ..

qed

from inf show "inf' \<sqsubseteq> inf"

proof (rule is_inf_greatest)

from inf' show "inf' \<sqsubseteq> x" ..

from inf' show "inf' \<sqsubseteq> y" ..

qed

qed

qed

theorem is_sup_uniq: "is_sup x y sup ==> is_sup x y sup' ==> sup = sup'"

proof -

assume sup: "is_sup x y sup" and sup': "is_sup x y sup'"

have "dual sup = dual sup'"

proof (rule is_inf_uniq)

from sup show "is_inf (dual x) (dual y) (dual sup)" ..

from sup' show "is_inf (dual x) (dual y) (dual sup')" ..

qed

then show "sup = sup'" ..

qed

theorem is_Inf_uniq: "is_Inf A inf ==> is_Inf A inf' ==> inf = inf'"

proof -

assume inf: "is_Inf A inf"

assume inf': "is_Inf A inf'"

show ?thesis

proof (rule leq_antisym)

from inf' show "inf \<sqsubseteq> inf'"

proof (rule is_Inf_greatest)

fix x assume "x ∈ A"

with inf show "inf \<sqsubseteq> x" ..

qed

from inf show "inf' \<sqsubseteq> inf"

proof (rule is_Inf_greatest)

fix x assume "x ∈ A"

with inf' show "inf' \<sqsubseteq> x" ..

qed

qed

qed

theorem is_Sup_uniq: "is_Sup A sup ==> is_Sup A sup' ==> sup = sup'"

proof -

assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"

have "dual sup = dual sup'"

proof (rule is_Inf_uniq)

from sup show "is_Inf (dual ` A) (dual sup)" ..

from sup' show "is_Inf (dual ` A) (dual sup')" ..

qed

then show "sup = sup'" ..

qed

subsection {* Related elements *}

text {*

The binary bound of related elements is either one of the argument.

*}

theorem is_inf_related [elim?]: "x \<sqsubseteq> y ==> is_inf x y x"

proof -

assume "x \<sqsubseteq> y"

show ?thesis

proof

show "x \<sqsubseteq> x" ..

show "x \<sqsubseteq> y" by fact

fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact

qed

qed

theorem is_sup_related [elim?]: "x \<sqsubseteq> y ==> is_sup x y y"

proof -

assume "x \<sqsubseteq> y"

show ?thesis

proof

show "x \<sqsubseteq> y" by fact

show "y \<sqsubseteq> y" ..

fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"

show "y \<sqsubseteq> z" by fact

qed

qed

subsection {* General versus binary bounds \label{sec:gen-bin-bounds} *}

text {*

General bounds of two-element sets coincide with binary bounds.

*}

theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"

proof -

let ?A = "{x, y}"

show ?thesis

proof

assume is_Inf: "is_Inf ?A inf"

show "is_inf x y inf"

proof

have "x ∈ ?A" by simp

with is_Inf show "inf \<sqsubseteq> x" ..

have "y ∈ ?A" by simp

with is_Inf show "inf \<sqsubseteq> y" ..

fix z assume zx: "z \<sqsubseteq> x" and zy: "z \<sqsubseteq> y"

from is_Inf show "z \<sqsubseteq> inf"

proof (rule is_Inf_greatest)

fix a assume "a ∈ ?A"

then have "a = x ∨ a = y" by blast

then show "z \<sqsubseteq> a"

proof

assume "a = x"

with zx show ?thesis by simp

next

assume "a = y"

with zy show ?thesis by simp

qed

qed

qed

next

assume is_inf: "is_inf x y inf"

show "is_Inf {x, y} inf"

proof

fix a assume "a ∈ ?A"

then have "a = x ∨ a = y" by blast

then show "inf \<sqsubseteq> a"

proof

assume "a = x"

also from is_inf have "inf \<sqsubseteq> x" ..

finally show ?thesis .

next

assume "a = y"

also from is_inf have "inf \<sqsubseteq> y" ..

finally show ?thesis .

qed

next

fix z assume z: "∀a ∈ ?A. z \<sqsubseteq> a"

from is_inf show "z \<sqsubseteq> inf"

proof (rule is_inf_greatest)

from z show "z \<sqsubseteq> x" by blast

from z show "z \<sqsubseteq> y" by blast

qed

qed

qed

qed

theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"

proof -

have "is_Sup {x, y} sup = is_Inf (dual ` {x, y}) (dual sup)"

by (simp only: dual_Inf)

also have "dual ` {x, y} = {dual x, dual y}"

by simp

also have "is_Inf … (dual sup) = is_inf (dual x) (dual y) (dual sup)"

by (rule is_Inf_binary)

also have "… = is_sup x y sup"

by (simp only: dual_inf)

finally show ?thesis .

qed

subsection {* Connecting general bounds \label{sec:connect-bounds} *}

text {*

Either kind of general bounds is sufficient to express the other.

The least upper bound (supremum) is the same as the the greatest

lower bound of the set of all upper bounds; the dual statements

holds as well; the dual statement holds as well.

*}

theorem Inf_Sup: "is_Inf {b. ∀a ∈ A. a \<sqsubseteq> b} sup ==> is_Sup A sup"

proof -

let ?B = "{b. ∀a ∈ A. a \<sqsubseteq> b}"

assume is_Inf: "is_Inf ?B sup"

show "is_Sup A sup"

proof

fix x assume x: "x ∈ A"

from is_Inf show "x \<sqsubseteq> sup"

proof (rule is_Inf_greatest)

fix y assume "y ∈ ?B"

then have "∀a ∈ A. a \<sqsubseteq> y" ..

from this x show "x \<sqsubseteq> y" ..

qed

next

fix z assume "∀x ∈ A. x \<sqsubseteq> z"

then have "z ∈ ?B" ..

with is_Inf show "sup \<sqsubseteq> z" ..

qed

qed

theorem Sup_Inf: "is_Sup {b. ∀a ∈ A. b \<sqsubseteq> a} inf ==> is_Inf A inf"

proof -

assume "is_Sup {b. ∀a ∈ A. b \<sqsubseteq> a} inf"

then have "is_Inf (dual ` {b. ∀a ∈ A. dual a \<sqsubseteq> dual b}) (dual inf)"

by (simp only: dual_Inf dual_leq)

also have "dual ` {b. ∀a ∈ A. dual a \<sqsubseteq> dual b} = {b'. ∀a' ∈ dual ` A. a' \<sqsubseteq> b'}"

by (auto iff: dual_ball dual_Collect simp add: image_Collect) (* FIXME !? *)

finally have "is_Inf … (dual inf)" .

then have "is_Sup (dual ` A) (dual inf)"

by (rule Inf_Sup)

then show ?thesis ..

qed

end