Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Sets/Examples.thy
changeset 10864 f0b0a125ae4b
parent 10341 6eb91805a012
child 12815 1f073030b97a
equal deleted inserted replaced
10863:fef84fefd33f 10864:f0b0a125ae4b 
     7 text{*membership, intersection *}
 
     7 text{*membership, intersection *}
 
     8 text{*difference and empty set*}
 
     8 text{*difference and empty set*}
 
     9 text{*complement, union and universal set*}
 
     9 text{*complement, union and universal set*}
 
    10 
    10 
    11 lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
 
    11 lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
 
    12   apply (blast)
 
    12 by blast
 
    13   done
 
       
    14 
    13 
    15 text{*
 
    14 text{*
 
    16 @{thm[display] IntI[no_vars]}
 
    15 @{thm[display] IntI[no_vars]}
 
    17 \rulename{IntI}
 
    16 \rulename{IntI}
 
    18 
    17 
    22 @{thm[display] IntD2[no_vars]}
 
    21 @{thm[display] IntD2[no_vars]}
 
    23 \rulename{IntD2}
 
    22 \rulename{IntD2}
 
    24 *}
 
    23 *}
 
    25 
    24 
    26 lemma "(x \<in> -A) = (x \<notin> A)"
 
    25 lemma "(x \<in> -A) = (x \<notin> A)"
 
    27   apply (blast)
 
    26 by blast
 
    28   done
 
       
    29 
    27 
    30 text{*
 
    28 text{*
 
    31 @{thm[display] Compl_iff[no_vars]}
 
    29 @{thm[display] Compl_iff[no_vars]}
 
    32 \rulename{Compl_iff}
 
    30 \rulename{Compl_iff}
 
    33 *}
 
    31 *}
 
    34 
    32 
    35 lemma "- (A \<union> B) = -A \<inter> -B"
 
    33 lemma "- (A \<union> B) = -A \<inter> -B"
 
    36   apply (blast)
 
    34 by blast
 
    37   done
 
       
    38 
    35 
    39 text{*
 
    36 text{*
 
    40 @{thm[display] Compl_Un[no_vars]}
 
    37 @{thm[display] Compl_Un[no_vars]}
 
    41 \rulename{Compl_Un}
 
    38 \rulename{Compl_Un}
 
    42 *}
 
    39 *}
 
    43 
    40 
    44 lemma "A-A = {}"
 
    41 lemma "A-A = {}"
 
    45   apply (blast)
 
    42 by blast
 
    46   done
 
       
    47 
    43 
    48 text{*
 
    44 text{*
 
    49 @{thm[display] Diff_disjoint[no_vars]}
 
    45 @{thm[display] Diff_disjoint[no_vars]}
 
    50 \rulename{Diff_disjoint}
 
    46 \rulename{Diff_disjoint}
 
    51 *}
 
    47 *}
 
    52 
    48 
    53   
    49   
    54 
    50 
    55 lemma "A \<union> -A = UNIV"
 
    51 lemma "A \<union> -A = UNIV"
 
    56   apply (blast)
 
    52 by blast
 
    57   done
 
       
    58 
    53 
    59 text{*
 
    54 text{*
 
    60 @{thm[display] Compl_partition[no_vars]}
 
    55 @{thm[display] Compl_partition[no_vars]}
 
    61 \rulename{Compl_partition}
 
    56 \rulename{Compl_partition}
 
    62 *}
 
    57 *}
 
    71 @{thm[display] subsetD[no_vars]}
 
    66 @{thm[display] subsetD[no_vars]}
 
    72 \rulename{subsetD}
 
    67 \rulename{subsetD}
 
    73 *}
 
    68 *}
 
    74 
    69 
    75 lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
 
    70 lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
 
    76   apply (blast)
 
    71 by blast
 
    77   done
 
       
    78 
    72 
    79 text{*
 
    73 text{*
 
    80 @{thm[display] Un_subset_iff[no_vars]}
 
    74 @{thm[display] Un_subset_iff[no_vars]}
 
    81 \rulename{Un_subset_iff}
 
    75 \rulename{Un_subset_iff}
 
    82 *}
 
    76 *}
 
    83 
    77 
    84 lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
 
    78 lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
 
    85   apply (blast)
 
    79 by blast
 
    86   done
 
       
    87 
    80 
    88 lemma "(A <= -B) = (B <= -A)"
 
    81 lemma "(A <= -B) = (B <= -A)"
 
    89   oops
 
    82   oops
 
    90 
    83 
    91 text{*ASCII version: blast fails because of overloading because
 
    84 text{*ASCII version: blast fails because of overloading because
 
    92  it doesn't have to be sets*}
 
    85  it doesn't have to be sets*}
 
    93 
    86 
    94 lemma "((A:: 'a set) <= -B) = (B <= -A)"
 
    87 lemma "((A:: 'a set) <= -B) = (B <= -A)"
 
    95   apply (blast)
 
    88 by blast
 
    96   done
 
       
    97 
    89 
    98 text{*A type constraint lets it work*}
 
    90 text{*A type constraint lets it work*}
 
    99 
    91 
   100 text{*An issue here: how do we discuss the distinction between ASCII and
 
    92 text{*An issue here: how do we discuss the distinction between ASCII and
 
   101 X-symbol notation?  Here the latter disambiguates.*}
 
    93 X-symbol notation?  Here the latter disambiguates.*}
 
   117 
   109 
   118 text{*finite sets: insertion and membership relation*}
 
   110 text{*finite sets: insertion and membership relation*}
 
   119 text{*finite set notation*}
 
   111 text{*finite set notation*}
 
   120 
   112 
   121 lemma "insert x A = {x} \<union> A"
 
   113 lemma "insert x A = {x} \<union> A"
 
   122   apply (blast)
 
   114 by blast
 
   123   done
 
       
   124 
   115 
   125 text{*
 
   116 text{*
 
   126 @{thm[display] insert_is_Un[no_vars]}
 
   117 @{thm[display] insert_is_Un[no_vars]}
 
   127 \rulename{insert_is_Un}
 
   118 \rulename{insert_is_Un}
 
   128 *}
 
   119 *}
 
   129 
   120 
   130 lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
 
   121 lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
 
   131   apply (blast)
 
   122 by blast
 
   132   done
 
       
   133 
   123 
   134 lemma "{a,b} \<inter> {b,c} = {b}"
 
   124 lemma "{a,b} \<inter> {b,c} = {b}"
 
   135   apply (auto)
 
   125 apply auto
 
   136   oops
 
   126 oops
 
   137 text{*fails because it isn't valid*}
 
   127 text{*fails because it isn't valid*}
 
   138 
   128 
   139 lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
 
   129 lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
 
   140   apply (simp)
 
   130 apply simp
 
   141   apply (blast)
 
   131 by blast
 
   142   done
 
       
   143 
   132 
   144 text{*or just force or auto.  blast alone can't handle the if-then-else*}
 
   133 text{*or just force or auto.  blast alone can't handle the if-then-else*}
 
   145 
   134 
   146 text{*next: some comprehension examples*}
 
   135 text{*next: some comprehension examples*}
 
   147 
   136 
   148 lemma "(a \<in> {z. P z}) = P a"
 
   137 lemma "(a \<in> {z. P z}) = P a"
 
   149   apply (blast)
 
   138 by blast
 
   150   done
 
       
   151 
   139 
   152 text{*
 
   140 text{*
 
   153 @{thm[display] mem_Collect_eq[no_vars]}
 
   141 @{thm[display] mem_Collect_eq[no_vars]}
 
   154 \rulename{mem_Collect_eq}
 
   142 \rulename{mem_Collect_eq}
 
   155 *}
 
   143 *}
 
   156 
   144 
   157 lemma "{x. x \<in> A} = A"
 
   145 lemma "{x. x \<in> A} = A"
 
   158   apply (blast)
 
   146 by blast
 
   159   done
 
       
   160   
   147   
   161 text{*
 
   148 text{*
 
   162 @{thm[display] Collect_mem_eq[no_vars]}
 
   149 @{thm[display] Collect_mem_eq[no_vars]}
 
   163 \rulename{Collect_mem_eq}
 
   150 \rulename{Collect_mem_eq}
 
   164 *}
 
   151 *}
 
   165 
   152 
   166 lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
 
   153 lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
 
   167   apply (blast)
 
   154 by blast
 
   168   done
 
       
   169 
   155 
   170 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
 
   156 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
 
   171   apply (blast)
 
   157 by blast
 
   172   done
 
       
   173 
   158 
   174 constdefs
 
   159 constdefs
 
   175   prime   :: "nat set"
 
   160   prime   :: "nat set"
 
   176     "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
 
   161     "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
 
   177 
   162 
   178 lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = 
   163 lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = 
   179        {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
 
   164        {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
 
   180   apply (blast)
 
   165 by (rule refl)
 
   181   done
 
       
   182 
   166 
   183 text{*binders*}
 
   167 text{*binders*}
 
   184 
   168 
   185 text{*bounded quantifiers*}
 
   169 text{*bounded quantifiers*}
 
   186 
   170 
   187 lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
 
   171 lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
 
   188   apply (blast)
 
   172 by blast
 
   189   done
 
       
   190 
   173 
   191 text{*
 
   174 text{*
 
   192 @{thm[display] bexI[no_vars]}
 
   175 @{thm[display] bexI[no_vars]}
 
   193 \rulename{bexI}
 
   176 \rulename{bexI}
 
   194 *}
 
   177 *}
 
   197 @{thm[display] bexE[no_vars]}
 
   180 @{thm[display] bexE[no_vars]}
 
   198 \rulename{bexE}
 
   181 \rulename{bexE}
 
   199 *}
 
   182 *}
 
   200 
   183 
   201 lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
 
   184 lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
 
   202   apply (blast)
 
   185 by blast
 
   203   done
 
       
   204 
   186 
   205 text{*
 
   187 text{*
 
   206 @{thm[display] ballI[no_vars]}
 
   188 @{thm[display] ballI[no_vars]}
 
   207 \rulename{ballI}
 
   189 \rulename{ballI}
 
   208 *}
 
   190 *}
 
   213 *}
 
   195 *}
 
   214 
   196 
   215 text{*indexed unions and variations*}
 
   197 text{*indexed unions and variations*}
 
   216 
   198 
   217 lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
 
   199 lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
 
   218   apply (blast)
 
   200 by blast
 
   219   done
 
       
   220 
   201 
   221 text{*
 
   202 text{*
 
   222 @{thm[display] UN_iff[no_vars]}
 
   203 @{thm[display] UN_iff[no_vars]}
 
   223 \rulename{UN_iff}
 
   204 \rulename{UN_iff}
 
   224 *}
 
   205 *}
 
   227 @{thm[display] Union_iff[no_vars]}
 
   208 @{thm[display] Union_iff[no_vars]}
 
   228 \rulename{Union_iff}
 
   209 \rulename{Union_iff}
 
   229 *}
 
   210 *}
 
   230 
   211 
   231 lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
 
   212 lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
 
   232   apply (blast)
 
   213 by blast
 
   233   done
 
       
   234 
   214 
   235 lemma "\<Union>S = (\<Union>x\<in>S. x)"
 
   215 lemma "\<Union>S = (\<Union>x\<in>S. x)"
 
   236   apply (blast)
 
   216 by blast
 
   237   done
 
       
   238 
   217 
   239 text{*
 
   218 text{*
 
   240 @{thm[display] UN_I[no_vars]}
 
   219 @{thm[display] UN_I[no_vars]}
 
   241 \rulename{UN_I}
 
   220 \rulename{UN_I}
 
   242 *}
 
   221 *}
 
   247 *}
 
   226 *}
 
   248 
   227 
   249 text{*indexed intersections*}
 
   228 text{*indexed intersections*}
 
   250 
   229 
   251 lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
 
   230 lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
 
   252   apply (blast)
 
   231 by blast
 
   253   done
 
       
   254 
   232 
   255 text{*
 
   233 text{*
 
   256 @{thm[display] INT_iff[no_vars]}
 
   234 @{thm[display] INT_iff[no_vars]}
 
   257 \rulename{INT_iff}
 
   235 \rulename{INT_iff}
 
   258 *}
 
   236 *}
isabelle