--- a/src/HOL/Hilbert_Choice.thy Mon Aug 08 17:47:51 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Aug 09 11:57:24 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 (simp add: LeastM_def)
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 (simp add: GreatestM_def)
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 17:47:51 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy Tue Aug 09 11:57:24 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"
--- a/src/Pure/consts.ML Mon Aug 08 17:47:51 2016 +0200
+++ b/src/Pure/consts.ML Tue Aug 09 11:57:24 2016 +0200
@@ -83,8 +83,15 @@
Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs);
fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes =
- let val nets = map_filter (Symtab.lookup rev_abbrevs) modes
- in fn t => maps (fn net => Item_Net.retrieve_matching net t) nets end;
+ let val nets = map_filter (Symtab.lookup rev_abbrevs) modes in
+ fn t =>
+ let
+ val retrieve =
+ if Term.could_beta_eta_contract t
+ then Item_Net.retrieve
+ else Item_Net.retrieve_matching
+ in maps (fn net => retrieve net t) nets end
+ end;
(* dest consts *)