author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 48611 | doc-src/TutorialI/Sets/Examples.thy@b34ff75c23a7 |
child 55159 | 608c157d743d |
permissions | -rw-r--r-- |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39795
diff
changeset
|
1 |
theory Examples imports Main "~~/src/HOL/Library/Binomial" begin |
10294 | 2 |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38798
diff
changeset
|
3 |
declare [[eta_contract = false]] |
10294 | 4 |
|
5 |
text{*membership, intersection *} |
|
6 |
text{*difference and empty set*} |
|
7 |
text{*complement, union and universal set*} |
|
8 |
||
9 |
lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
10 |
by blast |
10294 | 11 |
|
12 |
text{* |
|
13 |
@{thm[display] IntI[no_vars]} |
|
14 |
\rulename{IntI} |
|
15 |
||
16 |
@{thm[display] IntD1[no_vars]} |
|
17 |
\rulename{IntD1} |
|
18 |
||
19 |
@{thm[display] IntD2[no_vars]} |
|
20 |
\rulename{IntD2} |
|
21 |
*} |
|
22 |
||
23 |
lemma "(x \<in> -A) = (x \<notin> A)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
24 |
by blast |
10294 | 25 |
|
26 |
text{* |
|
27 |
@{thm[display] Compl_iff[no_vars]} |
|
28 |
\rulename{Compl_iff} |
|
29 |
*} |
|
30 |
||
31 |
lemma "- (A \<union> B) = -A \<inter> -B" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
32 |
by blast |
10294 | 33 |
|
34 |
text{* |
|
35 |
@{thm[display] Compl_Un[no_vars]} |
|
36 |
\rulename{Compl_Un} |
|
37 |
*} |
|
38 |
||
39 |
lemma "A-A = {}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
40 |
by blast |
10294 | 41 |
|
42 |
text{* |
|
43 |
@{thm[display] Diff_disjoint[no_vars]} |
|
44 |
\rulename{Diff_disjoint} |
|
45 |
*} |
|
46 |
||
47 |
||
48 |
||
49 |
lemma "A \<union> -A = UNIV" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
50 |
by blast |
10294 | 51 |
|
52 |
text{* |
|
53 |
@{thm[display] Compl_partition[no_vars]} |
|
54 |
\rulename{Compl_partition} |
|
55 |
*} |
|
56 |
||
57 |
text{*subset relation*} |
|
58 |
||
59 |
||
60 |
text{* |
|
61 |
@{thm[display] subsetI[no_vars]} |
|
62 |
\rulename{subsetI} |
|
63 |
||
64 |
@{thm[display] subsetD[no_vars]} |
|
65 |
\rulename{subsetD} |
|
66 |
*} |
|
67 |
||
68 |
lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
69 |
by blast |
10294 | 70 |
|
71 |
text{* |
|
72 |
@{thm[display] Un_subset_iff[no_vars]} |
|
73 |
\rulename{Un_subset_iff} |
|
74 |
*} |
|
75 |
||
76 |
lemma "(A \<subseteq> -B) = (B \<subseteq> -A)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
77 |
by blast |
10294 | 78 |
|
79 |
lemma "(A <= -B) = (B <= -A)" |
|
80 |
oops |
|
81 |
||
82 |
text{*ASCII version: blast fails because of overloading because |
|
83 |
it doesn't have to be sets*} |
|
84 |
||
85 |
lemma "((A:: 'a set) <= -B) = (B <= -A)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
86 |
by blast |
10294 | 87 |
|
88 |
text{*A type constraint lets it work*} |
|
89 |
||
90 |
text{*An issue here: how do we discuss the distinction between ASCII and |
|
12815 | 91 |
symbol notation? Here the latter disambiguates.*} |
10294 | 92 |
|
93 |
||
94 |
text{* |
|
95 |
set extensionality |
|
96 |
||
39795 | 97 |
@{thm[display] set_eqI[no_vars]} |
98 |
\rulename{set_eqI} |
|
10294 | 99 |
|
100 |
@{thm[display] equalityI[no_vars]} |
|
101 |
\rulename{equalityI} |
|
102 |
||
103 |
@{thm[display] equalityE[no_vars]} |
|
104 |
\rulename{equalityE} |
|
105 |
*} |
|
106 |
||
107 |
||
108 |
text{*finite sets: insertion and membership relation*} |
|
109 |
text{*finite set notation*} |
|
110 |
||
111 |
lemma "insert x A = {x} \<union> A" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
112 |
by blast |
10294 | 113 |
|
114 |
text{* |
|
115 |
@{thm[display] insert_is_Un[no_vars]} |
|
116 |
\rulename{insert_is_Un} |
|
117 |
*} |
|
118 |
||
119 |
lemma "{a,b} \<union> {c,d} = {a,b,c,d}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
120 |
by blast |
10294 | 121 |
|
122 |
lemma "{a,b} \<inter> {b,c} = {b}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
123 |
apply auto |
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
124 |
oops |
10294 | 125 |
text{*fails because it isn't valid*} |
126 |
||
127 |
lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
128 |
apply simp |
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
129 |
by blast |
10294 | 130 |
|
131 |
text{*or just force or auto. blast alone can't handle the if-then-else*} |
|
132 |
||
133 |
text{*next: some comprehension examples*} |
|
134 |
||
135 |
lemma "(a \<in> {z. P z}) = P a" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
136 |
by blast |
10294 | 137 |
|
138 |
text{* |
|
139 |
@{thm[display] mem_Collect_eq[no_vars]} |
|
140 |
\rulename{mem_Collect_eq} |
|
141 |
*} |
|
142 |
||
143 |
lemma "{x. x \<in> A} = A" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
144 |
by blast |
10294 | 145 |
|
146 |
text{* |
|
147 |
@{thm[display] Collect_mem_eq[no_vars]} |
|
148 |
\rulename{Collect_mem_eq} |
|
149 |
*} |
|
150 |
||
151 |
lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
152 |
by blast |
10294 | 153 |
|
154 |
lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
155 |
by blast |
10294 | 156 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32833
diff
changeset
|
157 |
definition prime :: "nat set" where |
10294 | 158 |
"prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" |
159 |
||
160 |
lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = |
|
161 |
{z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
162 |
by (rule refl) |
10294 | 163 |
|
164 |
text{*binders*} |
|
165 |
||
166 |
text{*bounded quantifiers*} |
|
167 |
||
168 |
lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
169 |
by blast |
10294 | 170 |
|
171 |
text{* |
|
172 |
@{thm[display] bexI[no_vars]} |
|
173 |
\rulename{bexI} |
|
174 |
*} |
|
175 |
||
176 |
text{* |
|
177 |
@{thm[display] bexE[no_vars]} |
|
178 |
\rulename{bexE} |
|
179 |
*} |
|
180 |
||
181 |
lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
182 |
by blast |
10294 | 183 |
|
184 |
text{* |
|
185 |
@{thm[display] ballI[no_vars]} |
|
186 |
\rulename{ballI} |
|
187 |
*} |
|
188 |
||
189 |
text{* |
|
190 |
@{thm[display] bspec[no_vars]} |
|
191 |
\rulename{bspec} |
|
192 |
*} |
|
193 |
||
194 |
text{*indexed unions and variations*} |
|
195 |
||
196 |
lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
197 |
by blast |
10294 | 198 |
|
199 |
text{* |
|
200 |
@{thm[display] UN_iff[no_vars]} |
|
201 |
\rulename{UN_iff} |
|
202 |
*} |
|
203 |
||
204 |
text{* |
|
205 |
@{thm[display] Union_iff[no_vars]} |
|
206 |
\rulename{Union_iff} |
|
207 |
*} |
|
208 |
||
209 |
lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
210 |
by blast |
10294 | 211 |
|
212 |
lemma "\<Union>S = (\<Union>x\<in>S. x)" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
213 |
by blast |
10294 | 214 |
|
215 |
text{* |
|
216 |
@{thm[display] UN_I[no_vars]} |
|
217 |
\rulename{UN_I} |
|
218 |
*} |
|
219 |
||
220 |
text{* |
|
221 |
@{thm[display] UN_E[no_vars]} |
|
222 |
\rulename{UN_E} |
|
223 |
*} |
|
224 |
||
225 |
text{*indexed intersections*} |
|
226 |
||
227 |
lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}" |
|
10864
f0b0a125ae4b
revisions corresponding to the new version of sets.tex
paulson
parents:
10341
diff
changeset
|
228 |
by blast |
10294 | 229 |
|
230 |
text{* |
|
231 |
@{thm[display] INT_iff[no_vars]} |
|
232 |
\rulename{INT_iff} |
|
233 |
*} |
|
234 |
||
235 |
text{* |
|
236 |
@{thm[display] Inter_iff[no_vars]} |
|
237 |
\rulename{Inter_iff} |
|
238 |
*} |
|
239 |
||
240 |
text{*mention also card, Pow, etc.*} |
|
241 |
||
242 |
||
243 |
text{* |
|
244 |
@{thm[display] card_Un_Int[no_vars]} |
|
245 |
\rulename{card_Un_Int} |
|
246 |
||
247 |
@{thm[display] card_Pow[no_vars]} |
|
248 |
\rulename{card_Pow} |
|
249 |
||
250 |
@{thm[display] n_subsets[no_vars]} |
|
251 |
\rulename{n_subsets} |
|
252 |
*} |
|
253 |
||
254 |
end |