--- a/src/HOL/Relation_Power.thy Wed Aug 04 19:11:02 2004 +0200
+++ b/src/HOL/Relation_Power.thy Wed Aug 04 19:12:15 2004 +0200
@@ -12,10 +12,10 @@
Examples: range(f^n) = A and Range(R^n) = B need constraints.
*)
-Relation_Power = Nat +
+theory Relation_Power = Nat:
instance
- set :: (type) power (* only ('a * 'a) set should be in power! *)
+ set :: (type) power .. (* only ('a * 'a) set should be in power! *)
primrec (relpow)
"R^0 = Id"
@@ -23,10 +23,13 @@
instance
- fun :: (type, type) power (* only 'a => 'a should be in power! *)
+ fun :: (type, type) power .. (* only 'a => 'a should be in power! *)
primrec (funpow)
"f^0 = id"
"f^(Suc n) = f o (f^n)"
+lemma funpow_add: "f ^ (m+n) = f^m o f^n"
+by(induct m) simp_all
+
end