# HG changeset patch # User wenzelm # Date 1451228441 -3600 # Node ID e1205f814159868a79f600eaecc372c402468a80 # Parent 2a9bed6cd6e5a78c39cfc190860bd03f5d7359e1 more proofs; diff -r 2a9bed6cd6e5 -r e1205f814159 src/HOL/Isar_Examples/Schroeder_Bernstein.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Sun Dec 27 16:00:41 2015 +0100 @@ -0,0 +1,59 @@ +(* 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 "~~/src/HOL/ex/Set_Theory.thy"} + \<^item> @{url "http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem"} + \<^item> Springer LNCS 828 (cover page) +\ + +theorem Schroeder_Bernstein: + fixes f :: "'a \ 'b" + and g :: "'b \ 'a" + assumes "inj f" and "inj g" + shows "\h :: 'a \ 'b. inj h \ surj h" +proof + def A \ "lfp (\X. - (g ` (- (f ` X))))" + def 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 diff -r 2a9bed6cd6e5 -r e1205f814159 src/HOL/ROOT --- a/src/HOL/ROOT Sun Dec 27 15:52:43 2015 +0100 +++ b/src/HOL/ROOT Sun Dec 27 16:00:41 2015 +0100 @@ -632,6 +632,7 @@ theories Basic_Logic Cantor + Schroeder_Bernstein Drinker Expr_Compiler Fibonacci