# HG changeset patch
# User Andreas Lochbihler
# Date 1340867938 -7200
# Node ID d07a0b9601aaeb922e0b4c093fff86fcf05ba57d
# Parent  e97369f20c301c5541339b18a47f41699a311e11
instantiate card_UNIV with nibble and code_numeral

diff -r e97369f20c30 -r d07a0b9601aa src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu Jun 28 09:16:00 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Thu Jun 28 09:18:58 2012 +0200
@@ -208,6 +208,12 @@
 instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
 end
 
+instantiation code_numeral :: card_UNIV begin
+definition "card_UNIV = Phantom(code_numeral) 0"
+instance 
+  by(intro_classes)(auto simp add: card_UNIV_code_numeral_def type_definition.univ[OF type_definition_code_numeral] card_eq_0_iff dest!: finite_imageD intro: inj_onI)
+end
+
 instantiation list :: (type) card_UNIV begin
 definition "card_UNIV = Phantom('a list) 0"
 instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
@@ -223,6 +229,11 @@
 instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
 end
 
+instantiation nibble :: card_UNIV begin
+definition "card_UNIV = Phantom(nibble) 16"
+instance by(intro_classes)(simp add: card_UNIV_nibble_def card_nibble)
+end
+
 instantiation char :: card_UNIV begin
 definition "card_UNIV = Phantom(char) 256"
 instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)