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