equal
deleted
inserted
replaced
164 |
164 |
165 (*transitivity of transitive closure!! -- by induction.*) |
165 (*transitivity of transitive closure!! -- by induction.*) |
166 lemma trans_rtrancl: "trans(r^*)" |
166 lemma trans_rtrancl: "trans(r^*)" |
167 apply (unfold trans_def) |
167 apply (unfold trans_def) |
168 apply (intro allI impI) |
168 apply (intro allI impI) |
169 apply (erule_tac b = "z" in rtrancl_induct, assumption) |
169 apply (erule_tac b = z in rtrancl_induct, assumption) |
170 apply (blast intro: rtrancl_into_rtrancl) |
170 apply (blast intro: rtrancl_into_rtrancl) |
171 done |
171 done |
172 |
172 |
173 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] |
173 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] |
174 |
174 |