# HG changeset patch
# User huffman
# Date 1325094635 -3600
# Node ID 272c63f83398b37124597ca4e4ad3b42e2e5465d
# Parent  0a29b51f0b0d8e2c4f1d6c9f861fee9c5fbd4b70
add lemma word_eq_iff

diff -r 0a29b51f0b0d -r 272c63f83398 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 28 18:33:03 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 28 18:50:35 2011 +0100
@@ -660,17 +660,16 @@
   apply fast
   done
 
-lemma word_eqI [rule_format] : 
+lemma word_eq_iff:
+  fixes x y :: "'a::len0 word"
+  shows "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
+  unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
+  by (metis test_bit_size [unfolded word_size])
+
+lemma word_eqI:
   fixes u :: "'a::len0 word"
   shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
-  apply (rule test_bit_eq_iff [THEN iffD1])
-  apply (rule ext)
-  apply (erule allE)
-  apply (erule impCE)
-   prefer 2
-   apply assumption
-  apply (auto dest!: test_bit_size simp add: word_size)
-  done
+  by (simp add: word_size word_eq_iff)
 
 lemma word_eqD: "(u::'a::len0 word) = v \<Longrightarrow> u !! x = v !! x"
   by simp