src/HOL/AxClasses/Lattice/OrdInsts.thy
author haftmann
Wed, 31 Oct 2007 10:10:50 +0100
changeset 25247 7bacd1798fc4
parent 2606 27cdd600a3b1
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     1
(*  Title:      OrdInsts.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 order instantiations.
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     6
*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     7
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     8
OrdInsts = OrdDefs +
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    10
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    11
(* binary / general products of quasi_orders / orders *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    12
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    13
instance
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    14
  "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    15
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    16
instance
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1440
diff changeset
    17
  "*" :: (partial_order, partial_order) partial_order   (le_prod_antisym)
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    18
  
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    19
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    20
instance
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    21
  fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    22
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    23
instance
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1440
diff changeset
    24
  fun :: (term, partial_order) partial_order            (le_fun_antisym)
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    25
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    26
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1440
diff changeset
    27
(* duals of quasi orders / partial orders / linear orders *)
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    28
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    29
instance
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    30
  dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    31
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    32
instance
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1440
diff changeset
    33
  dual :: (partial_order) partial_order                 (le_dual_antisym)
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    34
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    35
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    36
(*FIXME: had to be moved to LatInsts.thy due to some unpleasant
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    37
  'feature' in Pure/type.ML
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    38
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    39
instance
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1440
diff changeset
    40
  dual :: (linear_order) linear_order                   (le_dual_lin)
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    41
*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    42
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    43
end