isabelle: src/HOL/ex/Fib.thy@82a5ca6290aa (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
4809 595f905cc348 proving fib(gcd(m,n)) = gcd(fib m, fib n) paulson parents: 3494 diff changeset	9	Fib = WF_Rel + 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"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	13	"fib 0 = 0"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	14	"fib 1 = 1"
4f5ffefa7799 New example of recdef and permutative rewriting paulson parents: diff changeset	15	"fib (Suc(Suc x)) = (fib x + fib (Suc x))"
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	paulson
	Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253	82a5ca6290aa
parent 4809	595f905cc348
child 6481	dbf2d9b3d6c8
permissions	-rw-r--r--