84 |
84 |
85 val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski); |
85 val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski); |
86 |
86 |
87 (*Reflexivity of rtrancl*) |
87 (*Reflexivity of rtrancl*) |
88 goal Trancl.thy "<a,a> : r^*"; |
88 goal Trancl.thy "<a,a> : r^*"; |
89 br (rtrancl_unfold RS ssubst) 1; |
89 by (rtac (rtrancl_unfold RS ssubst) 1); |
90 by (fast_tac comp_cs 1); |
90 by (fast_tac comp_cs 1); |
91 val rtrancl_refl = result(); |
91 val rtrancl_refl = result(); |
92 |
92 |
93 (*Closure under composition with r*) |
93 (*Closure under composition with r*) |
94 val prems = goal Trancl.thy |
94 val prems = goal Trancl.thy |
95 "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*"; |
95 "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*"; |
96 br (rtrancl_unfold RS ssubst) 1; |
96 by (rtac (rtrancl_unfold RS ssubst) 1); |
97 by (fast_tac (comp_cs addIs prems) 1); |
97 by (fast_tac (comp_cs addIs prems) 1); |
98 val rtrancl_into_rtrancl = result(); |
98 val rtrancl_into_rtrancl = result(); |
99 |
99 |
100 (*rtrancl of r contains r*) |
100 (*rtrancl of r contains r*) |
101 val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*"; |
101 val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*"; |