src/HOL/Relation.ML
author paulson
Wed Jul 25 13:13:01 2001 +0200 (2001-07-25)
changeset 11451 8abfb4f7bd02
parent 11136 e34e7f6d9b57
child 11655 923e4d0d36d5
permissions -rw-r--r--
partial restructuring to reduce dependence on Axiom of Choice
clasohm@1465
     1
(*  Title:      Relation.ML
nipkow@1128
     2
    ID:         $Id$
paulson@1985
     3
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1985
     4
    Copyright   1996  University of Cambridge
nipkow@1128
     5
*)
nipkow@1128
     6
nipkow@1128
     7
(** Identity relation **)
nipkow@1128
     8
nipkow@5608
     9
Goalw [Id_def] "(a,a) : Id";  
paulson@2891
    10
by (Blast_tac 1);
nipkow@5608
    11
qed "IdI";
nipkow@1128
    12
nipkow@5608
    13
val major::prems = Goalw [Id_def]
nipkow@5608
    14
    "[| p: Id;  !!x.[| p = (x,x) |] ==> P  \
nipkow@1128
    15
\    |] ==>  P";  
nipkow@1128
    16
by (rtac (major RS CollectE) 1);
nipkow@1128
    17
by (etac exE 1);
nipkow@1128
    18
by (eresolve_tac prems 1);
nipkow@5608
    19
qed "IdE";
nipkow@1128
    20
nipkow@5608
    21
Goalw [Id_def] "(a,b):Id = (a=b)";
paulson@2891
    22
by (Blast_tac 1);
nipkow@5608
    23
qed "pair_in_Id_conv";
nipkow@8265
    24
AddIffs [pair_in_Id_conv];
nipkow@1128
    25
paulson@6806
    26
Goalw [refl_def] "reflexive Id";
paulson@6806
    27
by Auto_tac;
paulson@6806
    28
qed "reflexive_Id";
paulson@6806
    29
paulson@6806
    30
(*A strange result, since Id is also symmetric.*)
paulson@6806
    31
Goalw [antisym_def] "antisym Id";
paulson@6806
    32
by Auto_tac;
paulson@6806
    33
qed "antisym_Id";
paulson@6806
    34
paulson@6806
    35
Goalw [trans_def] "trans Id";
paulson@6806
    36
by Auto_tac;
paulson@6806
    37
qed "trans_Id";
paulson@6806
    38
nipkow@1128
    39
paulson@5978
    40
(** Diagonal relation: indentity restricted to some set **)
paulson@5978
    41
paulson@5978
    42
(*** Equality : the diagonal relation ***)
paulson@5978
    43
paulson@5978
    44
Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
paulson@5978
    45
by (Blast_tac 1);
paulson@5978
    46
qed "diag_eqI";
paulson@5978
    47
wenzelm@9108
    48
bind_thm ("diagI", refl RS diag_eqI |> standard);
paulson@5978
    49
paulson@5978
    50
(*The general elimination rule*)
paulson@5978
    51
val major::prems = Goalw [diag_def]
paulson@5978
    52
    "[| c : diag(A);  \
paulson@5978
    53
\       !!x y. [| x:A;  c = (x,x) |] ==> P \
paulson@5978
    54
\    |] ==> P";
paulson@5978
    55
by (rtac (major RS UN_E) 1);
paulson@5978
    56
by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
paulson@5978
    57
qed "diagE";
paulson@5978
    58
paulson@5978
    59
AddSIs [diagI];
paulson@5978
    60
AddSEs [diagE];
paulson@5978
    61
paulson@5978
    62
Goal "((x,y) : diag A) = (x=y & x : A)";
paulson@5978
    63
by (Blast_tac 1);
paulson@5978
    64
qed "diag_iff";
paulson@5978
    65
nipkow@8703
    66
Goal "diag(A) <= A <*> A";
paulson@5978
    67
by (Blast_tac 1);
paulson@5995
    68
qed "diag_subset_Times";
paulson@5978
    69
paulson@5978
    70
paulson@5978
    71
nipkow@1128
    72
(** Composition of two relations **)
nipkow@1128
    73
wenzelm@5069
    74
Goalw [comp_def]
paulson@5148
    75
    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
