# HG changeset patch
# User Andreas Lochbihler
# Date 1361957610 -3600
# Node ID be7e9a675ec9f67f3a15ce6e65c8f4e950fe8447
# Parent  546a9a1c315d84f4a248104342efe335dc928700
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)

diff -r 546a9a1c315d -r be7e9a675ec9 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Mon Feb 25 20:55:48 2013 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Feb 27 10:33:30 2013 +0100
@@ -287,10 +287,9 @@
 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit0", standard, simp]
 declare eq_numeral_iff_iszero [where 'a="('a::finite) bit1", standard, simp]
 
-subsection {* Linorder instance *}
+subsection {* Order instances *}
 
 instantiation bit0 and bit1 :: (finite) linorder begin
-
 definition "a < b \<longleftrightarrow> Rep_bit0 a < Rep_bit0 b"
 definition "a \<le> b \<longleftrightarrow> Rep_bit0 a \<le> Rep_bit0 b"
 definition "a < b \<longleftrightarrow> Rep_bit1 a < Rep_bit1 b"
@@ -299,8 +298,23 @@
 instance
   by(intro_classes)
     (auto simp add: less_eq_bit0_def less_bit0_def less_eq_bit1_def less_bit1_def Rep_bit0_inject Rep_bit1_inject)
+end
 
-end
+lemma (in preorder) tranclp_less: "op <\<^sup>+\<^sup>+ = op <"
+by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)
+
+instance bit0 and bit1 :: (finite) wellorder
+proof -
+  have "wf {(x :: 'a bit0, y). x < y}"
+    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
+  thus "OFCLASS('a bit0, wellorder_class)"
+    by(rule wf_wellorderI) intro_classes
+next
+  have "wf {(x :: 'a bit1, y). x < y}"
+    by(auto simp add: trancl_def tranclp_less intro!: finite_acyclic_wf acyclicI)
+  thus "OFCLASS('a bit1, wellorder_class)"
+    by(rule wf_wellorderI) intro_classes
+qed
 
 subsection {* Code setup and type classes for code generation *}