src/HOL/Library/Product_ord.thy
changeset 22177 515021e98684
parent 21458 475b321982f7
child 22483 86064f2f2188
     1.1 --- a/src/HOL/Library/Product_ord.thy	Thu Jan 25 09:32:35 2007 +0100
     1.2 +++ b/src/HOL/Library/Product_ord.thy	Thu Jan 25 09:32:36 2007 +0100
     1.3 @@ -10,11 +10,16 @@
     1.4  begin
     1.5  
     1.6  instance "*" :: (ord, ord) ord
     1.7 -  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x \<le> snd y)"
     1.8 -  prod_less_def: "(x < y) \<equiv> (fst x < fst y) | (fst x = fst y & snd x < snd y)" ..
     1.9 +  prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
    1.10 +  prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
    1.11  
    1.12  lemmas prod_ord_defs = prod_less_def prod_le_def
    1.13  
    1.14 +lemma [code func]:
    1.15 +  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    1.16 +  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
    1.17 +  unfolding prod_ord_defs by simp_all
    1.18 +
    1.19  lemma [code]:
    1.20    "(x1, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
    1.21    "(x1, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"