neuper@42130: theory Functions imports Main begin
neuper@42130: 
neuper@42130: fun fib :: "nat \<Rightarrow> nat"
neuper@42130: where
neuper@42130: "fib 0 = 1"
neuper@42130: | "fib (Suc 0) = 1"
neuper@42130: | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
neuper@42130: 
neuper@42130: thm fib.simps
neuper@42130: 
neuper@42130: (*"fib (Suc (Suc n))"*)
neuper@42130: 
neuper@42130: lemma "fib 0 = 1"
neuper@42130: by simp
neuper@42130: lemma "fib (Suc 0) = 1"
neuper@42130: by simp
neuper@42130: lemma "fib (Suc (Suc (Suc 0))) = (Suc (Suc (Suc 0)))"
neuper@42130: by simp
neuper@42130: 
neuper@42130: (*fun sep :: "’a \<Rightarrow> ’a list \<Rightarrow> ’a list"
neuper@42130: where
neuper@42130: "sep a (x#y#xs) = x # a # sep a (y # xs)"
neuper@42130: | "sep a xs
neuper@42130: = xs"*)
neuper@42130: 
neuper@42130: 
neuper@42130: end