src/HOL/Import/HOL4Compat.thy
changeset 30952 7ab2716dd93b
parent 30660 53e1b1641f09
child 30971 7fbebf75b3ef
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Fri Apr 17 16:41:31 2009 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Apr 20 09:32:07 2009 +0200
     1.3 @@ -202,19 +202,13 @@
     1.4  
     1.5  constdefs
     1.6    FUNPOW :: "('a => 'a) => nat => 'a => 'a"
     1.7 -  "FUNPOW f n == f ^ n"
     1.8 +  "FUNPOW f n == f o^ n"
     1.9  
    1.10 -lemma FUNPOW: "(ALL f x. (f ^ 0) x = x) &
    1.11 -  (ALL f n x. (f ^ Suc n) x = (f ^ n) (f x))"
    1.12 -proof auto
    1.13 -  fix f n x
    1.14 -  have "ALL x. f ((f ^ n) x) = (f ^ n) (f x)"
    1.15 -    by (induct n,auto)
    1.16 -  thus "f ((f ^ n) x) = (f ^ n) (f x)"
    1.17 -    ..
    1.18 -qed
    1.19 +lemma FUNPOW: "(ALL f x. (f o^ 0) x = x) &
    1.20 +  (ALL f n x. (f o^ Suc n) x = (f o^ n) (f x))"
    1.21 +  by (simp add: funpow_swap1)
    1.22  
    1.23 -lemma [hol4rew]: "FUNPOW f n = f ^ n"
    1.24 +lemma [hol4rew]: "FUNPOW f n = f o^ n"
    1.25    by (simp add: FUNPOW_def)
    1.26  
    1.27  lemma ADD: "(!n. (0::nat) + n = n) & (!m n. Suc m + n = Suc (m + n))"
    1.28 @@ -224,7 +218,7 @@
    1.29    by simp
    1.30  
    1.31  lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
    1.32 -  by (simp, arith)
    1.33 +  by (simp) arith
    1.34  
    1.35  lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
    1.36    by (simp add: max_def)