src/HOL/AxClasses/Lattice/LatMorph.thy
author wenzelm
Tue, 30 May 2000 16:08:38 +0200
changeset 9000 c20d58286a51
parent 1573 6d66b59f94a9
permissions -rw-r--r--
cleaned up;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     1
(*  Title:      LatMorph.thy
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     4
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     5
Some lattice morphisms.
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     6
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     7
TODO:
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     8
  more morphisms (?)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
  more theorems
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    10
*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    11
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    12
LatMorph = LatInsts +
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    13
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    14
constdefs
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    15
  is_mono       :: "('a::le => 'b::le) => bool"
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    16
  "is_mono f == ALL x y. x [= y --> f x [= f y"
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    17
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    18
  is_inf_morph  :: "('a::lattice => 'b::lattice) => bool"
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    19
  "is_inf_morph f == ALL x y. f (x && y) = f x && f y"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    20
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    21
  is_sup_morph  :: "('a::lattice => 'b::lattice) => bool"
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    22
  "is_sup_morph f == ALL x y. f (x || y) = f x || f y"
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    23
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    24
  is_Inf_morph  :: "('a::clattice => 'b::clattice) => bool"
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    25
  "is_Inf_morph f == ALL A. f (Inf A) = Inf {f x |x. x:A}"
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    26
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    27
  is_Sup_morph  :: "('a::clattice => 'b::clattice) => bool"
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    28
  "is_Sup_morph f == ALL A. f (Sup A) = Sup {f x |x. x:A}"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    29
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    30
end