instantiate card_UNIV with nibble and code_numeral
authorAndreas Lochbihler
Thu Jun 28 09:18:58 2012 +0200 (2012-06-28)
changeset 48165d07a0b9601aa
parent 48164 e97369f20c30
child 48166 1bee47c0c278
child 48167 da1a1eae93fa
child 48175 fea68365c975
instantiate card_UNIV with nibble and code_numeral
src/HOL/Library/Cardinality.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Thu Jun 28 09:16:00 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Thu Jun 28 09:18:58 2012 +0200
     1.3 @@ -208,6 +208,12 @@
     1.4  instance by intro_classes (simp add: card_UNIV_int_def infinite_UNIV_int)
     1.5  end
     1.6  
     1.7 +instantiation code_numeral :: card_UNIV begin
     1.8 +definition "card_UNIV = Phantom(code_numeral) 0"
     1.9 +instance 
    1.10 +  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)
    1.11 +end
    1.12 +
    1.13  instantiation list :: (type) card_UNIV begin
    1.14  definition "card_UNIV = Phantom('a list) 0"
    1.15  instance by intro_classes (simp add: card_UNIV_list_def infinite_UNIV_listI)
    1.16 @@ -223,6 +229,11 @@
    1.17  instance by(intro_classes)(simp add: card_UNIV_bool_def card_UNIV_bool)
    1.18  end
    1.19  
    1.20 +instantiation nibble :: card_UNIV begin
    1.21 +definition "card_UNIV = Phantom(nibble) 16"
    1.22 +instance by(intro_classes)(simp add: card_UNIV_nibble_def card_nibble)
    1.23 +end
    1.24 +
    1.25  instantiation char :: card_UNIV begin
    1.26  definition "card_UNIV = Phantom(char) 256"
    1.27  instance by intro_classes (simp add: card_UNIV_char_def card_UNIV_char)