diff -r 95c3ae4baba8 -r f8e556c8ad6f src/HOL/Isar_Examples/Schroeder_Bernstein.thy --- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Sat Oct 01 17:16:35 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,56 +0,0 @@ -(* Title: HOL/Isar_Examples/Schroeder_Bernstein.thy - Author: Makarius -*) - -section \SchrÃ¶der-Bernstein Theorem\ - -theory Schroeder_Bernstein - imports Main -begin - -text \ - See also: - \<^item> \<^file>\\$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\ - \<^item> \<^url>\http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\ - \<^item> Springer LNCS 828 (cover page) -\ - -theorem Schroeder_Bernstein: \\h :: 'a \ 'b. inj h \ surj h\ if \inj f\ and \inj g\ - for f :: \'a \ 'b\ and g :: \'b \ 'a\ -proof - define A where \A = lfp (\X. - (g ` (- (f ` X))))\ - define g' where \g' = inv g\ - let \?h\ = \\z. if z \ A then f z else g' z\ - - have \A = - (g ` (- (f ` A)))\ - unfolding A_def by (rule lfp_unfold) (blast intro: monoI) - then have A_compl: \- A = g ` (- (f ` A))\ by blast - then have *: \g' ` (- A) = - (f ` A)\ - using g'_def \inj g\ by auto - - show \inj ?h \ surj ?h\ - proof - from * show \surj ?h\ by auto - have \inj_on f A\ - using \inj f\ by (rule subset_inj_on) blast - moreover - have \inj_on g' (- A)\ - unfolding g'_def - proof (rule inj_on_inv_into) - have \g ` (- (f ` A)) \ range g\ by blast - then show \- A \ range g\ by (simp only: A_compl) - qed - moreover - have \False\ if eq: \f a = g' b\ and a: \a \ A\ and b: \b \ - A\ for a b - proof - - from a have fa: \f a \ f ` A\ by (rule imageI) - from b have \g' b \ g' ` (- A)\ by (rule imageI) - with * have \g' b \ - (f ` A)\ by simp - with eq fa show \False\ by simp - qed - ultimately show \inj ?h\ - unfolding inj_on_def by (metis ComplI) - qed -qed - -end