1.1 --- a/src/HOL/IsaMakefile Thu Aug 18 16:52:19 2011 +0900
1.2 +++ b/src/HOL/IsaMakefile Thu Aug 18 13:10:24 2011 +0200
1.3 @@ -1039,32 +1039,30 @@
1.4
1.5 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
1.6 Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
1.7 - ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
1.8 - ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
1.9 - ex/CTL.thy ex/Case_Product.thy \
1.10 - ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
1.11 - ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
1.12 - ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
1.13 - ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
1.14 - ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
1.15 - ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
1.16 + ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
1.17 + ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \
1.18 + ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \
1.19 + ex/CodegenSML_Test.thy ex/Coercion_Examples.thy ex/Coherent.thy \
1.20 + ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
1.21 + ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
1.22 + ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
1.23 + ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
1.24 + ex/Iff_Oracle.thy ex/Induction_Schema.thy \
1.25 ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
1.26 ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
1.27 ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
1.28 ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
1.29 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
1.30 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
1.31 - ex/Quickcheck_Narrowing_Examples.thy \
1.32 - ex/Quicksort.thy ex/ROOT.ML ex/Records.thy \
1.33 - ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
1.34 - ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
1.35 - ex/sledgehammer_tactics.ML ex/Sqrt.thy \
1.36 - ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
1.37 - ex/Transfer_Ex.thy ex/Tree23.thy \
1.38 + ex/Quickcheck_Narrowing_Examples.thy ex/Quicksort.thy ex/ROOT.ML \
1.39 + ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
1.40 + ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
1.41 + ex/Set_Algebras.thy ex/SVC_Oracle.thy ex/sledgehammer_tactics.ML \
1.42 + ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy \
1.43 + ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
1.44 ex/Unification.thy ex/While_Combinator_Example.thy \
1.45 - ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
1.46 - ex/svc_test.thy \
1.47 - ../Tools/interpretation_with_defs.ML
1.48 + ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \
1.49 + ex/svc_test.thy ../Tools/interpretation_with_defs.ML
1.50 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
1.51
1.52
2.1 --- a/src/HOL/ex/ROOT.ML Thu Aug 18 16:52:19 2011 +0900
2.2 +++ b/src/HOL/ex/ROOT.ML Thu Aug 18 13:10:24 2011 +0200
2.3 @@ -48,7 +48,7 @@
2.4 "Primrec",
2.5 "Tarski",
2.6 "Classical",
2.7 - "set",
2.8 + "Set_Theory",
2.9 "Meson_Test",
2.10 "Termination",
2.11 "Coherent",
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/ex/Set_Theory.thy Thu Aug 18 13:10:24 2011 +0200
3.3 @@ -0,0 +1,227 @@
3.4 +(* Title: HOL/ex/Set_Theory.thy
3.5 + Author: Tobias Nipkow and Lawrence C Paulson
3.6 + Copyright 1991 University of Cambridge
3.7 +*)
3.8 +
3.9 +header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
3.10 +
3.11 +theory Set_Theory
3.12 +imports Main
3.13 +begin
3.14 +
3.15 +text{*
3.16 + These two are cited in Benzmueller and Kohlhase's system description
3.17 + of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
3.18 + prove.
3.19 +*}
3.20 +
3.21 +lemma "(X = Y \<union> Z) =
3.22 + (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
3.23 + by blast
3.24 +
3.25 +lemma "(X = Y \<inter> Z) =
3.26 + (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
3.27 + by blast
3.28 +
3.29 +text {*
3.30 + Trivial example of term synthesis: apparently hard for some provers!
3.31 +*}
3.32 +
3.33 +schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
3.34 + by blast
3.35 +
3.36 +
3.37 +subsection {* Examples for the @{text blast} paper *}
3.38 +
3.39 +lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
3.40 + -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
3.41 + by blast
3.42 +
3.43 +lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
3.44 + -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
3.45 + by blast
3.46 +
3.47 +lemma singleton_example_1:
3.48 + "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
3.49 + by blast
3.50 +
3.51 +lemma singleton_example_2:
3.52 + "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
3.53 + -- {*Variant of the problem above. *}
3.54 + by blast
3.55 +
3.56 +lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
3.57 + -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
3.58 + by metis
3.59 +
3.60 +
3.61 +subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
3.62 +
3.63 +lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
3.64 + -- {* Requires best-first search because it is undirectional. *}
3.65 + by best
3.66 +
3.67 +schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
3.68 + -- {*This form displays the diagonal term. *}
3.69 + by best
3.70 +
3.71 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
3.72 + -- {* This form exploits the set constructs. *}
3.73 + by (rule notI, erule rangeE, best)
3.74 +
3.75 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
3.76 + -- {* Or just this! *}
3.77 + by best
3.78 +
3.79 +
3.80 +subsection {* The Schröder-Berstein Theorem *}
3.81 +
3.82 +lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
3.83 + by blast
3.84 +
3.85 +lemma surj_if_then_else:
3.86 + "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
3.87 + by (simp add: surj_def) blast
3.88 +
3.89 +lemma bij_if_then_else:
3.90 + "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
3.91 + h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
3.92 + apply (unfold inj_on_def)
3.93 + apply (simp add: surj_if_then_else)
3.94 + apply (blast dest: disj_lemma sym)
3.95 + done
3.96 +
3.97 +lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
3.98 + apply (rule exI)
3.99 + apply (rule lfp_unfold)
3.100 + apply (rule monoI, blast)
3.101 + done
3.102 +
3.103 +theorem Schroeder_Bernstein:
3.104 + "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
3.105 + \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
3.106 + apply (rule decomposition [where f=f and g=g, THEN exE])
3.107 + apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
3.108 + --{*The term above can be synthesized by a sufficiently detailed proof.*}
3.109 + apply (rule bij_if_then_else)
3.110 + apply (rule_tac [4] refl)
3.111 + apply (rule_tac [2] inj_on_inv_into)
3.112 + apply (erule subset_inj_on [OF _ subset_UNIV])
3.113 + apply blast
3.114 + apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
3.115 + done
3.116 +
3.117 +
3.118 +subsection {* A simple party theorem *}
3.119 +
3.120 +text{* \emph{At any party there are two people who know the same
3.121 +number of people}. Provided the party consists of at least two people
3.122 +and the knows relation is symmetric. Knowing yourself does not count
3.123 +--- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
3.124 +at TPHOLs 2007.) *}
3.125 +
3.126 +lemma equal_number_of_acquaintances:
3.127 +assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
3.128 +shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
3.129 +proof -
3.130 + let ?N = "%a. card(R `` {a} - {a})"
3.131 + let ?n = "card A"
3.132 + have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
3.133 + have 0: "R `` A <= A" using `sym R` `Domain R <= A`
3.134 + unfolding Domain_def sym_def by blast
3.135 + have h: "ALL a:A. R `` {a} <= A" using 0 by blast
3.136 + hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
3.137 + by(blast intro: finite_subset)
3.138 + have sub: "?N ` A <= {0..<?n}"
3.139 + proof -
3.140 + have "ALL a:A. R `` {a} - {a} < A" using h by blast
3.141 + thus ?thesis using psubset_card_mono[OF `finite A`] by auto
3.142 + qed
3.143 + show "~ inj_on ?N A" (is "~ ?I")
3.144 + proof
3.145 + assume ?I
3.146 + hence "?n = card(?N ` A)" by(rule card_image[symmetric])
3.147 + with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
3.148 + using subset_card_intvl_is_intvl[of _ 0] by(auto)
3.149 + have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
3.150 + then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
3.151 + by (auto simp del: 2)
3.152 + have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
3.153 + have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
3.154 + hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
3.155 + hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
3.156 + hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
3.157 + have 4: "finite (A - {a,b})" using `finite A` by simp
3.158 + have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
3.159 + then show False using Nb `card A \<ge> 2` by arith
3.160 + qed
3.161 +qed
3.162 +
3.163 +text {*
3.164 + From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
3.165 + 293-314.
3.166 +
3.167 + Isabelle can prove the easy examples without any special mechanisms,
3.168 + but it can't prove the hard ones.
3.169 +*}
3.170 +
3.171 +lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
3.172 + -- {* Example 1, page 295. *}
3.173 + by force
3.174 +
3.175 +lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
3.176 + -- {* Example 2. *}
3.177 + by force
3.178 +
3.179 +lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
3.180 + -- {* Example 3. *}
3.181 + by force
3.182 +
3.183 +lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
3.184 + -- {* Example 4. *}
3.185 + by force
3.186 +
3.187 +lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
3.188 + -- {*Example 5, page 298. *}
3.189 + by force
3.190 +
3.191 +lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
3.192 + -- {* Example 6. *}
3.193 + by force
3.194 +
3.195 +lemma "\<exists>A. a \<notin> A"
3.196 + -- {* Example 7. *}
3.197 + by force
3.198 +
3.199 +lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
3.200 + \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
3.201 + -- {* Example 8 now needs a small hint. *}
3.202 + by (simp add: abs_if, force)
3.203 + -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
3.204 +
3.205 +text {* Example 9 omitted (requires the reals). *}
3.206 +
3.207 +text {* The paper has no Example 10! *}
3.208 +
3.209 +lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
3.210 + P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
3.211 + -- {* Example 11: needs a hint. *}
3.212 +by(metis nat.induct)
3.213 +
3.214 +lemma
3.215 + "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
3.216 + \<and> P n \<longrightarrow> P m"
3.217 + -- {* Example 12. *}
3.218 + by auto
3.219 +
3.220 +lemma
3.221 + "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
3.222 + (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
3.223 + -- {* Example EO1: typo in article, and with the obvious fix it seems
3.224 + to require arithmetic reasoning. *}
3.225 + apply clarify
3.226 + apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
3.227 + apply metis+
3.228 + done
3.229 +
3.230 +end
4.1 --- a/src/HOL/ex/set.thy Thu Aug 18 16:52:19 2011 +0900
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,225 +0,0 @@
4.4 -(* Title: HOL/ex/set.thy
4.5 - Author: Tobias Nipkow and Lawrence C Paulson
4.6 - Copyright 1991 University of Cambridge
4.7 -*)
4.8 -
4.9 -header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}
4.10 -
4.11 -theory set imports Main begin
4.12 -
4.13 -text{*
4.14 - These two are cited in Benzmueller and Kohlhase's system description
4.15 - of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
4.16 - prove.
4.17 -*}
4.18 -
4.19 -lemma "(X = Y \<union> Z) =
4.20 - (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
4.21 - by blast
4.22 -
4.23 -lemma "(X = Y \<inter> Z) =
4.24 - (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
4.25 - by blast
4.26 -
4.27 -text {*
4.28 - Trivial example of term synthesis: apparently hard for some provers!
4.29 -*}
4.30 -
4.31 -schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
4.32 - by blast
4.33 -
4.34 -
4.35 -subsection {* Examples for the @{text blast} paper *}
4.36 -
4.37 -lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)"
4.38 - -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
4.39 - by blast
4.40 -
4.41 -lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
4.42 - -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
4.43 - by blast
4.44 -
4.45 -lemma singleton_example_1:
4.46 - "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
4.47 - by blast
4.48 -
4.49 -lemma singleton_example_2:
4.50 - "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
4.51 - -- {*Variant of the problem above. *}
4.52 - by blast
4.53 -
4.54 -lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
4.55 - -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
4.56 - by metis
4.57 -
4.58 -
4.59 -subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}
4.60 -
4.61 -lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
4.62 - -- {* Requires best-first search because it is undirectional. *}
4.63 - by best
4.64 -
4.65 -schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
4.66 - -- {*This form displays the diagonal term. *}
4.67 - by best
4.68 -
4.69 -schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
4.70 - -- {* This form exploits the set constructs. *}
4.71 - by (rule notI, erule rangeE, best)
4.72 -
4.73 -schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
4.74 - -- {* Or just this! *}
4.75 - by best
4.76 -
4.77 -
4.78 -subsection {* The Schröder-Berstein Theorem *}
4.79 -
4.80 -lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
4.81 - by blast
4.82 -
4.83 -lemma surj_if_then_else:
4.84 - "-(f ` X) = g ` (-X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)"
4.85 - by (simp add: surj_def) blast
4.86 -
4.87 -lemma bij_if_then_else:
4.88 - "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
4.89 - h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h"
4.90 - apply (unfold inj_on_def)
4.91 - apply (simp add: surj_if_then_else)
4.92 - apply (blast dest: disj_lemma sym)
4.93 - done
4.94 -
4.95 -lemma decomposition: "\<exists>X. X = - (g ` (- (f ` X)))"
4.96 - apply (rule exI)
4.97 - apply (rule lfp_unfold)
4.98 - apply (rule monoI, blast)
4.99 - done
4.100 -
4.101 -theorem Schroeder_Bernstein:
4.102 - "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
4.103 - \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
4.104 - apply (rule decomposition [where f=f and g=g, THEN exE])
4.105 - apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI)
4.106 - --{*The term above can be synthesized by a sufficiently detailed proof.*}
4.107 - apply (rule bij_if_then_else)
4.108 - apply (rule_tac [4] refl)
4.109 - apply (rule_tac [2] inj_on_inv_into)
4.110 - apply (erule subset_inj_on [OF _ subset_UNIV])
4.111 - apply blast
4.112 - apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
4.113 - done
4.114 -
4.115 -
4.116 -subsection {* A simple party theorem *}
4.117 -
4.118 -text{* \emph{At any party there are two people who know the same
4.119 -number of people}. Provided the party consists of at least two people
4.120 -and the knows relation is symmetric. Knowing yourself does not count
4.121 ---- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
4.122 -at TPHOLs 2007.) *}
4.123 -
4.124 -lemma equal_number_of_acquaintances:
4.125 -assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
4.126 -shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
4.127 -proof -
4.128 - let ?N = "%a. card(R `` {a} - {a})"
4.129 - let ?n = "card A"
4.130 - have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
4.131 - have 0: "R `` A <= A" using `sym R` `Domain R <= A`
4.132 - unfolding Domain_def sym_def by blast
4.133 - have h: "ALL a:A. R `` {a} <= A" using 0 by blast
4.134 - hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
4.135 - by(blast intro: finite_subset)
4.136 - have sub: "?N ` A <= {0..<?n}"
4.137 - proof -
4.138 - have "ALL a:A. R `` {a} - {a} < A" using h by blast
4.139 - thus ?thesis using psubset_card_mono[OF `finite A`] by auto
4.140 - qed
4.141 - show "~ inj_on ?N A" (is "~ ?I")
4.142 - proof
4.143 - assume ?I
4.144 - hence "?n = card(?N ` A)" by(rule card_image[symmetric])
4.145 - with sub `finite A` have 2[simp]: "?N ` A = {0..<?n}"
4.146 - using subset_card_intvl_is_intvl[of _ 0] by(auto)
4.147 - have "0 : ?N ` A" and "?n - 1 : ?N ` A" using `card A \<ge> 2` by simp+
4.148 - then obtain a b where ab: "a:A" "b:A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
4.149 - by (auto simp del: 2)
4.150 - have "a \<noteq> b" using Na Nb `card A \<ge> 2` by auto
4.151 - have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
4.152 - hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
4.153 - hence "a \<notin> R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
4.154 - hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
4.155 - have 4: "finite (A - {a,b})" using `finite A` by simp
4.156 - have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
4.157 - then show False using Nb `card A \<ge> 2` by arith
4.158 - qed
4.159 -qed
4.160 -
4.161 -text {*
4.162 - From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
4.163 - 293-314.
4.164 -
4.165 - Isabelle can prove the easy examples without any special mechanisms,
4.166 - but it can't prove the hard ones.
4.167 -*}
4.168 -
4.169 -lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
4.170 - -- {* Example 1, page 295. *}
4.171 - by force
4.172 -
4.173 -lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
4.174 - -- {* Example 2. *}
4.175 - by force
4.176 -
4.177 -lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
4.178 - -- {* Example 3. *}
4.179 - by force
4.180 -
4.181 -lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
4.182 - -- {* Example 4. *}
4.183 - by force
4.184 -
4.185 -lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
4.186 - -- {*Example 5, page 298. *}
4.187 - by force
4.188 -
4.189 -lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
4.190 - -- {* Example 6. *}
4.191 - by force
4.192 -
4.193 -lemma "\<exists>A. a \<notin> A"
4.194 - -- {* Example 7. *}
4.195 - by force
4.196 -
4.197 -lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
4.198 - \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
4.199 - -- {* Example 8 now needs a small hint. *}
4.200 - by (simp add: abs_if, force)
4.201 - -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
4.202 -
4.203 -text {* Example 9 omitted (requires the reals). *}
4.204 -
4.205 -text {* The paper has no Example 10! *}
4.206 -
4.207 -lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
4.208 - P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
4.209 - -- {* Example 11: needs a hint. *}
4.210 -by(metis nat.induct)
4.211 -
4.212 -lemma
4.213 - "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
4.214 - \<and> P n \<longrightarrow> P m"
4.215 - -- {* Example 12. *}
4.216 - by auto
4.217 -
4.218 -lemma
4.219 - "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
4.220 - (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
4.221 - -- {* Example EO1: typo in article, and with the obvious fix it seems
4.222 - to require arithmetic reasoning. *}
4.223 - apply clarify
4.224 - apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)
4.225 - apply metis+
4.226 - done
4.227 -
4.228 -end