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"
```