| changeset 25295 | 12985023be5e |
| parent 23743 | 52fbc991039f |
| child 25425 | 9191942c4ead |
--- a/src/HOL/Transitive_Closure.thy Mon Nov 05 22:00:21 2007 +0100 +++ b/src/HOL/Transitive_Closure.thy Mon Nov 05 22:48:37 2007 +0100 @@ -449,6 +449,10 @@ lemmas tranclD = tranclpD [to_set] +lemma tranclD2: + "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" + by (blast elim: tranclE intro: trancl_into_rtrancl) + lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+" by (blast elim: tranclE dest: trancl_into_rtrancl)