src/HOL/Library/Cardinality.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 42247 12fe41a92cd5
child 44142 8e27e0177518
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
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
haftmann@30663
     8
imports 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 \<subseteq> UNIV" by (rule subset_UNIV)
kleing@24332
    18
  show "UNIV \<subseteq> 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 \<in> A" by (rule Rep)
kleing@24332
    23
    ultimately show "x \<in> 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 \<Colon> '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 \<times> '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) \<notin> 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@30001
    65
  by (simp add: infinite_UNIV_nat 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 \<le> 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 \<le> 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