# HG changeset patch
# User huffman
# Date 1321538866 -3600
# Node ID 94c37f3df10f431da463e820ff5741607c648c70
# Parent  6dd3e88de4c21bbc6c8fc245aa4fa4cb9f48ac22
HOL-Word: removed more duplicate theorems

diff -r 6dd3e88de4c2 -r 94c37f3df10f NEWS
--- a/NEWS	Thu Nov 17 14:52:05 2011 +0100
+++ b/NEWS	Thu Nov 17 15:07:46 2011 +0100
@@ -57,6 +57,10 @@
   word_mult_ac ~> mult_ac
   word_plus_ac0 ~> add_0_left add_0_right add_ac
   word_times_ac1 ~> mult_1_left mult_1_right mult_ac
+  word_order_trans ~> order_trans
+  word_order_refl ~> order_refl
+  word_order_antisym ~> order_antisym
+  word_order_linear ~> linorder_linear
 
 * Clarified attribute "mono_set": pure declararation without modifying
 the result of the fact expression.
diff -r 6dd3e88de4c2 -r 94c37f3df10f src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Nov 17 14:52:05 2011 +0100
+++ b/src/HOL/Word/Word.thy	Thu Nov 17 15:07:46 2011 +0100
@@ -199,7 +199,7 @@
 where
   "word_pred a = word_of_int (Int.pred (uint a))"
 
-instantiation word :: (len0) "{number, Divides.div, ord, comm_monoid_mult, comm_ring}"
+instantiation word :: (len0) "{number, Divides.div, comm_monoid_mult, comm_ring}"
 begin
 
 definition
@@ -229,12 +229,6 @@
 definition
   word_number_of_def: "number_of w = word_of_int w"
 
-definition
-  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
-
-definition
-  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
-
 lemmas word_arith_wis = 
   word_add_def word_mult_def word_minus_def 
   word_succ_def word_pred_def word_0_wi word_1_wi
@@ -316,6 +310,23 @@
 definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
   "a udvd b = (EX n>=0. uint b = n * uint a)"
 
+
+subsection "Ordering"
+
+instantiation word :: (len0) linorder
+begin
+
+definition
+  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
+
+definition
+  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
+
+instance
+  by default (auto simp: word_less_def word_le_def)
+
+end
+
 definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
   "a <=s b = (sint a <= sint b)"
 
@@ -1265,26 +1276,10 @@
 
 subsection "Order on fixed-length words"
 
-lemma word_order_trans: "x <= y \<Longrightarrow> y <= z \<Longrightarrow> x <= (z :: 'a :: len0 word)"
-  unfolding word_le_def by auto
-
-lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
-  unfolding word_le_def by auto
-
-lemma word_order_antisym: "x <= y \<Longrightarrow> y <= x \<Longrightarrow> x = (y :: 'a :: len0 word)"
-  unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
-
-lemma word_order_linear:
-  "y <= x | x <= (y :: 'a :: len0 word)"
-  unfolding word_le_def by auto
-
 lemma word_zero_le [simp] :
   "0 <= (y :: 'a :: len0 word)"
   unfolding word_le_def by auto
   
-instance word :: (len0) linorder
-  by intro_classes (auto simp: word_less_def word_le_def)
-
 lemma word_m1_ge [simp] : "word_pred 0 >= y"
   unfolding word_le_def
   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto