| author | wneuper <Walther.Neuper@jku.at> |
| Sun, 31 Dec 2023 09:42:27 +0100 | |
| changeset 60787 | 26037efefd61 |
| parent 52107 | f8845fc8f38d |
| 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