paulson@2891
    76
by (Blast_tac 1);
nipkow@1128
    77
qed "compI";
nipkow@1128
    78
nipkow@1128
    79
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
paulson@5316
    80
val prems = Goalw [comp_def]
nipkow@1128
    81
    "[| xz : r O s;  \
nipkow@1128
    82
\       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
nipkow@1128
    83
\    |] ==> P";
nipkow@1128
    84
by (cut_facts_tac prems 1);
paulson@1985
    85
by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
paulson@1985
    86
     ORELSE ares_tac prems 1));
nipkow@1128
    87
qed "compE";
nipkow@1128
    88
paulson@5316
    89
val prems = Goal
nipkow@1128
    90
    "[| (a,c) : r O s;  \
nipkow@1128
    91
\       !!y. [| (a,y):s;  (y,c):r |] ==> P \
nipkow@1128
    92
\    |] ==> P";
nipkow@1128
    93
by (rtac compE 1);
nipkow@1128
    94
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
nipkow@1128
    95
qed "compEpair";
nipkow@1128
    96
nipkow@5608
    97
AddIs [compI, IdI];
nipkow@5608
    98
AddSEs [compE, IdE];
berghofe@1754
    99
nipkow@5608
   100
Goal "R O Id = R";
paulson@4673
   101
by (Fast_tac 1);
nipkow@5608
   102
qed "R_O_Id";
paulson@4673
   103
nipkow@5608
   104
Goal "Id O R = R";
paulson@4673
   105
by (Fast_tac 1);
nipkow@5608
   106
qed "Id_O_R";
paulson@4673
   107
nipkow@5608
   108
Addsimps [R_O_Id,Id_O_R];
paulson@4673
   109
wenzelm@5069
   110
Goal "(R O S) O T = R O (S O T)";
nipkow@4830
   111
by (Blast_tac 1);
nipkow@4830
   112
qed "O_assoc";
nipkow@4830
   113
paulson@9113
   114
Goalw [trans_def] "trans r ==> r O r <= r";
paulson@9113
   115
by (Blast_tac 1);
paulson@9113
   116
qed "trans_O_subset";
paulson@9113
   117
paulson@5143
   118
Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
paulson@2891
   119
by (Blast_tac 1);
nipkow@1128
   120
qed "comp_mono";
nipkow@1128
   121
nipkow@8703
   122
Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
paulson@2891
   123
by (Blast_tac 1);
nipkow@1128
   124
qed "comp_subset_Sigma";
nipkow@1128
   125
paulson@6806
   126
(** Natural deduction for refl(r) **)
paulson@6806
   127
paulson@6806
   128
val prems = Goalw [refl_def]
nipkow@8703
   129
    "[| r <= A <*> A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
paulson@6806
   130
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
paulson@6806
   131
qed "reflI";
paulson@6806
   132
paulson@6806
   133
Goalw [refl_def] "[| refl A r; a:A |] ==> (a,a):r";
paulson@6806
   134
by (Blast_tac 1);
paulson@6806
   135
qed "reflD";
paulson@6806
   136
paulson@6806
   137
(** Natural deduction for antisym(r) **)
paulson@6806
   138
paulson@6806
   139
val prems = Goalw [antisym_def]
paulson@6806
   140
    "(!! x y. [| (x,y):r;  (y,x):r |] ==> x=y) ==> antisym(r)";
paulson@6806
   141
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
paulson@6806
   142
qed "antisymI";
paulson@6806
   143
paulson@6806
   144
Goalw [antisym_def] "[| antisym(r);  (a,b):r;  (b,a):r |] ==> a=b";
paulson@6806
   145
by (Blast_tac 1);
paulson@6806
   146
qed "antisymD";
paulson@6806
   147
nipkow@1128
   148
(** Natural deduction for trans(r) **)
nipkow@1128
   149
paulson@5316
   150
val prems = Goalw [trans_def]
nipkow@1128
   151
    "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
nipkow@1128
   152
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
nipkow@1128
   153
qed "transI";
nipkow@1128
   154
paulson@5148
   155
Goalw [trans_def] "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
paulson@2891
   156
by (Blast_tac 1);
nipkow@1128
   157
