--- a/src/HOL/Word/WordArith.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Word/WordArith.thy Sun Oct 21 14:53:44 2007 +0200
@@ -117,28 +117,28 @@
lemmas unat_eq_zero = unat_0_iff
lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
- by (simp add : neq0_conv unat_0_iff [symmetric])
+by (auto simp: unat_0_iff [symmetric])
lemma ucast_0 [simp] : "ucast 0 = 0"
- unfolding ucast_def
- by simp (simp add: word_0_wi)
+unfolding ucast_def
+by simp (simp add: word_0_wi)
lemma sint_0 [simp] : "sint 0 = 0"
- unfolding sint_uint
- by (simp add: Pls_def [symmetric])
+unfolding sint_uint
+by (simp add: Pls_def [symmetric])
lemma scast_0 [simp] : "scast 0 = 0"
- apply (unfold scast_def)
- apply simp
- apply (simp add: word_0_wi)
- done
+apply (unfold scast_def)
+apply simp
+apply (simp add: word_0_wi)
+done
lemma sint_n1 [simp] : "sint -1 = -1"
- apply (unfold word_m1_wi_Min)
- apply (simp add: word_sbin.eq_norm)
- apply (unfold Min_def number_of_eq)
- apply simp
- done
+apply (unfold word_m1_wi_Min)
+apply (simp add: word_sbin.eq_norm)
+apply (unfold Min_def number_of_eq)
+apply simp
+done
lemma scast_n1 [simp] : "scast -1 = -1"
apply (unfold scast_def sint_n1)
@@ -1242,15 +1242,15 @@
lemmas card_word = trans [OF card_eq card_lessThan', standard]
lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
- apply (rule contrapos_np)
- prefer 2
- apply (erule card_infinite)
- apply (simp add : card_word neq0_conv)
- done
+apply (rule contrapos_np)
+ prefer 2
+ apply (erule card_infinite)
+apply (simp add: card_word)
+done
lemma card_word_size:
"card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
- unfolding word_size by (rule card_word)
+unfolding word_size by (rule card_word)
end