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