src/HOL/Library/Countable_Set.thy
author paulson
Tue, 26 May 2015 21:58:04 +0100
changeset 60303 00c06f1315d0
parent 60058 f17bb06599f6
child 60500 903bb1495239
permissions -rw-r--r--
New material about paths, and some lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     1
(*  Title:      HOL/Library/Countable_Set.thy
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     2
    Author:     Johannes Hölzl
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     3
    Author:     Andrei Popescu
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     4
*)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     5
58881
b9556a055632 modernized header;
wenzelm
parents: 57234
diff changeset
     6
section {* Countable sets *}
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     7
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
     8
theory Countable_Set
51542
738598beeb26 tuned imports;
wenzelm
parents: 50936
diff changeset
     9
imports Countable Infinite_Set
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    10
begin
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    11
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    12
subsection {* Predicate for countable sets *}
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    13
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    14
definition countable :: "'a set \<Rightarrow> bool" where
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    15
  "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    16
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    17
lemma countableE:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    18
  assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    19
  using S by (auto simp: countable_def)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    20
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    21
lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    22
  by (auto simp: countable_def)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    23
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    24
lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    25
  using comp_inj_on[of f S to_nat] by (auto intro: countableI)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    26
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    27
lemma countableE_bij:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    28
  assumes S: "countable S" obtains f :: "nat \<Rightarrow> 'a" and C :: "nat set" where "bij_betw f C S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    29
  using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    30
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    31
lemma countableI_bij: "bij_betw f (C::nat set) S \<Longrightarrow> countable S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    32
  by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    33
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    34
lemma countable_finite: "finite S \<Longrightarrow> countable S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    35
  by (blast dest: finite_imp_inj_to_nat_seg countableI)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    36
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    37
lemma countableI_bij1: "bij_betw f A B \<Longrightarrow> countable A \<Longrightarrow> countable B"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    38
  by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    39
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    40
lemma countableI_bij2: "bij_betw f B A \<Longrightarrow> countable A \<Longrightarrow> countable B"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    41
  by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    42
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    43
lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    44
  by (blast intro: countableI_bij1 countableI_bij2)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    45
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    46
lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    47
  by (auto simp: countable_def intro: subset_inj_on)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    48
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    49
lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    50
  using countableI[of to_nat A] by auto
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    51
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    52
subsection {* Enumerate a countable set *}
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    53
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    54
lemma countableE_infinite:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    55
  assumes "countable S" "infinite S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    56
  obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    57
proof -
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
    58
  obtain f :: "'a \<Rightarrow> nat" where "inj_on f S"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
    59
    using `countable S` by (rule countableE)
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    60
  then have "bij_betw f S (f`S)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    61
    unfolding bij_betw_def by simp
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    62
  moreover
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    63
  from `inj_on f S` `infinite S` have inf_fS: "infinite (f`S)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    64
    by (auto dest: finite_imageD)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    65
  then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    66
    by (intro bij_betw_the_inv_into bij_enumerate)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    67
  ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    68
    by (rule bij_betw_trans)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    69
  then show thesis ..
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    70
qed
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    71
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    72
lemma countable_enum_cases:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    73
  assumes "countable S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    74
  obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    75
        | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    76
  using ex_bij_betw_finite_nat[of S] countableE_infinite `countable S`
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    77
  by (cases "finite S") (auto simp add: atLeast0LessThan)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    78
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    79
definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    80
  "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    81
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    82
definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    83
  "from_nat_into S n = (if n \<in> to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\<in>S)"
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    84
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    85
lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    86
  using ex_bij_betw_finite_nat unfolding to_nat_on_def
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    87
  by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    88
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    89
lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    90
  using countableE_infinite unfolding to_nat_on_def
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    91
  by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
    92
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
    93
lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    94
  unfolding from_nat_into_def[abs_def]
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    95
  using to_nat_on_finite[of S]
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    96
  apply (subst bij_betw_cong)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    97
  apply (split split_if)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    98
  apply (simp add: bij_betw_def)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
    99
  apply (auto cong: bij_betw_cong
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   100
              intro: bij_betw_inv_into to_nat_on_finite)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   101
  done
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   102
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   103
lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   104
  unfolding from_nat_into_def[abs_def]
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   105
  using to_nat_on_infinite[of S, unfolded bij_betw_def]
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   106
  by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   107
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   108
lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   109
  using to_nat_on_infinite[of A] to_nat_on_finite[of A]
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   110
  by (cases "finite A") (auto simp: bij_betw_def)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   111
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   112
lemma to_nat_on_inj[simp]:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   113
  "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   114
  using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   115
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   116
lemma from_nat_into_to_nat_on[simp]: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   117
  by (auto simp: from_nat_into_def intro!: inv_into_f_f)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   118
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   119
lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   120
  by (auto intro: from_nat_into_to_nat_on[symmetric])
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   121
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   122
lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   123
  unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   124
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   125
lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   126
  using from_nat_into[of A] by auto
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   127
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   128
lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A"
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   129
  by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   130
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   131
lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   132
  using to_nat_on_infinite[of A] by (simp add: bij_betw_def)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   133
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   134
lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   135
  by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   136
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   137
lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   138
  by (simp add: f_inv_into_f from_nat_into_def)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   139
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   140
lemma to_nat_on_from_nat_into_infinite[simp]:
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   141
  "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   142
  by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   143
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   144
lemma from_nat_into_inj:
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   145
  "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   146
    from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   147
  by (subst to_nat_on_inj[symmetric, of A]) auto
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   149
lemma from_nat_into_inj_infinite[simp]:
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   150
  "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   151
  using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   152
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   153
lemma eq_from_nat_into_iff:
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   154
  "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> i \<in> to_nat_on A ` A \<Longrightarrow> x = from_nat_into A i \<longleftrightarrow> i = to_nat_on A x"
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   155
  by auto
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   156
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   157
lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   158
  by (rule exI[of _ "to_nat_on A a"]) simp
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   159
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   160
lemma from_nat_into_inject[simp]:
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   161
  "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   162
  by (metis range_from_nat_into)
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   163
50148
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   164
lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
b8cff6a8fda2 Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents: 50144
diff changeset
   165
  unfolding inj_on_def by auto
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   166
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   167
subsection {* Closure properties of countability *}
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   168
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   169
lemma countable_SIGMA[intro, simp]:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   170
  "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   171
  by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   172
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
   173
lemma countable_image[intro, simp]:
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
   174
  assumes "countable A"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
   175
  shows "countable (f`A)"
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   176
proof -
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
   177
  obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 51542
diff changeset
   178
    using assms by (rule countableE)
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   179
  moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   180
    by (auto intro: inj_on_inv_into inv_into_into)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   181
  ultimately show ?thesis
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   182
    by (blast dest: comp_inj_on subset_inj_on intro: countableI)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   183
qed
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   184
60303
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   185
lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   186
  by (metis countable_image the_inv_into_onto)
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   187
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   188
lemma countable_UN[intro, simp]:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   189
  fixes I :: "'i set" and A :: "'i => 'a set"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   190
  assumes I: "countable I"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   191
  assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   192
  shows "countable (\<Union>i\<in>I. A i)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   193
proof -
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   194
  have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   195
  then show ?thesis by (simp add: assms)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   196
qed
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   197
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   198
lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   199
  by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified])
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   200
     (simp split: bool.split)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   201
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   202
lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   203
  by (metis countable_Un countable_subset inf_sup_ord(3,4))
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   204
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   205
lemma countable_Plus[intro, simp]:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   206
  "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   207
  by (simp add: Plus_def)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   208
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   209
lemma countable_empty[intro, simp]: "countable {}"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   210
  by (blast intro: countable_finite)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   211
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   212
lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   213
  using countable_Un[of "{a}" A] by (auto simp: countable_finite)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   214
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   215
lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   216
  by (force intro: countable_subset)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   217
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   218
lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   219
  by (blast intro: countable_subset)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   220
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   221
lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   222
  by (blast intro: countable_subset)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   223
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   224
lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   225
  by (blast intro: countable_subset)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   226
60303
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   227
lemma countable_insert_eq [simp]: "countable (insert x A) = countable A"
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   228
    by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   229
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   230
lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   231
  by (metis Int_absorb2 assms countable_image image_vimage_eq)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   232
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   233
lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   234
  by (metis countable_vimage top_greatest)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   235
