doc-src/TutorialI/Sets/Examples.thy
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 12815 1f073030b97a
child 16417 9bc16273c2d4
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10341
6eb91805a012 added the $Id:$ line
paulson
parents: 10294
diff changeset
     1
(* ID:         $Id$ *)
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     2
theory Examples = Main:
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     3
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     4
ML "reset eta_contract"
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     5
ML "Pretty.setmargin 64"
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     6
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     7
text{*membership, intersection *}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     8
text{*difference and empty set*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     9
text{*complement, union and universal set*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    10
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    11
lemma "(x \<in> A \<inter> B) = (x \<in> A \<and> x \<in> B)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    12
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    13
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    14
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    15
@{thm[display] IntI[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    16
\rulename{IntI}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    17
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    18
@{thm[display] IntD1[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    19
\rulename{IntD1}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    20
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    21
@{thm[display] IntD2[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    22
\rulename{IntD2}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    23
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    24
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    25
lemma "(x \<in> -A) = (x \<notin> A)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    26
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    27
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    28
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    29
@{thm[display] Compl_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    30
\rulename{Compl_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    31
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    32
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    33
lemma "- (A \<union> B) = -A \<inter> -B"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    34
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    35
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    36
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    37
@{thm[display] Compl_Un[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    38
\rulename{Compl_Un}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    39
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    40
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    41
lemma "A-A = {}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    42
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    43
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    44
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    45
@{thm[display] Diff_disjoint[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    46
\rulename{Diff_disjoint}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    47
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    48
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    49
  
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    50
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    51
lemma "A \<union> -A = UNIV"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    52
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    53
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    54
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    55
@{thm[display] Compl_partition[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    56
\rulename{Compl_partition}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    57
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    58
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    59
text{*subset relation*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    60
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    61
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    62
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    63
@{thm[display] subsetI[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    64
\rulename{subsetI}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    65
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    66
@{thm[display] subsetD[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    67
\rulename{subsetD}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    68
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    69
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    70
lemma "((A \<union> B) \<subseteq> C) = (A \<subseteq> C \<and> B \<subseteq> C)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    71
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    72
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    73
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    74
@{thm[display] Un_subset_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    75
\rulename{Un_subset_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    76
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    77
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    78
lemma "(A \<subseteq> -B) = (B \<subseteq> -A)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    79
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    80
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    81
lemma "(A <= -B) = (B <= -A)"
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    82
  oops
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    83
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    84
text{*ASCII version: blast fails because of overloading because
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    85
 it doesn't have to be sets*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    86
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    87
lemma "((A:: 'a set) <= -B) = (B <= -A)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
    88
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    89
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    90
text{*A type constraint lets it work*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    91
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    92
text{*An issue here: how do we discuss the distinction between ASCII and
12815
wenzelm
parents: 10864
diff changeset
    93
symbol notation?  Here the latter disambiguates.*}
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    94
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    95
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    96
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    97
set extensionality
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    98
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    99
@{thm[display] set_ext[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   100
\rulename{set_ext}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   101
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   102
@{thm[display] equalityI[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   103
\rulename{equalityI}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   104
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   105
@{thm[display] equalityE[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   106
\rulename{equalityE}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   107
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   108
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   109
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   110
text{*finite sets: insertion and membership relation*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   111
text{*finite set notation*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   112
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   113
lemma "insert x A = {x} \<union> A"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   114
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   115
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   116
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   117
@{thm[display] insert_is_Un[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   118
\rulename{insert_is_Un}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   119
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   120
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   121
lemma "{a,b} \<union> {c,d} = {a,b,c,d}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   122
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   123
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   124
lemma "{a,b} \<inter> {b,c} = {b}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   125
apply auto
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   126
oops
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   127
text{*fails because it isn't valid*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   128
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   129
lemma "{a,b} \<inter> {b,c} = (if a=c then {a,b} else {b})"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   130
apply simp
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   131
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   132
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   133
text{*or just force or auto.  blast alone can't handle the if-then-else*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   134
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   135
text{*next: some comprehension examples*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   136
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   137
lemma "(a \<in> {z. P z}) = P a"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   138
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   139
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   140
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   141
@{thm[display] mem_Collect_eq[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   142
\rulename{mem_Collect_eq}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   143
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   144
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   145
lemma "{x. x \<in> A} = A"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   146
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   147
  
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   148
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   149
@{thm[display] Collect_mem_eq[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   150
\rulename{Collect_mem_eq}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   151
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   152
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   153
lemma "{x. P x \<or> x \<in> A} = {x. P x} \<union> A"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   154
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   155
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   156
lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   157
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   158
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   159
constdefs
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   160
  prime   :: "nat set"
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   161
    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   162
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   163
lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} = 
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   164
       {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   165
by (rule refl)
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   166
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   167
text{*binders*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   168
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   169
text{*bounded quantifiers*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   170
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   171
lemma "(\<exists>x\<in>A. P x) = (\<exists>x. x\<in>A \<and> P x)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   172
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   173
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   174
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   175
@{thm[display] bexI[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   176
\rulename{bexI}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   177
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   178
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   179
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   180
@{thm[display] bexE[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   181
\rulename{bexE}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   182
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   183
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   184
lemma "(\<forall>x\<in>A. P x) = (\<forall>x. x\<in>A \<longrightarrow> P x)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   185
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   186
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   187
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   188
@{thm[display] ballI[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   189
\rulename{ballI}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   190
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   191
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   192
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   193
@{thm[display] bspec[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   194
\rulename{bspec}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   195
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   196
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   197
text{*indexed unions and variations*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   198
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   199
lemma "(\<Union>x. B x) = (\<Union>x\<in>UNIV. B x)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   200
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   201
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   202
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   203
@{thm[display] UN_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   204
\rulename{UN_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   205
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   206
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   207
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   208
@{thm[display] Union_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   209
\rulename{Union_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   210
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   211
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   212
lemma "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   213
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   214
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   215
lemma "\<Union>S = (\<Union>x\<in>S. x)"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   216
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   217
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   218
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   219
@{thm[display] UN_I[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   220
\rulename{UN_I}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   221
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   222
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   223
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   224
@{thm[display] UN_E[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   225
\rulename{UN_E}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   226
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   227
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   228
text{*indexed intersections*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   229
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   230
lemma "(\<Inter>x. B x) = {y. \<forall>x. y \<in> B x}"
10864
f0b0a125ae4b revisions corresponding to the new version of sets.tex
paulson
parents: 10341
diff changeset
   231
by blast
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   232
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   233
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   234
@{thm[display] INT_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   235
\rulename{INT_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   236
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   237
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   238
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   239
@{thm[display] Inter_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   240
\rulename{Inter_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   241
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   242
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   243
text{*mention also card, Pow, etc.*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   244
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   245
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   246
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   247
@{thm[display] card_Un_Int[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   248
\rulename{card_Un_Int}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   249
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   250
@{thm[display] card_Pow[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   251
\rulename{card_Pow}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   252
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   253
@{thm[display] n_subsets[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   254
\rulename{n_subsets}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   255
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   256
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
   257
end