src/HOL/Library/Product_ord.thy
author haftmann
Fri Mar 27 10:05:11 2009 +0100 (2009-03-27)
changeset 30738 0842e906300c
parent 28562 4e74209f113e
child 31040 996ae76c9eda
permissions -rw-r--r--
normalized imports
     1 (*  Title:      HOL/Library/Product_ord.thy
     2     Author:     Norbert Voelker
     3 *)
     4 
     5 header {* Order on product types *}
     6 
     7 theory Product_ord
     8 imports Main
     9 begin
    10 
    11 instantiation "*" :: (ord, ord) ord
    12 begin
    13 
    14 definition
    15   prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
    16 
    17 definition
    18   prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
    19 
    20 instance ..
    21 
    22 end
    23 
    24 lemma [code]:
    25   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    26   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
    27   unfolding prod_le_def prod_less_def by simp_all
    28 
    29 instance * :: (order, order) order
    30   by default (auto simp: prod_le_def prod_less_def intro: order_less_trans)
    31 
    32 instance * :: (linorder, linorder) linorder
    33   by default (auto simp: prod_le_def)
    34 
    35 instantiation * :: (linorder, linorder) distrib_lattice
    36 begin
    37 
    38 definition
    39   inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    40 
    41 definition
    42   sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    43 
    44 instance
    45   by intro_classes
    46     (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    47 
    48 end
    49 
    50 end