50144
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   236
lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}"
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   237
  by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)
885deccc264e renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents: 50134
diff changeset
   238
54410
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   239
lemma countable_Image:
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   240
  assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   241
  assumes "countable Y"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   242
  shows "countable (X `` Y)"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   243
proof -
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   244
  have "countable (X `` (\<Union>y\<in>Y. {y}))"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   245
    unfolding Image_UN by (intro countable_UN assms)
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   246
  then show ?thesis by simp
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   247
qed
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   248
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   249
lemma countable_relpow:
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   250
  fixes X :: "'a rel"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   251
  assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   252
  assumes Y: "countable Y"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   253
  shows "countable ((X ^^ i) `` Y)"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   254
  using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   255
60058
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   256
lemma countable_funpow:
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   257
  fixes f :: "'a set \<Rightarrow> 'a set"
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   258
  assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   259
  and "countable A"
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   260
  shows "countable ((f ^^ n) A)"
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   261
by(induction n)(simp_all add: assms)
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   262
54410
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   263
lemma countable_rtrancl:
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   264
  "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   265
  unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
0a578fb7fb73 countability of the image of a reflexive transitive closure
hoelzl
parents: 53381
diff changeset
   266
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   267
lemma countable_lists[intro, simp]:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   268
  assumes A: "countable A" shows "countable (lists A)"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   269
proof -
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   270
  have "countable (lists (range (from_nat_into A)))"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   271
    by (auto simp: lists_image)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   272
  with A show ?thesis
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   273
    by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   274
qed
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   275
50245
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50148
diff changeset
   276
lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50148
diff changeset
   277
  using finite_list by auto
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50148
diff changeset
   278
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50148
diff changeset
   279
lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50148
diff changeset
   280
  by (simp add: Collect_finite_eq_lists)
dea9363887a6 based countable topological basis on Countable_Set
immler
parents: 50148
diff changeset
   281
50936
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   282
lemma countable_rat: "countable \<rat>"
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   283
  unfolding Rats_def by auto
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   284
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   285
lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T"
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   286
  using finite_list by (auto simp: lists_eq_set)
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   287
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   288
lemma countable_Collect_finite_subset:
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   289
  "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   290
  unfolding Collect_finite_subset_eq_lists by auto
b28f258ebc1a countablility of finite subsets and rational numbers
hoelzl
parents: 50245
diff changeset
   291
60058
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   292
lemma countable_set_option [simp]: "countable (set_option x)"
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   293
by(cases x) auto
f17bb06599f6 add lemmas
Andreas Lochbihler
parents: 58881
diff changeset
   294
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   295
subsection {* Misc lemmas *}
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   296
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   297
lemma countable_all:
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   298
  assumes S: "countable S"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   299
  shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   300
  using S[THEN subset_range_from_nat_into] by auto
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   301
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   302
lemma finite_sequence_to_countable_set:
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   303
   assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   304
proof -  show thesis
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   305
    apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   306
    apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   307
  proof -
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   308
    fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   309
    with from_nat_into_surj[OF `countable X` `x \<in> X`]
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   310
    show False
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   311
      by auto
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   312
  qed
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   313
qed
e7fd64f82876 add various lemmas
hoelzl
parents: 54410
diff changeset
   314
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   315
subsection {* Uncountable *}
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   316
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   317
abbreviation uncountable where
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   318
  "uncountable A \<equiv> \<not> countable A"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   319
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   320
lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   321
  by (auto intro: inj_on_inv_into simp: countable_def)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   322
     (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   323
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   324
lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   325
  unfolding bij_betw_def by (metis countable_image)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   326
  
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   327
lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   328
  by (metis countable_finite)
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   329
  
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   330
lemma uncountable_minus_countable:
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   331
  "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   332
  using countable_Un[of B "A - B"] assms by auto
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   333
60303
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   334
lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   335
  by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
00c06f1315d0 New material about paths, and some lemmas
paulson
parents: 60058
diff changeset
   336
50134
13211e07d931 add Countable_Set theory
hoelzl
parents:
diff changeset
   337
end