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