*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 23 Nov 2007 09:13:32 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4745CB22.8010800@uni-muenster.de>*References*: <4745CB22.8010800@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

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

**References**:**[isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph***From:*Peter Lammich

- Previous by Date: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph
- Next by Date: [isabelle] Announcing Isabelle2007
- Previous by Thread: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph
- Next by Thread: [isabelle] Announcing Isabelle2007
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list