src/HOL/NumberTheory/Fib.thy
author wenzelm
Tue Oct 03 22:37:16 2000 +0200 (2000-10-03)
changeset 10147 178deaacb244
parent 9944 2a705d1af4dc
child 11049 7eef34adb852
permissions -rw-r--r--
tuned deps;
paulson@9944
     1
(*  Title:      ex/Fib
paulson@9944
     2
    ID:         $Id$
paulson@9944
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9944
     4
    Copyright   1997  University of Cambridge
paulson@9944
     5
paulson@9944
     6
The Fibonacci function.  Demonstrates the use of recdef.
paulson@9944
     7
*)
paulson@9944
     8
wenzelm@10147
     9
Fib = Primes +
paulson@9944
    10
paulson@9944
    11
consts fib  :: "nat => nat"
paulson@9944
    12
recdef fib "less_than"
paulson@9944
    13
  zero    "fib 0 = 0"
paulson@9944
    14
  one     "fib 1 = 1"
paulson@9944
    15
  Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
paulson@9944
    16
paulson@9944
    17
end