dissolved 'Fun_More_FP' (a BNF dependency)
authorblanchet
Thu Jan 16 18:26:41 2014 +0100 (2014-01-16)
changeset 5502096b05fd2aee4
parent 55019 0d5e831175de
child 55021 e40090032de9
dissolved 'Fun_More_FP' (a BNF dependency)
src/HOL/Cardinals/Fun_More.thy
src/HOL/Cardinals/Fun_More_FP.thy
src/HOL/Cardinals/README.txt
src/HOL/Cardinals/Wellorder_Embedding_FP.thy
src/HOL/Finite_Set.thy
src/HOL/Hilbert_Choice.thy
     1.1 --- a/src/HOL/Cardinals/Fun_More.thy	Thu Jan 16 16:50:41 2014 +0100
     1.2 +++ b/src/HOL/Cardinals/Fun_More.thy	Thu Jan 16 18:26:41 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* More on Injections, Bijections and Inverses *}
     1.5  
     1.6  theory Fun_More
     1.7 -imports Fun_More_FP Main
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  
     2.1 --- a/src/HOL/Cardinals/Fun_More_FP.thy	Thu Jan 16 16:50:41 2014 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,150 +0,0 @@
     2.4 -(*  Title:      HOL/Cardinals/Fun_More_FP.thy
     2.5 -    Author:     Andrei Popescu, TU Muenchen
     2.6 -    Copyright   2012
     2.7 -
     2.8 -More on injections, bijections and inverses (FP).
     2.9 -*)
    2.10 -
    2.11 -header {* More on Injections, Bijections and Inverses (FP) *}
    2.12 -
    2.13 -theory Fun_More_FP
    2.14 -imports Hilbert_Choice
    2.15 -begin
    2.16 -
    2.17 -
    2.18 -text {* This section proves more facts (additional to those in @{text "Fun.thy"},
    2.19 -@{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}),
    2.20 -mainly concerning injections, bijections, inverses and (numeric) cardinals of
    2.21 -finite sets. *}
    2.22 -
    2.23 -
    2.24 -subsection {* Properties involving finite and infinite sets *}
    2.25 -
    2.26 -
    2.27 -lemma inj_on_finite:
    2.28 -assumes "inj_on f A" "f ` A \<le> B" "finite B"
    2.29 -shows "finite A"
    2.30 -using assms by (metis finite_imageD finite_subset)
    2.31 -
    2.32 -
    2.33 -lemma infinite_imp_bij_betw:
    2.34 -assumes INF: "\<not> finite A"
    2.35 -shows "\<exists>h. bij_betw h A (A - {a})"
    2.36 -proof(cases "a \<in> A")
    2.37 -  assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
    2.38 -  thus ?thesis using bij_betw_id[of A] by auto
    2.39 -next
    2.40 -  assume Case2: "a \<in> A"
    2.41 -find_theorems "\<not> finite _"
    2.42 -  have "\<not> finite (A - {a})" using INF by auto
    2.43 -  with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
    2.44 -  where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
    2.45 -  obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
    2.46 -  obtain A' where A'_def: "A' = g ` UNIV" by blast
    2.47 -  have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
    2.48 -  have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
    2.49 -  proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
    2.50 -        case_tac "x = 0", auto simp add: 2)
    2.51 -    fix y  assume "a = (if y = 0 then a else f (Suc y))"
    2.52 -    thus "y = 0" using temp by (case_tac "y = 0", auto)
    2.53 -  next
    2.54 -    fix x y
    2.55 -    assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
    2.56 -    thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
    2.57 -  next
    2.58 -    fix n show "f (Suc n) \<in> A" using 2 by blast
    2.59 -  qed
    2.60 -  hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
    2.61 -  using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
    2.62 -  hence 5: "bij_betw (inv g) A' UNIV"
    2.63 -  by (auto simp add: bij_betw_inv_into)
    2.64 -  (*  *)
    2.65 -  obtain n where "g n = a" using 3 by auto
    2.66 -  hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
    2.67 -  using 3 4 unfolding A'_def
    2.68 -  by clarify (rule bij_betw_subset, auto simp: image_set_diff)
    2.69 -  (*  *)
    2.70 -  obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
    2.71 -  have 7: "bij_betw v UNIV (UNIV - {n})"
    2.72 -  proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
    2.73 -    fix m1 m2 assume "v m1 = v m2"
    2.74 -    thus "m1 = m2"
    2.75 -    by(case_tac "m1 < n", case_tac "m2 < n",
    2.76 -       auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
    2.77 -  next
    2.78 -    show "v ` UNIV = UNIV - {n}"
    2.79 -    proof(auto simp add: v_def)
    2.80 -      fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
    2.81 -      {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
    2.82 -       then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
    2.83 -       with 71 have "n \<le> m'" by auto
    2.84 -       with 72 ** have False by auto
    2.85 -      }
    2.86 -      thus "m < n" by force
    2.87 -    qed
    2.88 -  qed
    2.89 -  (*  *)
    2.90 -  obtain h' where h'_def: "h' = g o v o (inv g)" by blast
    2.91 -  hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
    2.92 -  by (auto simp add: bij_betw_trans)
    2.93 -  (*  *)
    2.94 -  obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
    2.95 -  have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
    2.96 -  hence "bij_betw h  A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
    2.97 -  moreover
    2.98 -  {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
    2.99 -   hence "bij_betw h  (A - A') (A - A')"
   2.100 -   using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
   2.101 -  }
   2.102 -  moreover
   2.103 -  have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
   2.104 -        ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
   2.105 -  using 4 by blast
   2.106 -  ultimately have "bij_betw h A (A - {a})"
   2.107 -  using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
   2.108 -  thus ?thesis by blast
   2.109 -qed
   2.110 -
   2.111 -
   2.112 -lemma infinite_imp_bij_betw2:
   2.113 -assumes INF: "\<not> finite A"
   2.114 -shows "\<exists>h. bij_betw h A (A \<union> {a})"
   2.115 -proof(cases "a \<in> A")
   2.116 -  assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
   2.117 -  thus ?thesis using bij_betw_id[of A] by auto
   2.118 -next
   2.119 -  let ?A' = "A \<union> {a}"
   2.120 -  assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
   2.121 -  moreover have "\<not> finite ?A'" using INF by auto
   2.122 -  ultimately obtain f where "bij_betw f ?A' A"
   2.123 -  using infinite_imp_bij_betw[of ?A' a] by auto
   2.124 -  hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
   2.125 -  thus ?thesis by auto
   2.126 -qed
   2.127 -
   2.128 -
   2.129 -subsection {* Properties involving Hilbert choice *}
   2.130 -
   2.131 -
   2.132 -lemma bij_betw_inv_into_left:
   2.133 -assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
   2.134 -shows "(inv_into A f) (f a) = a"
   2.135 -using assms unfolding bij_betw_def
   2.136 -by clarify (rule inv_into_f_f)
   2.137 -
   2.138 -lemma bij_betw_inv_into_right:
   2.139 -assumes "bij_betw f A A'" "a' \<in> A'"
   2.140 -shows "f(inv_into A f a') = a'"
   2.141 -using assms unfolding bij_betw_def using f_inv_into_f by force
   2.142 -
   2.143 -
   2.144 -lemma bij_betw_inv_into_subset:
   2.145 -assumes BIJ: "bij_betw f A A'" and
   2.146 -        SUB: "B \<le> A" and IM: "f ` B = B'"
   2.147 -shows "bij_betw (inv_into A f) B' B"
   2.148 -using assms unfolding bij_betw_def
   2.149 -by (auto intro: inj_on_inv_into)
   2.150 -
   2.151 -
   2.152 -
   2.153 -end
     3.1 --- a/src/HOL/Cardinals/README.txt	Thu Jan 16 16:50:41 2014 +0100
     3.2 +++ b/src/HOL/Cardinals/README.txt	Thu Jan 16 18:26:41 2014 +0100
     3.3 @@ -149,7 +149,7 @@
     3.4  Notes for anyone who would like to enrich these theories in the future
     3.5  --------------------------------------------------------------------------------------
     3.6  
     3.7 -Theory Fun_More (and Fun_More_FP):
     3.8 +Theory Fun_More:
     3.9  - Careful: "inj" is an abbreviation for "inj_on UNIV", while  
    3.10    "bij" is not an abreviation for "bij_betw UNIV UNIV", but 
    3.11    a defined constant; there is no "surj_betw", but only "surj". 
     4.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Thu Jan 16 16:50:41 2014 +0100
     4.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy	Thu Jan 16 18:26:41 2014 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  header {* Well-Order Embeddings (FP) *}
     4.5  
     4.6  theory Wellorder_Embedding_FP
     4.7 -imports Zorn Fun_More_FP Wellorder_Relation_FP
     4.8 +imports Zorn Wellorder_Relation_FP
     4.9  begin
    4.10  
    4.11  
     5.1 --- a/src/HOL/Finite_Set.thy	Thu Jan 16 16:50:41 2014 +0100
     5.2 +++ b/src/HOL/Finite_Set.thy	Thu Jan 16 18:26:41 2014 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  (*  Title:      HOL/Finite_Set.thy
     5.5      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     5.6 -                with contributions by Jeremy Avigad
     5.7 +                with contributions by Jeremy Avigad and Andrei Popescu
     5.8  *)
     5.9  
    5.10  header {* Finite sets *}
    5.11 @@ -1575,6 +1575,11 @@
    5.12  using assms unfolding bij_betw_def
    5.13  using finite_imageD[of f A] by auto
    5.14  
    5.15 +lemma inj_on_finite:
    5.16 +assumes "inj_on f A" "f ` A \<le> B" "finite B"
    5.17 +shows "finite A"
    5.18 +using assms finite_imageD finite_subset by blast
    5.19 +
    5.20  
    5.21  subsubsection {* Pigeonhole Principles *}
    5.22  
     6.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Jan 16 16:50:41 2014 +0100
     6.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jan 16 18:26:41 2014 +0100
     6.3 @@ -827,6 +827,121 @@
     6.4    using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
     6.5  
     6.6  
     6.7 +subsection {* More on injections, bijections, and inverses *}
     6.8 +
     6.9 +lemma infinite_imp_bij_betw:
    6.10 +assumes INF: "\<not> finite A"
    6.11 +shows "\<exists>h. bij_betw h A (A - {a})"
    6.12 +proof(cases "a \<in> A")
    6.13 +  assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
    6.14 +  thus ?thesis using bij_betw_id[of A] by auto
    6.15 +next
    6.16 +  assume Case2: "a \<in> A"
    6.17 +find_theorems "\<not> finite _"
    6.18 +  have "\<not> finite (A - {a})" using INF by auto
    6.19 +  with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
    6.20 +  where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
    6.21 +  obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
    6.22 +  obtain A' where A'_def: "A' = g ` UNIV" by blast
    6.23 +  have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
    6.24 +  have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
    6.25 +  proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
    6.26 +        case_tac "x = 0", auto simp add: 2)
    6.27 +    fix y  assume "a = (if y = 0 then a else f (Suc y))"
    6.28 +    thus "y = 0" using temp by (case_tac "y = 0", auto)
    6.29 +  next
    6.30 +    fix x y
    6.31 +    assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
    6.32 +    thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
    6.33 +  next
    6.34 +    fix n show "f (Suc n) \<in> A" using 2 by blast
    6.35 +  qed
    6.36 +  hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
    6.37 +  using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
    6.38 +  hence 5: "bij_betw (inv g) A' UNIV"
    6.39 +  by (auto simp add: bij_betw_inv_into)
    6.40 +  (*  *)
    6.41 +  obtain n where "g n = a" using 3 by auto
    6.42 +  hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
    6.43 +  using 3 4 unfolding A'_def
    6.44 +  by clarify (rule bij_betw_subset, auto simp: image_set_diff)
    6.45 +  (*  *)
    6.46 +  obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
    6.47 +  have 7: "bij_betw v UNIV (UNIV - {n})"
    6.48 +  proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
    6.49 +    fix m1 m2 assume "v m1 = v m2"
    6.50 +    thus "m1 = m2"
    6.51 +    by(case_tac "m1 < n", case_tac "m2 < n",
    6.52 +       auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
    6.53 +  next
    6.54 +    show "v ` UNIV = UNIV - {n}"
    6.55 +    proof(auto simp add: v_def)
    6.56 +      fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
    6.57 +      {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
    6.58 +       then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
    6.59 +       with 71 have "n \<le> m'" by auto
    6.60 +       with 72 ** have False by auto
    6.61 +      }
    6.62 +      thus "m < n" by force
    6.63 +    qed
    6.64 +  qed
    6.65 +  (*  *)
    6.66 +  obtain h' where h'_def: "h' = g o v o (inv g)" by blast
    6.67 +  hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
    6.68 +  by (auto simp add: bij_betw_trans)
    6.69 +  (*  *)
    6.70 +  obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
    6.71 +  have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
    6.72 +  hence "bij_betw h  A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
    6.73 +  moreover
    6.74 +  {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
    6.75 +   hence "bij_betw h  (A - A') (A - A')"
    6.76 +   using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
    6.77 +  }
    6.78 +  moreover
    6.79 +  have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
    6.80 +        ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
    6.81 +  using 4 by blast
    6.82 +  ultimately have "bij_betw h A (A - {a})"
    6.83 +  using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
    6.84 +  thus ?thesis by blast
    6.85 +qed
    6.86 +
    6.87 +lemma infinite_imp_bij_betw2:
    6.88 +assumes INF: "\<not> finite A"
    6.89 +shows "\<exists>h. bij_betw h A (A \<union> {a})"
    6.90 +proof(cases "a \<in> A")
    6.91 +  assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
    6.92 +  thus ?thesis using bij_betw_id[of A] by auto
    6.93 +next
    6.94 +  let ?A' = "A \<union> {a}"
    6.95 +  assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
    6.96 +  moreover have "\<not> finite ?A'" using INF by auto
    6.97 +  ultimately obtain f where "bij_betw f ?A' A"
    6.98 +  using infinite_imp_bij_betw[of ?A' a] by auto
    6.99 +  hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
   6.100 +  thus ?thesis by auto
   6.101 +qed
   6.102 +
   6.103 +lemma bij_betw_inv_into_left:
   6.104 +assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
   6.105 +shows "(inv_into A f) (f a) = a"
   6.106 +using assms unfolding bij_betw_def
   6.107 +by clarify (rule inv_into_f_f)
   6.108 +
   6.109 +lemma bij_betw_inv_into_right:
   6.110 +assumes "bij_betw f A A'" "a' \<in> A'"
   6.111 +shows "f(inv_into A f a') = a'"
   6.112 +using assms unfolding bij_betw_def using f_inv_into_f by force
   6.113 +
   6.114 +lemma bij_betw_inv_into_subset:
   6.115 +assumes BIJ: "bij_betw f A A'" and
   6.116 +        SUB: "B \<le> A" and IM: "f ` B = B'"
   6.117 +shows "bij_betw (inv_into A f) B' B"
   6.118 +using assms unfolding bij_betw_def
   6.119 +by (auto intro: inj_on_inv_into)
   6.120 +
   6.121 +
   6.122  subsection {* Specification package -- Hilbertized version *}
   6.123  
   6.124  lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"