src/HOL/Library/Product_ord.thy
author haftmann
Wed, 22 Nov 2006 10:20:18 +0100
changeset 21458 475b321982f7
parent 19736 d8d0f8f51d69
child 22177 515021e98684
permissions -rw-r--r--
added code lemmas
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
21458
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    12
instance "*" :: (ord, ord) ord
19736
wenzelm
parents: 17200
diff changeset
    13
  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
21458
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    14
  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" ..
15737
nipkow
parents:
diff changeset
    15
nipkow
parents:
diff changeset
    16
lemmas prod_ord_defs = prod_less_def prod_le_def
nipkow
parents:
diff changeset
    17
21458
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    18
lemma [code]:
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    19
  "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    20
  "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    21
  unfolding prod_ord_defs by simp_all
475b321982f7 added code lemmas
haftmann
parents: 19736
diff changeset
    22
19736
wenzelm
parents: 17200
diff changeset
    23
instance * :: (order, order) order
wenzelm
parents: 17200
diff changeset
    24
  by default (auto simp: prod_ord_defs intro: order_less_trans)
15737
nipkow
parents:
diff changeset
    25
19736
wenzelm
parents: 17200
diff changeset
    26
instance * :: (linorder, linorder) linorder
wenzelm
parents: 17200
diff changeset
    27
  by default (auto simp: prod_le_def)
15737
nipkow
parents:
diff changeset
    28
19736
wenzelm
parents: 17200
diff changeset
    29
end