src/ZF/equalities.thy
author wenzelm
Sun Nov 20 20:15:02 2011 +0100 (2011-11-20)
changeset 45602 2a858377c3d2
parent 42793 88bee9f6eec7
child 46820 c656222c4dc1
permissions -rw-r--r--
eliminated obsolete "standard";
wenzelm@35762
     1
(*  Title:      ZF/equalities.thy
paulson@13165
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13165
     3
    Copyright   1992  University of Cambridge
paulson@13165
     4
*)
paulson@13165
     5
paulson@13356
     6
header{*Basic Equalities and Inclusions*}
paulson@13356
     7
haftmann@16417
     8
theory equalities imports pair begin
paulson@13168
     9
paulson@13356
    10
text{*These cover union, intersection, converse, domain, range, etc.  Philippe
paulson@13356
    11
de Groote proved many of the inclusions.*}
paulson@13356
    12
paulson@14095
    13
lemma in_mono: "A\<subseteq>B ==> x\<in>A --> x\<in>B"
paulson@13259
    14
by blast
paulson@13259
    15
paulson@13174
    16
lemma the_eq_0 [simp]: "(THE x. False) = 0"
paulson@13174
    17
by (blast intro: the_0)
paulson@13168
    18
paulson@13356
    19
subsection{*Bounded Quantifiers*}
paulson@13356
    20
text {* \medskip 
paulson@13178
    21
paulson@13178
    22
  The following are not added to the default simpset because
paulson@13356
    23
  (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
paulson@13178
    24
paulson@13178
    25
lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
paulson@13178
    26
  by blast
paulson@13178
    27
paulson@13178
    28
lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
paulson@13178
    29
  by blast
paulson@13178
    30
paulson@13615
    31
lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
paulson@13178
    32
  by blast
paulson@13178
    33
paulson@13615
    34
lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
paulson@13178
    35
  by blast
paulson@13178
    36
paulson@13356
    37
subsection{*Converse of a Relation*}
paulson@13168
    38
paulson@14095
    39
lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
paulson@13169
    40
by (unfold converse_def, blast)
paulson@13168
    41
paulson@14095
    42
lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
paulson@13169
    43
by (unfold converse_def, blast)
paulson@13168
    44
paulson@14095
    45
lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r"
paulson@13169
    46
by (unfold converse_def, blast)
paulson@13168
    47
paulson@13168
    48
lemma converseE [elim!]:
paulson@14095
    49
    "[| yx \<in> converse(r);   
paulson@14095
    50
        !!x y. [| yx=<y,x>;  <x,y>\<in>r |] ==> P |]
paulson@13168
    51
     ==> P"
paulson@13174
    52
by (unfold converse_def, blast) 
paulson@13168
    53
paulson@14095
    54
lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r"
paulson@13169
    55
by blast
paulson@13168
    56
paulson@14095
    57
lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A"
paulson@13169
    58
by blast
paulson@13168
    59
paulson@13168
    60
lemma converse_prod [simp]: "converse(A*B) = B*A"
paulson@13169
    61
by blast
paulson@13168
    62
paulson@13168
    63
lemma converse_empty [simp]: "converse(0) = 0"
paulson@13169
    64
by blast
paulson@13168
    65
paulson@13174
    66
lemma converse_subset_iff:
paulson@14095
    67
     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
paulson@13169
    68
by blast
paulson@13168
    69
paulson@13168
    70
paulson@13356
    71
subsection{*Finite Set Constructions Using @{term cons}*}
paulson@13168
    72
paulson@14095
    73
lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C"
paulson@13169
    74
by blast
paulson@13168
    75
paulson@14095
    76
lemma subset_consI: "B \<subseteq> cons(a,B)"
paulson@13169
    77
by blast
paulson@13168
    78
paulson@14095
    79
lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
paulson@13169
    80
by blast
paulson@13168
    81
paulson@13259
    82
(*A safe special case of subset elimination, adding no new variables 
paulson@14095
    83
  [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
wenzelm@45602
    84
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
paulson@13168
    85
paulson@14095
    86
lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
paulson@13168
    87
by blast
paulson@13168
    88
paulson@14095
    89
lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
paulson@13169
    90
by blast
paulson@13168
    91
paulson@13165
    92
(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
paulson@13165
    93
lemma cons_eq: "{a} Un B = cons(a,B)"
paulson@13165
    94
by blast
paulson@13165
    95
paulson@13165
    96
lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
paulson@13165
    97
by blast
paulson@13165
    98
paulson@13165
    99
lemma cons_absorb: "a: B ==> cons(a,B) = B"
paulson@13165
   100
by blast
paulson@13165
   101
paulson@13165
   102
lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
paulson@13165
   103
by blast
paulson@13165
   104
paulson@14071
   105
lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))" 
paulson@14071
   106
by auto
paulson@14071
   107
paulson@13615
   108
lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
paulson@13165
   109
by blast
paulson@13165
   110
paulson@13172
   111
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
paulson@13172
   112
by blast
paulson@13165
   113
paulson@13259
   114
(** singletons **)
paulson@13259
   115
paulson@14095
   116
lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C"
paulson@13259
   117
by blast
paulson@13259
   118
paulson@14095
   119
lemma singleton_subsetD: "{a} \<subseteq> C  ==>  a\<in>C"
paulson@13259
   120
by blast
paulson@13259
   121
paulson@13259
   122
paulson@13356
   123
(** succ **)
paulson@13259
   124
paulson@14095
   125
lemma subset_succI: "i \<subseteq> succ(i)"
paulson@13259
   126
by blast
paulson@13259
   127
paulson@14095
   128
(*But if j is an ordinal or is transitive, then i\<in>j implies i\<subseteq>j! 
paulson@13259
   129
  See ordinal/Ord_succ_subsetI*)
paulson@14095
   130
lemma succ_subsetI: "[| i\<in>j;  i\<subseteq>j |] ==> succ(i)\<subseteq>j"
paulson@13259
   131
by (unfold succ_def, blast)
paulson@13165
   132
paulson@13259
   133
lemma succ_subsetE:
paulson@14095
   134
    "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
paulson@13356
   135
by (unfold succ_def, blast) 
paulson@13259
   136
paulson@14095
   137
lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
paulson@13259
   138
by (unfold succ_def, blast)
paulson@13259
   139
paulson@13259
   140
paulson@13356
   141
subsection{*Binary Intersection*}
paulson@13259
   142
paulson@13259
   143
(** Intersection is the greatest lower bound of two sets **)
paulson@13259
   144
paulson@14095
   145
lemma Int_subset_iff: "C \<subseteq> A Int B <-> C \<subseteq> A & C \<subseteq> B"
paulson@13259
   146
by blast
paulson@13259
   147
paulson@14095
   148
lemma Int_lower1: "A Int B \<subseteq> A"
paulson@13259
   149
by blast
paulson@13259
   150
paulson@14095
   151
lemma Int_lower2: "A Int B \<subseteq> B"
paulson@13259
   152
by blast
paulson@13259
   153
paulson@14095
   154
lemma Int_greatest: "[| C\<subseteq>A;  C\<subseteq>B |] ==> C \<subseteq> A Int B"
paulson@13259
   155
by blast
paulson@13259
   156
paulson@14095
   157
lemma Int_cons: "cons(a,B) Int C \<subseteq> cons(a, B Int C)"
paulson@13165
   158
by blast
paulson@13165
   159
paulson@13165
   160
lemma Int_absorb [simp]: "A Int A = A"
paulson@13165
   161
by blast
paulson@13165
   162
paulson@13165
   163
lemma Int_left_absorb: "A Int (A Int B) = A Int B"
paulson@13165
   164
by blast
paulson@13165
   165
paulson@13165
   166
lemma Int_commute: "A Int B = B Int A"
paulson@13165
   167
by blast
paulson@13165
   168
paulson@13165
   169
lemma Int_left_commute: "A Int (B Int C) = B Int (A Int C)"
paulson@13165
   170
by blast
paulson@13165
   171
paulson@13165
   172
lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
paulson@13165
   173
by blast
paulson@13165
   174
paulson@13165
   175
(*Intersection is an AC-operator*)
paulson@13165
   176
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute
paulson@13165
   177
paulson@14046
   178
lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
paulson@14046
   179
  by blast
paulson@14046
   180
paulson@14046
   181
lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
paulson@14046
   182
  by blast
paulson@14046
   183
paulson@13165
   184
lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)"
paulson@13165
   185
by blast
paulson@13165
   186
paulson@13165
   187
lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)"
paulson@13165
   188
