| 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-- |
| 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 |