theory Iterate 
imports Main

begin

consts
  iterate :: "nat \\<Rightarrow> ('a \\<Rightarrow> 'a) \\<Rightarrow> 'a \\<Rightarrow> 'a"

primrec
  "iterate 0 f a = a"
  "iterate (Suc n) f a = f (iterate n f a)"


end