by blast
paulson@13165
   189
paulson@14095
   190
lemma subset_Int_iff: "A\<subseteq>B <-> A Int B = A"
paulson@13165
   191
by (blast elim!: equalityE)
paulson@13165
   192
paulson@14095
   193
lemma subset_Int_iff2: "A\<subseteq>B <-> B Int A = A"
paulson@13165
   194
by (blast elim!: equalityE)
paulson@13165
   195
paulson@14095
   196
lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) Int C = C-B"
paulson@13165
   197
by blast
paulson@13165
   198
paulson@14071
   199
lemma Int_cons_left:
paulson@14095
   200
     "cons(a,A) Int B = (if a \<in> B then cons(a, A Int B) else A Int B)"
paulson@14071
   201
by auto
paulson@14071
   202
paulson@14071
   203
lemma Int_cons_right:
paulson@14095
   204
     "A Int cons(a, B) = (if a \<in> A then cons(a, A Int B) else A Int B)"
paulson@14071
   205
by auto
paulson@14071
   206
paulson@14076
   207
lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)"
paulson@14076
   208
by auto
paulson@14076
   209
paulson@13356
   210
subsection{*Binary Union*}
paulson@13259
   211
paulson@13259
   212
(** Union is the least upper bound of two sets *)
paulson@13259
   213
paulson@14095
   214
lemma Un_subset_iff: "A Un B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
paulson@13259
   215
by blast
paulson@13259
   216
paulson@14095
   217
lemma Un_upper1: "A \<subseteq> A Un B"
paulson@13259
   218
by blast
paulson@13259
   219
paulson@14095
   220
lemma Un_upper2: "B \<subseteq> A Un B"
paulson@13259
   221
by blast
paulson@13259
   222
paulson@14095
   223
lemma Un_least: "[| A\<subseteq>C;  B\<subseteq>C |] ==> A Un B \<subseteq> C"
paulson@13259
   224
by blast
paulson@13165
   225
paulson@13165
   226
lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
paulson@13165
   227
by blast
paulson@13165
   228
paulson@13165
   229
lemma Un_absorb [simp]: "A Un A = A"
paulson@13165
   230
by blast
paulson@13165
   231
paulson@13165
   232
lemma Un_left_absorb: "A Un (A Un B) = A Un B"
paulson@13165
   233
by blast
paulson@13165
   234
paulson@13165
   235
lemma Un_commute: "A Un B = B Un A"
paulson@13165
   236
by blast
paulson@13165
   237
paulson@13165
   238
lemma Un_left_commute: "A Un (B Un C) = B Un (A Un C)"
paulson@13165
   239
by blast
paulson@13165
   240
paulson@13165
   241
lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
paulson@13165
   242
by blast
paulson@13165
   243
paulson@13165
   244
(*Union is an AC-operator*)
paulson@13165
   245
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
paulson@13165
   246
paulson@14046
   247
lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
paulson@14046
   248
  by blast
paulson@14046
   249
paulson@14046
   250
lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
paulson@14046
   251
  by blast
paulson@14046
   252
paulson@13165
   253
lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
paulson@13165
   254
by blast
paulson@13165
   255
paulson@14095
   256
lemma subset_Un_iff: "A\<subseteq>B <-> A Un B = B"
paulson@13165
   257
by (blast elim!: equalityE)
paulson@13165
   258
paulson@14095
   259
lemma subset_Un_iff2: "A\<subseteq>B <-> B Un A = B"
paulson@13165
   260
by (blast elim!: equalityE)
paulson@13165
   261
paulson@13165
   262
lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)"
paulson@13165
   263
by blast
paulson@13165
   264
paulson@13165
   265
lemma Un_eq_Union: "A Un B = Union({A, B})"
paulson@13165
   266
by blast
paulson@13165
   267
paulson@13356
   268
subsection{*Set Difference*}
paulson@13259
   269
paulson@14095
   270
lemma Diff_subset: "A-B \<subseteq> A"
paulson@13259
   271
by blast
paulson@13259
   272
paulson@14095
   273
lemma Diff_contains: "[| C\<subseteq>A;  C Int B = 0 |] ==> C \<subseteq> A-B"
paulson@13259
   274
by blast
paulson@13259
   275
paulson@14095
   276
lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  <->  B\<subseteq>A-C & c ~: B"
paulson@13259
   277
by blast
paulson@13165
   278
paulson@13165
   279
lemma Diff_cancel: "A - A = 0"
paulson@13165
   280
by blast
paulson@13165
   281
paulson@13165
   282
lemma Diff_triv: "A  Int B = 0 ==> A - B = A"
paulson@13165
   283
by blast
paulson@13165
   284
paulson@13165
   285
lemma empty_Diff [simp]: "0 - A = 0"
paulson@13165
   286
by blast
paulson@13165
   287
paulson@13165
   288
lemma Diff_0 [simp]: "A - 0 = A"
paulson@13165
   289
by blast
paulson@13165
   290
paulson@14095
   291
lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
paulson@13165
   292
by (blast elim: equalityE)
paulson@13165
   293
paulson@13165
   294
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
paulson@13165
   295
lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
paulson@13165
   296
by blast
paulson@13165
   297
paulson@13165
   298
(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
paulson@13165
   299
lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
paulson@13165
   300
by blast
paulson@13165
   301
paulson@13165
   302
lemma Diff_disjoint: "A Int (B-A) = 0"
paulson@13165
   303
by blast
paulson@13165
   304
paulson@14095
   305
lemma Diff_partition: "A\<subseteq>B ==> A Un (B-A) = B"
paulson@13165
   306
by blast
paulson@13165
   307
paulson@14095
   308
lemma subset_Un_Diff: "A \<subseteq> B Un (A - B)"
paulson@13165
   309
by blast
paulson@13165
   310
paulson@14095
   311
lemma double_complement: "[| A\<subseteq>B; B\<subseteq>C |] ==> B-(C-A) = A"
paulson@13165
   312
by blast
paulson@13165
   313
paulson@13165
   314
lemma double_complement_Un: "(A Un B) - (B-A) = A"
paulson@13165
   315
by blast
paulson@13165
   316
paulson@13165
   317
lemma Un_Int_crazy: 
paulson@13165
   318
 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
paulson@13165
   319
apply blast
paulson@13165
   320
done
paulson@13165
   321
paulson@13165
   322
lemma Diff_Un: "A - (B Un C) = (A-B) Int (A-C)"
paulson@13165
   323
by blast
paulson@13165
   324
paulson@13165
   325
lemma Diff_Int: "A - (B Int C) = (A-B) Un (A-C)"
paulson@13165
   326
by blast
paulson@13165
   327
paulson@13165
   328
lemma Un_Diff: "(A Un B) - C = (A - C) Un (B - C)"
paulson@13165
   329
by blast
paulson@13165
   330
paulson@13165
   331
lemma Int_Diff: "(A Int B) - C = A Int (B - C)"
paulson@13165
   332
by blast
paulson@13165
   333
paulson@13165
   334
lemma Diff_Int_distrib: "C Int (A-B) = (C Int A) - (C Int B)"
paulson@13165
   335
by blast
paulson@13165
   336
paulson@13165
   337
lemma Diff_Int_distrib2: "(A-B) Int C = (A Int C) - (B Int C)"
paulson@13165
   338
by blast
paulson@13165
   339
paulson@13165
   340
(*Halmos, Naive Set Theory, page 16.*)
paulson@14095
   341
lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C)  <->  C\<subseteq>A"
paulson@13165
   342
by (blast elim!: equalityE)
paulson@13165
   343
paulson@13165
   344
paulson@13356
   345
subsection{*Big Union and Intersection*}
paulson@13259
   346
paulson@13259
   347
(** Big Union is the least upper bound of a set  **)
paulson@13259
   348
paulson@14095
   349
lemma Union_subset_iff: "Union(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
paulson@13259
   350
by blast
paulson@13259
   351
paulson@14095
   352
lemma Union_upper: "B\<in>A ==> B \<subseteq> Union(A)"
paulson@13259
   353
by blast
paulson@13259
   354
paulson@14095
   355
lemma Union_least: "[| !!x. x\<in>A ==> x\<subseteq>C |] ==> Union(A) \<subseteq> C"
paulson@13259
   356
by blast
paulson@13165
   357
paulson@13165
   358
lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
paulson@13165
   359
by blast
paulson@13165
   360
paulson@13165
   361
lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
paulson@13165
   362
by blast
paulson@13165
   363
paulson@14095
   364
lemma Union_Int_subset: "Union(A Int B) \<subseteq> Union(A) Int Union(B)"
paulson@13165
   365
by blast
paulson@13165
   366
paulson@13615
   367
lemma Union_disjoint: "Union(C) Int A = 0 <-> (\<forall>B\<in>C. B Int A = 0)"
paulson@13165
   368
by (blast elim!: equalityE)
paulson@13165
   369
paulson@13615
   370
lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
paulson@13165
   371
by blast
paulson@13165
   372
paulson@14095
   373
lemma Int_Union2: "Union(B) Int A = (\<Union>C\<in>B. C Int A)"
paulson@14084
   374
by blast
paulson@14084
   375
paulson@13259
   376
(** Big Intersection is the greatest lower bound of a nonempty set **)
paulson@13259
   377
paulson@14095
   378
lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> Inter(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
paulson@13259
   379
by blast
paulson@13259
   380
paulson@14095
   381
lemma Inter_lower: "B\<in>A ==> Inter(A) \<subseteq> B"
paulson@13259
   382
by blast
paulson@13259
   383
paulson@14095
   384
lemma Inter_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>x |] ==> C \<subseteq> Inter(A)"
paulson@13259
   385
