Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semim...

Email Gateway (Aug 18 2022 at 11:02):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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 ?

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

Email Gateway (Aug 18 2022 at 11:02):

From: Tobias Nipkow <nipkow@in.tum.de>

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

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.

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

Last updated: Nov 21 2024 at 12:39 UTC