src/HOL/ex/Fib.thy
author paulson
Thu May 22 15:11:23 1997 +0200 (1997-05-22)
changeset 3300 4f5ffefa7799
child 3375 d9b30c300f1e
permissions -rw-r--r--
New example of recdef and permutative rewriting
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@3300
     6
Fibonacci numbers and other simple examples of recursive definitions
paulson@3300
     7
	(the TFL package)
paulson@3300
     8
*)
paulson@3300
     9
paulson@3300
    10
Fib = WF_Rel +
paulson@3300
    11
paulson@3300
    12
consts fib  :: "nat => nat"
paulson@3300
    13
recdef fib "less_than"
paulson@3300
    14
    "fib 0 = 0"
paulson@3300
    15
    "fib 1 = 1"
paulson@3300
    16
    "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
paulson@3300
    17
paulson@3300
    18
end