src/HOL/Library/Product_ord.thy
author wenzelm
Sat May 27 17:42:02 2006 +0200 (2006-05-27)
changeset 19736 d8d0f8f51d69
parent 17200 3a4d03d1a31b
child 21458 475b321982f7
permissions -rw-r--r--
tuned;
nipkow@15737
     1
(*  Title:      HOL/Library/Product_ord.thy
nipkow@15737
     2
    ID:         $Id$
nipkow@15737
     3
    Author:     Norbert Voelker
nipkow@15737
     4
*)
nipkow@15737
     5
wenzelm@17200
     6
header {* Order on product types *}
nipkow@15737
     7
nipkow@15737
     8
theory Product_ord
nipkow@15737
     9
imports Main
nipkow@15737
    10
begin
nipkow@15737
    11
wenzelm@19736
    12
instance "*" :: (ord, ord) ord ..
nipkow@15737
    13
nipkow@15737
    14
defs (overloaded)
wenzelm@19736
    15
  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
nipkow@15737
    16
  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)"
nipkow@15737
    17
nipkow@15737
    18
nipkow@15737
    19
lemmas prod_ord_defs = prod_less_def prod_le_def
nipkow@15737
    20
wenzelm@19736
    21
instance * :: (order, order) order
wenzelm@19736
    22
  by default (auto simp: prod_ord_defs intro: order_less_trans)
nipkow@15737
    23
wenzelm@19736
    24
instance * :: (linorder, linorder) linorder
wenzelm@19736
    25
  by default (auto simp: prod_le_def)
nipkow@15737
    26
wenzelm@19736
    27
end