merged

--- a/NEWS	Fri Mar 30 08:44:01 2012 +0200
+++ b/NEWS	Fri Mar 30 09:32:18 2012 +0200
@@ -163,7 +163,8 @@
   mod_mult_distrib2 ~> mult_mod_right
 
 * More default pred/set conversions on a couple of relation operations
-and predicates.  Consolidation of some relation theorems:
+and predicates.  Added powers of predicate relations.
+Consolidation of some relation theorems:
 
   converse_def ~> converse_unfold
   rel_comp_def ~> rel_comp_unfold

--- a/src/HOL/Transitive_Closure.thy	Fri Mar 30 08:44:01 2012 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri Mar 30 09:32:18 2012 +0200
@@ -710,14 +710,24 @@
 
 overloading
   relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
+  relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
 begin
 
 primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
     "relpow 0 R = Id"
   | "relpow (Suc n) R = (R ^^ n) O R"
 
+primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
+    "relpowp 0 R = HOL.eq"
+  | "relpowp (Suc n) R = (R ^^ n) OO R"
+
 end
 
+lemma relpowp_relpow_eq [pred_set_conv]:
+  fixes R :: "'a rel"
+  shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
+  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
+
 text {* for code generation *}
 
 definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where