|
1 (* Title: HOL/trancl |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For trancl.thy. Theorems about the transitive closure of a relation |
|
7 *) |
|
8 |
|
9 open Trancl; |
|
10 |
|
11 (** Natural deduction for trans(r) **) |
|
12 |
|
13 val prems = goalw Trancl.thy [trans_def] |
|
14 "(!! x y z. [| <x,y>:r; <y,z>:r |] ==> <x,z>:r) ==> trans(r)"; |
|
15 by (REPEAT (ares_tac (prems@[allI,impI]) 1)); |
|
16 val transI = result(); |
|
17 |
|
18 val major::prems = goalw Trancl.thy [trans_def] |
|
19 "[| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r"; |
|
20 by (cut_facts_tac [major] 1); |
|
21 by (fast_tac (HOL_cs addIs prems) 1); |
|
22 val transD = result(); |
|
23 |
|
24 (** Identity relation **) |
|
25 |
|
26 goalw Trancl.thy [id_def] "<a,a> : id"; |
|
27 by (rtac CollectI 1); |
|
28 by (rtac exI 1); |
|
29 by (rtac refl 1); |
|
30 val idI = result(); |
|
31 |
|
32 val major::prems = goalw Trancl.thy [id_def] |
|
33 "[| p: id; !!x.[| p = <x,x> |] ==> P \ |
|
34 \ |] ==> P"; |
|
35 by (rtac (major RS CollectE) 1); |
|
36 by (etac exE 1); |
|
37 by (eresolve_tac prems 1); |
|
38 val idE = result(); |
|
39 |
|
40 (** Composition of two relations **) |
|
41 |
|
42 val prems = goalw Trancl.thy [comp_def] |
|
43 "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s"; |
|
44 by (fast_tac (set_cs addIs prems) 1); |
|
45 val compI = result(); |
|
46 |
|
47 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*) |
|
48 val prems = goalw Trancl.thy [comp_def] |
|
49 "[| xz : r O s; \ |
|
50 \ !!x y z. [| xz = <x,z>; <x,y>:s; <y,z>:r |] ==> P \ |
|
51 \ |] ==> P"; |
|
52 by (cut_facts_tac prems 1); |
|
53 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1)); |
|
54 val compE = result(); |
|
55 |
|
56 val prems = goal Trancl.thy |
|
57 "[| <a,c> : r O s; \ |
|
58 \ !!y. [| <a,y>:s; <y,c>:r |] ==> P \ |
|
59 \ |] ==> P"; |
|
60 by (rtac compE 1); |
|
61 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1)); |
|
62 val compEpair = result(); |
|
63 |
|
64 val comp_cs = set_cs addIs [compI,idI] |
|
65 addSEs [compE,idE,Pair_inject]; |
|
66 |
|
67 val prems = goal Trancl.thy |
|
68 "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; |
|
69 by (cut_facts_tac prems 1); |
|
70 by (fast_tac comp_cs 1); |
|
71 val comp_mono = result(); |
|
72 |
|
73 val prems = goal Trancl.thy |
|
74 "[| s <= Sigma(A,%x.B); r <= Sigma(B,%x.C) |] ==> \ |
|
75 \ (r O s) <= Sigma(A,%x.C)"; |
|
76 by (cut_facts_tac prems 1); |
|
77 by (fast_tac (comp_cs addIs [SigmaI] addSEs [SigmaE2]) 1); |
|
78 val comp_subset_Sigma = result(); |
|
79 |
|
80 |
|
81 (** The relation rtrancl **) |
|
82 |
|
83 goal Trancl.thy "mono(%s. id Un (r O s))"; |
|
84 by (rtac monoI 1); |
|
85 by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1)); |
|
86 val rtrancl_fun_mono = result(); |
|
87 |
|
88 val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski); |
|
89 |
|
90 (*Reflexivity of rtrancl*) |
|
91 goal Trancl.thy "<a,a> : r^*"; |
|
92 by (stac rtrancl_unfold 1); |
|
93 by (fast_tac comp_cs 1); |
|
94 val rtrancl_refl = result(); |
|
95 |
|
96 (*Closure under composition with r*) |
|
97 val prems = goal Trancl.thy |
|
98 "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*"; |
|
99 by (stac rtrancl_unfold 1); |
|
100 by (fast_tac (comp_cs addIs prems) 1); |
|
101 val rtrancl_into_rtrancl = result(); |
|
102 |
|
103 (*rtrancl of r contains r*) |
|
104 val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*"; |
|
105 by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1); |
|
106 by (rtac prem 1); |
|
107 val r_into_rtrancl = result(); |
|
108 |
|
109 (*monotonicity of rtrancl*) |
|
110 goalw Trancl.thy [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*"; |
|
111 by(REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1)); |
|
112 val rtrancl_mono = result(); |
|
113 |
|
114 (** standard induction rule **) |
|
115 |
|
116 val major::prems = goal Trancl.thy |
|
117 "[| <a,b> : r^*; \ |
|
118 \ !!x. P(<x,x>); \ |
|
119 \ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \ |
|
120 \ ==> P(<a,b>)"; |
|
121 by (rtac (major RS (rtrancl_def RS def_induct)) 1); |
|
122 by (rtac rtrancl_fun_mono 1); |
|
123 by (fast_tac (comp_cs addIs prems) 1); |
|
124 val rtrancl_full_induct = result(); |
|
125 |
|
126 (*nice induction rule*) |
|
127 val major::prems = goal Trancl.thy |
|
128 "[| <a::'a,b> : r^*; \ |
|
129 \ P(a); \ |
|
130 \ !!y z.[| <a,y> : r^*; <y,z> : r; P(y) |] ==> P(z) |] \ |
|
131 \ ==> P(b)"; |
|
132 (*by induction on this formula*) |
|
133 by (subgoal_tac "! y. <a::'a,b> = <a,y> --> P(y)" 1); |
|
134 (*now solve first subgoal: this formula is sufficient*) |
|
135 by (fast_tac HOL_cs 1); |
|
136 (*now do the induction*) |
|
137 by (resolve_tac [major RS rtrancl_full_induct] 1); |
|
138 by (fast_tac (comp_cs addIs prems) 1); |
|
139 by (fast_tac (comp_cs addIs prems) 1); |
|
140 val rtrancl_induct = result(); |
|
141 |
|
142 (*transitivity of transitive closure!! -- by induction.*) |
|
143 goal Trancl.thy "trans(r^*)"; |
|
144 by (rtac transI 1); |
|
145 by (res_inst_tac [("b","z")] rtrancl_induct 1); |
|
146 by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1)); |
|
147 val trans_rtrancl = result(); |
|
148 |
|
149 (*elimination of rtrancl -- by induction on a special formula*) |
|
150 val major::prems = goal Trancl.thy |
|
151 "[| <a::'a,b> : r^*; (a = b) ==> P; \ |
|
152 \ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P \ |
|
153 \ |] ==> P"; |
|
154 by (subgoal_tac "a::'a = b | (? y. <a,y> : r^* & <y,b> : r)" 1); |
|
155 by (rtac (major RS rtrancl_induct) 2); |
|
156 by (fast_tac (set_cs addIs prems) 2); |
|
157 by (fast_tac (set_cs addIs prems) 2); |
|
158 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); |
|
159 val rtranclE = result(); |
|
160 |
|
161 |
|
162 (**** The relation trancl ****) |
|
163 |
|
164 (** Conversions between trancl and rtrancl **) |
|
165 |
|
166 val [major] = goalw Trancl.thy [trancl_def] |
|
167 "<a,b> : r^+ ==> <a,b> : r^*"; |
|
168 by (resolve_tac [major RS compEpair] 1); |
|
169 by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1)); |
|
170 val trancl_into_rtrancl = result(); |
|
171 |
|
172 (*r^+ contains r*) |
|
173 val [prem] = goalw Trancl.thy [trancl_def] |
|
174 "[| <a,b> : r |] ==> <a,b> : r^+"; |
|
175 by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1)); |
|
176 val r_into_trancl = result(); |
|
177 |
|
178 (*intro rule by definition: from rtrancl and r*) |
|
179 val prems = goalw Trancl.thy [trancl_def] |
|
180 "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+"; |
|
181 by (REPEAT (resolve_tac ([compI]@prems) 1)); |
|
182 val rtrancl_into_trancl1 = result(); |
|
183 |
|
184 (*intro rule from r and rtrancl*) |
|
185 val prems = goal Trancl.thy |
|
186 "[| <a,b> : r; <b,c> : r^* |] ==> <a,c> : r^+"; |
|
187 by (resolve_tac (prems RL [rtranclE]) 1); |
|
188 by (etac subst 1); |
|
189 by (resolve_tac (prems RL [r_into_trancl]) 1); |
|
190 by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1); |
|
191 by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1)); |
|
192 val rtrancl_into_trancl2 = result(); |
|
193 |
|
194 (*elimination of r^+ -- NOT an induction rule*) |
|
195 val major::prems = goal Trancl.thy |
|
196 "[| <a::'a,b> : r^+; \ |
|
197 \ <a,b> : r ==> P; \ |
|
198 \ !!y.[| <a,y> : r^+; <y,b> : r |] ==> P \ |
|
199 \ |] ==> P"; |
|
200 by (subgoal_tac "<a::'a,b> : r | (? y. <a,y> : r^+ & <y,b> : r)" 1); |
|
201 by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); |
|
202 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); |
|
203 by (etac rtranclE 1); |
|
204 by (fast_tac comp_cs 1); |
|
205 by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1); |
|
206 val tranclE = result(); |
|
207 |
|
208 (*Transitivity of r^+. |
|
209 Proved by unfolding since it uses transitivity of rtrancl. *) |
|
210 goalw Trancl.thy [trancl_def] "trans(r^+)"; |
|
211 by (rtac transI 1); |
|
212 by (REPEAT (etac compEpair 1)); |
|
213 by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1); |
|
214 by (REPEAT (assume_tac 1)); |
|
215 val trans_trancl = result(); |
|
216 |
|
217 val prems = goal Trancl.thy |
|
218 "[| <a,b> : r; <b,c> : r^+ |] ==> <a,c> : r^+"; |
|
219 by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1); |
|
220 by (resolve_tac prems 1); |
|
221 by (resolve_tac prems 1); |
|
222 val trancl_into_trancl2 = result(); |
|
223 |
|
224 |
|
225 val major::prems = goal Trancl.thy |
|
226 "[| <a,b> : r^*; r <= Sigma(A,%x.A) |] ==> a=b | a:A"; |
|
227 by (cut_facts_tac prems 1); |
|
228 by (rtac (major RS rtrancl_induct) 1); |
|
229 by (rtac (refl RS disjI1) 1); |
|
230 by (fast_tac (comp_cs addSEs [SigmaE2]) 1); |
|
231 val trancl_subset_Sigma_lemma = result(); |
|
232 |
|
233 val prems = goalw Trancl.thy [trancl_def] |
|
234 "r <= Sigma(A,%x.A) ==> trancl(r) <= Sigma(A,%x.A)"; |
|
235 by (cut_facts_tac prems 1); |
|
236 by (fast_tac (comp_cs addIs [SigmaI] |
|
237 addSDs [trancl_subset_Sigma_lemma] |
|
238 addSEs [SigmaE2]) 1); |
|
239 val trancl_subset_Sigma = result(); |
|
240 |