# HG changeset patch
# User huffman
# Date 1323550096 -3600
# Node ID 2bee94cbae7250382bc979447cce9115abdb5839
# Parent  d26e933da5f0a9753200ab8766e54aecd24f9743
finite class instance for word type; remove unused lemmas

diff -r d26e933da5f0 -r 2bee94cbae72 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Dec 10 21:07:59 2011 +0100
+++ b/src/HOL/Word/Word.thy	Sat Dec 10 21:48:16 2011 +0100
@@ -2115,22 +2115,14 @@
 
 subsection "Cardinality, finiteness of set of words"
 
-lemmas card_lessThan' = card_lessThan [unfolded lessThan_def]
-
-lemmas card_eq =
-  word_unat.Abs_inj_on [THEN card_image, unfolded word_unat.image, unfolded unats_def]
-
-lemmas card_word = trans [OF card_eq card_lessThan']
-
-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)
-done
+instance word :: (len0) finite
+  by (default, simp add: type_definition.univ [OF type_definition_word])
+
+lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
+  by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
 
 lemma card_word_size: 
-  "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
+  "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"
 unfolding word_size by (rule card_word)