src/HOL/ex/Fib.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 3494 f7ac2d1e2051
child 4809 595f905cc348
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      ex/Fib
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 The Fibonacci function.  Demonstrates the use of recdef.
     7 *)
     8 
     9 Fib = WF_Rel + Divides +
    10 
    11 consts fib  :: "nat => nat"
    12 recdef fib "less_than"
    13     "fib 0 = 0"
    14     "fib 1 = 1"
    15     "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
    16 
    17 end