equal
deleted
inserted
replaced
|
1 theory Functions imports Main begin |
|
2 |
|
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)" |
|
8 |
|
9 thm fib.simps |
|
10 |
|
11 (*"fib (Suc (Suc n))"*) |
|
12 |
|
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 |
|
19 |
|
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"*) |
|
25 |
|
26 |
|
27 end |