author | paulson |
Mon, 26 Jul 1999 16:29:38 +0200 | |
changeset 7083 | 9663eb2bce05 |
parent 7031 | 972b5f62f476 |
child 7822 | 09aabe6d04b8 |
permissions | -rw-r--r-- |
1465 | 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 | 9 |
Goalw [Id_def] "(a,a) : Id"; |
2891 | 10 |
by (Blast_tac 1); |
5608 | 11 |
qed "IdI"; |
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
12 |
|
5608 | 13 |
val major::prems = Goalw [Id_def] |
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 | 19 |
qed "IdE"; |
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
20 |
|
5608 | 21 |
Goalw [Id_def] "(a,b):Id = (a=b)"; |
2891 | 22 |
by (Blast_tac 1); |
5608 | 23 |
qed "pair_in_Id_conv"; |
24 |
Addsimps [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 |
|
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset
|
66 |
Goal "diag(A) <= A Times A"; |
fa2c2dd74f8c
moved diag (diagonal relation) from Univ to Relation
paulson
parents:
5811
diff
changeset
|
67 |
by (Blast_tac 1); |
5995 | 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 | 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 | 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 | 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 | 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 | 97 |
AddIs [compI, IdI]; |
98 |
AddSEs [compE, IdE]; |
|
1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1694
diff
changeset
|
99 |
|
5608 | 100 |
Goal "R O Id = R"; |
4673 | 101 |
by (Fast_tac 1); |
5608 | 102 |
qed "R_O_Id"; |
4673 | 103 |
|
5608 | 104 |
Goal "Id O R = R"; |
4673 | 105 |
by (Fast_tac 1); |
5608 | 106 |
qed "Id_O_R"; |
4673 | 107 |
|
5608 | 108 |
Addsimps [R_O_Id,Id_O_R]; |
4673 | 109 |
|
5069 | 110 |
Goal "(R O S) O T = R O (S O T)"; |
4830 | 111 |
by (Blast_tac 1); |
112 |
qed "O_assoc"; |
|
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 | 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 |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
118 |
Goal "[| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C"; |
2891 | 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] |
43c081a0858d
new preficates refl, sym [from Integ/Equiv], antisym
paulson
parents:
6005
diff
changeset
|
125 |
"[| r <= A Times A; !! x. x:A ==> (x,x):r |] ==> refl A r"; |
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 | 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 | 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 | 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 | 159 |
qed "converse_iff"; |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
160 |
|
4746 | 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 | 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 | 168 |
by (Blast_tac 1); |
4746 | 169 |
qed "converseD"; |
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
170 |
|
4746 | 171 |
(*More general than converseD, as it "splits" the member of the relation*) |
7031 | 172 |
|
173 |
val [major,minor] = Goalw [converse_def] |
|
3439 | 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 | 176 |
\ |] ==> P"; |
177 |
by (rtac (major RS CollectE) 1); |
|
178 |
by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)); |
|
179 |
by (assume_tac 1); |
|
180 |
qed "converseE"; |
|
4746 | 181 |
AddSEs [converseE]; |
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
182 |
|
5069 | 183 |
Goalw [converse_def] "(r^-1)^-1 = r"; |
2891 | 184 |
by (Blast_tac 1); |
4746 | 185 |
qed "converse_converse"; |
186 |
Addsimps [converse_converse]; |
|
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2891
diff
changeset
|
187 |
|
5069 | 188 |
Goal "(r O s)^-1 = s^-1 O r^-1"; |
4423 | 189 |
by (Blast_tac 1); |
4746 | 190 |
qed "converse_comp"; |
1605 | 191 |
|
5608 | 192 |
Goal "Id^-1 = Id"; |
4644 | 193 |
by (Blast_tac 1); |
5608 | 194 |
qed "converse_Id"; |
195 |
Addsimps [converse_Id]; |
|
4644 | 196 |
|
5995 | 197 |
Goal "(diag A) ^-1 = diag A"; |
198 |
by (Blast_tac 1); |
|
199 |
qed "converse_diag"; |
|
200 |
Addsimps [converse_diag]; |
|
201 |
||
7083 | 202 |
Goalw [refl_def] "refl A r ==> refl A (converse r)"; |
203 |
by (Blast_tac 1); |
|
204 |
qed "refl_converse"; |
|
205 |
||
206 |
Goalw [antisym_def] "antisym (converse r) = antisym r"; |
|
207 |
by (Blast_tac 1); |
|
208 |
qed "antisym_converse"; |
|
209 |
||
210 |
Goalw [trans_def] "trans (converse r) = trans r"; |
|
211 |
by (Blast_tac 1); |
|
212 |
qed "trans_converse"; |
|
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 | 216 |
Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)"; |
217 |
by (Blast_tac 1); |
|
218 |
qed "Domain_iff"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
219 |
|
7007 | 220 |
Goal "(a,b): r ==> a: Domain(r)"; |
221 |
by (etac (exI RS (Domain_iff RS iffD2)) 1) ; |
|
222 |
qed "DomainI"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
223 |
|
7007 | 224 |
val prems= Goal "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P"; |
225 |
by (rtac (Domain_iff RS iffD1 RS exE) 1); |
|
226 |
by (REPEAT (ares_tac prems 1)) ; |
|
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 | 232 |
Goal "Domain Id = UNIV"; |
4644 | 233 |
by (Blast_tac 1); |
5608 | 234 |
qed "Domain_Id"; |
235 |
Addsimps [Domain_Id]; |
|
4644 | 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 | 242 |
Goal "Domain(A Un B) = Domain(A) Un Domain(B)"; |
243 |
by (Blast_tac 1); |
|
244 |
qed "Domain_Un_eq"; |
|
245 |
||
246 |
Goal "Domain(A Int B) <= Domain(A) Int Domain(B)"; |
|
247 |
by (Blast_tac 1); |
|
248 |
qed "Domain_Int_subset"; |
|
249 |
||
250 |
Goal "Domain(A) - Domain(B) <= Domain(A - B)"; |
|
251 |
by (Blast_tac 1); |
|
252 |
qed "Domain_Diff_subset"; |
|
253 |
||
6005 | 254 |
Goal "Domain (Union S) = (UN A:S. Domain A)"; |
255 |
by (Blast_tac 1); |
|
256 |
qed "Domain_Union"; |
|
257 |
||
5811 | 258 |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
259 |
(** Range **) |
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
260 |
|
5811 | 261 |
Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)"; |
262 |
by (Blast_tac 1); |
|
263 |
qed "Range_iff"; |
|
264 |
||
7031 | 265 |
Goalw [Range_def] "(a,b): r ==> b : Range(r)"; |
266 |
by (etac (converseI RS DomainI) 1); |
|
267 |
qed "RangeI"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
268 |
|
7031 | 269 |
val major::prems = Goalw [Range_def] |
270 |
"[| b : Range(r); !!x. (x,b): r ==> P |] ==> P"; |
|
271 |
by (rtac (major RS DomainE) 1); |
|
272 |
by (resolve_tac prems 1); |
|
273 |
by (etac converseD 1) ; |
|
274 |
qed "RangeE"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
275 |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
276 |
AddIs [RangeI]; |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
277 |
AddSEs [RangeE]; |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
278 |
|
5608 | 279 |
Goal "Range Id = UNIV"; |
4644 | 280 |
by (Blast_tac 1); |
5608 | 281 |
qed "Range_Id"; |
282 |
Addsimps [Range_Id]; |
|
4644 | 283 |
|
5995 | 284 |
Goal "Range (diag A) = A"; |
285 |
by Auto_tac; |
|
286 |
qed "Range_diag"; |
|
287 |
Addsimps [Range_diag]; |
|
288 |
||
5811 | 289 |
Goal "Range(A Un B) = Range(A) Un Range(B)"; |
290 |
by (Blast_tac 1); |
|
291 |
qed "Range_Un_eq"; |
|
292 |
||
293 |
Goal "Range(A Int B) <= Range(A) Int Range(B)"; |
|
294 |
by (Blast_tac 1); |
|
295 |
qed "Range_Int_subset"; |
|
296 |
||
297 |
Goal "Range(A) - Range(B) <= Range(A - B)"; |
|
298 |
by (Blast_tac 1); |
|
299 |
qed "Range_Diff_subset"; |
|
300 |
||
6005 | 301 |
Goal "Range (Union S) = (UN A:S. Range A)"; |
302 |
by (Blast_tac 1); |
|
303 |
qed "Range_Union"; |
|
304 |
||
5811 | 305 |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
306 |
(*** Image of a set under a relation ***) |
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
307 |
|
5649 | 308 |
overload_1st_set "Relation.op ^^"; |
5335 | 309 |
|
7031 | 310 |
Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)"; |
311 |
by (Blast_tac 1); |
|
312 |
qed "Image_iff"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
313 |
|
7031 | 314 |
Goalw [Image_def] "r^^{a} = {b. (a,b):r}"; |
315 |
by (Blast_tac 1); |
|
316 |
qed "Image_singleton"; |
|
4673 | 317 |
|
7031 | 318 |
Goal "(b : r^^{a}) = ((a,b):r)"; |
7007 | 319 |
by (rtac (Image_iff RS trans) 1); |
320 |
by (Blast_tac 1); |
|
321 |
qed "Image_singleton_iff"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
322 |
|
4673 | 323 |
AddIffs [Image_singleton_iff]; |
324 |
||
7007 | 325 |
Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r^^A"; |
326 |
by (Blast_tac 1); |
|
327 |
qed "ImageI"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
328 |
|
7031 | 329 |
val major::prems = Goalw [Image_def] |
330 |
"[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"; |
|
331 |
by (rtac (major RS CollectE) 1); |
|
332 |
by (Clarify_tac 1); |
|
333 |
by (rtac (hd prems) 1); |
|
334 |
by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ; |
|
335 |
qed "ImageE"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
336 |
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
337 |
AddIs [ImageI]; |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
338 |
AddSEs [ImageE]; |
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
339 |
|
4593 | 340 |
|
7031 | 341 |
Goal "R^^{} = {}"; |
7007 | 342 |
by (Blast_tac 1); |
343 |
qed "Image_empty"; |
|
4593 | 344 |
|
345 |
Addsimps [Image_empty]; |
|
346 |
||
5608 | 347 |
Goal "Id ^^ A = A"; |
4601 | 348 |
by (Blast_tac 1); |
5608 | 349 |
qed "Image_Id"; |
4601 | 350 |
|
5998 | 351 |
Goal "diag A ^^ B = A Int B"; |
5995 | 352 |
by (Blast_tac 1); |
353 |
qed "Image_diag"; |
|
354 |
||
355 |
Addsimps [Image_Id, Image_diag]; |
|
4601 | 356 |
|
7007 | 357 |
Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B"; |
358 |
by (Blast_tac 1); |
|
359 |
qed "Image_Int_subset"; |
|
4593 | 360 |
|
7007 | 361 |
Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B"; |
362 |
by (Blast_tac 1); |
|
363 |
qed "Image_Un"; |
|
4593 | 364 |
|
7007 | 365 |
Goal "r <= A Times B ==> r^^C <= B"; |
366 |
by (rtac subsetI 1); |
|
367 |
by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ; |
|
368 |
qed "Image_subset"; |
|
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
369 |
|
4733
2c984ac036f5
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents:
4673
diff
changeset
|
370 |
(*NOT suitable for rewriting*) |
5069 | 371 |
Goal "r^^B = (UN y: B. r^^{y})"; |
4673 | 372 |
by (Blast_tac 1); |
4733
2c984ac036f5
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
paulson
parents:
4673
diff
changeset
|
373 |
qed "Image_eq_UN"; |
4760
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset
|
374 |
|
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset
|
375 |
|
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset
|
376 |
section "Univalent"; |
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset
|
377 |
|
7031 | 378 |
Goalw [Univalent_def] |
379 |
"!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r"; |
|
380 |
by (assume_tac 1); |
|
381 |
qed "UnivalentI"; |
|
4760
9cdbd5a1d25a
added introduction and elimination rules for Univalent
oheimb
parents:
4746
diff
changeset
|
382 |
|
7031 | 383 |
Goalw [Univalent_def] |
384 |
"[| Univalent r; (x,y):r; (x,z):r|] ==> y=z"; |
|
385 |
by Auto_tac; |
|
386 |
qed "UnivalentD"; |
|
5231 | 387 |
|
388 |
||
389 |
(** Graphs of partial functions **) |
|
390 |
||
391 |
Goal "Domain{(x,y). y = f x & P x} = {x. P x}"; |
|
392 |
by (Blast_tac 1); |
|
393 |
qed "Domain_partial_func"; |
|
394 |
||
395 |
Goal "Range{(x,y). y = f x & P x} = f``{x. P x}"; |
|
396 |
by (Blast_tac 1); |
|
397 |
qed "Range_partial_func"; |
|
398 |
||
7014
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
399 |
|
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
400 |
(** Composition of function and relation **) |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
401 |
|
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
402 |
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
|
403 |
by (Fast_tac 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
404 |
qed "fun_rel_comp_mono"; |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
405 |
|
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
406 |
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
|
407 |
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
|
408 |
by (rtac CollectI 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
409 |
by (rtac allI 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
410 |
by (etac allE 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
411 |
by (rtac (select_eq_Ex RS iffD2) 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
412 |
by (etac ex1_implies_ex 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
413 |
by (rtac ext 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
414 |
by (etac CollectE 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
415 |
by (REPEAT (etac allE 1)); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
416 |
by (rtac (select1_equality RS sym) 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
417 |
by (atac 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
418 |
by (atac 1); |
11ee650edcd2
Added some definitions and theorems needed for the
berghofe
parents:
7007
diff
changeset
|
419 |
qed "fun_rel_comp_unique"; |