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-- |
neuper@42130 | 1 |
theory Functions imports Main begin |
neuper@42130 | 2 |
|
neuper@42130 | 3 |
fun fib :: "nat \<Rightarrow> nat" |
neuper@42130 | 4 |
where |
neuper@42130 | 5 |
"fib 0 = 1" |
neuper@42130 | 6 |
| "fib (Suc 0) = 1" |
neuper@42130 | 7 |
| "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
neuper@42130 | 8 |
|
neuper@42130 | 9 |
thm fib.simps |
neuper@42130 | 10 |
|
neuper@42130 | 11 |
(*"fib (Suc (Suc n))"*) |
neuper@42130 | 12 |
|
neuper@42130 | 13 |
lemma "fib 0 = 1" |
neuper@42130 | 14 |
by simp |
neuper@42130 | 15 |
lemma "fib (Suc 0) = 1" |
neuper@42130 | 16 |
by simp |
neuper@42130 | 17 |
lemma "fib (Suc (Suc (Suc 0))) = (Suc (Suc (Suc 0)))" |
neuper@42130 | 18 |
by simp |
neuper@42130 | 19 |
|
neuper@42130 | 20 |
(*fun sep :: "’a \<Rightarrow> ’a list \<Rightarrow> ’a list" |
neuper@42130 | 21 |
where |
neuper@42130 | 22 |
"sep a (x#y#xs) = x # a # sep a (y # xs)" |
neuper@42130 | 23 |
| "sep a xs |
neuper@42130 | 24 |
= xs"*) |
neuper@42130 | 25 |
|
neuper@42130 | 26 |
|
neuper@42130 | 27 |
end |