author  wenzelm 
Tue, 07 May 2002 14:27:39 +0200  
changeset 13107  8743cc847224 
parent 13058  ad6106d7b4bb 
child 14353  79f9fbef9106 
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 

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

9 
theory set = Main: 

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 

13107  43 
lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}" 
44 
 {* Singleton I. Nice demonstration of @{text blast}and its limitations. *} 

45 
 {* For some unfathomable reason, @{text UNIV_I} increases the search space greatly. *} 

46 
by (blast del: UNIV_I) 

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

47 

13107  48 
lemma "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" 
49 
 {*Singleton II. Variant of the benchmark above. *} 

50 
by (blast del: UNIV_I) 

51 

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

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

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

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

56 
apply (erule arg_cong) 

57 
done 

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

58 

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

59 

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

60 

13107  61 
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

62 

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

65 
by best 

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

66 

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

69 
by best 

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

70 

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

73 
by (rule notI, erule rangeE, best) 

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

74 

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

77 
by best 

78 

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

79 

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

81 

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

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

84 

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

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

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

88 

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

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

92 
apply (unfold inj_on_def) 

93 
apply (simp add: surj_if_then_else) 

94 
apply (blast dest: disj_lemma sym) 

95 
done 

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

96 

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

99 
apply (rule lfp_unfold) 

100 
apply (rule monoI, blast) 

101 
done 

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

102 

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

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

106 
apply (rule decomposition [THEN exE]) 

107 
apply (rule exI) 

108 
apply (rule bij_if_then_else) 

109 
apply (rule_tac [4] refl) 

110 
apply (rule_tac [2] inj_on_inv) 

111 
apply (erule subset_inj_on [OF subset_UNIV]) 

112 
txt {* Tricky variable instantiations! *} 

113 
apply (erule ssubst, subst double_complement) 

114 
apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) 

115 
apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) 

116 
done 

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

117 

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

118 

13107  119 
subsection {* Set variable instantiation examples *} 
13058
ad6106d7b4bb
converted theory "set" to Isar and added some SETVAR examples
paulson
parents:
9100
diff
changeset

120 

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

123 
293314. 

124 

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

126 
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

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

128 

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

131 
by force 

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

132 

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

135 
by force 

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

136 

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

139 
by force 

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

140 

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

143 
by force 

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

144 

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

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 6. *} 

151 
by force 

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

152 

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

155 
by force 

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

156 

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

159 
 {* Example 8. *} 

160 
by force  {* 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

161 

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

163 

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

165 

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

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

169 
apply clarify 

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

171 
apply force 

172 
done 

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

173 

13107  174 
lemma 
175 
"(\<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) 

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

177 
 {* Example 12. *} 

178 
by auto 

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

179 

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

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

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

184 
to require arithmetic reasoning. *} 

185 
apply clarify 

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

187 
apply (case_tac v, auto) 

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

189 
done 

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

190 

9100  191 
end 