Re: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph

Here's the missing dual version (join_semimorph) of the lemma

We will add your contributions, thanks.

btw. Wasn't there a special email address where to send such lemmas ?

There was, but we closed it down because almost all we ever got was spam.



text {*
  \medskip A semi-morphisms is a function $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.
*}  (* FIXME dual version !? *)

theorem meet_semimorph:
  "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y)
\<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x
\<sqsubseteq> f y)"

Here's the dual version:

lemma join_semimorph: "(\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x
\<squnion> y)) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow>
f x \<sqsubseteq> f y)"
  assume morph: "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x
\<squnion> y)"
  fix x y :: "'a::lattice"
  assume S: "x \<sqsubseteq> y"
  have "f x \<sqsubseteq> f x \<squnion> f y" by (rule join_upper1)
  also have "\<dots> \<sqsubseteq> f (x \<squnion> y)" by (rule morph)
  also from S have "\<dots> = f y" by (simp add: join_related)
  finally show "f x \<sqsubseteq> f y" .
  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x
\<sqsubseteq> f y"
  show "\<And>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)"
      have "x \<sqsubseteq> x \<squnion> y" .. thus "f x \<sqsubseteq> f
(x \<squnion> y)" by (rule mono)
      have "y \<sqsubseteq> x \<squnion> y" .. thus "f y \<sqsubseteq> f
(x \<squnion> y)" by (rule mono)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.