qed "transD";
nipkow@1128
   158
nipkow@3439
   159
(** Natural deduction for r^-1 **)
nipkow@1128
   160
paulson@5143
   161
Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
paulson@1985
   162
by (Simp_tac 1);
paulson@4746
   163
qed "converse_iff";
paulson@1985
   164
paulson@4746
   165
AddIffs [converse_iff];
paulson@1985
   166
paulson@5143
   167
Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
clasohm@1264
   168
by (Simp_tac 1);
paulson@4746
   169
qed "converseI";
nipkow@1128
   170
paulson@5143
   171
Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
paulson@2891
   172
by (Blast_tac 1);
paulson@4746
   173
qed "converseD";
nipkow@1128
   174
paulson@4746
   175
(*More general than converseD, as it "splits" the member of the relation*)
paulson@7031
   176
paulson@7031
   177
val [major,minor] = Goalw [converse_def]
nipkow@3439
   178
    "[| yx : r^-1;  \
nipkow@1128
   179
\       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
paulson@7031
   180
\    |] ==> P";
paulson@7031
   181
by (rtac (major RS CollectE) 1);
paulson@7031
   182
by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
paulson@7031
   183
by (assume_tac 1);
paulson@7031
   184
qed "converseE";
paulson@4746
   185
AddSEs [converseE];
nipkow@1128
   186
wenzelm@5069
   187
Goalw [converse_def] "(r^-1)^-1 = r";
paulson@2891
   188
by (Blast_tac 1);
paulson@4746
   189
qed "converse_converse";
paulson@4746
   190
Addsimps [converse_converse];
nipkow@3413
   191
wenzelm@5069
   192
Goal "(r O s)^-1 = s^-1 O r^-1";
wenzelm@4423
   193
by (Blast_tac 1);
paulson@4746
   194
qed "converse_comp";
nipkow@1605
   195
nipkow@5608
   196
Goal "Id^-1 = Id";
paulson@4644
   197
by (Blast_tac 1);
nipkow@5608
   198
qed "converse_Id";
nipkow@5608
   199
Addsimps [converse_Id];
paulson@4644
   200
paulson@5995
   201
Goal "(diag A) ^-1 = diag A";
paulson@5995
   202
by (Blast_tac 1);
paulson@5995
   203
qed "converse_diag";
paulson@5995
   204
Addsimps [converse_diag];
paulson@5995
   205
paulson@7083
   206
Goalw [refl_def] "refl A r ==> refl A (converse r)";
paulson@7083
   207
by (Blast_tac 1);
paulson@7083
   208
qed "refl_converse";
paulson@7083
   209
paulson@7083
   210
Goalw [antisym_def] "antisym (converse r) = antisym r";
paulson@7083
   211
by (Blast_tac 1);
paulson@7083
   212
qed "antisym_converse";
paulson@7083
   213
paulson@7083
   214
Goalw [trans_def] "trans (converse r) = trans r";
paulson@7083
   215
by (Blast_tac 1);
paulson@7083
   216
qed "trans_converse";
paulson@7083
   217
nipkow@1128
   218
(** Domain **)
nipkow@1128
   219
paulson@5811
   220
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
paulson@5811
   221
by (Blast_tac 1);
paulson@5811
   222
qed "Domain_iff";
nipkow@1128
   223
paulson@7007
   224
Goal "(a,b): r ==> a: Domain(r)";
paulson@7007
   225
by (etac (exI RS (Domain_iff RS iffD2)) 1) ;
paulson@7007
   226
qed "DomainI";
nipkow@1128
   227
paulson@7007
   228
val prems= Goal "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P";
paulson@7007
   229
by (rtac (Domain_iff RS iffD1 RS exE) 1);
paulson@7007
   230
by (REPEAT (ares_tac prems 1)) ;
paulson@7007
   231
qed "DomainE";
nipkow@1128
   232
paulson@1985
   233
AddIs  [DomainI];
paulson@1985
   234
AddSEs [DomainE];
paulson@1985
   235
paulson@10786
   236
Goal "Domain {} = {}";
paulson@10786
   237
by (Blast_tac 1); 
paulson@10786
   238
qed "Domain_empty";
paulson@10786
   239
