--- 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
--- 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