tranclD2 (tranclD at the other end) + trancl_power

--- a/src/HOL/Relation_Power.thy	Mon Nov 05 22:00:21 2007 +0100
+++ b/src/HOL/Relation_Power.thy	Mon Nov 05 22:48:37 2007 +0100
@@ -128,6 +128,22 @@
 lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
   by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
 
+lemma trancl_power:
+  "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)"
+  apply (cases x)
+  apply simp
+  apply (rule iffI)
+   apply (drule tranclD2)
+   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
+   apply (rule_tac x="Suc x" in exI)
+   apply (clarsimp simp: rel_comp_def)
+   apply fastsimp
+  apply clarsimp
+  apply (case_tac n, simp)
+  apply clarsimp
+  apply (drule rel_pow_imp_rtrancl)
+  apply fastsimp
+  done
 
 lemma single_valued_rel_pow:
     "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"

--- 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)