Addsimps [Domain_empty];
paulson@10786
   240
paulson@10786
   241
Goal "Domain (insert (a, b) r) = insert a (Domain r)";
paulson@10786
   242
by (Blast_tac 1); 
paulson@10786
   243
qed "Domain_insert";
paulson@10786
   244
nipkow@5608
   245
Goal "Domain Id = UNIV";
paulson@4644
   246
by (Blast_tac 1);
nipkow@5608
   247
qed "Domain_Id";
nipkow@5608
   248
Addsimps [Domain_Id];
paulson@4644
   249
paulson@5978
   250
Goal "Domain (diag A) = A";
paulson@5978
   251
by Auto_tac;
paulson@5978
   252
qed "Domain_diag";
paulson@5978
   253
Addsimps [Domain_diag];
paulson@5978
   254
paulson@5811
   255
Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
paulson@5811
   256
by (Blast_tac 1);
paulson@5811
   257
qed "Domain_Un_eq";
paulson@5811
   258
paulson@5811
   259
Goal "Domain(A Int B) <= Domain(A) Int Domain(B)";
paulson@5811
   260
by (Blast_tac 1);
paulson@5811
   261
qed "Domain_Int_subset";
paulson@5811
   262
paulson@5811
   263
Goal "Domain(A) - Domain(B) <= Domain(A - B)";
paulson@5811
   264
by (Blast_tac 1);
paulson@5811
   265
qed "Domain_Diff_subset";
paulson@5811
   266
paulson@6005
   267
Goal "Domain (Union S) = (UN A:S. Domain A)";
paulson@6005
   268
by (Blast_tac 1);
paulson@6005
   269
qed "Domain_Union";
paulson@6005
   270
paulson@7822
   271
Goal "r <= s ==> Domain r <= Domain s";
paulson@7822
   272
by (Blast_tac 1);
paulson@7822
   273
qed "Domain_mono";
paulson@7822
   274
paulson@5811
   275
nipkow@1128
   276
(** Range **)
nipkow@1128
   277
paulson@5811
   278
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
paulson@5811
   279
by (Blast_tac 1);
paulson@5811
   280
qed "Range_iff";
paulson@5811
   281
paulson@7031
   282
Goalw [Range_def] "(a,b): r ==> b : Range(r)";
paulson@7031
   283
by (etac (converseI RS DomainI) 1);
paulson@7031
   284
qed "RangeI";
nipkow@1128
   285
paulson@7031
   286
val major::prems = Goalw [Range_def] 
paulson@7031
   287
    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P";
paulson@7031
   288
by (rtac (major RS DomainE) 1);
paulson@7031
   289
by (resolve_tac prems 1);
paulson@7031
   290
by (etac converseD 1) ;
paulson@7031
   291
qed "RangeE";
nipkow@1128
   292
paulson@1985
   293
AddIs  [RangeI];
paulson@1985
   294
AddSEs [RangeE];
paulson@1985
   295
paulson@10786
   296
Goal "Range {} = {}";
paulson@10786
   297
by (Blast_tac 1); 
paulson@10786
   298
qed "Range_empty";
paulson@10786
   299
Addsimps [Range_empty];
paulson@10786
   300
paulson@10786
   301
Goal "Range (insert (a, b) r) = insert b (Range r)";
paulson@10786
   302
by (Blast_tac 1); 
paulson@10786
   303
qed "Range_insert";
paulson@10786
   304
nipkow@5608
   305
Goal "Range Id = UNIV";
paulson@4644
   306
by (Blast_tac 1);
nipkow@5608
   307
qed "Range_Id";
nipkow@5608
   308
Addsimps [Range_Id];
paulson@4644
   309
paulson@5995
   310
Goal "Range (diag A) = A";
paulson@5995
   311
by Auto_tac;
paulson@5995
   312
qed "Range_diag";
paulson@5995
   313
Addsimps [Range_diag];
paulson@5995
   314
paulson@5811
   315
Goal "Range(A Un B) = Range(A) Un Range(B)";
paulson@5811
   316
by (Blast_tac 1);
paulson@5811
   317
qed "Range_Un_eq";
paulson@5811
   318
