1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Sets/Examples.thy Mon Oct 23 16:24:52 2000 +0200
1.3 @@ -0,0 +1,278 @@
1.4 +theory Examples = Main:
1.5 +
1.6 +ML "reset eta_contract"
1.7 +ML "Pretty.setmargin 64"
1.8 +
1.9 +text{*membership, intersection *}
1.10 +text{*difference and empty set*}
1.11 +text{*complement, union and universal set*}
1.12 +
1.13 +lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
1.14 + apply (blast)
1.15 + done
1.16 +
1.17 +text{*
1.18 +@{thm[display] IntI[no_vars]}
1.19 +\rulename{IntI}
1.20 +
1.21 +@{thm[display] IntD1[no_vars]}
1.22 +\rulename{IntD1}
1.23 +
1.24 +@{thm[display] IntD2[no_vars]}
1.25 +\rulename{IntD2}
1.26 +*}
1.27 +
1.28 +lemma "(x \<in> -A) = (x \<notin> A)"
1.29 + apply (blast)
1.30 + done
1.31 +
1.32 +text{*
1.33 +@{thm[display] Compl_iff[no_vars]}
1.34 +\rulename{Compl_iff}
1.35 +*}
1.36 +
1.37 +lemma "- (A \<union> B) = -A \<inter> -B"
1.38 + apply (blast)
1.39 + done
1.40 +
1.41 +text{*
1.42 +@{thm[display] Compl_Un[no_vars]}
1.43 +\rulename{Compl_Un}
1.44 +*}
1.45 +
1.46 +lemma "A-A = {}"
1.47 + apply (blast)
1.48 + done
1.49 +
1.50 +text{*
1.51 +@{thm[display] Diff_disjoint[no_vars]}
1.52 +\rulename{Diff_disjoint}
1.53 +*}
1.54 +
1.55 +
1.56 +
1.57 +lemma "A \<union> -A = UNIV"
1.58 + apply (blast)
1.59 + done
1.60 +
1.61 +text{*
1.62 +@{thm[display] Compl_partition[no_vars]}
1.63 +\rulename{Compl_partition}
1.64 +*}
1.65 +
1.66 +text{*subset relation*}
1.67 +
1.68 +
1.69 +text{*
1.70 +@{thm[display] subsetI[no_vars]}
1.71 +\rulename{subsetI}
1.72 +
1.73 +@{thm[display] subsetD[no_vars]}
1.74 +\rulename{subsetD}
1.75 +*}
1.76 +
1.77 +lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
1.78 + apply (blast)
1.79 + done
1.80 +
1.81 +text{*
1.82 +@{thm[display] Un_subset_iff[no_vars]}
1.83 +\rulename{Un_subset_iff}
1.84 +*}
1.85 +
1.86 +lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
1.87 + apply (blast)
1.88 + done
1.89 +
1.90 +lemma "(A <= -B) = (B <= -A)"
1.91 + oops
1.92 +
1.93 +text{*ASCII version: blast fails because of overloading because
1.94 + it doesn't have to be sets*}
1.95 +
1.96 +lemma "((A:: 'a set) <= -B) = (B <= -A)"
1.97 + apply (blast)
1.98 + done
1.99 +
1.100 +text{*A type constraint lets it work*}
1.101 +
1.102 +text{*An issue here: how do we discuss the distinction between ASCII and
1.103 +X-symbol notation? Here the latter disambiguates.*}
1.104 +
1.105 +
1.106 +text{*
1.107 +set extensionality
1.108 +
1.109 +@{thm[display] set_ext[no_vars]}
1.110 +\rulename{set_ext}
1.111 +
1.112 +@{thm[display] equalityI[no_vars]}
1.113 +\rulename{equalityI}
1.114 +
1.115 +@{thm[display] equalityE[no_vars]}
1.116 +\rulename{equalityE}
1.117 +*}
1.118 +
1.119 +
1.120 +text{*finite sets: insertion and membership relation*}
1.121 +text{*finite set notation*}
1.122 +
1.123 +lemma "insert x A = {x} \<union> A"
1.124 + apply (blast)
1.125 + done
1.126 +
1.127 +text{*
1.128 +@{thm[display] insert_is_Un[no_vars]}
1.129 +\rulename{insert_is_Un}
1.130 +*}
1.131 +
1.132 +lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
1.133 + apply (blast)
1.134 + done
1.135 +
1.136 +lemma "{a,b} \<inter> {b,c} = {b}"
1.137 + apply (auto)
1.138 + oops
1.139 +text{*fails because it isn't valid*}
1.140 +
1.141 +lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
1.142 + apply (simp)
1.143 + apply (blast)
1.144 + done
1.145 +
1.146 +text{*or just force or auto. blast alone can't handle the if-then-else*}
1.147 +
1.148 +text{*next: some comprehension examples*}
1.149 +
1.150 +lemma "(a \<in> {z. P z}) = P a"
1.151 + apply (blast)
1.152 + done
1.153 +
1.154 +text{*
1.155 +@{thm[display] mem_Collect_eq[no_vars]}
1.156 +\rulename{mem_Collect_eq}
1.157 +*}
1.158 +
1.159 +lemma "{x. x \<in> A} = A"
1.160 + apply (blast)
1.161 + done
1.162 +
1.163 +text{*
1.164 +@{thm[display] Collect_mem_eq[no_vars]}
1.165 +\rulename{Collect_mem_eq}
1.166 +*}
1.167 +
1.168 +lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
1.169 + apply (blast)
1.170 + done
1.171 +
1.172 +lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
1.173 + apply (blast)
1.174 + done
1.175 +
1.176 +constdefs
1.177 + prime :: "nat set"
1.178 + "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
1.179 +
1.180 +lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} =
1.181 + {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
1.182 + apply (blast)
1.183 + done
1.184 +
1.185 +text{*binders*}
1.186 +
1.187 +text{*bounded quantifiers*}
1.188 +
1.189 +lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
1.190 + apply (blast)
1.191 + done
1.192 +
1.193 +text{*
1.194 +@{thm[display] bexI[no_vars]}
1.195 +\rulename{bexI}
1.196 +*}
1.197 +
1.198 +text{*
1.199 +@{thm[display] bexE[no_vars]}
1.200 +\rulename{bexE}
1.201 +*}
1.202 +
1.203 +lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
1.204 + apply (blast)
1.205 + done
1.206 +
1.207 +text{*
1.208 +@{thm[display] ballI[no_vars]}
1.209 +\rulename{ballI}
1.210 +*}
1.211 +
1.212 +text{*
1.213 +@{thm[display] bspec[no_vars]}
1.214 +\rulename{bspec}
1.215 +*}
1.216 +
1.217 +text{*indexed unions and variations*}
1.218 +
1.219 +lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
1.220 + apply (blast)
1.221 + done
1.222 +
1.223 +text{*
1.224 +@{thm[display] UN_iff[no_vars]}
1.225 +\rulename{UN_iff}
1.226 +*}
1.227 +
1.228 +text{*
1.229 +@{thm[display] Union_iff[no_vars]}
1.230 +\rulename{Union_iff}
1.231 +*}
1.232 +
1.233 +lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
1.234 + apply (blast)
1.235 + done
1.236 +
1.237 +lemma "\<Union>S = (\<Union>x\<in>S. x)"
1.238 + apply (blast)
1.239 + done
1.240 +
1.241 +text{*
1.242 +@{thm[display] UN_I[no_vars]}
1.243 +\rulename{UN_I}
1.244 +*}
1.245 +
1.246 +text{*
1.247 +@{thm[display] UN_E[no_vars]}
1.248 +\rulename{UN_E}
1.249 +*}
1.250 +
1.251 +text{*indexed intersections*}
1.252 +
1.253 +lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
1.254 + apply (blast)
1.255 + done
1.256 +
1.257 +text{*
1.258 +@{thm[display] INT_iff[no_vars]}
1.259 +\rulename{INT_iff}
1.260 +*}
1.261 +
1.262 +text{*
1.263 +@{thm[display] Inter_iff[no_vars]}
1.264 +\rulename{Inter_iff}
1.265 +*}
1.266 +
1.267 +text{*mention also card, Pow, etc.*}
1.268 +
1.269 +
1.270 +text{*
1.271 +@{thm[display] card_Un_Int[no_vars]}
1.272 +\rulename{card_Un_Int}
1.273 +
1.274 +@{thm[display] card_Pow[no_vars]}
1.275 +\rulename{card_Pow}
1.276 +
1.277 +@{thm[display] n_subsets[no_vars]}
1.278 +\rulename{n_subsets}
1.279 +*}
1.280 +
1.281 +end