author wenzelm Mon, 08 Aug 2016 19:39:23 +0200 changeset 63631 2edc8da89edc parent 63627 6ddb43c6b711 (current diff) parent 63630 b2a6a1a49d39 (diff) child 63632 a59d9b81be24
merged
```--- a/src/HOL/Hilbert_Choice.thy	Mon Aug 08 14:13:14 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Aug 08 19:39:23 2016 +0200
@@ -68,7 +68,7 @@
lemma some_equality [intro]: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x = a) \<Longrightarrow> (SOME x. P x) = a"
by (blast intro: someI2)

-lemma some1_equality: "EX!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a"
+lemma some1_equality: "\<exists>!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a"
by blast

lemma some_eq_ex: "P (SOME x. P x) \<longleftrightarrow> (\<exists>x. P x)"
@@ -269,17 +269,18 @@
and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
shows "finite (UNIV :: 'a set)"
proof -
-  from fin have finb: "finite (UNIV :: 'b set)"
+  let ?UNIV_b = "UNIV :: 'b set"
+  from fin have "finite ?UNIV_b"
by (rule finite_fun_UNIVD2)
-  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
-    by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
-  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)"
-    by auto
-  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)"
-    by (auto simp add: card_Suc_eq)
-  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
+  with card have "card ?UNIV_b \<ge> Suc (Suc 0)"
+    by (cases "card ?UNIV_b") (auto simp: card_eq_0_iff)
+  then have "card ?UNIV_b = Suc (Suc (card ?UNIV_b - Suc (Suc 0)))"
+    by simp
+  then obtain b1 b2 :: 'b where b1b2: "b1 \<noteq> b2"
+    by (auto simp: card_Suc_eq)
+  from fin have fin': "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
by (rule finite_imageI)
-  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
+  have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
proof (rule UNIV_eq_I)
fix x :: 'a
from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1"
@@ -287,7 +288,7 @@
then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)"
by blast
qed
-  ultimately show "finite (UNIV :: 'a set)"
+  with fin' show ?thesis
by simp
qed

@@ -304,8 +305,8 @@
\<close>

lemma infinite_countable_subset:
-  assumes inf: "\<not> finite (S::'a set)"
-  shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
+  assumes inf: "\<not> finite S"
+  shows "\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S"
\<comment> \<open>Courtesy of Stephan Merz\<close>
proof -
define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
@@ -326,7 +327,7 @@
ultimately show ?thesis by blast
qed

-lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
+lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f::nat \<Rightarrow> 'a. inj f \<and> range f \<subseteq> S)"
\<comment> \<open>Courtesy of Stephan Merz\<close>
using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto

@@ -365,7 +366,7 @@

lemma inj_on_iff_surj:
assumes "A \<noteq> {}"
-  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
+  shows "(\<exists>f. inj_on f A \<and> f ` A \<subseteq> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
proof safe
fix f
assume inj: "inj_on f A" and incl: "f ` A \<subseteq> A'"
@@ -429,7 +430,7 @@
qed

lemma Ex_inj_on_UNION_Sigma:
-  "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i))"
+  "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i))"
proof
let ?phi = "\<lambda>a i. i \<in> I \<and> a \<in> A i"
let ?sm = "\<lambda>a. SOME i. ?phi a i"
@@ -439,9 +440,9 @@
moreover
have "?sm a \<in> I \<and> a \<in> A(?sm a)" if "i \<in> I" and "a \<in> A i" for i a
using that someI[of "?phi a" i] by auto
-  then have "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+  then have "?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)"
by auto
-  ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+  ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<subseteq> (SIGMA i : I. A i)"
by auto
qed

@@ -625,8 +626,8 @@
apply blast
done

-lemma LeastM_equality:
-  "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m k \<le> m x) \<Longrightarrow> m (LEAST x WRT m. P x) = (m k :: 'a::order)"
+lemma LeastM_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m k \<le> m x) \<Longrightarrow> m (LEAST x WRT m. P x) = m k"
+  for m :: "_ \<Rightarrow> 'a::order"
apply (rule LeastMI2)
apply assumption
apply blast
@@ -640,14 +641,16 @@
apply force
done

-lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> (m y :: nat))"
+lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
+  for m :: "'a \<Rightarrow> nat"
apply (simp only: pred_nat_trancl_eq_le [symmetric])
apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
apply assumption
done

-lemma LeastM_nat_lemma: "P k \<Longrightarrow> P (LeastM m P) \<and> (\<forall>y. P y \<longrightarrow> m (LeastM m P) \<le> (m y :: nat))"
+lemma LeastM_nat_lemma: "P k \<Longrightarrow> P (LeastM m P) \<and> (\<forall>y. P y \<longrightarrow> m (LeastM m P) \<le> m y)"
+  for m :: "'a \<Rightarrow> nat"
apply (rule someI_ex)
apply (erule ex_has_least_nat)
@@ -655,7 +658,8 @@

lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]

-lemma LeastM_nat_le: "P x \<Longrightarrow> m (LeastM m P) \<le> (m x :: nat)"
+lemma LeastM_nat_le: "P x \<Longrightarrow> m (LeastM m P) \<le> m x"
+  for m :: "'a \<Rightarrow> nat"
by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])

@@ -683,10 +687,8 @@
apply blast
done

-lemma GreatestM_equality:
-  "P k \<Longrightarrow>
-    (\<And>x. P x \<Longrightarrow> m x \<le> m k) \<Longrightarrow>
-    m (GREATEST x WRT m. P x) = (m k :: 'a::order)"
+lemma GreatestM_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m x \<le> m k) \<Longrightarrow> m (GREATEST x WRT m. P x) = m k"
+  for m :: "_ \<Rightarrow> 'a::order"
apply (rule GreatestMI2 [where m = m])
apply assumption
apply blast
@@ -701,11 +703,13 @@
done

lemma ex_has_greatest_nat_lemma:
-  "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> m y \<le> (m x :: nat)) \<Longrightarrow> \<exists>y. P y \<and> \<not> m y < m k + n"
+  "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> m y \<le> m x) \<Longrightarrow> \<exists>y. P y \<and> \<not> m y < m k + n"
+  for m :: "'a \<Rightarrow> nat"
by (induct n) (force simp: le_Suc_eq)+

lemma ex_has_greatest_nat:
-  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> (m x :: nat))"
+  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m x)"
+  for m :: "'a \<Rightarrow> nat"
apply (rule ccontr)
apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
apply (subgoal_tac [3] "m k \<le> b")
@@ -713,8 +717,8 @@
done

lemma GreatestM_nat_lemma:
-  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow>
-    P (GreatestM m P) \<and> (\<forall>y. P y \<longrightarrow> (m y :: nat) \<le> m (GreatestM m P))"
+  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> P (GreatestM m P) \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m (GreatestM m P))"
+  for m :: "'a \<Rightarrow> nat"
apply (rule someI_ex)
apply (erule ex_has_greatest_nat)
@@ -723,7 +727,8 @@

lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1]

-lemma GreatestM_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> (m x :: nat) \<le> m (GreatestM m P)"
+lemma GreatestM_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> m x \<le> m (GreatestM m P)"
+  for m :: "'a \<Rightarrow> nat"
by (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])

```
```--- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Mon Aug 08 14:13:14 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Mon Aug 08 19:39:23 2016 +0200
@@ -16,7 +16,7 @@
It is formalised in the Isabelle/Isar theorem proving system.

\<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
-  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective.
+  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that \<open>f\<close> is surjective.

\<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
Diagonalisation argument. The proof presented here is not this one.
@@ -28,7 +28,7 @@
interval is a subset of the last) is non-empty. We then assume a surjective
function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
range of \<open>f\<close> by generating a sequence of closed intervals then using the
-  NIP.
+  Nested Interval Property.
\<close>

theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"```