| changeset 45116 | f947eeef6b6f |
| parent 44921 | 58eef4843641 |
| child 45137 | 6e422d180de8 |
--- 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)"