# HG changeset patch
# User huffman
# Date 1323550842 -3600
# Node ID 024947a0e4924cfc21cce04448cc2e80b9d19dfd
# Parent  2bee94cbae7250382bc979447cce9115abdb5839
prove class instances without extra lemmas

diff -r 2bee94cbae72 -r 024947a0e492 NEWS
--- 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.
diff -r 2bee94cbae72 -r 024947a0e492 src/HOL/Word/Word.thy
--- 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)"