src/HOL/Library/Cardinality.thy
changeset 52147 9943f8067f11
parent 52143 36ffe23b25f8
child 53015 a1119cf551e8
equal deleted inserted replaced
52146:ceb31e1ded30 52147:9943f8067f11
    41 
    41 
    42 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    42 syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    43 
    43 
    44 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    44 translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    45 
    45 
    46 typed_print_translation {*
    46 print_translation {*
    47   let
    47   let
    48     fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    48     fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    49       Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    49       Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    50   in [(@{const_syntax card}, card_univ_tr')] end
    50   in [(@{const_syntax card}, card_univ_tr')] end
    51 *}
    51 *}
    52 
    52 
    53 lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"
    53 lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"