src/HOL/Relation.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9969 4753185f1dd2
child 10786 04ee73606993
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 9097
diff changeset
    48
bind_thm ("diagI", refl RS diag_eqI |> standard);
5978
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
9113
e221d4f81d52 new theorem trans_O_subset
paulson
parents: 9108
diff changeset
   114
Goalw [trans_def] "trans r ==> r O r <= r";
e221d4f81d52 new theorem trans_O_subset
paulson
parents: 9108
diff changeset
   115
by (Blast_tac 1);
e221d4f81d52 new theorem trans_O_subset
paulson
parents: 9108
diff changeset
   116
qed "trans_O_subset";
e221d4f81d52 new theorem trans_O_subset
paulson
parents: 9108
diff changeset
   117
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   118
Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
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_mono";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   121
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
   122
Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   123
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   124
qed "comp_subset_Sigma";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   125
6806
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   126
(** Natural deduction for refl(r) **)
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   127
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   128
val prems = Goalw [refl_def]
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
   129
    "[| 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
   130
by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   131
qed "reflI";
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
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
   134
by (Blast_tac 1);
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   135
qed "reflD";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   136
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   137
(** Natural deduction for antisym(r) **)
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   138
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   139
val prems = Goalw [antisym_def]
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   140
    "(!! 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
   141
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   142
qed "antisymI";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   143
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   144
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
   145
by (Blast_tac 1);
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   146
qed "antisymD";
43c081a0858d new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents: 6005
diff changeset
   147
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   148
(** Natural deduction for trans(r) **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   149
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5231
diff changeset
   150
val prems = Goalw [trans_def]
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   151
    "(!! 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
   152
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
   153
qed "transI";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   154
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   155
Goalw [trans_def] "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   156
by (Blast_tac 1);
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   157
qed "transD";
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   158
3439
54785105178c converse -> ^-1
nipkow
parents: 3413
diff changeset
   159
(** Natural deduction for r^-1 **)
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   160
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   161
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
   162
by (Simp_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   163
qed "converse_iff";
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   164
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   165
AddIffs [converse_iff];
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   166
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   167
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
   168
by (Simp_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   169
qed "converseI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   170
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   171
Goalw [converse_def] "(a,b) : r^-1 ==> (b,a) : r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   172
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   173
qed "converseD";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   174
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   175
(*More general than converseD, as it "splits" the member of the relation*)
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   176
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   177
val [major,minor] = Goalw [converse_def]
3439
54785105178c converse -> ^-1
nipkow
parents: 3413
diff changeset
   178
    "[| yx : r^-1;  \
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   179
\       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   180
\    |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   181
by (rtac (major RS CollectE) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   182
by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   183
by (assume_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   184
qed "converseE";
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   185
AddSEs [converseE];
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   186
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   187
Goalw [converse_def] "(r^-1)^-1 = r";
2891
d8f254ad1ab9 Calls Blast_tac
paulson
parents: 2637
diff changeset
   188
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   189
qed "converse_converse";
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   190
Addsimps [converse_converse];
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 2891
diff changeset
   191
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   192
Goal "(r O s)^-1 = s^-1 O r^-1";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
   193
by (Blast_tac 1);
4746
a5dcd7e4a37d inverse -> converse
paulson
parents: 4733
diff changeset
   194
qed "converse_comp";
1605
248e1e125ca0 added converse_converse
nipkow
parents: 1552
diff changeset
   195
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   196
Goal "Id^-1 = Id";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   197
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   198
qed "converse_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   199
Addsimps [converse_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   200
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   201
Goal "(diag A) ^-1 = diag A";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   202
by (Blast_tac 1);
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   203
qed "converse_diag";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   204
Addsimps [converse_diag];
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   205
7083
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   206
Goalw [refl_def] "refl A r ==> refl A (converse 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 "refl_converse";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   209
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   210
Goalw [antisym_def] "antisym (converse r) = antisym 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 "antisym_converse";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   213
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   214
Goalw [trans_def] "trans (converse r) = trans r";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   215
by (Blast_tac 1);
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   216
qed "trans_converse";
9663eb2bce05 three new theorems
paulson
parents: 7031
diff changeset
   217
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   218
(** Domain **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   219
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   220
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   221
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   222
qed "Domain_iff";
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
Goal "(a,b): r ==> a: Domain(r)";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   225
by (etac (exI RS (Domain_iff RS iffD2)) 1) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   226
qed "DomainI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   227
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   228
val prems= Goal "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   229
by (rtac (Domain_iff RS iffD1 RS exE) 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   230
by (REPEAT (ares_tac prems 1)) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   231
qed "DomainE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   232
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   233
AddIs  [DomainI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   234
AddSEs [DomainE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   235
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   236
Goal "Domain Id = UNIV";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   237
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   238
qed "Domain_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   239
Addsimps [Domain_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   240
5978
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   241
Goal "Domain (diag A) = A";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   242
by Auto_tac;
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   243
qed "Domain_diag";
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   244
Addsimps [Domain_diag];
fa2c2dd74f8c moved diag (diagonal relation) from Univ to Relation
paulson
parents: 5811
diff changeset
   245
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   246
Goal "Domain(A Un B) = Domain(A) Un 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_Un_eq";
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 Int B) <= Domain(A) Int Domain(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_Int_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   253
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   254
Goal "Domain(A) - Domain(B) <= Domain(A - B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   255
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   256
qed "Domain_Diff_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   257
6005
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   258
Goal "Domain (Union S) = (UN A:S. Domain A)";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   259
by (Blast_tac 1);
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   260
qed "Domain_Union";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   261
7822
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   262
Goal "r <= s ==> Domain r <= Domain s";
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   263
by (Blast_tac 1);
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   264
qed "Domain_mono";
09aabe6d04b8 new thm Domain_mono
paulson
parents: 7083
diff changeset
   265
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   266
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   267
(** Range **)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   268
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   269
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   270
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   271
qed "Range_iff";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   272
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   273
Goalw [Range_def] "(a,b): r ==> b : Range(r)";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   274
by (etac (converseI RS DomainI) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   275
qed "RangeI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   276
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   277
val major::prems = Goalw [Range_def] 
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   278
    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   279
by (rtac (major RS DomainE) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   280
by (resolve_tac prems 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   281
by (etac converseD 1) ;
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   282
qed "RangeE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   283
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   284
AddIs  [RangeI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   285
AddSEs [RangeE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   286
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   287
Goal "Range Id = UNIV";
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   288
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   289
qed "Range_Id";
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   290
Addsimps [Range_Id];
4644
ecf8f17f6fe0 New laws for id
paulson
parents: 4601
diff changeset
   291
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   292
Goal "Range (diag A) = A";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   293
by Auto_tac;
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   294
qed "Range_diag";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   295
Addsimps [Range_diag];
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   296
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   297
Goal "Range(A Un B) = Range(A) Un 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_Un_eq";
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 Int B) <= Range(A) Int Range(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_Int_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   304
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   305
Goal "Range(A) - Range(B) <= Range(A - B)";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   306
by (Blast_tac 1);
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   307
qed "Range_Diff_subset";
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   308
6005
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   309
Goal "Range (Union S) = (UN A:S. Range A)";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   310
by (Blast_tac 1);
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   311
qed "Range_Union";
45186ec4d8b6 new theorems Domain_Union, Range_Union
paulson
parents: 5998
diff changeset
   312
5811
0867068942e6 new Domain/Range rules
paulson
parents: 5649
diff changeset
   313
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   314
(*** Image of a set under a relation ***)
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   315
8004
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   316
overload_1st_set "Relation.Image";
5335
07fb8999de62 Overloading decl should assist Blast_tac
paulson
parents: 5316
diff changeset
   317
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   318
Goalw [Image_def] "b : r^^A = (? x:A. (x,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_iff";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   321
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   322
Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   323
by (Blast_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   324
qed "Image_singleton";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   325
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   326
Goal "(b : r^^{a}) = ((a,b):r)";
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   327
by (rtac (Image_iff RS trans) 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   328
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   329
qed "Image_singleton_iff";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   330
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   331
AddIffs [Image_singleton_iff];
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   332
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   333
Goalw [Image_def] "[| (a,b): r;  a:A |] ==> b : r^^A";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   334
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   335
qed "ImageI";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   336
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   337
val major::prems = Goalw [Image_def]
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   338
    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P";
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   339
by (rtac (major RS CollectE) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   340
by (Clarify_tac 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   341
by (rtac (hd prems) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   342
by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   343
qed "ImageE";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   344
1985
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   345
AddIs  [ImageI];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   346
AddSEs [ImageE];
84cf16192e03 Tidied many proofs, using AddIffs to let equivalences take
paulson
parents: 1842
diff changeset
   347
8174
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   348
(*This version's more effective when we already have the required "a"*)
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   349
Goal  "[| a:A;  (a,b): r |] ==> b : r^^A";
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   350
by (Blast_tac 1);
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   351
qed "rev_ImageI";
56d9baa2ddb0 new theorem rev_ImageI
paulson
parents: 8004
diff changeset
   352
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   353
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   354
Goal "R^^{} = {}";
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   355
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   356
qed "Image_empty";
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   357
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   358
Addsimps [Image_empty];
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   359
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   360
Goal "Id ^^ A = A";
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   361
by (Blast_tac 1);
5608
a82a038a3e7a id <-> Id
nipkow
parents: 5335
diff changeset
   362
qed "Image_Id";
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   363
5998
b2ecd577b8a3 better version of Image_diag
paulson
parents: 5995
diff changeset
   364
Goal "diag A ^^ B = A Int B";
5995
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   365
by (Blast_tac 1);
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   366
qed "Image_diag";
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   367
450cd1f0270b new theorems about diag
paulson
parents: 5978
diff changeset
   368
Addsimps [Image_Id, Image_diag];
4601
87fc0d44b837 New theorem Image_id
paulson
parents: 4593
diff changeset
   369
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   370
Goal "R ^^ (A Int B) <= R ^^ A Int 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_Int_subset";
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   373
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   374
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   375
by (Blast_tac 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   376
qed "Image_Un";
4593
6fc8f224655f Three new facts about Image
paulson
parents: 4423
diff changeset
   377
8703
816d8f6513be Times -> <*>
nipkow
parents: 8268
diff changeset
   378
Goal "r <= A <*> B ==> r^^C <= B";
7007
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   379
by (rtac subsetI 1);
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   380
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
b46ccfee8e59 qed_goal -> Goal
paulson
parents: 6806
diff changeset
   381
qed "Image_subset";
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff changeset
   382
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   383
(*NOT suitable for rewriting*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4830
diff changeset
   384
Goal "r^^B = (UN y: B. r^^{y})";
4673
59d80bacee62 New theorems; tidied
paulson
parents: 4650
diff changeset
   385
by (Blast_tac 1);
4733
2c984ac036f5 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents: 4673
diff changeset
   386
qed "Image_eq_UN";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   387
7913
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   388
Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)";
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_mono";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   391
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   392
Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   393
by (Blast_tac 1);
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   394
qed "Image_UN";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   395
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   396
(*Converse inclusion fails*)
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   397
Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   398
by (Blast_tac 1);
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   399
qed "Image_INT_subset";
86be2946bb0b new theorems on Image
paulson
parents: 7822
diff changeset
   400
8004
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   401
Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))";
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   402
by (Blast_tac 1);
6273f58ea2c1 Fixed obsolete use of "op ^^"; new lemma
paulson
parents: 7913
diff changeset
   403
qed "Image_subset_eq";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   404
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   405
section "univalent";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   406
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   407
Goalw [univalent_def]
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   408
     "!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
   409
by (assume_tac 1);
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   410
qed "univalentI";
4760
9cdbd5a1d25a added introduction and elimination rules for Univalent
oheimb
parents: 4746
diff changeset
   411
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   412
Goalw [univalent_def]
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   413
     "[| univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 7014
diff changeset
   414
by Auto_tac;
8268
722074b93cdd renamed Univalent to univalent
oheimb
parents: 8265
diff changeset
   415
qed "univalentD";
5231
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   416
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   417
9097
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   418
(** Graphs given by Collect **)
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   419
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   420
Goal "Domain{(x,y). P x y} = {x. EX y. P x y}";
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   421
by Auto_tac; 
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   422
qed "Domain_Collect_split";
5231
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   423
9097
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   424
Goal "Range{(x,y). P x y} = {y. EX x. P x y}";
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   425
by Auto_tac; 
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   426
qed "Range_Collect_split";
5231
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   427
9097
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   428
Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}";
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   429
by Auto_tac; 
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   430
qed "Image_Collect_split";
5231
2a454140ae24 new theorems for partial funcs
paulson
parents: 5148
diff changeset
   431
9097
44cd0f9f8e5b generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
paulson
parents: 8703
diff changeset
   432
Addsimps [Domain_Collect_split, Range_Collect_split, Image_Collect_split];
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   433
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   434
(** Composition of function and relation **)
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   435
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   436
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
   437
by (Fast_tac 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   438
qed "fun_rel_comp_mono";
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   439
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   440
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
   441
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
   442
by (rtac CollectI 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   443
by (rtac allI 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   444
by (etac allE 1);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9113
diff changeset
   445
by (rtac (some_eq_ex RS iffD2) 1);
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   446
by (etac ex1_implies_ex 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   447
by (rtac ext 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   448
by (etac CollectE 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   449
by (REPEAT (etac allE 1));
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9113
diff changeset
   450
by (rtac (some1_equality RS sym) 1);
7014
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   451
by (atac 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   452
by (atac 1);
11ee650edcd2 Added some definitions and theorems needed for the
berghofe
parents: 7007
diff changeset
   453
qed "fun_rel_comp_unique";