author | Walther Neuper <neuper@ist.tugraz.at> |
Mon, 16 Sep 2013 12:27:20 +0200 | |
changeset 52106 | 7f3760f39bdc |
parent 52056 | f5d9bceb4dc0 |
permissions | -rw-r--r-- |
1 theory Functions imports Main begin
3 fun fib :: "nat \<Rightarrow> nat"
4 where
5 "fib 0 = 1"
6 | "fib (Suc 0) = 1"
7 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
9 thm fib.simps
11 (*"fib (Suc (Suc n))"*)
13 lemma "fib 0 = 1"
14 by simp
15 lemma "fib (Suc 0) = 1"
16 by simp
17 lemma "fib (Suc (Suc (Suc 0))) = (Suc (Suc (Suc 0)))"
18 by simp
20 (*fun sep :: "’a \<Rightarrow> ’a list \<Rightarrow> ’a list"
21 where
22 "sep a (x#y#xs) = x # a # sep a (y # xs)"
23 | "sep a xs
24 = xs"*)
27 end