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