isabelle: src/HOL/ex/Fib.thy@3cf533397c5a (annotated)

3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	1	(* Title: ex/Fib
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	2	ID: $Id$
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	4	Copyright 1997 University of Cambridge
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	5
3494 f7ac2d1e2051 Fixed comments paulson parents: 3375 diff changeset	6	The Fibonacci function. Demonstrates the use of recdef.
3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	7	*)
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	8
6481 dbf2d9b3d6c8 recdef requires theory Recdef; wenzelm parents: 4809 diff changeset	9	Fib = Divides + Primes +
3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	10
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	11	consts fib :: "nat => nat"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	12	recdef fib "less_than"
8658 3cf533397c5a proper naming of fib equations; wenzelm parents: 6481 diff changeset	13	zero "fib 0 = 0"
3cf533397c5a proper naming of fib equations; wenzelm parents: 6481 diff changeset	14	one "fib 1 = 1"
3cf533397c5a proper naming of fib equations; wenzelm parents: 6481 diff changeset	15	Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
3300 4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	16
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	17	end

author	wenzelm
	Sat, 01 Apr 2000 20:22:46 +0200
changeset 8658	3cf533397c5a
parent 6481	dbf2d9b3d6c8
permissions	-rw-r--r--