adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure

--- a/src/HOL/Transitive_Closure.thy	Mon Oct 03 14:43:12 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Oct 03 14:43:13 2011 +0200
@@ -775,6 +775,10 @@
 lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
 by (induct n) (simp, simp add: O_assoc [symmetric])
 
+lemma rel_pow_empty:
+  "0 < n ==> ({} :: 'a * 'a => bool) ^^ n = {}"
+by (cases n) auto
+
 lemma rtrancl_imp_UN_rel_pow:
   assumes "p \<in> R^*"
   shows "p \<in> (\<Union>n. R ^^ n)"