30 by (fast_tac (rel_cs addIs prems) 1); |
30 by (fast_tac (rel_cs addIs prems) 1); |
31 qed "rtrancl_into_rtrancl"; |
31 qed "rtrancl_into_rtrancl"; |
32 |
32 |
33 (*rtrancl of r contains r*) |
33 (*rtrancl of r contains r*) |
34 goal Trancl.thy "!!p. p : r ==> p : r^*"; |
34 goal Trancl.thy "!!p. p : r ==> p : r^*"; |
35 by(split_all_tac 1); |
35 by (split_all_tac 1); |
36 by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1); |
36 by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1); |
37 qed "r_into_rtrancl"; |
37 qed "r_into_rtrancl"; |
38 |
38 |
39 (*monotonicity of rtrancl*) |
39 (*monotonicity of rtrancl*) |
40 goalw Trancl.thy [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*"; |
40 goalw Trancl.thy [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*"; |
41 by(REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1)); |
41 by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1)); |
42 qed "rtrancl_mono"; |
42 qed "rtrancl_mono"; |
43 |
43 |
44 (** standard induction rule **) |
44 (** standard induction rule **) |
45 |
45 |
46 val major::prems = goal Trancl.thy |
46 val major::prems = goal Trancl.thy |
69 qed "rtrancl_induct"; |
69 qed "rtrancl_induct"; |
70 |
70 |
71 (*transitivity of transitive closure!! -- by induction.*) |
71 (*transitivity of transitive closure!! -- by induction.*) |
72 goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*"; |
72 goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*"; |
73 by (eres_inst_tac [("b","c")] rtrancl_induct 1); |
73 by (eres_inst_tac [("b","c")] rtrancl_induct 1); |
74 by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl]))); |
74 by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl]))); |
75 qed "rtrancl_trans"; |
75 qed "rtrancl_trans"; |
76 |
76 |
77 (*elimination of rtrancl -- by induction on a special formula*) |
77 (*elimination of rtrancl -- by induction on a special formula*) |
78 val major::prems = goal Trancl.thy |
78 val major::prems = goal Trancl.thy |
79 "[| (a::'a,b) : r^*; (a = b) ==> P; \ |
79 "[| (a::'a,b) : r^*; (a = b) ==> P; \ |
85 by (fast_tac (set_cs addIs prems) 2); |
85 by (fast_tac (set_cs addIs prems) 2); |
86 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); |
86 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); |
87 qed "rtranclE"; |
87 qed "rtranclE"; |
88 |
88 |
89 goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*"; |
89 goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*"; |
90 be rtrancl_induct 1; |
90 by (etac rtrancl_induct 1); |
91 by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1); |
91 by (fast_tac (HOL_cs addIs [r_into_rtrancl]) 1); |
92 by(fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1); |
92 by (fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1); |
93 val lemma = result(); |
93 val lemma = result(); |
94 |
94 |
95 goal Trancl.thy "!!R. [| (x,y) : R; (y,z) : R^* |] ==> (x,z) : R^*"; |
95 goal Trancl.thy "!!R. [| (x,y) : R; (y,z) : R^* |] ==> (x,z) : R^*"; |
96 by(fast_tac (HOL_cs addDs [lemma]) 1); |
96 by (fast_tac (HOL_cs addDs [lemma]) 1); |
97 qed "rtrancl_into_rtrancl2"; |
97 qed "rtrancl_into_rtrancl2"; |
98 |
98 |
99 |
99 |
100 (**** The relation trancl ****) |
100 (**** The relation trancl ****) |
101 |
101 |
161 |
161 |
162 (** More about r^* **) |
162 (** More about r^* **) |
163 |
163 |
164 goal Trancl.thy "(r^*)^* = r^*"; |
164 goal Trancl.thy "(r^*)^* = r^*"; |
165 by (rtac set_ext 1); |
165 by (rtac set_ext 1); |
166 by(res_inst_tac [("p","x")] PairE 1); |
166 by (res_inst_tac [("p","x")] PairE 1); |
167 by(hyp_subst_tac 1); |
167 by (hyp_subst_tac 1); |
168 by (rtac iffI 1); |
168 by (rtac iffI 1); |
169 by (etac rtrancl_induct 1); |
169 by (etac rtrancl_induct 1); |
170 by (rtac rtrancl_refl 1); |
170 by (rtac rtrancl_refl 1); |
171 by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1); |
171 by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1); |
172 by (etac r_into_rtrancl 1); |
172 by (etac r_into_rtrancl 1); |
173 qed "rtrancl_idemp"; |
173 qed "rtrancl_idemp"; |
174 Addsimps [rtrancl_idemp]; |
174 Addsimps [rtrancl_idemp]; |
175 |
175 |
176 goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*"; |
176 goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*"; |
177 by (dtac rtrancl_mono 1); |
177 by (dtac rtrancl_mono 1); |
178 by (dtac rtrancl_mono 1); |
178 by (dtac rtrancl_mono 1); |
179 by(Asm_full_simp_tac 1); |
179 by (Asm_full_simp_tac 1); |
180 by(fast_tac eq_cs 1); |
180 by (fast_tac eq_cs 1); |
181 qed "rtrancl_subset"; |
181 qed "rtrancl_subset"; |
182 |
182 |
183 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*"; |
183 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*"; |
184 by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl, |
184 by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl, |
185 rtrancl_mono RS subsetD]) 1); |
185 rtrancl_mono RS subsetD]) 1); |
186 qed "trancl_Un_trancl"; |
186 qed "trancl_Un_trancl"; |
187 |
187 |
188 goal Trancl.thy "(R^=)^* = R^*"; |
188 goal Trancl.thy "(R^=)^* = R^*"; |
189 by(fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1); |
189 by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1); |
190 qed "rtrancl_reflcl"; |
190 qed "rtrancl_reflcl"; |
191 Addsimps [rtrancl_reflcl]; |
191 Addsimps [rtrancl_reflcl]; |
192 |
192 |
193 goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)"; |
193 goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)"; |
194 by (rtac converseI 1); |
194 by (rtac converseI 1); |
195 by (etac rtrancl_induct 1); |
195 by (etac rtrancl_induct 1); |
196 by (rtac rtrancl_refl 1); |
196 by (rtac rtrancl_refl 1); |
197 by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1); |
197 by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1); |
198 qed "rtrancl_converseD"; |
198 qed "rtrancl_converseD"; |
199 |
199 |
200 goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*"; |
200 goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*"; |
201 by (dtac converseD 1); |
201 by (dtac converseD 1); |
202 by (etac rtrancl_induct 1); |
202 by (etac rtrancl_induct 1); |
203 by (rtac rtrancl_refl 1); |
203 by (rtac rtrancl_refl 1); |
204 by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1); |
204 by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1); |
205 qed "rtrancl_converseI"; |
205 qed "rtrancl_converseI"; |
206 |
206 |
207 goal Trancl.thy "(converse r)^* = converse(r^*)"; |
207 goal Trancl.thy "(converse r)^* = converse(r^*)"; |
208 by(safe_tac (rel_eq_cs addSIs [rtrancl_converseI])); |
208 by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI])); |
209 by(res_inst_tac [("p","x")] PairE 1); |
209 by (res_inst_tac [("p","x")] PairE 1); |
210 by(hyp_subst_tac 1); |
210 by (hyp_subst_tac 1); |
211 by (etac rtrancl_converseD 1); |
211 by (etac rtrancl_converseD 1); |
212 qed "rtrancl_converse"; |
212 qed "rtrancl_converse"; |
213 |
213 |
214 |
214 |
215 val major::prems = goal Trancl.thy |
215 val major::prems = goal Trancl.thy |