doc-src/TutorialI/Sets/Examples.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39795 9e59b4c11039
child 48611 b34ff75c23a7
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 theory Examples imports Main "~~/src/HOL/Library/Binomial" begin
     2 
     3 declare [[eta_contract = false]]
     4 ML "Pretty.margin_default := 64"
     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)"
    11 by blast
    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)"
    25 by blast
    26 
    27 text{*
    28 @{thm[display] Compl_iff[no_vars]}
    29 \rulename{Compl_iff}
    30 *}
    31 
    32 lemma "- (A \<union> B) = -A \<inter> -B"
    33 by blast
    34 
    35 text{*
    36 @{thm[display] Compl_Un[no_vars]}
    37 \rulename{Compl_Un}
    38 *}
    39 
    40 lemma "A-A = {}"
    41 by blast
    42 
    43 text{*
    44 @{thm[display] Diff_disjoint[no_vars]}
    45 \rulename{Diff_disjoint}
    46 *}
    47 
    48   
    49 
    50 lemma "A \<union> -A = UNIV"
    51 by blast
    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)"
    70 by blast
    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)"
    78 by blast
    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)"
    87 by blast
    88 
    89 text{*A type constraint lets it work*}
    90 
    91 text{*An issue here: how do we discuss the distinction between ASCII and
    92 symbol notation?  Here the latter disambiguates.*}
    93 
    94 
    95 text{*
    96 set extensionality
    97 
    98 @{thm[display] set_eqI[no_vars]}
    99 \rulename{set_eqI}
   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"
   113 by blast
   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}"
   121 by blast
   122 
   123 lemma "{a,b} \<inter> {b,c} = {b}"
   124 apply auto
   125 oops
   126 text{*fails because it isn't valid*}
   127 
   128 lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
   129 apply simp
   130 by blast
   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"
   137 by blast
   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"
   145 by blast
   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"
   153 by blast
   154 
   155 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
   156 by blast
   157 
   158 definition prime :: "nat set" where
   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}"
   163 by (rule refl)
   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)"
   170 by blast
   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)"
   183 by blast
   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)"
   198 by blast
   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}"
   211 by blast
   212 
   213 lemma "\<Union>S = (\<Union>x\<in>S. x)"
   214 by blast
   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}"
   229 by blast
   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