author  paulson 
Tue, 01 Feb 2005 18:01:57 +0100  
changeset 15481  fc075ae929e4 
parent 15306  51f3d31e8eea 
child 15488  7c638a46dcbb 
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) 

15306  111 
apply (erule subset_inj_on [OF _ subset_UNIV]) 
13107  112 
txt {* Tricky variable instantiations! *} 
15481  113 
apply (erule ssubst, simplesubst double_complement) 
13107  114 
apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) 
15481  115 
apply (erule ssubst, simplesubst double_complement, erule inv_image_comp [symmetric]) 
13107  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)" 

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

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

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

161 
 {* 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

162 

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

164 

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

166 

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

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

170 
apply clarify 

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

172 
apply force 

173 
done 

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

174 

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

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

178 
 {* Example 12. *} 

179 
by auto 

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

180 

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

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

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

185 
to require arithmetic reasoning. *} 

186 
apply clarify 

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

188 
apply (case_tac v, auto) 

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

190 
done 

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

191 

9100  192 
end 