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
paulson@3300
     1
(*  Title:      ex/Fib
paulson@3300
     2
    ID:         $Id$
paulson@3300
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3300
     4
    Copyright   1997  University of Cambridge
paulson@3300
     5
paulson@3494
     6
The Fibonacci function.  Demonstrates the use of recdef.
paulson@3300
     7
*)
paulson@3300
     8
paulson@3375
     9
Fib = WF_Rel + Divides +
paulson@3300
    10
paulson@3300
    11
consts fib  :: "nat => nat"
paulson@3300
    12
recdef fib "less_than"
paulson@3300
    13
    "fib 0 = 0"
paulson@3300
    14
    "fib 1 = 1"
paulson@3300
    15
    "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
paulson@3300
    16
paulson@3300
    17
end