# HG changeset patch
# User huffman
# Date 1312818949 25200
# Node ID 4588597ba37e90d5d127bda445b643172359bfc5
# Parent  65cdd08bd7fd7631c510aa487e624cca2b2a441b
Library/Product_ord: wellorder instance for products

diff -r 65cdd08bd7fd -r 4588597ba37e src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Mon Aug 08 13:48:38 2011 +0200
+++ b/src/HOL/Library/Product_ord.thy	Mon Aug 08 08:55:49 2011 -0700
@@ -71,4 +71,27 @@
 
 end
 
+text {* A stronger version of the definition holds for partial orders. *}
+
+lemma prod_less_eq:
+  fixes x y :: "'a::order \<times> 'b::ord"
+  shows "x < y \<longleftrightarrow> fst x < fst y \<or> (fst x = fst y \<and> snd x < snd y)"
+  unfolding prod_less_def fst_conv snd_conv le_less by auto
+
+instance prod :: (wellorder, wellorder) wellorder
+proof
+  fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
+  assume P: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  show "P z"
+  proof (induct z)
+    case (Pair a b)
+    show "P (a, b)"
+      apply (induct a arbitrary: b rule: less_induct)
+      apply (rule less_induct [where 'a='b])
+      apply (rule P)
+      apply (auto simp add: prod_less_eq)
+      done
+  qed
+qed
+
 end