###### Cookies disclaimer

Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# FDS Week 8 Homework

Week 8 homework.

## Resources

Download Files

### Definitions File

```theory Defs
imports Complex_Main "HOL-Library.Tree"
begin

fun fib :: "nat \<Rightarrow> nat" where
fib0: "fib 0 = 0"
| fib1: "fib (Suc 0) = 1"
| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"

lemma f_alt_induct [consumes 1, case_names 1 2 rec]:
assumes "n > 0"
and "P (Suc 0)" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))"
shows   "P n"
using assms(1)
proof (induction n rule: fib.induct)
case (3 n)
thus ?case using assms by (cases n) (auto simp: eval_nat_numeral)
qed (auto simp: \<open>P (Suc 0)\<close> \<open>P 2\<close>)

end```

### Template File

```theory Template
imports Defs
begin

fun avl :: "'a tree \<Rightarrow> bool" where
"avl _ = undefined"

lemma fib_lowerbound: "n > 0 \<Longrightarrow> real (fib n) \<ge> 1.5 ^ n / 3"
sorry

lemma avl_two_bound: "avl t \<Longrightarrow> height t = n \<Longrightarrow> 2 ^ (n div 2) \<le> size1 t"
sorry

end```

### Check File

```theory Check
imports Template
begin

lemma fib_lowerbound: "n > 0 \<Longrightarrow> real (Defs.fib n) \<ge> 1.5 ^ n / 3"
by(rule fib_lowerbound)

lemma avl_two_bound: "avl t \<Longrightarrow> height t = n \<Longrightarrow> 2 ^ (n div 2) \<le> size1 t"
by(rule avl_two_bound)

end```

Terms and Conditions