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

```Here's the missing dual version (join_semimorph) of the lemma
HOL/Lattice/Lattice.meet_semimorph.
```
```

```
```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.

Tobias

```
```regards
Peter

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)"
proof
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" .
next
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)"
proof
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)
qed
qed
qed

```
```

```

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