equal
deleted
inserted
replaced
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) |