src/HOL/Library/Product_ord.thy
changeset 25571 c9e39eafc7a0
parent 25502 9200b36280c0
child 25594 43c718438f9f
     1.1 --- a/src/HOL/Library/Product_ord.thy	Fri Dec 07 15:07:56 2007 +0100
     1.2 +++ b/src/HOL/Library/Product_ord.thy	Fri Dec 07 15:07:59 2007 +0100
     1.3 @@ -9,9 +9,18 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -instance "*" :: (ord, ord) ord
     1.8 +instantiation "*" :: (ord, ord) ord
     1.9 +begin
    1.10 +
    1.11 +definition
    1.12    prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
    1.13 -  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" ..
    1.14 +
    1.15 +definition
    1.16 +  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
    1.17 +
    1.18 +instance ..
    1.19 +
    1.20 +end
    1.21  
    1.22  lemma [code func]:
    1.23    "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    1.24 @@ -29,10 +38,19 @@
    1.25  instance * :: (linorder, linorder) linorder
    1.26    by default (auto simp: prod_le_def)
    1.27  
    1.28 -instance * :: (linorder, linorder) distrib_lattice
    1.29 +instantiation * :: (linorder, linorder) distrib_lattice
    1.30 +begin
    1.31 +
    1.32 +definition
    1.33    inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
    1.34 +
    1.35 +definition
    1.36    sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
    1.37 +
    1.38 +instance
    1.39    by intro_classes
    1.40      (auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
    1.41  
    1.42  end
    1.43 +
    1.44 +end