FDS Week 8 Homework

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