wneuper/isa: doc-src/TutorialI/Sets/Examples.thy@403585a89772

     1 (* ID:         $Id$ *)

     2 theory Examples imports Main Binomial begin

     4 ML "Unsynchronized.reset eta_contract"

     5 ML "Pretty.margin_default := 64"

     7 text{*membership, intersection *}

     8 text{*difference and empty set*}

     9 text{*complement, union and universal set*}

    11 lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"

    12 by blast

    14 text{*

    15 @{thm[display] IntI[no_vars]}

    16 \rulename{IntI}

    18 @{thm[display] IntD1[no_vars]}

    19 \rulename{IntD1}

    21 @{thm[display] IntD2[no_vars]}

    22 \rulename{IntD2}

    23 *}

    25 lemma "(x \<in> -A) = (x \<notin> A)"

    26 by blast

    28 text{*

    29 @{thm[display] Compl_iff[no_vars]}

    30 \rulename{Compl_iff}

    31 *}

    33 lemma "- (A \<union> B) = -A \<inter> -B"

    34 by blast

    36 text{*

    37 @{thm[display] Compl_Un[no_vars]}

    38 \rulename{Compl_Un}

    39 *}

    41 lemma "A-A = {}"

    42 by blast

    44 text{*

    45 @{thm[display] Diff_disjoint[no_vars]}

    46 \rulename{Diff_disjoint}

    47 *}

    51 lemma "A \<union> -A = UNIV"

    52 by blast

    54 text{*

    55 @{thm[display] Compl_partition[no_vars]}

    56 \rulename{Compl_partition}

    57 *}

    59 text{*subset relation*}

    62 text{*

    63 @{thm[display] subsetI[no_vars]}

    64 \rulename{subsetI}

    66 @{thm[display] subsetD[no_vars]}

    67 \rulename{subsetD}

    68 *}

    70 lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"

    71 by blast

    73 text{*

    74 @{thm[display] Un_subset_iff[no_vars]}

    75 \rulename{Un_subset_iff}

    76 *}

    78 lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"

    79 by blast

    81 lemma "(A <= -B) = (B <= -A)"

    82   oops

    84 text{*ASCII version: blast fails because of overloading because

    85  it doesn't have to be sets*}

    87 lemma "((A:: 'a set) <= -B) = (B <= -A)"

    88 by blast

    90 text{*A type constraint lets it work*}

    92 text{*An issue here: how do we discuss the distinction between ASCII and

    93 symbol notation?  Here the latter disambiguates.*}

    96 text{*

    97 set extensionality

    99 @{thm[display] set_ext[no_vars]}

   100 \rulename{set_ext}

   102 @{thm[display] equalityI[no_vars]}

   103 \rulename{equalityI}

   105 @{thm[display] equalityE[no_vars]}

   106 \rulename{equalityE}

   107 *}

   110 text{*finite sets: insertion and membership relation*}

   111 text{*finite set notation*}

   113 lemma "insert x A = {x} \<union> A"

   114 by blast

   116 text{*

   117 @{thm[display] insert_is_Un[no_vars]}

   118 \rulename{insert_is_Un}

   119 *}

   121 lemma "{a,b} \<union> {c,d} = {a,b,c,d}"

   122 by blast

   124 lemma "{a,b} \<inter> {b,c} = {b}"

   125 apply auto

   126 oops

   127 text{*fails because it isn't valid*}

   129 lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"

   130 apply simp

   131 by blast

   133 text{*or just force or auto.  blast alone can't handle the if-then-else*}

   135 text{*next: some comprehension examples*}

   137 lemma "(a \<in> {z. P z}) = P a"

   138 by blast

   140 text{*

   141 @{thm[display] mem_Collect_eq[no_vars]}

   142 \rulename{mem_Collect_eq}

   143 *}

   145 lemma "{x. x \<in> A} = A"

   146 by blast

   148 text{*

   149 @{thm[display] Collect_mem_eq[no_vars]}

   150 \rulename{Collect_mem_eq}

   151 *}

   153 lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"

   154 by blast

   156 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"

   157 by blast

   159 definition prime :: "nat set" where

   160     "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"

   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}"

   164 by (rule refl)

   166 text{*binders*}

   168 text{*bounded quantifiers*}

   170 lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"

   171 by blast

   173 text{*

   174 @{thm[display] bexI[no_vars]}

   175 \rulename{bexI}

   176 *}

   178 text{*

   179 @{thm[display] bexE[no_vars]}

   180 \rulename{bexE}

   181 *}

   183 lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"

   184 by blast

   186 text{*

   187 @{thm[display] ballI[no_vars]}

   188 \rulename{ballI}

   189 *}

   191 text{*

   192 @{thm[display] bspec[no_vars]}

   193 \rulename{bspec}

   194 *}

   196 text{*indexed unions and variations*}

   198 lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"

   199 by blast

   201 text{*

   202 @{thm[display] UN_iff[no_vars]}

   203 \rulename{UN_iff}

   204 *}

   206 text{*

   207 @{thm[display] Union_iff[no_vars]}

   208 \rulename{Union_iff}

   209 *}

   211 lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"

   212 by blast

   214 lemma "\<Union>S = (\<Union>x\<in>S. x)"

   215 by blast

   217 text{*

   218 @{thm[display] UN_I[no_vars]}

   219 \rulename{UN_I}

   220 *}

   222 text{*

   223 @{thm[display] UN_E[no_vars]}

   224 \rulename{UN_E}

   225 *}

   227 text{*indexed intersections*}

   229 lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"

   230 by blast

   232 text{*

   233 @{thm[display] INT_iff[no_vars]}

   234 \rulename{INT_iff}

   235 *}

   237 text{*

   238 @{thm[display] Inter_iff[no_vars]}

   239 \rulename{Inter_iff}

   240 *}

   242 text{*mention also card, Pow, etc.*}

   245 text{*

   246 @{thm[display] card_Un_Int[no_vars]}

   247 \rulename{card_Un_Int}

   249 @{thm[display] card_Pow[no_vars]}

   250 \rulename{card_Pow}

   252 @{thm[display] n_subsets[no_vars]}

   253 \rulename{n_subsets}

   254 *}

   256 end

author	wenzelm
	Sat, 08 May 2010 19:14:13 +0200
changeset 36754	403585a89772
parent 35413	d8d7d1b785af
child 39065	89f273ab1d42
permissions	-rw-r--r--