by blast
paulson@13259
   386
paulson@13259
   387
(** Intersection of a family of sets  **)
paulson@13259
   388
paulson@14095
   389
lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)"
paulson@13259
   390
by blast
paulson@13259
   391
paulson@14095
   392
lemma INT_greatest: "[| A\<noteq>0;  !!x. x\<in>A ==> C\<subseteq>B(x) |] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))"
paulson@14095
   393
by force
paulson@13259
   394
paulson@14095
   395
lemma Inter_0 [simp]: "Inter(0) = 0"
paulson@13165
   396
by (unfold Inter_def, blast)
paulson@13165
   397
paulson@13259
   398
lemma Inter_Un_subset:
paulson@14095
   399
     "[| z\<in>A; z\<in>B |] ==> Inter(A) Un Inter(B) \<subseteq> Inter(A Int B)"
paulson@13165
   400
by blast
paulson@13165
   401
paulson@13165
   402
(* A good challenge: Inter is ill-behaved on the empty set *)
paulson@13165
   403
lemma Inter_Un_distrib:
paulson@14095
   404
     "[| A\<noteq>0;  B\<noteq>0 |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"
paulson@13165
   405
by blast
paulson@13165
   406
paulson@13165
   407
lemma Union_singleton: "Union({b}) = b"
paulson@13165
   408
by blast
paulson@13165
   409
paulson@13165
   410
lemma Inter_singleton: "Inter({b}) = b"
paulson@13165
   411
by blast
paulson@13165
   412
paulson@13165
   413
lemma Inter_cons [simp]:
paulson@13165
   414
     "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
paulson@13165
   415
by force
paulson@13165
   416
paulson@13356
   417
subsection{*Unions and Intersections of Families*}
paulson@13259
   418
paulson@14095
   419
lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A Int B(i))"
paulson@13259
   420
by (blast elim!: equalityE)
paulson@13259
   421
paulson@14095
   422
lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
paulson@13259
   423
by blast
paulson@13259
   424
paulson@14095
   425
lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
paulson@13259
   426
by (erule RepFunI [THEN Union_upper])
paulson@13259
   427
paulson@14095
   428
lemma UN_least: "[| !!x. x\<in>A ==> B(x)\<subseteq>C |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C"
paulson@13259
   429
by blast
paulson@13165
   430
paulson@13615
   431
lemma Union_eq_UN: "Union(A) = (\<Union>x\<in>A. x)"
paulson@13165
   432
by blast
paulson@13165
   433
paulson@13615
   434
lemma Inter_eq_INT: "Inter(A) = (\<Inter>x\<in>A. x)"
paulson@13165
   435
by (unfold Inter_def, blast)
paulson@13165
   436
paulson@13615
   437
lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0"
paulson@13165
   438
by blast
paulson@13165
   439
paulson@13615
   440
lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A"
paulson@13165
   441
by blast
paulson@13165
   442
paulson@13615
   443
lemma UN_Un: "(\<Union>i\<in> A Un B. C(i)) = (\<Union>i\<in> A. C(i)) Un (\<Union>i\<in>B. C(i))"
paulson@13165
   444
by blast
paulson@13165
   445
paulson@14095
   446
lemma INT_Un: "(\<Inter>i\<in>I Un J. A(i)) = 
paulson@14095
   447
               (if I=0 then \<Inter>j\<in>J. A(j)  
paulson@14095
   448
                       else if J=0 then \<Inter>i\<in>I. A(i)  
paulson@14095
   449
                       else ((\<Inter>i\<in>I. A(i)) Int  (\<Inter>j\<in>J. A(j))))"
paulson@14095
   450
by (simp, blast intro!: equalityI)
paulson@13165
   451
paulson@13615
   452
lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))"
paulson@13165
   453
by blast
paulson@13165
   454
paulson@13165
   455
(*Halmos, Naive Set Theory, page 35.*)
paulson@13615
   456
lemma Int_UN_distrib: "B Int (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B Int A(i))"
paulson@13165
   457
by blast
paulson@13165
   458
paulson@14095
   459
lemma Un_INT_distrib: "I\<noteq>0 ==> B Un (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B Un A(i))"
paulson@14095
   460
by auto
paulson@13165
   461
paulson@13165
   462
lemma Int_UN_distrib2:
paulson@13615
   463
     "(\<Union>i\<in>I. A(i)) Int (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) Int B(j))"
paulson@13165
   464
by blast
paulson@13165
   465
paulson@14095
   466
lemma Un_INT_distrib2: "[| I\<noteq>0;  J\<noteq>0 |] ==>  
paulson@13615
   467
      (\<Inter>i\<in>I. A(i)) Un (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) Un B(j))"
paulson@14095
   468
by auto
paulson@13165
   469
paulson@14095
   470
lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)"
paulson@14095
   471
by force
paulson@13165
   472
paulson@14095
   473
lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)"
paulson@14095
   474
by force
paulson@13165
   475
paulson@13615
   476
lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
paulson@13165
   477
by blast
paulson@13165
   478
paulson@13615
   479
lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x))    = (\<Inter>a\<in>A. B(f(a)))"
paulson@13165
   480
by (auto simp add: Inter_def)
paulson@13165
   481
paulson@13165
   482
lemma INT_Union_eq:
paulson@13615
   483
     "0 ~: A ==> (\<Inter>x\<in> Union(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))"
paulson@13615
   484
apply (subgoal_tac "\<forall>x\<in>A. x~=0")
paulson@13615
   485
 prefer 2 apply blast
paulson@13615
   486
apply (force simp add: Inter_def ball_conj_distrib) 
paulson@13165
   487
done
paulson@13165
   488
paulson@13615
   489
lemma INT_UN_eq:
paulson@13615
   490
     "(\<forall>x\<in>A. B(x) ~= 0)  
paulson@13615
   491
      ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
paulson@13165
   492
apply (subst INT_Union_eq, blast)
paulson@13165
   493
