# HG changeset patch
# User bulwahn
# Date 1317645793 -7200
# Node ID f947eeef6b6fe02e15461b45e2b7a84d45468826
# Parent  93c1ac6727a3a259db6d47ea44fe032c3402dc4b
adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure

diff -r 93c1ac6727a3 -r f947eeef6b6f src/HOL/Transitive_Closure.thy
--- 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)"