(* Title: HOL/ex/Set_Theory.thy Author: Tobias Nipkow and Lawrence C Paulson Copyright 1991 University of Cambridge *) section ‹Set Theory examples: Cantor's Theorem, SchrÃ¶der-Bernstein Theorem, etc.› theory Set_Theory imports Main begin text‹ These two are cited in Benzmueller and Kohlhase's system description of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove. › lemma "(X = Y ∪ Z) = (Y ⊆ X ∧ Z ⊆ X ∧ (∀V. Y ⊆ V ∧ Z ⊆ V ⟶ X ⊆ V))" by blast lemma "(X = Y ∩ Z) = (X ⊆ Y ∧ X ⊆ Z ∧ (∀V. V ⊆ Y ∧ V ⊆ Z ⟶ V ⊆ X))" by blast text ‹ Trivial example of term synthesis: apparently hard for some provers! › schematic_goal "a ≠ b ⟹ a ∈ ?X ∧ b ∉ ?X" by blast subsection ‹Examples for the ‹blast› paper› lemma "(⋃x ∈ C. f x ∪ g x) = ⋃(f ` C) ∪ ⋃(g ` C)" ― ‹Union-image, called ‹Un_Union_image› in Main HOL› by blast lemma "(⋂x ∈ C. f x ∩ g x) = ⋂(f ` C) ∩ ⋂(g ` C)" ― ‹Inter-image, called ‹Int_Inter_image› in Main HOL› by blast lemma singleton_example_1: "⋀S::'a set set. ∀x ∈ S. ∀y ∈ S. x ⊆ y ⟹ ∃z. S ⊆ {z}" by blast lemma singleton_example_2: "∀x ∈ S. ⋃S ⊆ x ⟹ ∃z. S ⊆ {z}" ― ‹Variant of the problem above.› by blast lemma "∃!x. f (g x) = x ⟹ ∃!y. g (f y) = y" ― ‹A unique fixpoint theorem --- ‹fast›/‹best›/‹meson› all fail.› by metis subsection ‹Cantor's Theorem: There is no surjection from a set to its powerset› lemma cantor1: "¬ (∃f:: 'a ⇒ 'a set. ∀S. ∃x. f x = S)" ― ‹Requires best-first search because it is undirectional.› by best schematic_goal "∀f:: 'a ⇒ 'a set. ∀x. f x ≠ ?S f" ― ‹This form displays the diagonal term.› by best schematic_goal "?S ∉ range (f :: 'a ⇒ 'a set)" ― ‹This form exploits the set constructs.› by (rule notI, erule rangeE, best) schematic_goal "?S ∉ range (f :: 'a ⇒ 'a set)" ― ‹Or just this!› by best subsection ‹The SchrÃ¶der-Bernstein Theorem› lemma disj_lemma: "- (f ` X) = g' ` (-X) ⟹ f a = g' b ⟹ a ∈ X ⟹ b ∈ 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 subsection ‹A simple party theorem› text‹\emph{At any party there are two people who know the same number of people}. Provided the party consists of at least two people and the knows relation is symmetric. Knowing yourself does not count --- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk at TPHOLs 2007.)› lemma equal_number_of_acquaintances: assumes "Domain R <= A" and "sym R" and "card A ≥ 2" shows "¬ inj_on (%a. card(R `` {a} - {a})) A" proof - let ?N = "%a. card(R `` {a} - {a})" let ?n = "card A" have "finite A" using ‹card A ≥ 2› by(auto intro:ccontr) have 0: "R `` A <= A" using ‹sym R› ‹Domain R <= A› unfolding Domain_unfold sym_def by blast have h: "ALL a:A. R `` {a} <= A" using 0 by blast hence 1: "ALL a:A. finite(R `` {a})" using ‹finite A› by(blast intro: finite_subset) have sub: "?N ` A <= {0..<?n}" proof - have "ALL a:A. R `` {a} - {a} < A" using h by blast thus ?thesis using psubset_card_mono[OF ‹finite A›] by auto qed show "~ inj_on ?N A" (is "~ ?I") proof assume ?I hence "?n = card(?N ` A)" by(rule card_image[symmetric]) with sub ‹finite A› have 2[simp]: "?N ` A = {0..<?n}" using subset_card_intvl_is_intvl[of _ 0] by(auto) have "0 : ?N ` A" and "?n - 1 : ?N ` A" using ‹card A ≥ 2› by simp+ then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1" by (auto simp del: 2) have "a ≠ b" using Na Nb ‹card A ≥ 2› by auto have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff) hence "b ∉ R `` {a}" using ‹a≠b› by blast hence "a ∉ R `` {b}" by (metis Image_singleton_iff assms(2) sym_def) hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast have 4: "finite (A - {a,b})" using ‹finite A› by simp have "?N b <= ?n - 2" using ab ‹a≠b› ‹finite A› card_mono[OF 4 3] by simp then show False using Nb ‹card A ≥ 2› by arith qed qed text ‹ From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages 293-314. Isabelle can prove the easy examples without any special mechanisms, but it can't prove the hard ones. › lemma "∃A. (∀x ∈ A. x ≤ (0::int))" ― ‹Example 1, page 295.› by force lemma "D ∈ F ⟹ ∃G. ∀A ∈ G. ∃B ∈ F. A ⊆ B" ― ‹Example 2.› by force lemma "P a ⟹ ∃A. (∀x ∈ A. P x) ∧ (∃y. y ∈ A)" ― ‹Example 3.› by force lemma "a < b ∧ b < (c::int) ⟹ ∃A. a ∉ A ∧ b ∈ A ∧ c ∉ A" ― ‹Example 4.› by auto ―‹slow› lemma "P (f b) ⟹ ∃s A. (∀x ∈ A. P x) ∧ f s ∈ A" ― ‹Example 5, page 298.› by force lemma "P (f b) ⟹ ∃s A. (∀x ∈ A. P x) ∧ f s ∈ A" ― ‹Example 6.› by force lemma "∃A. a ∉ A" ― ‹Example 7.› by force lemma "(∀u v. u < (0::int) ⟶ u ≠ ¦v¦) ⟶ (∃A::int set. -2 ∈ A & (∀y. ¦y¦ ∉ A))" ― ‹Example 8 needs a small hint.› by force ― ‹not ‹blast›, which can't simplify ‹-2 < 0›› text ‹Example 9 omitted (requires the reals).› text ‹The paper has no Example 10!› lemma "(∀A. 0 ∈ A ∧ (∀x ∈ A. Suc x ∈ A) ⟶ n ∈ A) ∧ P 0 ∧ (∀x. P x ⟶ P (Suc x)) ⟶ P n" ― ‹Example 11: needs a hint.› by(metis nat.induct) lemma "(∀A. (0, 0) ∈ A ∧ (∀x y. (x, y) ∈ A ⟶ (Suc x, Suc y) ∈ A) ⟶ (n, m) ∈ A) ∧ P n ⟶ P m" ― ‹Example 12.› by auto lemma "(∀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 end