1.1 --- a/NEWS	Fri Mar 30 00:01:30 2012 +0100
     1.2 +++ b/NEWS	Fri Mar 30 09:04:29 2012 +0200
     1.3 @@ -163,7 +163,8 @@
     1.4    mod_mult_distrib2 ~> mult_mod_right
     1.5  
     1.6  * More default pred/set conversions on a couple of relation operations
     1.7 -and predicates.  Consolidation of some relation theorems:
     1.8 +and predicates.  Added powers of predicate relations.
     1.9 +Consolidation of some relation theorems:
    1.10  
    1.11    converse_def ~> converse_unfold
    1.12    rel_comp_def ~> rel_comp_unfold

     2.1 --- a/src/HOL/Transitive_Closure.thy	Fri Mar 30 00:01:30 2012 +0100
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 30 09:04:29 2012 +0200
     2.3 @@ -710,14 +710,24 @@
     2.4  
     2.5  overloading
     2.6    relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
     2.7 +  relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
     2.8  begin
     2.9  
    2.10  primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
    2.11      "relpow 0 R = Id"
    2.12    | "relpow (Suc n) R = (R ^^ n) O R"
    2.13  
    2.14 +primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
    2.15 +    "relpowp 0 R = HOL.eq"
    2.16 +  | "relpowp (Suc n) R = (R ^^ n) OO R"
    2.17 +
    2.18  end
    2.19  
    2.20 +lemma relpowp_relpow_eq [pred_set_conv]:
    2.21 +  fixes R :: "'a rel"
    2.22 +  shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"
    2.23 +  by (induct n) (simp_all add: rel_compp_rel_comp_eq)
    2.24 +
    2.25  text {* for code generation *}
    2.26  
    2.27  definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where