equal
deleted
inserted
replaced
|
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 |