src/HOL/Relation.ML
author paulson
Fri, 27 Nov 1998 10:40:29 +0100
changeset 5978 fa2c2dd74f8c
parent 5811 0867068942e6
child 5995 450cd1f0270b
permissions -rw-r--r--
moved diag (diagonal relation) from Univ to Relation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1454
diff changeset
     1
(*  Title:      Relation.ML
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
     3
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
     4
    Copyright   1996  University of Cambridge
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     5
*)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     6
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     7
open Relation;
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     8
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     9
(** Identity relation **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    10
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    11
Goalw [Id_def] "(a,a) : Id";  
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    12
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    13
qed "IdI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    14
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    15
val major::prems = Goalw [Id_def]
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    16
    "[| p: Id;  !!x.[| p = (x,x) |] ==> P  \
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    17
\    |] ==>  P";  
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    18
by (rtac (major RS CollectE) 1);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    19
by (etac exE 1);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    20
by (eresolve_tac prems 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    21
qed "IdE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    22
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    23
Goalw [Id_def] "(a,b):Id = (a=b)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    24
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    25
qed "pair_in_Id_conv";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    26
Addsimps [pair_in_Id_conv];
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    27
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    28
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    29
(** Diagonal relation: indentity restricted to some set **)
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    30
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    31
(*** Equality : the diagonal relation ***)
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    32
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    33
Goalw [diag_def] "[| a=b;  a:A |] ==> (a,b) : diag(A)";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    34
by (Blast_tac 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    35
qed "diag_eqI";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    36
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    37
val diagI = refl RS diag_eqI |> standard;
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    38
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    39
(*The general elimination rule*)
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    40
val major::prems = Goalw [diag_def]
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    41
    "[| c : diag(A);  \
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    42
\       !!x y. [| x:A;  c = (x,x) |] ==> P \
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    43
\    |] ==> P";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    44
by (rtac (major RS UN_E) 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    45
by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    46
qed "diagE";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    47
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    48
AddSIs [diagI];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    49
AddSEs [diagE];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    50
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    51
Goal "((x,y) : diag A) = (x=y & x : A)";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    52
by (Blast_tac 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    53
qed "diag_iff";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    54
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    55
Goal "diag(A) <= A Times A";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    56
by (Blast_tac 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    57
qed "diag_subset_Sigma";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    58
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    59
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    60
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    61
(** Composition of two relations **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    62
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
    63
Goalw [comp_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
    64
    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    65
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    66
qed "compI";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    67
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    68
(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5231
diff changeset
    69
val prems = Goalw [comp_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    70
    "[| xz : r O s;  \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    71
\       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    72
\    |] ==> P";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    73
by (cut_facts_tac prems 1);
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
    74
by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
    75
     ORELSE ares_tac prems 1));
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    76
qed "compE";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    77
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5231
diff changeset
    78
val prems = Goal
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    79
    "[| (a,c) : r O s;  \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    80
\       !!y. [| (a,y):s;  (y,c):r |] ==> P \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    81
\    |] ==> P";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    82
by (rtac compE 1);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    83
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    84
qed "compEpair";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    85
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    86
AddIs [compI, IdI];
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    87
AddSEs [compE, IdE];
1754
852093aeb0ab Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents: 1694
diff changeset
    88
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    89
Goal "R O Id = R";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
    90
by (Fast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    91
qed "R_O_Id";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
    92
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    93
Goal "Id O R = R";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
    94
by (Fast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    95
qed "Id_O_R";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
    96
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    97
Addsimps [R_O_Id,Id_O_R];
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
    98
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
    99
Goal "(R O S) O T = R O (S O T)";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4760
diff changeset
   100
by (Blast_tac 1);
bd73675adbed Added a few lemmas.
nipkow
parents: 4760
diff changeset
   101
qed "O_assoc";
bd73675adbed Added a few lemmas.
nipkow
parents: 4760
diff changeset
   102
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   103
Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   104
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   105
qed "comp_mono";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   106
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   107
Goal "[| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   108
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   109
qed "comp_subset_Sigma";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   110
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   111
(** Natural deduction for trans(r) **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   112
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5231
diff changeset
   113
val prems = Goalw [trans_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   114
    "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   115
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   116
qed "transI";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   117
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   118
Goalw [trans_def] "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   119
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   120
qed "transD";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   121
3439
54785105178c converse -> ^-1
nipkow
parents: 3413
diff changeset
   122
(** Natural deduction for r^-1 **)
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   123
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   124
Goalw [converse_def] "((a,b): r^-1) = ((b,a):r)";
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   125
by (Simp_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   126
qed "converse_iff";
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   127
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   128
AddIffs [converse_iff];
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   129
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   130
Goalw [converse_def] "(a,b):r ==> (b,a): r^-1";
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1128
diff changeset
   131
by (Simp_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   132
qed "converseI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   133
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   134
Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   135
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   136
qed "converseD";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   137
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   138
(*More general than converseD, as it "splits" the member of the relation*)
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   139
qed_goalw "converseE" thy [converse_def]
3439
54785105178c converse -> ^-1
nipkow
parents: 3413
diff changeset
   140
    "[| yx : r^-1;  \
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   141
\       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   142
\    |] ==> P"
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   143
 (fn [major,minor]=>
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   144
  [ (rtac (major RS CollectE) 1),
1454
d0266c81a85e Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents: 1264
diff changeset
   145
    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   146
    (assume_tac 1) ]);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   147
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   148
AddSEs [converseE];
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   149
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   150
Goalw [converse_def] "(r^-1)^-1 = r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   151
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   152
qed "converse_converse";
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   153
Addsimps [converse_converse];
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 2891
diff changeset
   154
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   155
Goal "(r O s)^-1 = s^-1 O r^-1";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
   156
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   157
qed "converse_comp";
1605
248e1e125ca0 added converse_converse
nipkow
parents: 1552
diff changeset
   158
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   159
Goal "Id^-1 = Id";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   160
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   161
qed "converse_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   162
Addsimps [converse_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   163
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   164
(** Domain **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   165
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   166
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   167
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   168
qed "Domain_iff";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   169
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   170
qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)"
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   171
 (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   172
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   173
qed_goal "DomainE" thy
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   174
    "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P"
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   175
 (fn prems=>
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   176
  [ (rtac (Domain_iff RS iffD1 RS exE) 1),
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   177
    (REPEAT (ares_tac prems 1)) ]);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   178
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   179
AddIs  [DomainI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   180
AddSEs [DomainE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   181
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   182
Goal "Domain Id = UNIV";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   183
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   184
qed "Domain_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   185
Addsimps [Domain_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   186
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   187
Goal "Domain (diag A) = A";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   188
by Auto_tac;
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   189
qed "Domain_diag";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   190
Addsimps [Domain_diag];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   191
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   192
Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   193
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   194
qed "Domain_Un_eq";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   195
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   196
Goal "Domain(A Int B) <= Domain(A) Int Domain(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   197
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   198
qed "Domain_Int_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   199
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   200
Goal "Domain(A) - Domain(B) <= Domain(A - B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   201
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   202
qed "Domain_Diff_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   203
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   204
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   205
(** Range **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   206
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   207
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   208
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   209
qed "Range_iff";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   210
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   211
qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   212
 (fn _ => [ (etac (converseI RS DomainI) 1) ]);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   213
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   214
qed_goalw "RangeE" thy [Range_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   215
    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   216
 (fn major::prems=>
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   217
  [ (rtac (major RS DomainE) 1),
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   218
    (resolve_tac prems 1),
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   219
    (etac converseD 1) ]);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   220
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   221
AddIs  [RangeI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   222
AddSEs [RangeE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   223
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   224
Goal "Range Id = UNIV";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   225
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   226
qed "Range_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   227
Addsimps [Range_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   228
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   229
Goal "Range(A Un B) = Range(A) Un Range(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   230
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   231
qed "Range_Un_eq";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   232
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   233
Goal "Range(A Int B) <= Range(A) Int Range(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   234
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   235
qed "Range_Int_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   236
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   237
Goal "Range(A) - Range(B) <= Range(A - B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   238
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   239
qed "Range_Diff_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   240
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   241
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   242
(*** Image of a set under a relation ***)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   243
5649
1bac26652f45 Uses overload_1st_set to specify overloading
paulson
parents: 5608
diff changeset
   244
overload_1st_set "Relation.op ^^";
5335
07fb8999de62 Overloading decl should assist Blast_tac
paulson
parents: 5316
diff changeset
   245
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   246
qed_goalw "Image_iff" thy [Image_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   247
    "b : r^^A = (? x:A. (x,b):r)"
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   248
 (fn _ => [ Blast_tac 1 ]);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   249
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   250
qed_goalw "Image_singleton" thy [Image_def]
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   251
    "r^^{a} = {b. (a,b):r}"
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   252
 (fn _ => [ Blast_tac 1 ]);
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   253
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   254
qed_goal "Image_singleton_iff" thy
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   255
    "(b : r^^{a}) = ((a,b):r)"
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   256
 (fn _ => [ rtac (Image_iff RS trans) 1,
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   257
            Blast_tac 1 ]);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   258
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   259
AddIffs [Image_singleton_iff];
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   260
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   261
qed_goalw "ImageI" thy [Image_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   262
    "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   263
 (fn _ => [ (Blast_tac 1)]);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   264
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   265
qed_goalw "ImageE" thy [Image_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   266
    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   267
 (fn major::prems=>
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   268
  [ (rtac (major RS CollectE) 1),
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3439
diff changeset
   269
    (Clarify_tac 1),
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   270
    (rtac (hd prems) 1),
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   271
    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   272
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   273
AddIs  [ImageI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   274
AddSEs [ImageE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   275
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   276
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   277
qed_goal "Image_empty" thy
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   278
    "R^^{} = {}"
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   279
 (fn _ => [ Blast_tac 1 ]);
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   280
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   281
Addsimps [Image_empty];
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   282
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   283
Goal "Id ^^ A = A";
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   284
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   285
qed "Image_Id";
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   286
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   287
Addsimps [Image_Id];
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   288
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   289
qed_goal "Image_Int_subset" thy
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   290
    "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   291
 (fn _ => [ Blast_tac 1 ]);
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   292
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   293
qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B"
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   294
 (fn _ => [ Blast_tac 1 ]);
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   295
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   296
qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B"
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   297
 (fn _ =>
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   298
  [ (rtac subsetI 1),
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   299
    (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   300
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   301
(*NOT suitable for rewriting*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   302
Goal "r^^B = (UN y: B. r^^{y})";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   303
by (Blast_tac 1);
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   304
qed "Image_eq_UN";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   305
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   306
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   307
section "Univalent";
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   308
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   309
qed_goalw "UnivalentI" Relation.thy [Univalent_def] 
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   310
   "!!r. !x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r" (K [atac 1]);
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   311
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   312
qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   313
	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);
5231
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   314
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   315
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   316
(** Graphs of partial functions **)
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   317
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   318
Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   319
by (Blast_tac 1);
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   320
qed "Domain_partial_func";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   321
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   322
Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   323
by (Blast_tac 1);
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   324
qed "Range_partial_func";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   325