apply (simp add: Inter_def)
paulson@13165
   494
done
paulson@13165
   495
paulson@13165
   496
paulson@13165
   497
(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
paulson@13165
   498
    Union of a family of unions **)
paulson@13165
   499
paulson@13165
   500
lemma UN_Un_distrib:
paulson@13615
   501
     "(\<Union>i\<in>I. A(i) Un B(i)) = (\<Union>i\<in>I. A(i))  Un  (\<Union>i\<in>I. B(i))"
paulson@13165
   502
by blast
paulson@13165
   503
paulson@13165
   504
lemma INT_Int_distrib:
paulson@14095
   505
     "I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) Int B(i)) = (\<Inter>i\<in>I. A(i)) Int (\<Inter>i\<in>I. B(i))"
paulson@14095
   506
by (blast elim!: not_emptyE)
paulson@13165
   507
paulson@13165
   508
lemma UN_Int_subset:
paulson@14095
   509
     "(\<Union>z\<in>I Int J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) Int (\<Union>z\<in>J. A(z))"
paulson@13165
   510
by blast
paulson@13165
   511
paulson@13165
   512
(** Devlin, page 12, exercise 5: Complements **)
paulson@13165
   513
paulson@14095
   514
lemma Diff_UN: "I\<noteq>0 ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
paulson@14095
   515
by (blast elim!: not_emptyE)
paulson@13165
   516
paulson@14095
   517
lemma Diff_INT: "I\<noteq>0 ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
paulson@14095
   518
by (blast elim!: not_emptyE)
paulson@14095
   519
paulson@13165
   520
paulson@13165
   521
(** Unions and Intersections with General Sum **)
paulson@13165
   522
paulson@13165
   523
(*Not suitable for rewriting: LOOPS!*)
paulson@13165
   524
lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"
paulson@13165
   525
by blast
paulson@13165
   526
paulson@13165
   527
(*Not suitable for rewriting: LOOPS!*)
paulson@13165
   528
lemma Sigma_cons2: "A * cons(b,B) = A*{b} Un A*B"
paulson@13165
   529
by blast
paulson@13165
   530
paulson@13165
   531
lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)"
paulson@13165
   532
by blast
paulson@13165
   533
paulson@13165
   534
lemma Sigma_succ2: "A * succ(B) = A*{B} Un A*B"
paulson@13165
   535
by blast
paulson@13165
   536
paulson@13165
   537
lemma SUM_UN_distrib1:
skalberg@14171
   538
     "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
paulson@13165
   539
by blast
paulson@13165
   540
paulson@13165
   541
lemma SUM_UN_distrib2:
skalberg@14171
   542
     "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
paulson@13165
   543
by blast
paulson@13165
   544
paulson@13165
   545
lemma SUM_Un_distrib1:
skalberg@14171
   546
     "(\<Sigma> i\<in>I Un J. C(i)) = (\<Sigma> i\<in>I. C(i)) Un (\<Sigma> j\<in>J. C(j))"
paulson@13165
   547
by blast
paulson@13165
   548
paulson@13165
   549
lemma SUM_Un_distrib2:
skalberg@14171
   550
     "(\<Sigma> i\<in>I. A(i) Un B(i)) = (\<Sigma> i\<in>I. A(i)) Un (\<Sigma> i\<in>I. B(i))"
paulson@13165
   551
by blast
paulson@13165
   552
paulson@13165
   553
(*First-order version of the above, for rewriting*)
paulson@13165
   554
lemma prod_Un_distrib2: "I * (A Un B) = I*A Un I*B"
paulson@13165
   555
by (rule SUM_Un_distrib2)
paulson@13165
   556
paulson@13165
   557
lemma SUM_Int_distrib1:
skalberg@14171
   558
     "(\<Sigma> i\<in>I Int J. C(i)) = (\<Sigma> i\<in>I. C(i)) Int (\<Sigma> j\<in>J. C(j))"
paulson@13165
   559
by blast
paulson@13165
   560
paulson@13165
   561
lemma SUM_Int_distrib2:
skalberg@14171
   562
     "(\<Sigma> i\<in>I. A(i) Int B(i)) = (\<Sigma> i\<in>I. A(i)) Int (\<Sigma> i\<in>I. B(i))"
paulson@13165
   563
by blast
paulson@13165
   564
paulson@13165
   565
(*First-order version of the above, for rewriting*)
paulson@13165
   566
lemma prod_Int_distrib2: "I * (A Int B) = I*A Int I*B"
paulson@13165
   567
by (rule SUM_Int_distrib2)
paulson@13165
   568
paulson@13165
   569
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
skalberg@14171
   570
lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
paulson@13165
   571
by blast
paulson@13165
   572
paulson@13544
   573
lemma times_subset_iff:
paulson@14095
   574
     "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
paulson@13544
   575
by blast
paulson@13544
   576
paulson@13544
   577
lemma Int_Sigma_eq:
skalberg@14171
   578
     "(\<Sigma> x \<in> A'. B'(x)) Int (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' Int A. B'(x) Int B(x))"
paulson@13544
   579
by blast
paulson@13544
   580
paulson@13165
   581
(** Domain **)
paulson@13165
   582
paulson@14095
   583
lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>\<in> r)"
paulson@13259
   584
by (unfold domain_def, blast)
paulson@13259
   585
paulson@14095
   586
lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
paulson@13259
   587
by (unfold domain_def, blast)
paulson@13259
   588
paulson@13259
   589
lemma domainE [elim!]:
paulson@14095
   590
    "[| a \<in> domain(r);  !!y. <a,y>\<in> r ==> P |] ==> P"
paulson@13259
   591
by (unfold domain_def, blast)
paulson@13259
   592
paulson@14095
   593
lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A"
paulson@13259
   594
by blast
paulson@13259
   595
paulson@14095
   596
lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A"
paulson@13165
   597
by blast
paulson@13165
   598
paulson@13165
   599
lemma domain_0 [simp]: "domain(0) = 0"
paulson@13165
   600
by blast
paulson@13165
   601
paulson@13165
   602
lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"
paulson@13165
   603
by blast
paulson@13165
   604
