# HG changeset patch # User wenzelm # Date 1465671271 -7200 # Node ID b1d7950285cfcec0fa42ae6c3944a280a06a18ef # Parent 9ac558ab0906aca7ff4ec1a8a0b4a494202f396b tuned; diff -r 9ac558ab0906 -r b1d7950285cf src/HOL/Isar_Examples/Schroeder_Bernstein.thy --- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Sat Jun 11 16:22:42 2016 +0200 +++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Sat Jun 11 20:54:31 2016 +0200 @@ -16,42 +16,42 @@ \ 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" + fixes f :: \'a \ 'b\ + and g :: \'b \ 'a\ + assumes \inj f\ and \inj g\ + shows \\h :: 'a \ 'b. inj h \ surj h\ 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" + 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)))" + 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)" + 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" + show \inj ?h \ surj ?h\ proof - from * show "surj ?h" by auto - have "inj_on f A" + 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)" + 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) + 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 + 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 + 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" + ultimately show \inj ?h\ unfolding inj_on_def by (metis ComplI) qed qed