|
1440
|
1 |
(* Title: LatMorph.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
|
4 |
|
|
|
5 |
Some lattice morphisms.
|
|
|
6 |
|
|
|
7 |
TODO:
|
|
|
8 |
more morphisms (?)
|
|
|
9 |
more theorems
|
|
|
10 |
*)
|
|
|
11 |
|
|
|
12 |
LatMorph = LatInsts +
|
|
|
13 |
|
|
|
14 |
consts
|
|
|
15 |
is_mono :: "('a::le => 'b::le) => bool"
|
|
|
16 |
is_inf_morph :: "('a::lattice => 'b::lattice) => bool"
|
|
|
17 |
is_sup_morph :: "('a::lattice => 'b::lattice) => bool"
|
|
|
18 |
is_Inf_morph :: "('a::clattice => 'b::clattice) => bool"
|
|
|
19 |
is_Sup_morph :: "('a::clattice => 'b::clattice) => bool"
|
|
|
20 |
|
|
|
21 |
defs
|
|
|
22 |
is_mono_def "is_mono f == ALL x y. x [= y --> f x [= f y"
|
|
|
23 |
is_inf_morph_def "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
|
|
|
24 |
is_sup_morph_def "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
|
|
|
25 |
is_Inf_morph_def "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
|
|
|
26 |
is_Sup_morph_def "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
|
|
|
27 |
|
|
|
28 |
end
|