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