# Theory Lattice

Up to index of Isabelle/HOL/HOL-Lattice

theory Lattice
imports Bounds
(*  Title:      HOL/Lattice/Lattice.thy    Author:     Markus Wenzel, TU Muenchen*)header {* Lattices *}theory Lattice imports Bounds beginsubsection {* Lattice operations *}text {*  A \emph{lattice} is a partial order with infimum and supremum of any  two elements (thus any \emph{finite} number of elements have bounds  as well).*}class lattice =  assumes ex_inf: "∃inf. is_inf x y inf"  assumes ex_sup: "∃sup. is_sup x y sup"text {*  The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such  infimum and supremum elements.*}definition  meet :: "'a::lattice => 'a => 'a"  (infixl "&&" 70) where  "x && y = (THE inf. is_inf x y inf)"definition  join :: "'a::lattice => 'a => 'a"  (infixl "||" 65) where  "x || y = (THE sup. is_sup x y sup)"notation (xsymbols)  meet  (infixl "\<sqinter>" 70) and  join  (infixl "\<squnion>" 65)text {*  Due to unique existence of bounds, the lattice operations may be  exhibited as follows.*}lemma meet_equality [elim?]: "is_inf x y inf ==> x \<sqinter> y = inf"proof (unfold meet_def)  assume "is_inf x y inf"  then show "(THE inf. is_inf x y inf) = inf"    by (rule the_equality) (rule is_inf_uniq [OF _ is_inf x y inf])qedlemma meetI [intro?]:    "inf \<sqsubseteq> x ==> inf \<sqsubseteq> y ==> (!!z. z \<sqsubseteq> x ==> z \<sqsubseteq> y ==> z \<sqsubseteq> inf) ==> x \<sqinter> y = inf"  by (rule meet_equality, rule is_infI) blast+lemma join_equality [elim?]: "is_sup x y sup ==> x \<squnion> y = sup"proof (unfold join_def)  assume "is_sup x y sup"  then show "(THE sup. is_sup x y sup) = sup"    by (rule the_equality) (rule is_sup_uniq [OF _ is_sup x y sup])qedlemma joinI [intro?]: "x \<sqsubseteq> sup ==> y \<sqsubseteq> sup ==>    (!!z. x \<sqsubseteq> z ==> y \<sqsubseteq> z ==> sup \<sqsubseteq> z) ==> x \<squnion> y = sup"  by (rule join_equality, rule is_supI) blast+text {*  \medskip The @{text \<sqinter>} and @{text \<squnion>} operations indeed determine  bounds on a lattice structure.*}lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"proof (unfold meet_def)  from ex_inf obtain inf where "is_inf x y inf" ..  then show "is_inf x y (THE inf. is_inf x y inf)"    by (rule theI) (rule is_inf_uniq [OF _ is_inf x y inf])qedlemma meet_greatest [intro?]: "z \<sqsubseteq> x ==> z \<sqsubseteq> y ==> z \<sqsubseteq> x \<sqinter> y"  by (rule is_inf_greatest) (rule is_inf_meet)lemma meet_lower1 [intro?]: "x \<sqinter> y \<sqsubseteq> x"  by (rule is_inf_lower) (rule is_inf_meet)lemma meet_lower2 [intro?]: "x \<sqinter> y \<sqsubseteq> y"  by (rule is_inf_lower) (rule is_inf_meet)lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"proof (unfold join_def)  from ex_sup obtain sup where "is_sup x y sup" ..  then show "is_sup x y (THE sup. is_sup x y sup)"    by (rule theI) (rule is_sup_uniq [OF _ is_sup x y sup])qedlemma join_least [intro?]: "x \<sqsubseteq> z ==> y \<sqsubseteq> z ==> x \<squnion> y \<sqsubseteq> z"  by (rule is_sup_least) (rule is_sup_join)lemma join_upper1 [intro?]: "x \<sqsubseteq> x \<squnion> y"  by (rule is_sup_upper) (rule is_sup_join)lemma join_upper2 [intro?]: "y \<sqsubseteq> x \<squnion> y"  by (rule is_sup_upper) (rule is_sup_join)subsection {* Duality *}text {*  The class of lattices is closed under formation of dual structures.  This means that for any theorem of lattice theory, the dualized  statement holds as well; this important fact simplifies many proofs  of lattice theory.*}instance dual :: (lattice) latticeproof  fix x' y' :: "'a::lattice dual"  show "∃inf'. is_inf x' y' inf'"  proof -    have "∃sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)    then have "∃sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"      by (simp only: dual_inf)    then show ?thesis by (simp add: dual_ex [symmetric])  qed  show "∃sup'. is_sup x' y' sup'"  proof -    have "∃inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)    then have "∃inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"      by (simp only: dual_sup)    then show ?thesis by (simp add: dual_ex [symmetric])  qedqedtext {*  Apparently, the @{text \<sqinter>} and @{text \<squnion>} operations are dual to each  other.*}theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"proof -  from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..  then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..  then show ?thesis ..qedtheorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"proof -  from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..  then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..  then show ?thesis ..qedsubsection {* Algebraic properties \label{sec:lattice-algebra} *}text {*  The @{text \<sqinter>} and @{text \<squnion>} operations have the following  characteristic algebraic properties: associative (A), commutative  (C), and absorptive (AB).*}theorem meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"proof  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y"  proof    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" ..    show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y"    proof -      have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..      also have "… \<sqsubseteq> y" ..      finally show ?thesis .    qed  qed  show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z"  proof -    have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" ..    also have "… \<sqsubseteq> z" ..    finally show ?thesis .  qed  fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z"  show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"  proof    show "w \<sqsubseteq> x"    proof -      have "w \<sqsubseteq> x \<sqinter> y" by fact      also have "… \<sqsubseteq> x" ..      finally show ?thesis .    qed    show "w \<sqsubseteq> y \<sqinter> z"    proof      show "w \<sqsubseteq> y"      proof -        have "w \<sqsubseteq> x \<sqinter> y" by fact        also have "… \<sqsubseteq> y" ..        finally show ?thesis .      qed      show "w \<sqsubseteq> z" by fact    qed  qedqedtheorem join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"proof -  have "dual ((x \<squnion> y) \<squnion> z) = (dual x \<sqinter> dual y) \<sqinter> dual z"    by (simp only: dual_join)  also have "… = dual x \<sqinter> (dual y \<sqinter> dual z)"    by (rule meet_assoc)  also have "… = dual (x \<squnion> (y \<squnion> z))"    by (simp only: dual_join)  finally show ?thesis ..qedtheorem meet_commute: "x \<sqinter> y = y \<sqinter> x"proof  show "y \<sqinter> x \<sqsubseteq> x" ..  show "y \<sqinter> x \<sqsubseteq> y" ..  fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"  then show "z \<sqsubseteq> y \<sqinter> x" ..qedtheorem join_commute: "x \<squnion> y = y \<squnion> x"proof -  have "dual (x \<squnion> y) = dual x \<sqinter> dual y" ..  also have "… = dual y \<sqinter> dual x"    by (rule meet_commute)  also have "… = dual (y \<squnion> x)"    by (simp only: dual_join)  finally show ?thesis ..qedtheorem meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x"proof  show "x \<sqsubseteq> x" ..  show "x \<sqsubseteq> x \<squnion> y" ..  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"  show "z \<sqsubseteq> x" by factqedtheorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"proof -  have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"    by (rule meet_join_absorb)  then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"    by (simp only: dual_meet dual_join)  then show ?thesis ..qedtext {*  \medskip Some further algebraic properties hold as well.  The  property idempotent (I) is a basic algebraic consequence of (AB).*}theorem meet_idem: "x \<sqinter> x = x"proof -  have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb)  also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb)  finally show ?thesis .qedtheorem join_idem: "x \<squnion> x = x"proof -  have "dual x \<sqinter> dual x = dual x"    by (rule meet_idem)  then have "dual (x \<squnion> x) = dual x"    by (simp only: dual_join)  then show ?thesis ..qedtext {*  Meet and join are trivial for related elements.*}theorem meet_related [elim?]: "x \<sqsubseteq> y ==> x \<sqinter> y = x"proof  assume "x \<sqsubseteq> y"  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 factqedtheorem join_related [elim?]: "x \<sqsubseteq> y ==> x \<squnion> y = y"proof -  assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..  then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)  also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)  also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)  finally show ?thesis ..qedsubsection {* Order versus algebraic structure *}text {*  The @{text \<sqinter>} and @{text \<squnion>} operations are connected with the  underlying @{text \<sqsubseteq>} relation in a canonical manner.*}theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"proof  assume "x \<sqsubseteq> y"  then have "is_inf x y x" ..  then show "x \<sqinter> y = x" ..next  have "x \<sqinter> y \<sqsubseteq> y" ..  also assume "x \<sqinter> y = x"  finally show "x \<sqsubseteq> y" .qedtheorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"proof  assume "x \<sqsubseteq> y"  then have "is_sup x y y" ..  then show "x \<squnion> y = y" ..next  have "x \<sqsubseteq> x \<squnion> y" ..  also assume "x \<squnion> y = y"  finally show "x \<sqsubseteq> y" .qedtext {*  \medskip The most fundamental result of the meta-theory of lattices  is as follows (we do not prove it here).  Given a structure with binary operations @{text \<sqinter>} and @{text \<squnion>}  such that (A), (C), and (AB) hold (cf.\  \S\ref{sec:lattice-algebra}).  This structure represents a lattice,  if the relation @{term "x \<sqsubseteq> y"} is defined as @{term "x \<sqinter> y = x"}  (alternatively as @{term "x \<squnion> y = y"}).  Furthermore, infimum and  supremum with respect to this ordering coincide with the original  @{text \<sqinter>} and @{text \<squnion>} operations.*}subsection {* Example instances *}subsubsection {* Linear orders *}text {*  Linear orders with @{term minimum} and @{term maximum} operations  are a (degenerate) example of lattice structures.*}definition  minimum :: "'a::linear_order => 'a => 'a" where  "minimum x y = (if x \<sqsubseteq> y then x else y)"definition  maximum :: "'a::linear_order => 'a => 'a" where  "maximum x y = (if x \<sqsubseteq> y then y else x)"lemma is_inf_minimum: "is_inf x y (minimum x y)"proof  let ?min = "minimum x y"  from leq_linear show "?min \<sqsubseteq> x" by (auto simp add: minimum_def)  from leq_linear show "?min \<sqsubseteq> y" by (auto simp add: minimum_def)  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"  with leq_linear show "z \<sqsubseteq> ?min" by (auto simp add: minimum_def)qedlemma is_sup_maximum: "is_sup x y (maximum x y)"      (* FIXME dualize!? *)proof  let ?max = "maximum x y"  from leq_linear show "x \<sqsubseteq> ?max" by (auto simp add: maximum_def)  from leq_linear show "y \<sqsubseteq> ?max" by (auto simp add: maximum_def)  fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"  with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)qedinstance linear_order ⊆ latticeproof  fix x y :: "'a::linear_order"  from is_inf_minimum show "∃inf. is_inf x y inf" ..  from is_sup_maximum show "∃sup. is_sup x y sup" ..qedtext {*  The lattice operations on linear orders indeed coincide with @{term  minimum} and @{term maximum}.*}theorem meet_mimimum: "x \<sqinter> y = minimum x y"  by (rule meet_equality) (rule is_inf_minimum)theorem meet_maximum: "x \<squnion> y = maximum x y"  by (rule join_equality) (rule is_sup_maximum)subsubsection {* Binary products *}text {*  The class of lattices is closed under direct binary products (cf.\  \S\ref{sec:prod-order}).*}lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"proof  show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> p"  proof -    have "fst p \<sqinter> fst q \<sqsubseteq> fst p" ..    moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd p" ..    ultimately show ?thesis by (simp add: leq_prod_def)  qed  show "(fst p \<sqinter> fst q, snd p \<sqinter> snd q) \<sqsubseteq> q"  proof -    have "fst p \<sqinter> fst q \<sqsubseteq> fst q" ..    moreover have "snd p \<sqinter> snd q \<sqsubseteq> snd q" ..    ultimately show ?thesis by (simp add: leq_prod_def)  qed  fix r assume rp: "r \<sqsubseteq> p" and rq: "r \<sqsubseteq> q"  show "r \<sqsubseteq> (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"  proof -    have "fst r \<sqsubseteq> fst p \<sqinter> fst q"    proof      from rp show "fst r \<sqsubseteq> fst p" by (simp add: leq_prod_def)      from rq show "fst r \<sqsubseteq> fst q" by (simp add: leq_prod_def)    qed    moreover have "snd r \<sqsubseteq> snd p \<sqinter> snd q"    proof      from rp show "snd r \<sqsubseteq> snd p" by (simp add: leq_prod_def)      from rq show "snd r \<sqsubseteq> snd q" by (simp add: leq_prod_def)    qed    ultimately show ?thesis by (simp add: leq_prod_def)  qedqedlemma is_sup_prod: "is_sup p q (fst p \<squnion> fst q, snd p \<squnion> snd q)"  (* FIXME dualize!? *)proof  show "p \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"  proof -    have "fst p \<sqsubseteq> fst p \<squnion> fst q" ..    moreover have "snd p \<sqsubseteq> snd p \<squnion> snd q" ..    ultimately show ?thesis by (simp add: leq_prod_def)  qed  show "q \<sqsubseteq> (fst p \<squnion> fst q, snd p \<squnion> snd q)"  proof -    have "fst q \<sqsubseteq> fst p \<squnion> fst q" ..    moreover have "snd q \<sqsubseteq> snd p \<squnion> snd q" ..    ultimately show ?thesis by (simp add: leq_prod_def)  qed  fix r assume "pr": "p \<sqsubseteq> r" and qr: "q \<sqsubseteq> r"  show "(fst p \<squnion> fst q, snd p \<squnion> snd q) \<sqsubseteq> r"  proof -    have "fst p \<squnion> fst q \<sqsubseteq> fst r"    proof      from "pr" show "fst p \<sqsubseteq> fst r" by (simp add: leq_prod_def)      from qr show "fst q \<sqsubseteq> fst r" by (simp add: leq_prod_def)    qed    moreover have "snd p \<squnion> snd q \<sqsubseteq> snd r"    proof      from "pr" show "snd p \<sqsubseteq> snd r" by (simp add: leq_prod_def)      from qr show "snd q \<sqsubseteq> snd r" by (simp add: leq_prod_def)    qed    ultimately show ?thesis by (simp add: leq_prod_def)  qedqedinstance prod :: (lattice, lattice) latticeproof  fix p q :: "'a::lattice × 'b::lattice"  from is_inf_prod show "∃inf. is_inf p q inf" ..  from is_sup_prod show "∃sup. is_sup p q sup" ..qedtext {*  The lattice operations on a binary product structure indeed coincide  with the products of the original ones.*}theorem meet_prod: "p \<sqinter> q = (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"  by (rule meet_equality) (rule is_inf_prod)theorem join_prod: "p \<squnion> q = (fst p \<squnion> fst q, snd p \<squnion> snd q)"  by (rule join_equality) (rule is_sup_prod)subsubsection {* General products *}text {*  The class of lattices is closed under general products (function  spaces) as well (cf.\ \S\ref{sec:fun-order}).*}lemma is_inf_fun: "is_inf f g (λx. f x \<sqinter> g x)"proof  show "(λx. f x \<sqinter> g x) \<sqsubseteq> f"  proof    fix x show "f x \<sqinter> g x \<sqsubseteq> f x" ..  qed  show "(λx. f x \<sqinter> g x) \<sqsubseteq> g"  proof    fix x show "f x \<sqinter> g x \<sqsubseteq> g x" ..  qed  fix h assume hf: "h \<sqsubseteq> f" and hg: "h \<sqsubseteq> g"  show "h \<sqsubseteq> (λx. f x \<sqinter> g x)"  proof    fix x    show "h x \<sqsubseteq> f x \<sqinter> g x"    proof      from hf show "h x \<sqsubseteq> f x" ..      from hg show "h x \<sqsubseteq> g x" ..    qed  qedqedlemma is_sup_fun: "is_sup f g (λx. f x \<squnion> g x)"   (* FIXME dualize!? *)proof  show "f \<sqsubseteq> (λx. f x \<squnion> g x)"  proof    fix x show "f x \<sqsubseteq> f x \<squnion> g x" ..  qed  show "g \<sqsubseteq> (λx. f x \<squnion> g x)"  proof    fix x show "g x \<sqsubseteq> f x \<squnion> g x" ..  qed  fix h assume fh: "f \<sqsubseteq> h" and gh: "g \<sqsubseteq> h"  show "(λx. f x \<squnion> g x) \<sqsubseteq> h"  proof    fix x    show "f x \<squnion> g x \<sqsubseteq> h x"    proof      from fh show "f x \<sqsubseteq> h x" ..      from gh show "g x \<sqsubseteq> h x" ..    qed  qedqedinstance "fun" :: (type, lattice) latticeproof  fix f g :: "'a => 'b::lattice"  show "∃inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from … show … .."} does not work!? unification incompleteness!? *)  show "∃sup. is_sup f g sup" by rule (rule is_sup_fun)qedtext {*  The lattice operations on a general product structure (function  space) indeed emerge by point-wise lifting of the original ones.*}theorem meet_fun: "f \<sqinter> g = (λx. f x \<sqinter> g x)"  by (rule meet_equality) (rule is_inf_fun)theorem join_fun: "f \<squnion> g = (λx. f x \<squnion> g x)"  by (rule join_equality) (rule is_sup_fun)subsection {* Monotonicity and semi-morphisms *}text {*  The lattice operations are monotone in both argument positions.  In  fact, monotonicity of the second position is trivial due to  commutativity.*}theorem meet_mono: "x \<sqsubseteq> z ==> y \<sqsubseteq> w ==> x \<sqinter> y \<sqsubseteq> z \<sqinter> w"proof -  {    fix a b c :: "'a::lattice"    assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"    proof      have "a \<sqinter> b \<sqsubseteq> a" ..      also have "… \<sqsubseteq> c" by fact      finally show "a \<sqinter> b \<sqsubseteq> c" .      show "a \<sqinter> b \<sqsubseteq> b" ..    qed  } note this [elim?]  assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..  also have "… = y \<sqinter> z" by (rule meet_commute)  also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..  also have "… = z \<sqinter> w" by (rule meet_commute)  finally show ?thesis .qedtheorem join_mono: "x \<sqsubseteq> z ==> y \<sqsubseteq> w ==> x \<squnion> y \<sqsubseteq> z \<squnion> w"proof -  assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..  moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..  ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"    by (rule meet_mono)  then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"    by (simp only: dual_join)  then show ?thesis ..qedtext {*  \medskip A semi-morphisms is a function @{text f} that preserves the  lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x  \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of  these properties is equivalent with monotonicity.*}theorem meet_semimorph:  "(!!x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) ≡ (!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y)"proof  assume morph: "!!x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"  fix x y :: "'a::lattice"  assume "x \<sqsubseteq> y"  then have "x \<sqinter> y = x" ..  then have "x = x \<sqinter> y" ..  also have "f … \<sqsubseteq> f x \<sqinter> f y" by (rule morph)  also have "… \<sqsubseteq> f y" ..  finally show "f x \<sqsubseteq> f y" .next  assume mono: "!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y"  show "!!x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"  proof -    fix x y    show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"    proof      have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)      have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)    qed  qedqedlemma join_semimorph:  "(!!x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)) ≡ (!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y)"proof  assume morph: "!!x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"  fix x y :: "'a::lattice"  assume "x \<sqsubseteq> y" then have "x \<squnion> y = y" ..  have "f x \<sqsubseteq> f x \<squnion> f y" ..  also have "… \<sqsubseteq> f (x \<squnion> y)" by (rule morph)  also from x \<sqsubseteq> y have "x \<squnion> y = y" ..  finally show "f x \<sqsubseteq> f y" .next  assume mono: "!!x y. x \<sqsubseteq> y ==> f x \<sqsubseteq> f y"  show "!!x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"  proof -    fix x y    show "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"    proof      have "x \<sqsubseteq> x \<squnion> y" .. then show "f x \<sqsubseteq> f (x \<squnion> y)" by (rule mono)      have "y \<sqsubseteq> x \<squnion> y" .. then show "f y \<sqsubseteq> f (x \<squnion> y)" by (rule mono)    qed  qedqedend