src/HOL/Library/Cardinality.thy
changeset 49689 b8a710806de9
parent 48176 3d9c1ddb9f47
child 49948 744934b818c7
equal deleted inserted replaced
49688:c517d900805a 49689:b8a710806de9
    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 (advanced) {*
    46 typed_print_translation (advanced) {*
    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)"
    54   unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    54   unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)