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