src/HOL/Library/Numeral_Type.thy
changeset 28920 4ed4b8b1988d
parent 27487 c8a6ce181805
child 29025 8c8859c0d734
equal deleted inserted replaced
28919:88b8cc1a2983 28920:4ed4b8b1988d
    50 
    50 
    51 subsection {* Cardinalities of types *}
    51 subsection {* Cardinalities of types *}
    52 
    52 
    53 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    53 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    54 
    54 
    55 translations "CARD(t)" => "CONST card (UNIV \<Colon> t set)"
    55 translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
    56 
    56 
    57 typed_print_translation {*
    57 typed_print_translation {*
    58 let
    58 let
    59   fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T]))] =
    59   fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
    60     Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
    60     Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
    61 in [("card", card_univ_tr')]
    61 in [(@{const_syntax card}, card_univ_tr')]
    62 end
    62 end
    63 *}
    63 *}
    64 
    64 
    65 lemma card_unit: "CARD(unit) = 1"
    65 lemma card_unit: "CARD(unit) = 1"
    66   unfolding UNIV_unit by simp
    66   unfolding UNIV_unit by simp
   239 
   239 
   240 subsection {* Examples *}
   240 subsection {* Examples *}
   241 
   241 
   242 lemma "CARD(0) = 0" by simp
   242 lemma "CARD(0) = 0" by simp
   243 lemma "CARD(17) = 17" by simp
   243 lemma "CARD(17) = 17" by simp
   244   
   244 
   245 end
   245 end