author  ballarin 
Tue, 04 Jul 2006 11:36:08 +0200  
changeset 19982  e4d50f8f3722 
parent 18391  2e901da7cd3a 
child 24573  5bbdc9b60648 
permissions  rwrr 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

1 
(* Title: HOL/ex/set.thy 
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

2 
ID: $Id$ 
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

3 
Author: Tobias Nipkow and Lawrence C Paulson 
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

4 
Copyright 1991 University of Cambridge 
13107  5 
*) 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

6 

19982  7 
header {* Set Theory examples: Cantor's Theorem, SchröderBernstein Theorem, etc. *} 
9100  8 

16417  9 
theory set imports Main begin 
9100  10 

13107  11 
text{* 
12 
These two are cited in Benzmueller and Kohlhase's system description 

13 
of LEO, CADE15, 1998 (pages 139143) as theorems LEO could not 

14 
prove. 

15 
*} 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

16 

13107  17 
lemma "(X = Y \<union> Z) = 
18 
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" 

19 
by blast 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

20 

13107  21 
lemma "(X = Y \<inter> Z) = 
22 
(X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))" 

23 
by blast 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

24 

13107  25 
text {* 
26 
Trivial example of term synthesis: apparently hard for some provers! 

27 
*} 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

28 

13107  29 
lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X" 
30 
by blast 

31 

32 

33 
subsection {* Examples for the @{text blast} paper *} 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

34 

13107  35 
lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C) \<union> \<Union>(g ` C)" 
36 
 {* Unionimage, called @{text Un_Union_image} in Main HOL *} 

37 
by blast 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

38 

13107  39 
lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)" 
40 
 {* Interimage, called @{text Int_Inter_image} in Main HOL *} 

41 
by blast 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

42 

16898  43 
lemma singleton_example_1: 
44 
"\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}" 

18391  45 
by blast 
46 
(*With removal of negated equality literals, this no longer works: 

16898  47 
by (meson subsetI subset_antisym insertCI) 
18391  48 
*) 
16898  49 

50 
lemma singleton_example_2: 

51 
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" 

52 
 {*Variant of the problem above. *} 

18391  53 
by blast 
54 
(*With removal of negated equality literals, this no longer works: 

16898  55 
by (meson subsetI subset_antisym insertCI UnionI) 
18391  56 
*) 
16898  57 

13107  58 

59 
lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y" 

60 
 {* A unique fixpoint theorem  @{text fast}/@{text best}/@{text meson} all fail. *} 

61 
apply (erule ex1E, rule ex1I, erule arg_cong) 

62 
apply (rule subst, assumption, erule allE, rule arg_cong, erule mp) 

63 
apply (erule arg_cong) 

64 
done 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

65 

ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

66 

ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

67 

13107  68 
subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *} 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

69 

13107  70 
lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)" 
71 
 {* Requires bestfirst search because it is undirectional. *} 

72 
by best 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

73 

13107  74 
lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f" 
75 
 {*This form displays the diagonal term. *} 

76 
by best 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

77 

13107  78 
lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)" 
79 
 {* This form exploits the set constructs. *} 

80 
by (rule notI, erule rangeE, best) 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

81 

13107  82 
lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)" 
83 
 {* Or just this! *} 

84 
by best 

85 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

86 

13107  87 
subsection {* The SchröderBerstein Theorem *} 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

88 

13107  89 
lemma disj_lemma: " (f ` X) = g ` (X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X" 
90 
by blast 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

91 

ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

92 
lemma surj_if_then_else: 
13107  93 
"(f ` X) = g ` (X) \<Longrightarrow> surj (\<lambda>z. if z \<in> X then f z else g z)" 
94 
by (simp add: surj_def) blast 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

95 

13107  96 
lemma bij_if_then_else: 
97 
"inj_on f X \<Longrightarrow> inj_on g (X) \<Longrightarrow> (f ` X) = g ` (X) \<Longrightarrow> 

98 
h = (\<lambda>z. if z \<in> X then f z else g z) \<Longrightarrow> inj h \<and> surj h" 

99 
apply (unfold inj_on_def) 

100 
apply (simp add: surj_if_then_else) 

101 
apply (blast dest: disj_lemma sym) 

102 
done 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

103 

13107  104 
lemma decomposition: "\<exists>X. X =  (g ` ( (f ` X)))" 
105 
apply (rule exI) 

106 
apply (rule lfp_unfold) 

107 
apply (rule monoI, blast) 

108 
done 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

109 

13107  110 
theorem Schroeder_Bernstein: 
111 
"inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a) 

112 
\<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h" 

15488  113 
apply (rule decomposition [where f=f and g=g, THEN exE]) 
114 
apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI) 

115 
{*The term above can be synthesized by a sufficiently detailed proof.*} 

13107  116 
apply (rule bij_if_then_else) 
117 
apply (rule_tac [4] refl) 

118 
apply (rule_tac [2] inj_on_inv) 

15306  119 
apply (erule subset_inj_on [OF _ subset_UNIV]) 
15488  120 
apply blast 
121 
apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) 

13107  122 
done 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

123 

ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

124 

13107  125 
text {* 
126 
From W. W. Bledsoe and Guohui Feng, SETVAR. JAR 11 (3), 1993, pages 

127 
293314. 

128 

129 
Isabelle can prove the easy examples without any special mechanisms, 

130 
but it can't prove the hard ones. 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

131 
*} 
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

132 

13107  133 
lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))" 
134 
 {* Example 1, page 295. *} 

135 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

136 

13107  137 
lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B" 
138 
 {* Example 2. *} 

139 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

140 

13107  141 
lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)" 
142 
 {* Example 3. *} 

143 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

144 

13107  145 
lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A" 
146 
 {* Example 4. *} 

147 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

148 

13107  149 
lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" 
150 
 {*Example 5, page 298. *} 

151 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

152 

13107  153 
lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" 
154 
 {* Example 6. *} 

155 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

156 

13107  157 
lemma "\<exists>A. a \<notin> A" 
158 
 {* Example 7. *} 

159 
by force 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

160 

13107  161 
lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v) 
162 
\<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> 2 \<in> A)" 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13107
diff
changeset

163 
 {* Example 8 now needs a small hint. *} 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13107
diff
changeset

164 
by (simp add: abs_if, force) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13107
diff
changeset

165 
 {* not @{text blast}, which can't simplify @{text "2 < 0"} *} 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

166 

13107  167 
text {* Example 9 omitted (requires the reals). *} 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

168 

13107  169 
text {* The paper has no Example 10! *} 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

170 

13107  171 
lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and> 
172 
P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n" 

173 
 {* Example 11: needs a hint. *} 

174 
apply clarify 

175 
apply (drule_tac x = "{x. P x}" in spec) 

176 
apply force 

177 
done 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

178 

13107  179 
lemma 
180 
"(\<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) 

181 
\<and> P n \<longrightarrow> P m" 

182 
 {* Example 12. *} 

183 
by auto 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

184 

13107  185 
lemma 
186 
"(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow> 

187 
(\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))" 

188 
 {* Example EO1: typo in article, and with the obvious fix it seems 

189 
to require arithmetic reasoning. *} 

190 
apply clarify 

191 
apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto) 

192 
apply (case_tac v, auto) 

193 
apply (drule_tac x = "Suc v" and P = "\<lambda>x. ?a x \<noteq> ?b x" in spec, force) 

194 
done 

13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

195 

9100  196 
end 