author | wneuper <Walther.Neuper@jku.at> |
Mon, 01 Jan 2024 11:31:16 +0100 | |
changeset 60789 | 8fa678b678e8 |
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