# HG changeset patch
# User haftmann
# Date 1333091069 -7200
# Node ID 69cee87927f074ac208539d654993843aa1f9f72
# Parent  06e6f352df1bff3fddc90edfa1b9a88d0e674edb
power on predicate relations

diff -r 06e6f352df1b -r 69cee87927f0 NEWS
--- a/NEWS	Fri Mar 30 00:01:30 2012 +0100
+++ b/NEWS	Fri Mar 30 09:04:29 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
diff -r 06e6f352df1b -r 69cee87927f0 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Mar 30 00:01:30 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Mar 30 09:04:29 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