src/HOL/Library/Numeral_Type.thy
changeset 48063 f02b4302d5dd
parent 47108 2a1953f0d20d
child 49834 b27bbb021df1
equal deleted inserted replaced
48054:60bcc6cf17d6 48063:f02b4302d5dd
    29   unfolding type_definition.card [OF type_definition_num0]
    29   unfolding type_definition.card [OF type_definition_num0]
    30   by simp
    30   by simp
    31 
    31 
    32 lemma card_num1 [simp]: "CARD(num1) = 1"
    32 lemma card_num1 [simp]: "CARD(num1) = 1"
    33   unfolding type_definition.card [OF type_definition_num1]
    33   unfolding type_definition.card [OF type_definition_num1]
    34   by (simp only: card_unit)
    34   by (simp only: card_UNIV_unit)
    35 
    35 
    36 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
    36 lemma card_bit0 [simp]: "CARD('a bit0) = 2 * CARD('a::finite)"
    37   unfolding type_definition.card [OF type_definition_bit0]
    37   unfolding type_definition.card [OF type_definition_bit0]
    38   by simp
    38   by simp
    39 
    39