paulson@13165
   605
lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)"
paulson@13165
   606
by blast
paulson@13165
   607
paulson@14095
   608
lemma domain_Int_subset: "domain(A Int B) \<subseteq> domain(A) Int domain(B)"
paulson@13165
   609
by blast
paulson@13165
   610
paulson@14095
   611
lemma domain_Diff_subset: "domain(A) - domain(B) \<subseteq> domain(A - B)"
paulson@13165
   612
by blast
paulson@13165
   613
paulson@13615
   614
lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
paulson@13165
   615
by blast
paulson@13165
   616
paulson@13615
   617
lemma domain_Union: "domain(Union(A)) = (\<Union>x\<in>A. domain(x))"
paulson@13165
   618
by blast
paulson@13165
   619
paulson@13165
   620
paulson@13165
   621
(** Range **)
paulson@13165
   622
paulson@14095
   623
lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)"
paulson@13259
   624
apply (unfold range_def)
paulson@13259
   625
apply (erule converseI [THEN domainI])
paulson@13259
   626
done
paulson@13259
   627
paulson@14095
   628
lemma rangeE [elim!]: "[| b \<in> range(r);  !!x. <x,b>\<in> r ==> P |] ==> P"
paulson@13259
   629
by (unfold range_def, blast)
paulson@13259
   630
paulson@14095
   631
lemma range_subset: "range(A*B) \<subseteq> B"
paulson@13259
   632
apply (unfold range_def)
paulson@13259
   633
apply (subst converse_prod)
paulson@13259
   634
apply (rule domain_subset)
paulson@13259
   635
done
paulson@13259
   636
paulson@14095
   637
lemma range_of_prod: "a\<in>A ==> range(A*B) = B"
paulson@13165
   638
by blast
paulson@13165
   639
paulson@13165
   640
lemma range_0 [simp]: "range(0) = 0"
paulson@13165
   641
by blast
paulson@13165
   642
paulson@13165
   643
lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"
paulson@13165
   644
by blast
paulson@13165
   645
paulson@13165
   646
lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)"
paulson@13165
   647
by blast
paulson@13165
   648
paulson@14095
   649
lemma range_Int_subset: "range(A Int B) \<subseteq> range(A) Int range(B)"
paulson@13165
   650
by blast
paulson@13165
   651
paulson@14095
   652
lemma range_Diff_subset: "range(A) - range(B) \<subseteq> range(A - B)"
paulson@13165
   653
by blast
paulson@13165
   654
paulson@13259
   655
lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
paulson@13259
   656
by blast
paulson@13259
   657
paulson@13165
   658
lemma range_converse [simp]: "range(converse(r)) = domain(r)"
paulson@13165
   659
by blast
paulson@13165
   660
paulson@13165
   661
paulson@13165
   662
(** Field **)
paulson@13165
   663
paulson@14095
   664
lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)"
paulson@13259
   665
by (unfold field_def, blast)
paulson@13259
   666
paulson@14095
   667
lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)"
paulson@13259
   668
by (unfold field_def, blast)
paulson@13259
   669
paulson@13259
   670
lemma fieldCI [intro]: 
paulson@14095
   671
    "(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> field(r)"
paulson@13259
   672
apply (unfold field_def, blast)
paulson@13259
   673
done
paulson@13259
   674
paulson@13259
   675
lemma fieldE [elim!]: 
paulson@14095
   676
     "[| a \<in> field(r);   
paulson@14095
   677
         !!x. <a,x>\<in> r ==> P;   
paulson@14095
   678
         !!x. <x,a>\<in> r ==> P        |] ==> P"
paulson@13259
   679
by (unfold field_def, blast)
paulson@13259
   680
paulson@14095
   681
lemma field_subset: "field(A*B) \<subseteq> A Un B"
paulson@13259
   682
by blast
paulson@13259
   683
paulson@14095
   684
lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
paulson@13259
   685
apply (unfold field_def)
paulson@13259
   686
apply (rule Un_upper1)
paulson@13259
   687
done
paulson@13259
   688
paulson@14095
   689
lemma range_subset_field: "range(r) \<subseteq> field(r)"
paulson@13259
   690
apply (unfold field_def)
paulson@13259
   691
apply (rule Un_upper2)
paulson@13259
   692
done
paulson@13259
   693
paulson@14095
   694
lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)"
paulson@13259
   695
by blast
paulson@13259
   696
paulson@14095
   697
lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)"
paulson@13259
   698
by blast
paulson@13259
   699
paulson@14095
   700
lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)"
paulson@13259
   701
by (simp add: relation_def, blast) 
paulson@13259
   702
paulson@13165
   703
lemma field_of_prod: "field(A*A) = A"
paulson@13165
   704
by blast
paulson@13165
   705
paulson@13165
   706
lemma field_0 [simp]: "field(0) = 0"
paulson@13165
   707
by blast
paulson@13165
   708
paulson@13165
   709
lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
paulson@13165
   710
by blast
paulson@13165
   711
paulson@13165
   712
lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)"
paulson@13165
   713
by blast
paulson@13165
   714
paulson@14095
   715
lemma field_Int_subset: "field(A Int B) \<subseteq> field(A) Int field(B)"
paulson@13165
   716
by blast
paulson@13165
   717
paulson@14095
   718
lemma field_Diff_subset: "field(A) - field(B) \<subseteq> field(A - B)"
paulson@13165
   719
by blast
paulson@13165
   720
paulson@13165
   721
lemma field_converse [simp]: "field(converse(r)) = field(r)"
paulson@13165
   722
by blast
paulson@13165
   723
paulson@13259
   724
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
paulson@14095
   725
lemma rel_Union: "(\<forall>x\<in>S. EX A B. x \<subseteq> A*B) ==>   
paulson@14095
   726
                  Union(S) \<subseteq> domain(Union(S)) * range(Union(S))"
paulson@13259
   727
by blast
paulson@13165
   728
paulson@13259
   729
