--- 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.
--- 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