# HG changeset patch
# User paulson
# Date 1087390618 -7200
# Node ID 27decf8d40ffd2299540ec827727122feda099b8
# Parent  47455995693d67ba035cae2ae14522bca98754b1
new fib example

diff -r 47455995693d -r 27decf8d40ff src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Wed Jun 16 14:56:39 2004 +0200
+++ b/src/HOL/ex/Recdefs.thy	Wed Jun 16 14:56:58 2004 +0200
@@ -19,6 +19,16 @@
   "Fact 0 = 1"
   "Fact (Suc x) = Fact x * Suc x"
 
+consts fib :: "int => int"
+recdef fib  "measure nat"
+  eqn:  "fib n = (if n < 1 then 0
+                  else if n=1 then 1
+                  else fib(n - 2) + fib(n - 1))";
+
+lemma "fib 7 = 13"
+by simp
+
+
 consts map2 :: "('a => 'b => 'c) * 'a list * 'b list => 'c list"
 recdef map2  "measure(\<lambda>(f, l1, l2). size l1)"
   "map2 (f, [], [])  = []"