isabelle: src/HOL/ex/Fib.thy@4ed64ad7fb42 (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
3375 d9b30c300f1e Now Divides must be the parent paulson parents: 3300 diff changeset	9	Fib = WF_Rel + Divides +
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
	Fri, 17 Oct 1997 11:00:00 +0200
changeset 3912	4ed64ad7fb42
parent 3494	f7ac2d1e2051
child 4809	595f905cc348
permissions	-rw-r--r--