paulson@5811
   319
Goal "Range(A Int B) <= Range(A) Int Range(B)";
paulson@5811
   320
by (Blast_tac 1);
paulson@5811
   321
qed "Range_Int_subset";
paulson@5811
   322
paulson@5811
   323
Goal "Range(A) - Range(B) <= Range(A - B)";
paulson@5811
   324
by (Blast_tac 1);
paulson@5811
   325
qed "Range_Diff_subset";
paulson@5811
   326
paulson@6005
   327
Goal "Range (Union S) = (UN A:S. Range A)";
paulson@6005
   328
by (Blast_tac 1);
paulson@6005
   329
qed "Range_Union";
paulson@6005
   330
paulson@5811
   331
nipkow@1128
   332
(*** Image of a set under a relation ***)
nipkow@1128
   333
paulson@8004
   334
overload_1st_set "Relation.Image";
paulson@5335
   335
paulson@11451
   336
Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
paulson@7031
   337
by (Blast_tac 1);
paulson@7031
   338
qed "Image_iff";
nipkow@1128
   339
nipkow@10832
   340
Goalw [Image_def] "r``{a} = {b. (a,b):r}";
paulson@7031
   341
by (Blast_tac 1);
paulson@7031
   342
qed "Image_singleton";
paulson@4673
   343
nipkow@10832
   344
Goal "(b : r``{a}) = ((a,b):r)";
paulson@7007
   345
by (rtac (Image_iff RS trans) 1);
paulson@7007
   346
by (Blast_tac 1);
paulson@7007
   347
qed "Image_singleton_iff";
nipkow@1128
   348
paulson@4673
   349
AddIffs [Image_singleton_iff];
paulson@4673
   350
nipkow@10832
   351
Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r``A";
paulson@7007
   352
by (Blast_tac 1);
paulson@7007
   353
qed "ImageI";
nipkow@1128
   354
paulson@7031
   355
val major::prems = Goalw [Image_def]
nipkow@10832
   356
    "[| b: r``A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
paulson@7031
   357
by (rtac (major RS CollectE) 1);
paulson@7031
   358
by (Clarify_tac 1);
paulson@7031
   359
by (rtac (hd prems) 1);
paulson@7031
   360
by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
paulson@7031
   361
qed "ImageE";
nipkow@1128
   362
paulson@1985
   363
AddIs  [ImageI];
paulson@1985
   364
AddSEs [ImageE];
paulson@1985
   365
paulson@8174
   366
