--- a/src/HOL/Import/HOL4Compat.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Mon Apr 20 09:32:07 2009 +0200
@@ -202,19 +202,13 @@
constdefs
FUNPOW :: "('a => 'a) => nat => 'a => 'a"
- "FUNPOW f n == f ^ n"
+ "FUNPOW f n == f o^ n"
-lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
- (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
-proof auto
- fix f n x
- have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
- by (induct n,auto)
- thus "f ((f ^ n) x) = (f ^ n) (f x)"
- ..
-qed
+lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
+ (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
+ by (simp add: funpow_swap1)
-lemma [hol4rew]: "FUNPOW f n = f ^ n"
+lemma [hol4rew]: "FUNPOW f n = f o^ n"
by (simp add: FUNPOW_def)
lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
@@ -224,7 +218,7 @@
by simp
lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
- by (simp, arith)
+ by (simp) arith
lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
by (simp add: max_def)