6 |
6 |
7 open Relation; |
7 open Relation; |
8 |
8 |
9 (** Identity relation **) |
9 (** Identity relation **) |
10 |
10 |
11 goalw Relation.thy [id_def] "(a,a) : id"; |
11 goalw thy [id_def] "(a,a) : id"; |
12 by (Blast_tac 1); |
12 by (Blast_tac 1); |
13 qed "idI"; |
13 qed "idI"; |
14 |
14 |
15 val major::prems = goalw Relation.thy [id_def] |
15 val major::prems = goalw thy [id_def] |
16 "[| p: id; !!x.[| p = (x,x) |] ==> P \ |
16 "[| p: id; !!x.[| p = (x,x) |] ==> P \ |
17 \ |] ==> P"; |
17 \ |] ==> P"; |
18 by (rtac (major RS CollectE) 1); |
18 by (rtac (major RS CollectE) 1); |
19 by (etac exE 1); |
19 by (etac exE 1); |
20 by (eresolve_tac prems 1); |
20 by (eresolve_tac prems 1); |
21 qed "idE"; |
21 qed "idE"; |
22 |
22 |
23 goalw Relation.thy [id_def] "(a,b):id = (a=b)"; |
23 goalw thy [id_def] "(a,b):id = (a=b)"; |
24 by (Blast_tac 1); |
24 by (Blast_tac 1); |
25 qed "pair_in_id_conv"; |
25 qed "pair_in_id_conv"; |
26 Addsimps [pair_in_id_conv]; |
26 Addsimps [pair_in_id_conv]; |
27 |
27 |
28 |
28 |
29 (** Composition of two relations **) |
29 (** Composition of two relations **) |
30 |
30 |
31 goalw Relation.thy [comp_def] |
31 goalw thy [comp_def] |
32 "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s"; |
32 "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s"; |
33 by (Blast_tac 1); |
33 by (Blast_tac 1); |
34 qed "compI"; |
34 qed "compI"; |
35 |
35 |
36 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) |
36 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) |
37 val prems = goalw Relation.thy [comp_def] |
37 val prems = goalw thy [comp_def] |
38 "[| xz : r O s; \ |
38 "[| xz : r O s; \ |
39 \ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \ |
39 \ !!x y z. [| xz = (x,z); (x,y):s; (y,z):r |] ==> P \ |
40 \ |] ==> P"; |
40 \ |] ==> P"; |
41 by (cut_facts_tac prems 1); |
41 by (cut_facts_tac prems 1); |
42 by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 |
42 by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 |
43 ORELSE ares_tac prems 1)); |
43 ORELSE ares_tac prems 1)); |
44 qed "compE"; |
44 qed "compE"; |
45 |
45 |
46 val prems = goal Relation.thy |
46 val prems = goal thy |
47 "[| (a,c) : r O s; \ |
47 "[| (a,c) : r O s; \ |
48 \ !!y. [| (a,y):s; (y,c):r |] ==> P \ |
48 \ !!y. [| (a,y):s; (y,c):r |] ==> P \ |
49 \ |] ==> P"; |
49 \ |] ==> P"; |
50 by (rtac compE 1); |
50 by (rtac compE 1); |
51 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); |
51 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); |
52 qed "compEpair"; |
52 qed "compEpair"; |
53 |
53 |
54 AddIs [compI, idI]; |
54 AddIs [compI, idI]; |
55 AddSEs [compE, idE]; |
55 AddSEs [compE, idE]; |
56 |
56 |
57 goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
57 goal thy "R O id = R"; |
|
58 by (Fast_tac 1); |
|
59 qed "R_O_id"; |
|
60 |
|
61 goal thy "id O R = R"; |
|
62 by (Fast_tac 1); |
|
63 qed "id_O_R"; |
|
64 |
|
65 Addsimps [R_O_id,id_O_R]; |
|
66 |
|
67 goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
58 by (Blast_tac 1); |
68 by (Blast_tac 1); |
59 qed "comp_mono"; |
69 qed "comp_mono"; |
60 |
70 |
61 goal Relation.thy |
71 goal thy |
62 "!!r s. [| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C"; |
72 "!!r s. [| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C"; |
63 by (Blast_tac 1); |
73 by (Blast_tac 1); |
64 qed "comp_subset_Sigma"; |
74 qed "comp_subset_Sigma"; |
65 |
75 |
66 (** Natural deduction for trans(r) **) |
76 (** Natural deduction for trans(r) **) |
67 |
77 |
68 val prems = goalw Relation.thy [trans_def] |
78 val prems = goalw thy [trans_def] |
69 "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)"; |
79 "(!! x y z. [| (x,y):r; (y,z):r |] ==> (x,z):r) ==> trans(r)"; |
70 by (REPEAT (ares_tac (prems@[allI,impI]) 1)); |
80 by (REPEAT (ares_tac (prems@[allI,impI]) 1)); |
71 qed "transI"; |
81 qed "transI"; |
72 |
82 |
73 goalw Relation.thy [trans_def] |
83 goalw thy [trans_def] |
74 "!!r. [| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; |
84 "!!r. [| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; |
75 by (Blast_tac 1); |
85 by (Blast_tac 1); |
76 qed "transD"; |
86 qed "transD"; |
77 |
87 |
78 (** Natural deduction for r^-1 **) |
88 (** Natural deduction for r^-1 **) |
79 |
89 |
80 goalw Relation.thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)"; |
90 goalw thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)"; |
81 by (Simp_tac 1); |
91 by (Simp_tac 1); |
82 qed "inverse_iff"; |
92 qed "inverse_iff"; |
83 |
93 |
84 AddIffs [inverse_iff]; |
94 AddIffs [inverse_iff]; |
85 |
95 |
86 goalw Relation.thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1"; |
96 goalw thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1"; |
87 by (Simp_tac 1); |
97 by (Simp_tac 1); |
88 qed "inverseI"; |
98 qed "inverseI"; |
89 |
99 |
90 goalw Relation.thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r"; |
100 goalw thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r"; |
91 by (Blast_tac 1); |
101 by (Blast_tac 1); |
92 qed "inverseD"; |
102 qed "inverseD"; |
93 |
103 |
94 (*More general than inverseD, as it "splits" the member of the relation*) |
104 (*More general than inverseD, as it "splits" the member of the relation*) |
95 qed_goalw "inverseE" Relation.thy [inverse_def] |
105 qed_goalw "inverseE" thy [inverse_def] |
96 "[| yx : r^-1; \ |
106 "[| yx : r^-1; \ |
97 \ !!x y. [| yx=(y,x); (x,y):r |] ==> P \ |
107 \ !!x y. [| yx=(y,x); (x,y):r |] ==> P \ |
98 \ |] ==> P" |
108 \ |] ==> P" |
99 (fn [major,minor]=> |
109 (fn [major,minor]=> |
100 [ (rtac (major RS CollectE) 1), |
110 [ (rtac (major RS CollectE) 1), |
101 (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)), |
111 (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)), |
102 (assume_tac 1) ]); |
112 (assume_tac 1) ]); |
103 |
113 |
104 AddSEs [inverseE]; |
114 AddSEs [inverseE]; |
105 |
115 |
106 goalw Relation.thy [inverse_def] "(r^-1)^-1 = r"; |
116 goalw thy [inverse_def] "(r^-1)^-1 = r"; |
107 by (Blast_tac 1); |
117 by (Blast_tac 1); |
108 qed "inverse_inverse"; |
118 qed "inverse_inverse"; |
109 Addsimps [inverse_inverse]; |
119 Addsimps [inverse_inverse]; |
110 |
120 |
111 goal Relation.thy "(r O s)^-1 = s^-1 O r^-1"; |
121 goal thy "(r O s)^-1 = s^-1 O r^-1"; |
112 by (Blast_tac 1); |
122 by (Blast_tac 1); |
113 qed "inverse_comp"; |
123 qed "inverse_comp"; |
114 |
124 |
115 goal Relation.thy "id^-1 = id"; |
125 goal thy "id^-1 = id"; |
116 by (Blast_tac 1); |
126 by (Blast_tac 1); |
117 qed "inverse_id"; |
127 qed "inverse_id"; |
118 Addsimps [inverse_id]; |
128 Addsimps [inverse_id]; |
119 |
129 |
120 (** Domain **) |
130 (** Domain **) |
121 |
131 |
122 qed_goalw "Domain_iff" Relation.thy [Domain_def] |
132 qed_goalw "Domain_iff" thy [Domain_def] |
123 "a: Domain(r) = (EX y. (a,y): r)" |
133 "a: Domain(r) = (EX y. (a,y): r)" |
124 (fn _=> [ (Blast_tac 1) ]); |
134 (fn _=> [ (Blast_tac 1) ]); |
125 |
135 |
126 qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)" |
136 qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)" |
127 (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); |
137 (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); |
128 |
138 |
129 qed_goal "DomainE" Relation.thy |
139 qed_goal "DomainE" thy |
130 "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P" |
140 "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P" |
131 (fn prems=> |
141 (fn prems=> |
132 [ (rtac (Domain_iff RS iffD1 RS exE) 1), |
142 [ (rtac (Domain_iff RS iffD1 RS exE) 1), |
133 (REPEAT (ares_tac prems 1)) ]); |
143 (REPEAT (ares_tac prems 1)) ]); |
134 |
144 |
160 qed "Range_id"; |
170 qed "Range_id"; |
161 Addsimps [Range_id]; |
171 Addsimps [Range_id]; |
162 |
172 |
163 (*** Image of a set under a relation ***) |
173 (*** Image of a set under a relation ***) |
164 |
174 |
165 qed_goalw "Image_iff" Relation.thy [Image_def] |
175 qed_goalw "Image_iff" thy [Image_def] |
166 "b : r^^A = (? x:A. (x,b):r)" |
176 "b : r^^A = (? x:A. (x,b):r)" |
167 (fn _ => [ Blast_tac 1 ]); |
177 (fn _ => [ Blast_tac 1 ]); |
168 |
178 |
169 qed_goal "Image_singleton_iff" Relation.thy |
179 qed_goalw "Image_singleton" thy [Image_def] |
|
180 "r^^{a} = {b. (a,b):r}" |
|
181 (fn _ => [ Blast_tac 1 ]); |
|
182 |
|
183 qed_goal "Image_singleton_iff" thy |
170 "(b : r^^{a}) = ((a,b):r)" |
184 "(b : r^^{a}) = ((a,b):r)" |
171 (fn _ => [ rtac (Image_iff RS trans) 1, |
185 (fn _ => [ rtac (Image_iff RS trans) 1, |
172 Blast_tac 1 ]); |
186 Blast_tac 1 ]); |
173 |
187 |
174 qed_goalw "ImageI" Relation.thy [Image_def] |
188 AddIffs [Image_singleton_iff]; |
|
189 |
|
190 qed_goalw "ImageI" thy [Image_def] |
175 "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" |
191 "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" |
176 (fn _ => [ (Blast_tac 1)]); |
192 (fn _ => [ (Blast_tac 1)]); |
177 |
193 |
178 qed_goalw "ImageE" Relation.thy [Image_def] |
194 qed_goalw "ImageE" thy [Image_def] |
179 "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" |
195 "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" |
180 (fn major::prems=> |
196 (fn major::prems=> |
181 [ (rtac (major RS CollectE) 1), |
197 [ (rtac (major RS CollectE) 1), |
182 (Clarify_tac 1), |
198 (Clarify_tac 1), |
183 (rtac (hd prems) 1), |
199 (rtac (hd prems) 1), |