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 by (rtac (rtrancl_unfold RS ssubst) 1); |
89 by (stac rtrancl_unfold 1); |
90 by (fast_tac comp_cs 1); |
90 by (fast_tac comp_cs 1); |
91 qed "rtrancl_refl"; |
91 qed "rtrancl_refl"; |
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 by (rtac (rtrancl_unfold RS ssubst) 1); |
96 by (stac rtrancl_unfold 1); |
97 by (fast_tac (comp_cs addIs prems) 1); |
97 by (fast_tac (comp_cs addIs prems) 1); |
98 qed "rtrancl_into_rtrancl"; |
98 qed "rtrancl_into_rtrancl"; |
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^*"; |