equal
deleted
inserted
replaced
42 *} |
42 *} |
43 |
43 |
44 lemma card_unit [simp]: "CARD(unit) = 1" |
44 lemma card_unit [simp]: "CARD(unit) = 1" |
45 unfolding UNIV_unit by simp |
45 unfolding UNIV_unit by simp |
46 |
46 |
47 lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a::finite) * CARD('b::finite)" |
47 lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)" |
48 unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) |
48 unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) |
49 |
49 |
50 lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" |
50 lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" |
51 unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus) |
51 unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus) |
52 |
52 |