1 theory Examples imports Main Binomial begin
3 ML "eta_contract := false"
4 ML "Pretty.margin_default := 64"
6 text{*membership, intersection *}
7 text{*difference and empty set*}
8 text{*complement, union and universal set*}
10 lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
14 @{thm[display] IntI[no_vars]}
17 @{thm[display] IntD1[no_vars]}
20 @{thm[display] IntD2[no_vars]}
24 lemma "(x \<in> -A) = (x \<notin> A)"
28 @{thm[display] Compl_iff[no_vars]}
32 lemma "- (A \<union> B) = -A \<inter> -B"
36 @{thm[display] Compl_Un[no_vars]}
44 @{thm[display] Diff_disjoint[no_vars]}
45 \rulename{Diff_disjoint}
50 lemma "A \<union> -A = UNIV"
54 @{thm[display] Compl_partition[no_vars]}
55 \rulename{Compl_partition}
58 text{*subset relation*}
62 @{thm[display] subsetI[no_vars]}
65 @{thm[display] subsetD[no_vars]}
69 lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
73 @{thm[display] Un_subset_iff[no_vars]}
74 \rulename{Un_subset_iff}
77 lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
80 lemma "(A <= -B) = (B <= -A)"
83 text{*ASCII version: blast fails because of overloading because
84 it doesn't have to be sets*}
86 lemma "((A:: 'a set) <= -B) = (B <= -A)"
89 text{*A type constraint lets it work*}
91 text{*An issue here: how do we discuss the distinction between ASCII and
92 symbol notation? Here the latter disambiguates.*}
98 @{thm[display] set_ext[no_vars]}
101 @{thm[display] equalityI[no_vars]}
104 @{thm[display] equalityE[no_vars]}
109 text{*finite sets: insertion and membership relation*}
110 text{*finite set notation*}
112 lemma "insert x A = {x} \<union> A"
116 @{thm[display] insert_is_Un[no_vars]}
117 \rulename{insert_is_Un}
120 lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
123 lemma "{a,b} \<inter> {b,c} = {b}"
126 text{*fails because it isn't valid*}
128 lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
132 text{*or just force or auto. blast alone can't handle the if-then-else*}
134 text{*next: some comprehension examples*}
136 lemma "(a \<in> {z. P z}) = P a"
140 @{thm[display] mem_Collect_eq[no_vars]}
141 \rulename{mem_Collect_eq}
144 lemma "{x. x \<in> A} = A"
148 @{thm[display] Collect_mem_eq[no_vars]}
149 \rulename{Collect_mem_eq}
152 lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
155 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
158 definition prime :: "nat set" where
159 "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
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}"
167 text{*bounded quantifiers*}
169 lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
173 @{thm[display] bexI[no_vars]}
178 @{thm[display] bexE[no_vars]}
182 lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
186 @{thm[display] ballI[no_vars]}
191 @{thm[display] bspec[no_vars]}
195 text{*indexed unions and variations*}
197 lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
201 @{thm[display] UN_iff[no_vars]}
206 @{thm[display] Union_iff[no_vars]}
210 lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
213 lemma "\<Union>S = (\<Union>x\<in>S. x)"
217 @{thm[display] UN_I[no_vars]}
222 @{thm[display] UN_E[no_vars]}
226 text{*indexed intersections*}
228 lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
232 @{thm[display] INT_iff[no_vars]}
237 @{thm[display] Inter_iff[no_vars]}
241 text{*mention also card, Pow, etc.*}
245 @{thm[display] card_Un_Int[no_vars]}
246 \rulename{card_Un_Int}
248 @{thm[display] card_Pow[no_vars]}
251 @{thm[display] n_subsets[no_vars]}