Cookies disclaimer

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