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 Relation.thy [id_def] "(a,a) : id"; |
12 by (Fast_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 Relation.thy [id_def] |
16 "[| p: id; !!x.[| p = (x,x) |] ==> P \ |
16 "[| p: id; !!x.[| p = (x,x) |] ==> P \ |
17 \ |] ==> P"; |
17 \ |] ==> P"; |
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 Relation.thy [id_def] "(a,b):id = (a=b)"; |
24 by (Fast_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 Relation.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 (Fast_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 Relation.thy [comp_def] |
38 "[| xz : r O s; \ |
38 "[| xz : r O s; \ |
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 Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
58 by (Fast_tac 1); |
58 by (Blast_tac 1); |
59 qed "comp_mono"; |
59 qed "comp_mono"; |
60 |
60 |
61 goal Relation.thy |
61 goal Relation.thy |
62 "!!r s. [| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C"; |
62 "!!r s. [| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C"; |
63 by (Fast_tac 1); |
63 by (Blast_tac 1); |
64 qed "comp_subset_Sigma"; |
64 qed "comp_subset_Sigma"; |
65 |
65 |
66 (** Natural deduction for trans(r) **) |
66 (** Natural deduction for trans(r) **) |
67 |
67 |
68 val prems = goalw Relation.thy [trans_def] |
68 val prems = goalw Relation.thy [trans_def] |
70 by (REPEAT (ares_tac (prems@[allI,impI]) 1)); |
70 by (REPEAT (ares_tac (prems@[allI,impI]) 1)); |
71 qed "transI"; |
71 qed "transI"; |
72 |
72 |
73 goalw Relation.thy [trans_def] |
73 goalw Relation.thy [trans_def] |
74 "!!r. [| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; |
74 "!!r. [| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r"; |
75 by (Fast_tac 1); |
75 by (Blast_tac 1); |
76 qed "transD"; |
76 qed "transD"; |
77 |
77 |
78 (** Natural deduction for converse(r) **) |
78 (** Natural deduction for converse(r) **) |
79 |
79 |
80 goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)"; |
80 goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)"; |
86 goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)"; |
86 goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)"; |
87 by (Simp_tac 1); |
87 by (Simp_tac 1); |
88 qed "converseI"; |
88 qed "converseI"; |
89 |
89 |
90 goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r"; |
90 goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r"; |
91 by (Fast_tac 1); |
91 by (Blast_tac 1); |
92 qed "converseD"; |
92 qed "converseD"; |
93 |
93 |
94 (*More general than converseD, as it "splits" the member of the relation*) |
94 (*More general than converseD, as it "splits" the member of the relation*) |
95 qed_goalw "converseE" Relation.thy [converse_def] |
95 qed_goalw "converseE" Relation.thy [converse_def] |
96 "[| yx : converse(r); \ |
96 "[| yx : converse(r); \ |
102 (assume_tac 1) ]); |
102 (assume_tac 1) ]); |
103 |
103 |
104 AddSEs [converseE]; |
104 AddSEs [converseE]; |
105 |
105 |
106 goalw Relation.thy [converse_def] "converse(converse R) = R"; |
106 goalw Relation.thy [converse_def] "converse(converse R) = R"; |
107 by (Fast_tac 1); |
107 by (Blast_tac 1); |
108 qed "converse_converse"; |
108 qed "converse_converse"; |
109 |
109 |
110 (** Domain **) |
110 (** Domain **) |
111 |
111 |
112 qed_goalw "Domain_iff" Relation.thy [Domain_def] |
112 qed_goalw "Domain_iff" Relation.thy [Domain_def] |
113 "a: Domain(r) = (EX y. (a,y): r)" |
113 "a: Domain(r) = (EX y. (a,y): r)" |
114 (fn _=> [ (Fast_tac 1) ]); |
114 (fn _=> [ (Blast_tac 1) ]); |
115 |
115 |
116 qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)" |
116 qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)" |
117 (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); |
117 (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); |
118 |
118 |
119 qed_goal "DomainE" Relation.thy |
119 qed_goal "DomainE" Relation.thy |
142 |
142 |
143 (*** Image of a set under a relation ***) |
143 (*** Image of a set under a relation ***) |
144 |
144 |
145 qed_goalw "Image_iff" Relation.thy [Image_def] |
145 qed_goalw "Image_iff" Relation.thy [Image_def] |
146 "b : r^^A = (? x:A. (x,b):r)" |
146 "b : r^^A = (? x:A. (x,b):r)" |
147 (fn _ => [ Fast_tac 1 ]); |
147 (fn _ => [ Blast_tac 1 ]); |
148 |
148 |
149 qed_goal "Image_singleton_iff" Relation.thy |
149 qed_goal "Image_singleton_iff" Relation.thy |
150 "(b : r^^{a}) = ((a,b):r)" |
150 "(b : r^^{a}) = ((a,b):r)" |
151 (fn _ => [ rtac (Image_iff RS trans) 1, |
151 (fn _ => [ rtac (Image_iff RS trans) 1, |
152 Fast_tac 1 ]); |
152 Blast_tac 1 ]); |
153 |
153 |
154 qed_goalw "ImageI" Relation.thy [Image_def] |
154 qed_goalw "ImageI" Relation.thy [Image_def] |
155 "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" |
155 "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" |
156 (fn _ => [ (Fast_tac 1)]); |
156 (fn _ => [ (Blast_tac 1)]); |
157 |
157 |
158 qed_goalw "ImageE" Relation.thy [Image_def] |
158 qed_goalw "ImageE" Relation.thy [Image_def] |
159 "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" |
159 "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" |
160 (fn major::prems=> |
160 (fn major::prems=> |
161 [ (rtac (major RS CollectE) 1), |
161 [ (rtac (major RS CollectE) 1), |