# HG changeset patch # User paulson # Date 1718785235 -7200 # Node ID 413a86331bf60ac0eb96d0c7cf8a5d6cc978827b # Parent 4953d52e04d282cf2efeca93107a729180c2a719 Updated some archaic proofs diff -r 4953d52e04d2 -r 413a86331bf6 src/HOL/ex/Set_Theory.thy --- a/src/HOL/ex/Set_Theory.thy Tue Jun 18 16:55:30 2024 +0200 +++ b/src/HOL/ex/Set_Theory.thy Wed Jun 19 10:20:35 2024 +0200 @@ -76,41 +76,29 @@ subsection \The Schröder-Bernstein Theorem\ -lemma disj_lemma: "- (f ` X) = g' ` (-X) \ f a = g' b \ a \ X \ b \ X" +lemma decomposition: + obtains X where "X = - (g ` (- (f ` X)))" + using lfp_unfold [OF monoI, of "\X. - g ` (- f ` X)"] by blast -lemma surj_if_then_else: - "-(f ` X) = g' ` (-X) \ surj (\z. if z \ X then f z else g' z)" - by (simp add: surj_def) blast - -lemma bij_if_then_else: - "inj_on f X \ inj_on g' (-X) \ -(f ` X) = g' ` (-X) \ - h = (\z. if z \ X then f z else g' z) \ inj h \ surj h" - apply (unfold inj_on_def) - apply (simp add: surj_if_then_else) - apply (blast dest: disj_lemma sym) - done - -lemma decomposition: "\X. X = - (g ` (- (f ` X)))" - apply (rule exI) - apply (rule lfp_unfold) - apply (rule monoI, blast) - done - theorem Schroeder_Bernstein: - "inj (f :: 'a \ 'b) \ inj (g :: 'b \ 'a) - \ \h:: 'a \ 'b. inj h \ surj h" - apply (rule decomposition [where f=f and g=g, THEN exE]) - apply (rule_tac x = "(\z. if z \ x then f z else inv g z)" in exI) - \ \The term above can be synthesized by a sufficiently detailed proof.\ - apply (rule bij_if_then_else) - apply (rule_tac [4] refl) - apply (rule_tac [2] inj_on_inv_into) - apply (erule subset_inj_on [OF _ subset_UNIV]) - apply blast - apply (erule ssubst, subst double_complement, erule image_inv_f_f [symmetric]) - done - + fixes f :: "'a \ 'b" and g :: "'b \ 'a" + assumes "inj f" "inj g" + obtains h:: "'a \ 'b" where "inj h" "surj h" +proof (rule decomposition) + fix X + assume X: "X = - (g ` (- (f ` X)))" + let ?h = "\z. if z \ X then f z else inv g z" + show thesis + proof + have "inj_on (inv g) (-X)" + by (metis X \inj g\ bij_betw_def double_complement inj_imp_bij_betw_inv) + with \inj f\ show "inj ?h" + unfolding inj_on_def by (metis Compl_iff X \inj g\ imageI image_inv_f_f) + show "surj ?h" + using \inj g\ X image_iff surj_def by fastforce + qed +qed subsection \A simple party theorem\ @@ -218,10 +206,7 @@ "(\x. (\u. x = 2 * u) = (\ (\v. Suc x = 2 * v))) \ (\A. \x. (x \ A) = (Suc x \ A))" \ \Example EO1: typo in article, and with the obvious fix it seems - to require arithmetic reasoning.\ - apply clarify - apply (rule_tac x = "{x. \u. x = 2 * u}" in exI, auto) - apply metis+ - done + to require arithmetic reasoning. 2024-06-19: now trivial for sledgehammer (LCP)\ + by (metis even_Suc mem_Collect_eq) end