--- a/NEWS Sat Dec 10 21:48:16 2011 +0100
+++ b/NEWS Sat Dec 10 22:00:42 2011 +0100
@@ -89,6 +89,8 @@
word_order_refl ~> order_refl
word_order_antisym ~> order_antisym
word_order_linear ~> linorder_linear
+ lenw1_zero_neq_one ~> zero_neq_one
+ word_number_of_eq ~> number_of_eq
* Clarified attribute "mono_set": pure declararation without modifying
the result of the fact expression.
--- a/src/HOL/Word/Word.thy Sat Dec 10 21:48:16 2011 +0100
+++ b/src/HOL/Word/Word.thy Sat Dec 10 22:00:42 2011 +0100
@@ -280,14 +280,13 @@
end
-lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
- unfolding word_arith_wis
- by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
-
-lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
-
instance word :: (len) comm_ring_1
- by (intro_classes) (simp add: lenw1_zero_neq_one)
+proof
+ have "0 < len_of TYPE('a)" by (rule len_gt_0)
+ then show "(0::'a word) \<noteq> 1"
+ unfolding word_0_wi word_1_wi
+ by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+qed
lemma word_of_nat: "of_nat n = word_of_int (int n)"
by (induct n) (auto simp add : word_of_int_hom_syms)
@@ -298,12 +297,8 @@
apply (simp add: word_of_nat word_of_int_sub_hom)
done
-lemma word_number_of_eq:
- "number_of w = (of_int w :: 'a :: len word)"
- unfolding word_number_of_def word_of_int by auto
-
instance word :: (len) number_ring
- by (intro_classes) (simp add : word_number_of_eq)
+ by (default, simp add: word_number_of_def word_of_int)
definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
"a udvd b = (EX n>=0. uint b = n * uint a)"