(* 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 decomposition:
obtains X
where "X = - (g ` (- (f ` X)))"
using lfp_unfold [OF monoI, of
"\X. - g ` (- f ` X)"]
by blast
theorem Schroeder_Bernstein:
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›
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:
"\a\A. R `` {a} <= A" using 0
by blast
hence 1:
"\a\A. finite(R `` {a})" using ‹finite A
›
by(blast intro: finite_subset)
have sub:
"?N ` A <= {0..
proof -
have "\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..
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. 2024-06-19: now trivial for sledgehammer (LCP)›
by (metis even_Suc mem_Collect_eq)
end
