src/HOL/Library/Cardinality.thy
 author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 47108 2a1953f0d20d child 47221 7205eb4a0a05 permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
 haftmann@37653 ` 1` ```(* Title: HOL/Library/Cardinality.thy ``` haftmann@29629 ` 2` ``` Author: Brian Huffman ``` kleing@24332 ` 3` ```*) ``` kleing@24332 ` 4` haftmann@37653 ` 5` ```header {* Cardinality of types *} ``` kleing@24332 ` 6` haftmann@37653 ` 7` ```theory Cardinality ``` huffman@47108 ` 8` ```imports "~~/src/HOL/Main" ``` kleing@24332 ` 9` ```begin ``` kleing@24332 ` 10` kleing@24332 ` 11` ```subsection {* Preliminary lemmas *} ``` kleing@24332 ` 12` ```(* These should be moved elsewhere *) ``` kleing@24332 ` 13` kleing@24332 ` 14` ```lemma (in type_definition) univ: ``` kleing@24332 ` 15` ``` "UNIV = Abs ` A" ``` kleing@24332 ` 16` ```proof ``` kleing@24332 ` 17` ``` show "Abs ` A \ UNIV" by (rule subset_UNIV) ``` kleing@24332 ` 18` ``` show "UNIV \ Abs ` A" ``` kleing@24332 ` 19` ``` proof ``` kleing@24332 ` 20` ``` fix x :: 'b ``` kleing@24332 ` 21` ``` have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) ``` kleing@24332 ` 22` ``` moreover have "Rep x \ A" by (rule Rep) ``` kleing@24332 ` 23` ``` ultimately show "x \ Abs ` A" by (rule image_eqI) ``` kleing@24332 ` 24` ``` qed ``` kleing@24332 ` 25` ```qed ``` kleing@24332 ` 26` kleing@24332 ` 27` ```lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" ``` kleing@24332 ` 28` ``` by (simp add: univ card_image inj_on_def Abs_inject) ``` kleing@24332 ` 29` kleing@24332 ` 30` kleing@24332 ` 31` ```subsection {* Cardinalities of types *} ``` kleing@24332 ` 32` kleing@24332 ` 33` ```syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") ``` kleing@24332 ` 34` wenzelm@35431 ` 35` ```translations "CARD('t)" => "CONST card (CONST UNIV \ 't set)" ``` kleing@24332 ` 36` wenzelm@42247 ` 37` ```typed_print_translation (advanced) {* ``` wenzelm@42247 ` 38` ``` let ``` wenzelm@42247 ` 39` ``` fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] = ``` wenzelm@42247 ` 40` ``` Syntax.const @{syntax_const "_type_card"} \$ Syntax_Phases.term_of_typ ctxt T; ``` wenzelm@42247 ` 41` ``` in [(@{const_syntax card}, card_univ_tr')] end ``` huffman@24407 ` 42` ```*} ``` huffman@24407 ` 43` huffman@30001 ` 44` ```lemma card_unit [simp]: "CARD(unit) = 1" ``` haftmann@26153 ` 45` ``` unfolding UNIV_unit by simp ``` kleing@24332 ` 46` huffman@30001 ` 47` ```lemma card_prod [simp]: "CARD('a \ 'b) = CARD('a::finite) * CARD('b::finite)" ``` haftmann@26153 ` 48` ``` unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) ``` kleing@24332 ` 49` huffman@30001 ` 50` ```lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" ``` haftmann@26153 ` 51` ``` unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus) ``` kleing@24332 ` 52` huffman@30001 ` 53` ```lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)" ``` nipkow@31080 ` 54` ``` unfolding UNIV_option_conv ``` kleing@24332 ` 55` ``` apply (subgoal_tac "(None::'a option) \ range Some") ``` huffman@29997 ` 56` ``` apply (simp add: card_image) ``` kleing@24332 ` 57` ``` apply fast ``` kleing@24332 ` 58` ``` done ``` kleing@24332 ` 59` huffman@30001 ` 60` ```lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" ``` haftmann@26153 ` 61` ``` unfolding Pow_UNIV [symmetric] ``` kleing@24332 ` 62` ``` by (simp only: card_Pow finite numeral_2_eq_2) ``` kleing@24332 ` 63` huffman@30001 ` 64` ```lemma card_nat [simp]: "CARD(nat) = 0" ``` huffman@44142 ` 65` ``` by (simp add: card_eq_0_iff) ``` huffman@30001 ` 66` huffman@30001 ` 67` huffman@30001 ` 68` ```subsection {* Classes with at least 1 and 2 *} ``` huffman@30001 ` 69` huffman@30001 ` 70` ```text {* Class finite already captures "at least 1" *} ``` huffman@30001 ` 71` huffman@30001 ` 72` ```lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)" ``` huffman@29997 ` 73` ``` unfolding neq0_conv [symmetric] by simp ``` huffman@29997 ` 74` huffman@30001 ` 75` ```lemma one_le_card_finite [simp]: "Suc 0 \ CARD('a::finite)" ``` huffman@30001 ` 76` ``` by (simp add: less_Suc_eq_le [symmetric]) ``` huffman@30001 ` 77` huffman@30001 ` 78` ```text {* Class for cardinality "at least 2" *} ``` huffman@30001 ` 79` huffman@30001 ` 80` ```class card2 = finite + ``` huffman@30001 ` 81` ``` assumes two_le_card: "2 \ CARD('a)" ``` huffman@30001 ` 82` huffman@30001 ` 83` ```lemma one_less_card: "Suc 0 < CARD('a::card2)" ``` huffman@30001 ` 84` ``` using two_le_card [where 'a='a] by simp ``` huffman@30001 ` 85` huffman@30001 ` 86` ```lemma one_less_int_card: "1 < int CARD('a::card2)" ``` huffman@30001 ` 87` ``` using one_less_card [where 'a='a] by simp ``` huffman@30001 ` 88` huffman@29997 ` 89` ```end ```