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