src/HOL/Relation.ML
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8703 816d8f6513be
child 9097 44cd0f9f8e5b
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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
(** Identity relation **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
     8
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
     9
Goalw [Id_def] "(a,a) : Id";  
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    10
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    11
qed "IdI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    12
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    13
val major::prems = Goalw [Id_def]
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    14
    "[| 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
    15
\    |] ==>  P";  
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    16
by (rtac (major RS CollectE) 1);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    17
by (etac exE 1);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    18
by (eresolve_tac prems 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    19
qed "IdE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    20
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    21
Goalw [Id_def] "(a,b):Id = (a=b)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    22
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    23
qed "pair_in_Id_conv";
8265
187cada50e19 A few lemmas and some Adds.
nipkow
parents: 8174
diff changeset
    24
AddIffs [pair_in_Id_conv];
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    25
6806
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    26
Goalw [refl_def] "reflexive Id";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    27
by Auto_tac;
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    28
qed "reflexive_Id";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    29
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    30
(*A strange result, since Id is also symmetric.*)
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    31
Goalw [antisym_def] "antisym Id";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    32
by Auto_tac;
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    33
qed "antisym_Id";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    34
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    35
Goalw [trans_def] "trans Id";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    36
by Auto_tac;
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    37
qed "trans_Id";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
    38
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    39
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    40
(** Diagonal relation: indentity restricted to some set **)
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    41
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    42
(*** Equality : the diagonal relation ***)
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    43
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    44
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
    45
by (Blast_tac 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    46
qed "diag_eqI";
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
val diagI = refl RS diag_eqI |> standard;
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    49
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    50
(*The general elimination rule*)
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    51
val major::prems = Goalw [diag_def]
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    52
    "[| c : diag(A);  \
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    53
\       !!x y. [| x:A;  c = (x,x) |] ==> P \
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    54
\    |] ==> P";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    55
by (rtac (major RS UN_E) 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    56
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
    57
qed "diagE";
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
AddSIs [diagI];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    60
AddSEs [diagE];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    61
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    62
Goal "((x,y) : diag A) = (x=y & x : A)";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    63
by (Blast_tac 1);
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    64
qed "diag_iff";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    65
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
    66
Goal "diag(A) <= A <*> A";
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    67
by (Blast_tac 1);
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
    68
qed "diag_subset_Times";
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    69
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    70
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
    71
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    72
(** Composition of two relations **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    73
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
    74
Goalw [comp_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
    75
    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
    76
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    77
qed "compI";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    78
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    79
(*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
    80
val prems = Goalw [comp_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    81
    "[| xz : r O s;  \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    82
\       !!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
    83
\    |] ==> P";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    84
by (cut_facts_tac prems 1);
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
    85
by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
    86
     ORELSE ares_tac prems 1));
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    87
qed "compE";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    88
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5231
diff changeset
    89
val prems = Goal
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    90
    "[| (a,c) : r O s;  \
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    91
\       !!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
    92
\    |] ==> P";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    93
by (rtac compE 1);
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    94
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
    95
qed "compEpair";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
    96
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    97
AddIs [compI, IdI];
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
    98
AddSEs [compE, IdE];
1754
852093aeb0ab Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents: 1694
diff changeset
    99
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   100
Goal "R O Id = R";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   101
by (Fast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   102
qed "R_O_Id";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   103
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   104
Goal "Id O R = R";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   105
by (Fast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   106
qed "Id_O_R";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   107
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   108
Addsimps [R_O_Id,Id_O_R];
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   109
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   110
Goal "(R O S) O T = R O (S O T)";
4830
bd73675adbed Added a few lemmas.
nipkow
parents: 4760
diff changeset
   111
by (Blast_tac 1);
bd73675adbed Added a few lemmas.
nipkow
parents: 4760
diff changeset
   112
qed "O_assoc";
bd73675adbed Added a few lemmas.
nipkow
parents: 4760
diff changeset
   113
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   114
Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   115
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   116
qed "comp_mono";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   117
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
   118
Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
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 "comp_subset_Sigma";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   121
6806
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   122
(** Natural deduction for refl(r) **)
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   123
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   124
val prems = Goalw [refl_def]
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
   125
    "[| r <= A <*> A;  !! x. x:A ==> (x,x):r |] ==> refl A r";
6806
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   126
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   127
qed "reflI";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   128
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   129
Goalw [refl_def] "[| refl A r; a:A |] ==> (a,a):r";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   130
by (Blast_tac 1);
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   131
qed "reflD";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   132
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   133
(** Natural deduction for antisym(r) **)
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   134
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   135
val prems = Goalw [antisym_def]
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   136
    "(!! x y. [| (x,y):r;  (y,x):r |] ==> x=y) ==> antisym(r)";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   137
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   138
qed "antisymI";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   139
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   140
Goalw [antisym_def] "[| antisym(r);  (a,b):r;  (b,a):r |] ==> a=b";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   141
by (Blast_tac 1);
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   142
qed "antisymD";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   143
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   144
(** Natural deduction for trans(r) **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   145
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5231
diff changeset
   146
val prems = Goalw [trans_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   147
    "(!! 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
   148
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
   149
qed "transI";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   150
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   151
Goalw [trans_def] "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   152
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   153
qed "transD";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   154
3439
54785105178c converse -> ^-1
nipkow
parents: 3413
diff changeset
   155
(** Natural deduction for r^-1 **)
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   156
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   157
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
   158
by (Simp_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   159
qed "converse_iff";
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   160
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   161
AddIffs [converse_iff];
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   162
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   163
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
   164
by (Simp_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   165
qed "converseI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   166
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   167
Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   168
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   169
qed "converseD";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   170
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   171
(*More general than converseD, as it "splits" the member of the relation*)
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   172
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   173
val [major,minor] = Goalw [converse_def]
3439
54785105178c converse -> ^-1
nipkow
parents: 3413
diff changeset
   174
    "[| yx : r^-1;  \
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   175
\       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   176
\    |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   177
by (rtac (major RS CollectE) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   178
by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   179
by (assume_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   180
qed "converseE";
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   181
AddSEs [converseE];
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   182
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   183
Goalw [converse_def] "(r^-1)^-1 = r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   184
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   185
qed "converse_converse";
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   186
Addsimps [converse_converse];
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 2891
diff changeset
   187
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   188
Goal "(r O s)^-1 = s^-1 O r^-1";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
   189
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   190
qed "converse_comp";
1605
248e1e125ca0 added converse_converse
nipkow
parents: 1552
diff changeset
   191
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   192
Goal "Id^-1 = Id";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   193
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   194
qed "converse_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   195
Addsimps [converse_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   196
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   197
Goal "(diag A) ^-1 = diag A";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   198
by (Blast_tac 1);
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   199
qed "converse_diag";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   200
Addsimps [converse_diag];
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   201
7083
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   202
Goalw [refl_def] "refl A r ==> refl A (converse r)";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   203
by (Blast_tac 1);
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   204
qed "refl_converse";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   205
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   206
Goalw [antisym_def] "antisym (converse r) = antisym r";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   207
by (Blast_tac 1);
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   208
qed "antisym_converse";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   209
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   210
Goalw [trans_def] "trans (converse r) = trans r";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   211
by (Blast_tac 1);
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   212
qed "trans_converse";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   213
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   214
(** Domain **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   215
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   216
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   217
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   218
qed "Domain_iff";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   219
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   220
Goal "(a,b): r ==> a: Domain(r)";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   221
by (etac (exI RS (Domain_iff RS iffD2)) 1) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   222
qed "DomainI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   223
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   224
val prems= Goal "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   225
by (rtac (Domain_iff RS iffD1 RS exE) 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   226
by (REPEAT (ares_tac prems 1)) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   227
qed "DomainE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   228
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   229
AddIs  [DomainI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   230
AddSEs [DomainE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   231
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   232
Goal "Domain Id = UNIV";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   233
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   234
qed "Domain_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   235
Addsimps [Domain_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   236
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   237
Goal "Domain (diag A) = A";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   238
by Auto_tac;
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   239
qed "Domain_diag";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   240
Addsimps [Domain_diag];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   241
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   242
Goal "Domain(A Un B) = Domain(A) Un Domain(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   243
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   244
qed "Domain_Un_eq";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   245
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   246
Goal "Domain(A Int B) <= Domain(A) Int Domain(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   247
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   248
qed "Domain_Int_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   249
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   250
Goal "Domain(A) - Domain(B) <= Domain(A - B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   251
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   252
qed "Domain_Diff_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   253
6005
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   254
Goal "Domain (Union S) = (UN A:S. Domain A)";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   255
by (Blast_tac 1);
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   256
qed "Domain_Union";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   257
7822
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   258
Goal "r <= s ==> Domain r <= Domain s";
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   259
by (Blast_tac 1);
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   260
qed "Domain_mono";
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   261
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   262
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   263
(** Range **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   264
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   265
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   266
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   267
qed "Range_iff";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   268
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   269
Goalw [Range_def] "(a,b): r ==> b : Range(r)";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   270
by (etac (converseI RS DomainI) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   271
qed "RangeI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   272
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   273
val major::prems = Goalw [Range_def] 
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   274
    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   275
by (rtac (major RS DomainE) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   276
by (resolve_tac prems 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   277
by (etac converseD 1) ;
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   278
qed "RangeE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   279
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   280
AddIs  [RangeI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   281
AddSEs [RangeE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   282
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   283
Goal "Range Id = UNIV";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   284
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   285
qed "Range_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   286
Addsimps [Range_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   287
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   288
Goal "Range (diag A) = A";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   289
by Auto_tac;
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   290
qed "Range_diag";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   291
Addsimps [Range_diag];
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   292
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   293
Goal "Range(A Un B) = Range(A) Un Range(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   294
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   295
qed "Range_Un_eq";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   296
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   297
Goal "Range(A Int B) <= Range(A) Int Range(B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   298
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   299
qed "Range_Int_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   300
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   301
Goal "Range(A) - Range(B) <= Range(A - B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   302
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   303
qed "Range_Diff_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   304
6005
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   305
Goal "Range (Union S) = (UN A:S. Range A)";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   306
by (Blast_tac 1);
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   307
qed "Range_Union";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   308
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   309
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   310
(*** Image of a set under a relation ***)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   311
8004
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   312
overload_1st_set "Relation.Image";
5335
07fb8999de62 Overloading decl should assist Blast_tac
paulson
parents: 5316
diff changeset
   313
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   314
Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   315
by (Blast_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   316
qed "Image_iff";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   317
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   318
Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   319
by (Blast_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   320
qed "Image_singleton";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   321
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   322
Goal "(b : r^^{a}) = ((a,b):r)";
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   323
by (rtac (Image_iff RS trans) 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   324
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   325
qed "Image_singleton_iff";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   326
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   327
AddIffs [Image_singleton_iff];
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   328
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   329
Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r^^A";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   330
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   331
qed "ImageI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   332
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   333
val major::prems = Goalw [Image_def]
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   334
    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   335
by (rtac (major RS CollectE) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   336
by (Clarify_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   337
by (rtac (hd prems) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   338
by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   339
qed "ImageE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   340
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   341
AddIs  [ImageI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   342
AddSEs [ImageE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   343
8174
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   344
(*This version's more effective when we already have the required "a"*)
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   345
Goal  "[| a:A;  (a,b): r |] ==> b : r^^A";
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   346
by (Blast_tac 1);
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   347
qed "rev_ImageI";
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   348
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   349
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   350
Goal "R^^{} = {}";
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   351
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   352
qed "Image_empty";
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   353
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   354
Addsimps [Image_empty];
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   355
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   356
Goal "Id ^^ A = A";
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   357
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   358
qed "Image_Id";
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   359
5998
b2ecd577b8a3 better version of Image_diag
paulson
parents: 5995
diff changeset
   360
Goal "diag A ^^ B = A Int B";
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   361
by (Blast_tac 1);
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   362
qed "Image_diag";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   363
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   364
Addsimps [Image_Id, Image_diag];
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   365
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   366
Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   367
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   368
qed "Image_Int_subset";
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   369
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   370
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   371
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   372
qed "Image_Un";
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   373
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
   374
Goal "r <= A <*> B ==> r^^C <= B";
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   375
by (rtac subsetI 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   376
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   377
qed "Image_subset";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   378
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   379
(*NOT suitable for rewriting*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   380
Goal "r^^B = (UN y: B. r^^{y})";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   381
by (Blast_tac 1);
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   382
qed "Image_eq_UN";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   383
7913
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   384
Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   385
by (Blast_tac 1);
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   386
qed "Image_mono";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   387
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   388
Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   389
by (Blast_tac 1);
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   390
qed "Image_UN";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   391
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   392
(*Converse inclusion fails*)
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   393
Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   394
by (Blast_tac 1);
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   395
qed "Image_INT_subset";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   396
8004
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   397
Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   398
by (Blast_tac 1);
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   399
qed "Image_subset_eq";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   400
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   401
section "univalent";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   402
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   403
Goalw [univalent_def]
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   404
     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> univalent r";
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   405
by (assume_tac 1);
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   406
qed "univalentI";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   407
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   408
Goalw [univalent_def]
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   409
     "[| univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   410
by Auto_tac;
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   411
qed "univalentD";
5231
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   412
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   413
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   414
(** Graphs of partial functions **)
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   415
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   416
Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   417
by (Blast_tac 1);
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   418
qed "Domain_partial_func";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   419
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   420
Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   421
by (Blast_tac 1);
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   422
qed "Range_partial_func";
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   423
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   424
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   425
(** Composition of function and relation **)
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   426
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   427
Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B";
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   428
by (Fast_tac 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   429
qed "fun_rel_comp_mono";
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   430
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   431
Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   432
by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   433
by (rtac CollectI 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   434
by (rtac allI 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   435
by (etac allE 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   436
by (rtac (select_eq_Ex RS iffD2) 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   437
by (etac ex1_implies_ex 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   438
by (rtac ext 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   439
by (etac CollectE 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   440
by (REPEAT (etac allE 1));
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   441
by (rtac (select1_equality RS sym) 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   442
by (atac 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   443
by (atac 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   444
qed "fun_rel_comp_unique";