theory HOARE
imports Hoare Divides NatArith Power List GCD Recdef 

begin 

consts 
  fac     :: "nat => nat"

primrec
  "fac 0 = Suc 0"
  "fac(Suc n) = (Suc n)*fac(n)"


consts 
       sum :: "nat => nat"
       min :: "('a::ord) list => nat => 'a"
       fib2 :: "nat => nat * nat"
       fib :: "nat => nat"

primrec
  "fib2 0 = (0,1)"
  "fib2 (Suc n) = (snd(fib2 n),fst(fib2 n)+snd(fib2 n))"
 
translations
  "fib n" == "fst(fib2 n)"

primrec
  "sum 0 = 0"
  "sum (Suc n) = (Suc n) + (sum n)" 

primrec
  "min t 0 = t!0"
  "min t (Suc n) = (if t!(Suc n) < min t n 
                                      then t!(Suc n) 
                                      else min t n)"
  
end