Library/Product_ord: wellorder instance for products
authorhuffman
Mon Aug 08 08:55:49 2011 -0700 (2011-08-08)
changeset 440634588597ba37e
parent 44055 65cdd08bd7fd
child 44064 5bce8ff0d9ae
child 44082 81e55342cb86
Library/Product_ord: wellorder instance for products
src/HOL/Library/Product_ord.thy
     1.1 --- a/src/HOL/Library/Product_ord.thy	Mon Aug 08 13:48:38 2011 +0200
     1.2 +++ b/src/HOL/Library/Product_ord.thy	Mon Aug 08 08:55:49 2011 -0700
     1.3 @@ -71,4 +71,27 @@
     1.4  
     1.5  end
     1.6  
     1.7 +text {* A stronger version of the definition holds for partial orders. *}
     1.8 +
     1.9 +lemma prod_less_eq:
    1.10 +  fixes x y :: "'a::order \<times> 'b::ord"
    1.11 +  shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)"
    1.12 +  unfolding prod_less_def fst_conv snd_conv le_less by auto
    1.13 +
    1.14 +instance prod :: (wellorder, wellorder) wellorder
    1.15 +proof
    1.16 +  fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
    1.17 +  assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
    1.18 +  show "P z"
    1.19 +  proof (induct z)
    1.20 +    case (Pair a b)
    1.21 +    show "P (a, b)"
    1.22 +      apply (induct a arbitrary: b rule: less_induct)
    1.23 +      apply (rule less_induct [where 'a='b])
    1.24 +      apply (rule P)
    1.25 +      apply (auto simp add: prod_less_eq)
    1.26 +      done
    1.27 +  qed
    1.28 +qed
    1.29 +
    1.30  end