(*This version's more effective when we already have the required "a"*)
nipkow@10832
   367
Goal  "[| a:A;  (a,b): r |] ==> b : r``A";
paulson@8174
   368
by (Blast_tac 1);
paulson@8174
   369
qed "rev_ImageI";
paulson@8174
   370
nipkow@10832
   371
Goal "R``{} = {}";
paulson@7007
   372
by (Blast_tac 1);
paulson@7007
   373
qed "Image_empty";
paulson@4593
   374
paulson@4593
   375
Addsimps [Image_empty];
paulson@4593
   376
nipkow@10832
   377
Goal "Id `` A = A";
paulson@4601
   378
by (Blast_tac 1);
nipkow@5608
   379
qed "Image_Id";
paulson@4601
   380
nipkow@10832
   381
Goal "diag A `` B = A Int B";
paulson@5995
   382
by (Blast_tac 1);
paulson@5995
   383
qed "Image_diag";
paulson@5995
   384
paulson@5995
   385
Addsimps [Image_Id, Image_diag];
paulson@4601
   386
nipkow@10832
   387
Goal "R `` (A Int B) <= R `` A Int R `` B";
paulson@7007
   388
by (Blast_tac 1);
paulson@7007
   389
qed "Image_Int_subset";
paulson@4593
   390
nipkow@10832
   391
Goal "R `` (A Un B) = R `` A Un R `` B";
paulson@7007
   392
by (Blast_tac 1);
paulson@7007
   393
qed "Image_Un";
paulson@4593
   394
nipkow@10832
   395
Goal "r <= A <*> B ==> r``C <= B";
paulson@7007
   396
by (rtac subsetI 1);
paulson@7007
   397
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
paulson@7007
   398
qed "Image_subset";
nipkow@1128
   399
paulson@4733
   400
(*NOT suitable for rewriting*)
nipkow@10832
   401
Goal "r``B = (UN y: B. r``{y})";
paulson@4673
   402
by (Blast_tac 1);
paulson@4733
   403
qed "Image_eq_UN";
oheimb@4760
   404
nipkow@10832
   405
Goal "[| r'<=r; A'<=A |] ==> (r' `` A') <= (r `` A)";
paulson@7913
   406
by (Blast_tac 1);
paulson@7913
   407
qed "Image_mono";
paulson@7913
   408
nipkow@10832
   409
Goal "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))";
paulson@7913
   410
by (Blast_tac 1);
paulson@7913
   411
qed "Image_UN";
paulson@7913
   412
paulson@7913
   413
(*Converse inclusion fails*)
nipkow@10832
   414
Goal "(r `` (INTER A B)) <= (INT x:A.(r `` (B x)))";
paulson@7913
   415
by (Blast_tac 1);
paulson@7913
   416
qed "Image_INT_subset";
paulson@7913
   417
nipkow@10832
   418
Goal "(r``A <= B) = (A <= - ((r^-1) `` (-B)))";
paulson@8004
   419
by (Blast_tac 1);
paulson@8004
   420
qed "Image_subset_eq";
oheimb@4760
   421
nipkow@10797
   422
section "single_valued";
oheimb@4760
   423
nipkow@10797
   424
Goalw [single_valued_def]
paulson@11451
   425
     "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r";
paulson@7031
   426
by (assume_tac 1);
nipkow@10797
   427
qed "single_valuedI";
oheimb@4760
   428
nipkow@10797
   429
Goalw [single_valued_def]
nipkow@10797
   430
     "[| single_valued r;  (x,y):r;  (x,z):r|] ==> y=z";
paulson@7031
   431
by Auto_tac;
nipkow@10797
   432
qed "single_valuedD";
paulson@5231
   433
paulson@5231
   434
paulson@9097
   435
(** Graphs given by Collect **)
paulson@9097
   436
paulson@9097
   437
Goal "Domain{(x,y). P x y} = {x. EX y. P x y}";
paulson@9097
   438
by Auto_tac; 
paulson@9097
   439
qed "Domain_Collect_split";
paulson@5231
   440
paulson@9097
   441
Goal "Range{(x,y). P x y} = {y. EX x. P x y}";
paulson@9097
   442
by Auto_tac; 
paulson@9097
   443
qed "Range_Collect_split";
paulson@5231
   444
nipkow@10832
   445
Goal "{(x,y). P x y} `` A = {y. EX x:A. P x y}";
paulson@9097
   446
by Auto_tac; 
paulson@9097
   447
qed "Image_Collect_split";
paulson@5231
   448
paulson@9097
   449
Addsimps [Domain_Collect_split, Range_Collect_split, Image_Collect_split];
berghofe@7014
   450
berghofe@7014
   451
(** Composition of function and relation **)
berghofe@7014
   452
berghofe@7014
   453
Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B";
berghofe@7014
   454
by (Fast_tac 1);
berghofe@7014
   455
qed "fun_rel_comp_mono";
berghofe@7014
   456
paulson@11451
   457
Goalw [fun_rel_comp_def]
paulson@11451
   458
     "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R";
paulson@11451
   459
by (res_inst_tac [("a","%x. THE y. (f x, y) : R")] ex1I 1);
paulson@11451
   460
by (fast_tac (claset() addSDs [theI']) 1); 
paulson@11451
   461
by (fast_tac (claset() addIs [ext, the1_equality RS sym]) 1);
berghofe@7014
   462
qed "fun_rel_comp_unique";
oheimb@11136
   463
oheimb@11136
   464
oheimb@11136
   465
section "inverse image";
oheimb@11136
   466
oheimb@11136
   467
Goalw [trans_def,inv_image_def]
paulson@11451
   468
    "trans r ==> trans (inv_image r f)";
oheimb@11136
   469
by (Simp_tac 1);
oheimb@11136
   470
by (Blast_tac 1);
oheimb@11136
   471
qed "trans_inv_image";
oheimb@11136
   472