--- a/src/HOL/Cardinals/Fun_More.thy Thu Jan 16 16:50:41 2014 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy Thu Jan 16 18:26:41 2014 +0100
@@ -8,7 +8,7 @@
header {* More on Injections, Bijections and Inverses *}
theory Fun_More
-imports Fun_More_FP Main
+imports Main
begin
--- a/src/HOL/Cardinals/Fun_More_FP.thy Thu Jan 16 16:50:41 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,150 +0,0 @@
-(* Title: HOL/Cardinals/Fun_More_FP.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-More on injections, bijections and inverses (FP).
-*)
-
-header {* More on Injections, Bijections and Inverses (FP) *}
-
-theory Fun_More_FP
-imports Hilbert_Choice
-begin
-
-
-text {* This section proves more facts (additional to those in @{text "Fun.thy"},
-@{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}),
-mainly concerning injections, bijections, inverses and (numeric) cardinals of
-finite sets. *}
-
-
-subsection {* Properties involving finite and infinite sets *}
-
-
-lemma inj_on_finite:
-assumes "inj_on f A" "f ` A \<le> B" "finite B"
-shows "finite A"
-using assms by (metis finite_imageD finite_subset)
-
-
-lemma infinite_imp_bij_betw:
-assumes INF: "\<not> finite A"
-shows "\<exists>h. bij_betw h A (A - {a})"
-proof(cases "a \<in> A")
- assume Case1: "a \<notin> A" hence "A - {a} = A" by blast
- thus ?thesis using bij_betw_id[of A] by auto
-next
- assume Case2: "a \<in> A"
-find_theorems "\<not> finite _"
- have "\<not> finite (A - {a})" using INF by auto
- with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
- where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
- obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
- obtain A' where A'_def: "A' = g ` UNIV" by blast
- have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
- have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
- proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
- case_tac "x = 0", auto simp add: 2)
- fix y assume "a = (if y = 0 then a else f (Suc y))"
- thus "y = 0" using temp by (case_tac "y = 0", auto)
- next
- fix x y
- assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
- thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
- next
- fix n show "f (Suc n) \<in> A" using 2 by blast
- qed
- hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
- using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
- hence 5: "bij_betw (inv g) A' UNIV"
- by (auto simp add: bij_betw_inv_into)
- (* *)
- obtain n where "g n = a" using 3 by auto
- hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
- using 3 4 unfolding A'_def
- by clarify (rule bij_betw_subset, auto simp: image_set_diff)
- (* *)
- obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
- have 7: "bij_betw v UNIV (UNIV - {n})"
- proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
- fix m1 m2 assume "v m1 = v m2"
- thus "m1 = m2"
- by(case_tac "m1 < n", case_tac "m2 < n",
- auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
- next
- show "v ` UNIV = UNIV - {n}"
- proof(auto simp add: v_def)
- fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
- {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
- then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
- with 71 have "n \<le> m'" by auto
- with 72 ** have False by auto
- }
- thus "m < n" by force
- qed
- qed
- (* *)
- obtain h' where h'_def: "h' = g o v o (inv g)" by blast
- hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
- by (auto simp add: bij_betw_trans)
- (* *)
- obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
- have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
- hence "bij_betw h A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
- moreover
- {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
- hence "bij_betw h (A - A') (A - A')"
- using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
- }
- moreover
- have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
- ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
- using 4 by blast
- ultimately have "bij_betw h A (A - {a})"
- using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
- thus ?thesis by blast
-qed
-
-
-lemma infinite_imp_bij_betw2:
-assumes INF: "\<not> finite A"
-shows "\<exists>h. bij_betw h A (A \<union> {a})"
-proof(cases "a \<in> A")
- assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast
- thus ?thesis using bij_betw_id[of A] by auto
-next
- let ?A' = "A \<union> {a}"
- assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
- moreover have "\<not> finite ?A'" using INF by auto
- ultimately obtain f where "bij_betw f ?A' A"
- using infinite_imp_bij_betw[of ?A' a] by auto
- hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
- thus ?thesis by auto
-qed
-
-
-subsection {* Properties involving Hilbert choice *}
-
-
-lemma bij_betw_inv_into_left:
-assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
-shows "(inv_into A f) (f a) = a"
-using assms unfolding bij_betw_def
-by clarify (rule inv_into_f_f)
-
-lemma bij_betw_inv_into_right:
-assumes "bij_betw f A A'" "a' \<in> A'"
-shows "f(inv_into A f a') = a'"
-using assms unfolding bij_betw_def using f_inv_into_f by force
-
-
-lemma bij_betw_inv_into_subset:
-assumes BIJ: "bij_betw f A A'" and
- SUB: "B \<le> A" and IM: "f ` B = B'"
-shows "bij_betw (inv_into A f) B' B"
-using assms unfolding bij_betw_def
-by (auto intro: inj_on_inv_into)
-
-
-
-end
--- a/src/HOL/Cardinals/README.txt Thu Jan 16 16:50:41 2014 +0100
+++ b/src/HOL/Cardinals/README.txt Thu Jan 16 18:26:41 2014 +0100
@@ -149,7 +149,7 @@
Notes for anyone who would like to enrich these theories in the future
--------------------------------------------------------------------------------------
-Theory Fun_More (and Fun_More_FP):
+Theory Fun_More:
- Careful: "inj" is an abbreviation for "inj_on UNIV", while
"bij" is not an abreviation for "bij_betw UNIV UNIV", but
a defined constant; there is no "surj_betw", but only "surj".
--- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 16:50:41 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 18:26:41 2014 +0100
@@ -8,7 +8,7 @@
header {* Well-Order Embeddings (FP) *}
theory Wellorder_Embedding_FP
-imports Zorn Fun_More_FP Wellorder_Relation_FP
+imports Zorn Wellorder_Relation_FP
begin
--- a/src/HOL/Finite_Set.thy Thu Jan 16 16:50:41 2014 +0100
+++ b/src/HOL/Finite_Set.thy Thu Jan 16 18:26:41 2014 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Finite_Set.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
- with contributions by Jeremy Avigad
+ with contributions by Jeremy Avigad and Andrei Popescu
*)
header {* Finite sets *}
@@ -1575,6 +1575,11 @@
using assms unfolding bij_betw_def
using finite_imageD[of f A] by auto
+lemma inj_on_finite:
+assumes "inj_on f A" "f ` A \<le> B" "finite B"
+shows "finite A"
+using assms finite_imageD finite_subset by blast
+
subsubsection {* Pigeonhole Principles *}
--- a/src/HOL/Hilbert_Choice.thy Thu Jan 16 16:50:41 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy Thu Jan 16 18:26:41 2014 +0100
@@ -827,6 +827,121 @@
using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
+subsection {* More on injections, bijections, and inverses *}
+
+lemma infinite_imp_bij_betw:
+assumes INF: "\<not> finite A"
+shows "\<exists>h. bij_betw h A (A - {a})"
+proof(cases "a \<in> A")
+ assume Case1: "a \<notin> A" hence "A - {a} = A" by blast
+ thus ?thesis using bij_betw_id[of A] by auto
+next
+ assume Case2: "a \<in> A"
+find_theorems "\<not> finite _"
+ have "\<not> finite (A - {a})" using INF by auto
+ with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
+ where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
+ obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
+ obtain A' where A'_def: "A' = g ` UNIV" by blast
+ have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
+ have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
+ proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
+ case_tac "x = 0", auto simp add: 2)
+ fix y assume "a = (if y = 0 then a else f (Suc y))"
+ thus "y = 0" using temp by (case_tac "y = 0", auto)
+ next
+ fix x y
+ assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
+ thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
+ next
+ fix n show "f (Suc n) \<in> A" using 2 by blast
+ qed
+ hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
+ using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
+ hence 5: "bij_betw (inv g) A' UNIV"
+ by (auto simp add: bij_betw_inv_into)
+ (* *)
+ obtain n where "g n = a" using 3 by auto
+ hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
+ using 3 4 unfolding A'_def
+ by clarify (rule bij_betw_subset, auto simp: image_set_diff)
+ (* *)
+ obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
+ have 7: "bij_betw v UNIV (UNIV - {n})"
+ proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
+ fix m1 m2 assume "v m1 = v m2"
+ thus "m1 = m2"
+ by(case_tac "m1 < n", case_tac "m2 < n",
+ auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
+ next
+ show "v ` UNIV = UNIV - {n}"
+ proof(auto simp add: v_def)
+ fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
+ {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
+ then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
+ with 71 have "n \<le> m'" by auto
+ with 72 ** have False by auto
+ }
+ thus "m < n" by force
+ qed
+ qed
+ (* *)
+ obtain h' where h'_def: "h' = g o v o (inv g)" by blast
+ hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
+ by (auto simp add: bij_betw_trans)
+ (* *)
+ obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
+ have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
+ hence "bij_betw h A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
+ moreover
+ {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
+ hence "bij_betw h (A - A') (A - A')"
+ using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
+ }
+ moreover
+ have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
+ ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
+ using 4 by blast
+ ultimately have "bij_betw h A (A - {a})"
+ using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
+ thus ?thesis by blast
+qed
+
+lemma infinite_imp_bij_betw2:
+assumes INF: "\<not> finite A"
+shows "\<exists>h. bij_betw h A (A \<union> {a})"
+proof(cases "a \<in> A")
+ assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast
+ thus ?thesis using bij_betw_id[of A] by auto
+next
+ let ?A' = "A \<union> {a}"
+ assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
+ moreover have "\<not> finite ?A'" using INF by auto
+ ultimately obtain f where "bij_betw f ?A' A"
+ using infinite_imp_bij_betw[of ?A' a] by auto
+ hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
+ thus ?thesis by auto
+qed
+
+lemma bij_betw_inv_into_left:
+assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
+shows "(inv_into A f) (f a) = a"
+using assms unfolding bij_betw_def
+by clarify (rule inv_into_f_f)
+
+lemma bij_betw_inv_into_right:
+assumes "bij_betw f A A'" "a' \<in> A'"
+shows "f(inv_into A f a') = a'"
+using assms unfolding bij_betw_def using f_inv_into_f by force
+
+lemma bij_betw_inv_into_subset:
+assumes BIJ: "bij_betw f A A'" and
+ SUB: "B \<le> A" and IM: "f ` B = B'"
+shows "bij_betw (inv_into A f) B' B"
+using assms unfolding bij_betw_def
+by (auto intro: inj_on_inv_into)
+
+
subsection {* Specification package -- Hilbertized version *}
lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"