(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
paulson@14095
   730
lemma rel_Un: "[| r \<subseteq> A*B;  s \<subseteq> C*D |] ==> (r Un s) \<subseteq> (A Un C) * (B Un D)"
paulson@13259
   731
by blast
paulson@13259
   732
paulson@14095
   733
lemma domain_Diff_eq: "[| <a,c> \<in> r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
paulson@13259
   734
by blast
paulson@13259
   735
paulson@14095
   736
lemma range_Diff_eq: "[| <c,b> \<in> r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
paulson@13259
   737
by blast
paulson@13259
   738
paulson@13259
   739
paulson@13356
   740
subsection{*Image of a Set under a Function or Relation*}
paulson@13259
   741
paulson@14095
   742
lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
paulson@13259
   743
by (unfold image_def, blast)
paulson@13259
   744
paulson@14095
   745
lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
paulson@13259
   746
by (rule image_iff [THEN iff_trans], blast)
paulson@13259
   747
paulson@14095
   748
lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
paulson@13259
   749
by (unfold image_def, blast)
paulson@13259
   750
paulson@13259
   751
lemma imageE [elim!]: 
paulson@14095
   752
    "[| b: r``A;  !!x.[| <x,b>\<in> r;  x\<in>A |] ==> P |] ==> P"
paulson@13259
   753
by (unfold image_def, blast)
paulson@13259
   754
paulson@14095
   755
lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B"
paulson@13259
   756
by blast
paulson@13165
   757
paulson@13165
   758
lemma image_0 [simp]: "r``0 = 0"
paulson@13165
   759
by blast
paulson@13165
   760
paulson@13165
   761
lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)"
paulson@13165
   762
by blast
paulson@13165
   763
paulson@14883
   764
lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))"
paulson@14883
   765
by blast
paulson@14883
   766
paulson@14883
   767
lemma Collect_image_eq:
paulson@14883
   768
     "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})"
paulson@14883
   769
by blast
paulson@14883
   770
paulson@14095
   771
lemma image_Int_subset: "r``(A Int B) \<subseteq> (r``A) Int (r``B)"
paulson@13165
   772
by blast
paulson@13165
   773
paulson@14095
   774
lemma image_Int_square_subset: "(r Int A*A)``B \<subseteq> (r``B) Int A"
paulson@13165
   775
by blast
paulson@13165
   776
paulson@14095
   777
lemma image_Int_square: "B\<subseteq>A ==> (r Int A*A)``B = (r``B) Int A"
paulson@13165
   778
by blast
paulson@13165
   779
paulson@13165
   780
paulson@13165
   781
(*Image laws for special relations*)
paulson@13165
   782
lemma image_0_left [simp]: "0``A = 0"
paulson@13165
   783
by blast
paulson@13165
   784
paulson@13165
   785
lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)"
paulson@13165
   786
by blast
paulson@13165
   787
paulson@14095
   788
lemma image_Int_subset_left: "(r Int s)``A \<subseteq> (r``A) Int (s``A)"
paulson@13165
   789
by blast
paulson@13165
   790
paulson@13165
   791
paulson@13356
   792
subsection{*Inverse Image of a Set under a Function or Relation*}
paulson@13259
   793
paulson@13259
   794
lemma vimage_iff: 
paulson@14095
   795
    "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
paulson@13259
   796
by (unfold vimage_def image_def converse_def, blast)
paulson@13259
   797
paulson@14095
   798
lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
paulson@13259
   799
by (rule vimage_iff [THEN iff_trans], blast)
paulson@13259
   800
paulson@14095
   801
lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
paulson@13259
   802
by (unfold vimage_def, blast)
paulson@13259
   803
paulson@13259
   804
lemma vimageE [elim!]: 
paulson@14095
   805
    "[| a: r-``B;  !!x.[| <a,x>\<in> r;  x\<in>B |] ==> P |] ==> P"
paulson@13259
   806
apply (unfold vimage_def, blast)
paulson@13259
   807
done
paulson@13259
   808
paulson@14095
   809
lemma vimage_subset: "r \<subseteq> A*B ==> r-``C \<subseteq> A"
paulson@13259
   810
apply (unfold vimage_def)
paulson@13259
   811
apply (erule converse_type [THEN image_subset])
paulson@13259
   812
done
paulson@13165
   813
paulson@13165
   814
lemma vimage_0 [simp]: "r-``0 = 0"
paulson@13165
   815
by blast
paulson@13165
   816
paulson@13165
   817
lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)"
paulson@13165
   818
by blast
paulson@13165
   819
paulson@14095
   820
lemma vimage_Int_subset: "r-``(A Int B) \<subseteq> (r-``A) Int (r-``B)"
paulson@13165
   821
by blast
paulson@13165
   822
paulson@13165
   823
(*NOT suitable for rewriting*)
paulson@13615
   824
lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})"
paulson@13165
   825
by blast
paulson@13165
   826
paulson@13165
   827
lemma function_vimage_Int:
paulson@13165
   828
     "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)"
paulson@13165
   829
by (unfold function_def, blast)
paulson@13165
   830
paulson@13165
   831
lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"
paulson@13165
   832
by (unfold function_def, blast)
paulson@13165
   833
paulson@14095
   834
lemma function_image_vimage: "function(f) ==> f `` (f-`` A) \<subseteq> A"
paulson@13165
   835
by (unfold function_def, blast)
paulson@13165
   836
paulson@14095
   837
lemma vimage_Int_square_subset: "(r Int A*A)-``B \<subseteq> (r-``B) Int A"
paulson@13165
   838
by blast
paulson@13165
   839
paulson@14095
   840
lemma vimage_Int_square: "B\<subseteq>A ==> (r Int A*A)-``B = (r-``B) Int A"
paulson@13165
   841
by blast
paulson@13165
   842
paulson@13165
   843
paulson@13165
   844
paulson@13165
   845
(*Invese image laws for special relations*)
paulson@13165
   846
lemma vimage_0_left [simp]: "0-``A = 0"
paulson@13165
   847
by blast
paulson@13165
   848
paulson@13165
   849
lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)"
paulson@13165
   850
by blast
paulson@13165
   851
paulson@14095
   852
