| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 17 Sep 2013 09:50:52 +0200 | |
| changeset 52107 | f8845fc8f38d |
| parent 52056 | src/Doc/isac/chuber/Functions.thy@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