# HG changeset patch
# User bulwahn
# Date 1327928123 -3600
# Node ID 5cb81e3fa79927f404ed40d366572324b8a304be
# Parent  9bc43dc49d0a4566583a603c8252294925096c28
adding code generation for relpow by copying the ideas for code generation of funpow

diff -r 9bc43dc49d0a -r 5cb81e3fa799 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Jan 30 13:55:22 2012 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Jan 30 13:55:23 2012 +0100
@@ -718,6 +718,18 @@
 
 end
 
+text {* for code generation *}
+
+definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
+  relpow_code_def [code_abbrev]: "relpow = compow"
+
+lemma [code]:
+  "relpow (Suc n) R = (relpow n R) O R"
+  "relpow 0 R = Id"
+  by (simp_all add: relpow_code_def)
+
+hide_const (open) relpow
+
 lemma rel_pow_1 [simp]:
   fixes R :: "('a \<times> 'a) set"
   shows "R ^^ 1 = R"