src/HOL/Library/Product_ord.thy
author wenzelm
Wed, 31 Aug 2005 15:46:37 +0200
changeset 17200 3a4d03d1a31b
parent 15737 c7e522520910
child 19736 d8d0f8f51d69
permissions -rw-r--r--
tuned presentation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15737
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/Product_ord.thy
nipkow
parents:
diff changeset
     2
    ID:         $Id$
nipkow
parents:
diff changeset
     3
    Author:     Norbert Voelker
nipkow
parents:
diff changeset
     4
*)
nipkow
parents:
diff changeset
     5
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
     6
header {* Order on product types *}
15737
nipkow
parents:
diff changeset
     7
nipkow
parents:
diff changeset
     8
theory Product_ord
nipkow
parents:
diff changeset
     9
imports Main
nipkow
parents:
diff changeset
    10
begin
nipkow
parents:
diff changeset
    11
nipkow
parents:
diff changeset
    12
instance "*" :: (ord,ord) ord ..
nipkow
parents:
diff changeset
    13
nipkow
parents:
diff changeset
    14
defs (overloaded)
nipkow
parents:
diff changeset
    15
  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)" 
nipkow
parents:
diff changeset
    16
  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
nipkow
parents:
diff changeset
    17
nipkow
parents:
diff changeset
    18
nipkow
parents:
diff changeset
    19
lemmas prod_ord_defs = prod_less_def prod_le_def
nipkow
parents:
diff changeset
    20
nipkow
parents:
diff changeset
    21
instance "*" :: (order,order) order 
nipkow
parents:
diff changeset
    22
  apply (intro_classes, unfold prod_ord_defs)
nipkow
parents:
diff changeset
    23
  by (auto intro: order_less_trans)
nipkow
parents:
diff changeset
    24
nipkow
parents:
diff changeset
    25
instance "*":: (linorder,linorder)linorder
nipkow
parents:
diff changeset
    26
  by (intro_classes, unfold prod_le_def, auto)
nipkow
parents:
diff changeset
    27
nipkow
parents:
diff changeset
    28
end