lemma vimage_Int_subset_left: "(r Int s)-``A \<subseteq> (r-``A) Int (s-``A)"
paulson@13165
   853
by blast
paulson@13165
   854
paulson@13165
   855
paulson@13165
   856
(** Converse **)
paulson@13165
   857
paulson@13165
   858
lemma converse_Un [simp]: "converse(A Un B) = converse(A) Un converse(B)"
paulson@13165
   859
by blast
paulson@13165
   860
paulson@13165
   861
lemma converse_Int [simp]: "converse(A Int B) = converse(A) Int converse(B)"
paulson@13165
   862
by blast
paulson@13165
   863
paulson@13165
   864
lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
paulson@13165
   865
by blast
paulson@13165
   866
paulson@13615
   867
lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))"
paulson@13165
   868
by blast
paulson@13165
   869
paulson@13165
   870
(*Unfolding Inter avoids using excluded middle on A=0*)
paulson@13165
   871
lemma converse_INT [simp]:
paulson@13615
   872
     "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))"
paulson@13165
   873
apply (unfold Inter_def, blast)
paulson@13165
   874
done
paulson@13165
   875
paulson@13356
   876
paulson@13356
   877
subsection{*Powerset Operator*}
paulson@13165
   878
paulson@13165
   879
lemma Pow_0 [simp]: "Pow(0) = {0}"
paulson@13165
   880
by blast
paulson@13165
   881
paulson@13165
   882
lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}"
paulson@13165
   883
apply (rule equalityI, safe)
paulson@13165
   884
apply (erule swap)
paulson@13165
   885
apply (rule_tac a = "x-{a}" in RepFun_eqI, auto) 
paulson@13165
   886
done
paulson@13165
   887
paulson@14095
   888
lemma Un_Pow_subset: "Pow(A) Un Pow(B) \<subseteq> Pow(A Un B)"
paulson@13165
   889
by blast
paulson@13165
   890
paulson@14095
   891
lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))"
paulson@13165
   892
by blast
paulson@13165
   893
paulson@14095
   894
lemma subset_Pow_Union: "A \<subseteq> Pow(Union(A))"
paulson@13165
   895
by blast
paulson@13165
   896
paulson@13165
   897
lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
paulson@13165
   898
by blast
paulson@13165
   899
paulson@14077
   900
lemma Union_Pow_iff: "Union(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
paulson@14077
   901
by blast
paulson@14077
   902
paulson@13165
   903
lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
paulson@13165
   904
by blast
paulson@13165
   905
paulson@14095
   906
lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
paulson@14095
   907
by (blast elim!: not_emptyE)
paulson@13165
   908
paulson@13356
   909
paulson@13356
   910
subsection{*RepFun*}
paulson@13259
   911
paulson@14095
   912
lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
paulson@13259
   913
by blast
paulson@13165
   914
paulson@14095
   915
lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
paulson@13165
   916
by blast
paulson@13165
   917
paulson@14095
   918
lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
paulson@14095
   919
by force
paulson@14095
   920
paulson@13165
   921
paulson@13356
   922
subsection{*Collect*}
paulson@13259
   923
paulson@14095
   924
lemma Collect_subset: "Collect(A,P) \<subseteq> A"
paulson@13259
   925
by blast
paulson@2469
   926
paulson@13165
   927
lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
paulson@13165
   928
by blast
paulson@13165
   929
paulson@13165
   930
lemma Collect_Int: "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)"
paulson@13165
   931
by blast
paulson@13165
   932
paulson@13165
   933
lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
paulson@13165
   934
by blast
paulson@13165
   935
paulson@14095
   936
lemma Collect_cons: "{x\<in>cons(a,B). P(x)} =  
paulson@14095
   937
      (if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})"
paulson@13165
   938
by (simp, blast)
paulson@13165
   939
paulson@13165
   940
lemma Int_Collect_self_eq: "A Int Collect(A,P) = Collect(A,P)"
paulson@13165
   941
by blast
paulson@13165
   942
paulson@13165
   943
lemma Collect_Collect_eq [simp]:
paulson@13165
   944
     "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
paulson@13165
   945
by blast
paulson@13165
   946
paulson@13165
   947
lemma Collect_Int_Collect_eq:
paulson@13165
   948
     "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
paulson@13165
   949
by blast
paulson@13165
   950
paulson@13203
   951
lemma Collect_Union_eq [simp]:
paulson@13203
   952
     "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
paulson@13203
   953
by blast
paulson@13203
   954
paulson@14095
   955
lemma Collect_Int_left: "{x\<in>A. P(x)} Int B = {x \<in> A Int B. P(x)}"
paulson@14084
   956
by blast
paulson@14084
   957
paulson@14095
   958
lemma Collect_Int_right: "A Int {x\<in>B. P(x)} = {x \<in> A Int B. P(x)}"
paulson@14084
   959
by blast
paulson@14084
   960
paulson@14095
   961
lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
paulson@14084
   962
by blast
paulson@14084
   963
paulson@14095
   964
lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
paulson@14084
   965
by blast
paulson@14084
   966
paulson@13259
   967
lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
paulson@13259
   968
                    Union_least UN_least Un_least 
paulson@13259
   969
                    Inter_greatest Int_greatest RepFun_subset
paulson@13259
   970
                    Un_upper1 Un_upper2 Int_lower1 Int_lower2
paulson@13259
   971
wenzelm@24893
   972
ML {*
wenzelm@42793
   973
val subset_cs =
wenzelm@42793
   974
  claset_of (@{context}
wenzelm@24893
   975
    delrules [@{thm subsetI}, @{thm subsetCE}]
wenzelm@24893
   976
    addSIs @{thms subset_SIs}
wenzelm@24893
   977
    addIs  [@{thm Union_upper}, @{thm Inter_lower}]
wenzelm@42793
   978
    addSEs [@{thm cons_subsetE}]);
paulson@13259
   979
wenzelm@42793
   980
val ZF_cs = claset_of (@{context} delrules [@{thm equalityI}]);
paulson@13165
   981
*}
paulson@14046
   982
 
paulson@13165
   983
end
paulson@13165
   984