src/HOL/Hilbert_Choice.thy
changeset 55020 96b05fd2aee4
parent 54744 1e7f2d296e19
child 55088 57c82e01022b
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Jan 16 16:50:41 2014 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jan 16 18:26:41 2014 +0100
     1.3 @@ -827,6 +827,121 @@
     1.4    using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
     1.5  
     1.6  
     1.7 +subsection {* More on injections, bijections, and inverses *}
     1.8 +
     1.9 +lemma infinite_imp_bij_betw:
    1.10 +assumes INF: "\<not> finite A"
    1.11 +shows "\<exists>h. bij_betw h A (A - {a})"
    1.12 +proof(cases "a \<in> A")
    1.13 +  assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
    1.14 +  thus ?thesis using bij_betw_id[of A] by auto
    1.15 +next
    1.16 +  assume Case2: "a \<in> A"
    1.17 +find_theorems "\<not> finite _"
    1.18 +  have "\<not> finite (A - {a})" using INF by auto
    1.19 +  with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
    1.20 +  where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
    1.21 +  obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
    1.22 +  obtain A' where A'_def: "A' = g ` UNIV" by blast
    1.23 +  have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
    1.24 +  have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
    1.25 +  proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
    1.26 +        case_tac "x = 0", auto simp add: 2)
    1.27 +    fix y  assume "a = (if y = 0 then a else f (Suc y))"
    1.28 +    thus "y = 0" using temp by (case_tac "y = 0", auto)
    1.29 +  next
    1.30 +    fix x y
    1.31 +    assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
    1.32 +    thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
    1.33 +  next
    1.34 +    fix n show "f (Suc n) \<in> A" using 2 by blast
    1.35 +  qed
    1.36 +  hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
    1.37 +  using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
    1.38 +  hence 5: "bij_betw (inv g) A' UNIV"
    1.39 +  by (auto simp add: bij_betw_inv_into)
    1.40 +  (*  *)
    1.41 +  obtain n where "g n = a" using 3 by auto
    1.42 +  hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
    1.43 +  using 3 4 unfolding A'_def
    1.44 +  by clarify (rule bij_betw_subset, auto simp: image_set_diff)
    1.45 +  (*  *)
    1.46 +  obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
    1.47 +  have 7: "bij_betw v UNIV (UNIV - {n})"
    1.48 +  proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
    1.49 +    fix m1 m2 assume "v m1 = v m2"
    1.50 +    thus "m1 = m2"
    1.51 +    by(case_tac "m1 < n", case_tac "m2 < n",
    1.52 +       auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
    1.53 +  next
    1.54 +    show "v ` UNIV = UNIV - {n}"
    1.55 +    proof(auto simp add: v_def)
    1.56 +      fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
    1.57 +      {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
    1.58 +       then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
    1.59 +       with 71 have "n \<le> m'" by auto
    1.60 +       with 72 ** have False by auto
    1.61 +      }
    1.62 +      thus "m < n" by force
    1.63 +    qed
    1.64 +  qed
    1.65 +  (*  *)
    1.66 +  obtain h' where h'_def: "h' = g o v o (inv g)" by blast
    1.67 +  hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
    1.68 +  by (auto simp add: bij_betw_trans)
    1.69 +  (*  *)
    1.70 +  obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
    1.71 +  have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
    1.72 +  hence "bij_betw h  A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
    1.73 +  moreover
    1.74 +  {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
    1.75 +   hence "bij_betw h  (A - A') (A - A')"
    1.76 +   using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
    1.77 +  }
    1.78 +  moreover
    1.79 +  have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
    1.80 +        ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
    1.81 +  using 4 by blast
    1.82 +  ultimately have "bij_betw h A (A - {a})"
    1.83 +  using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
    1.84 +  thus ?thesis by blast
    1.85 +qed
    1.86 +
    1.87 +lemma infinite_imp_bij_betw2:
    1.88 +assumes INF: "\<not> finite A"
    1.89 +shows "\<exists>h. bij_betw h A (A \<union> {a})"
    1.90 +proof(cases "a \<in> A")
    1.91 +  assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
    1.92 +  thus ?thesis using bij_betw_id[of A] by auto
    1.93 +next
    1.94 +  let ?A' = "A \<union> {a}"
    1.95 +  assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
    1.96 +  moreover have "\<not> finite ?A'" using INF by auto
    1.97 +  ultimately obtain f where "bij_betw f ?A' A"
    1.98 +  using infinite_imp_bij_betw[of ?A' a] by auto
    1.99 +  hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
   1.100 +  thus ?thesis by auto
   1.101 +qed
   1.102 +
   1.103 +lemma bij_betw_inv_into_left:
   1.104 +assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
   1.105 +shows "(inv_into A f) (f a) = a"
   1.106 +using assms unfolding bij_betw_def
   1.107 +by clarify (rule inv_into_f_f)
   1.108 +
   1.109 +lemma bij_betw_inv_into_right:
   1.110 +assumes "bij_betw f A A'" "a' \<in> A'"
   1.111 +shows "f(inv_into A f a') = a'"
   1.112 +using assms unfolding bij_betw_def using f_inv_into_f by force
   1.113 +
   1.114 +lemma bij_betw_inv_into_subset:
   1.115 +assumes BIJ: "bij_betw f A A'" and
   1.116 +        SUB: "B \<le> A" and IM: "f ` B = B'"
   1.117 +shows "bij_betw (inv_into A f) B' B"
   1.118 +using assms unfolding bij_betw_def
   1.119 +by (auto intro: inj_on_inv_into)
   1.120 +
   1.121 +
   1.122  subsection {* Specification package -- Hilbertized version *}
   1.123  
   1.124  lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"