summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Inductive.thy

changeset 63980 | f8e556c8ad6f |

parent 63979 | 95c3ae4baba8 |

child 63981 | 6f7db4f8df4c |

1.1 --- a/src/HOL/Inductive.thy Sat Oct 01 17:16:35 2016 +0200 1.2 +++ b/src/HOL/Inductive.thy Sat Oct 01 17:38:14 2016 +0200 1.3 @@ -422,6 +422,94 @@ 1.4 induct_rulify_fallback 1.5 1.6 1.7 +subsection \<open>The Schroeder-Bernstein Theorem\<close> 1.8 + 1.9 +text \<open> 1.10 + See also: 1.11 + \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close> 1.12 + \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close> 1.13 + \<^item> Springer LNCS 828 (cover page) 1.14 +\<close> 1.15 + 1.16 +theorem Schroeder_Bernstein: 1.17 + fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a" 1.18 + and A :: "'a set" and B :: "'b set" 1.19 + assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B" 1.20 + and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A" 1.21 + shows "\<exists>h. bij_betw h A B" 1.22 +proof (rule exI, rule bij_betw_imageI) 1.23 + define X where "X = lfp (\<lambda>X. A - (g ` (B - (f ` X))))" 1.24 + define g' where "g' = the_inv_into (B - (f ` X)) g" 1.25 + let ?h = "\<lambda>z. if z \<in> X then f z else g' z" 1.26 + 1.27 + have X: "X = A - (g ` (B - (f ` X)))" 1.28 + unfolding X_def by (rule lfp_unfold) (blast intro: monoI) 1.29 + then have X_compl: "A - X = g ` (B - (f ` X))" 1.30 + using sub2 by blast 1.31 + 1.32 + from inj2 have inj2': "inj_on g (B - (f ` X))" 1.33 + by (rule inj_on_subset) auto 1.34 + with X_compl have *: "g' ` (A - X) = B - (f ` X)" 1.35 + by (simp add: g'_def) 1.36 + 1.37 + from X have X_sub: "X \<subseteq> A" by auto 1.38 + from X sub1 have fX_sub: "f ` X \<subseteq> B" by auto 1.39 + 1.40 + show "?h ` A = B" 1.41 + proof - 1.42 + from X_sub have "?h ` A = ?h ` (X \<union> (A - X))" by auto 1.43 + also have "\<dots> = ?h ` X \<union> ?h ` (A - X)" by (simp only: image_Un) 1.44 + also have "?h ` X = f ` X" by auto 1.45 + also from * have "?h ` (A - X) = B - (f ` X)" by auto 1.46 + also from fX_sub have "f ` X \<union> (B - f ` X) = B" by blast 1.47 + finally show ?thesis . 1.48 + qed 1.49 + show "inj_on ?h A" 1.50 + proof - 1.51 + from inj1 X_sub have on_X: "inj_on f X" 1.52 + by (rule subset_inj_on) 1.53 + 1.54 + have on_X_compl: "inj_on g' (A - X)" 1.55 + unfolding g'_def X_compl 1.56 + by (rule inj_on_the_inv_into) (rule inj2') 1.57 + 1.58 + have impossible: False if eq: "f a = g' b" and a: "a \<in> X" and b: "b \<in> A - X" for a b 1.59 + proof - 1.60 + from a have fa: "f a \<in> f ` X" by (rule imageI) 1.61 + from b have "g' b \<in> g' ` (A - X)" by (rule imageI) 1.62 + with * have "g' b \<in> - (f ` X)" by simp 1.63 + with eq fa show False by simp 1.64 + qed 1.65 + 1.66 + show ?thesis 1.67 + proof (rule inj_onI) 1.68 + fix a b 1.69 + assume h: "?h a = ?h b" 1.70 + assume "a \<in> A" and "b \<in> A" 1.71 + then consider "a \<in> X" "b \<in> X" | "a \<in> A - X" "b \<in> A - X" 1.72 + | "a \<in> X" "b \<in> A - X" | "a \<in> A - X" "b \<in> X" 1.73 + by blast 1.74 + then show "a = b" 1.75 + proof cases 1.76 + case 1 1.77 + with h on_X show ?thesis by (simp add: inj_on_eq_iff) 1.78 + next 1.79 + case 2 1.80 + with h on_X_compl show ?thesis by (simp add: inj_on_eq_iff) 1.81 + next 1.82 + case 3 1.83 + with h impossible [of a b] have False by simp 1.84 + then show ?thesis .. 1.85 + next 1.86 + case 4 1.87 + with h impossible [of b a] have False by simp 1.88 + then show ?thesis .. 1.89 + qed 1.90 + qed 1.91 + qed 1.92 +qed 1.93 + 1.94 + 1.95 subsection \<open>Inductive datatypes and primitive recursion\<close> 1.96 1.97 text \<open>Package setup.\<close>