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.

Homework 5

This is the task corresponding to homework 5.

Resources

Download Files

Definitions File

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

fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
"sumto f 0 = 0" |
"sumto f (Suc n) = sumto f n + f(Suc n)"


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

definition "\<Phi> \<equiv> (1 + sqrt 5) / 2"
definition "\<Psi> \<equiv> (1 - sqrt 5) / 2"

lemma \<Phi>_square: "\<Phi>^2 = 1+\<Phi>"
  by (simp add: field_simps \<Phi>_def power2_eq_square) 
lemma \<Psi>_square: "\<Psi>^2 = 1+\<Psi>"
  by (simp add: field_simps \<Psi>_def power2_eq_square)

end

Template File

theory Submission
  imports Defs
begin

lemma nth_root_of_plus_1_bound:
  fixes x :: real and n :: nat
  assumes "x\<ge>0" and "n>0" 
  shows "root n (1+x) \<le> 1 + x/n" 
  sorry

lemma binet: "fib n = (\<Phi>^n - \<Psi>^n) / sqrt 5"
proof(induction n rule: fib.induct)
  case 1
  show "(fib 0) = (\<Phi> ^ 0 - \<Psi> ^ 0) / sqrt 5"
    sorry
next
  case 2
  show "fib (Suc 0) = (\<Phi>^(Suc 0) - \<Psi>^(Suc 0)) / sqrt 5"
    sorry
next
  case (3 n)
  assume IH1: "fib n = (\<Phi>^n - \<Psi>^n) / sqrt 5"
  assume IH2: "fib (Suc n) = (\<Phi>^(Suc n) - \<Psi>^(Suc n)) / sqrt 5"
  show "fib (Suc (Suc n)) = (\<Phi>^(Suc (Suc n)) - \<Psi>^(Suc (Suc n))) / sqrt 5"
    sorry
qed

lemma trisecting: 
  "\<exists>xs ys zs . length xs = length as div 3 \<and> length ys = length as div 3 \<and> as = xs @ ys @ zs"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma nth_root_of_plus_1_bound:
  "x\<ge>0 \<Longrightarrow> n>0 \<Longrightarrow> root n (1+x) \<le> 1 + x/n" 
  by (rule Submission.nth_root_of_plus_1_bound)

lemma binet: "fib n = (\<Phi>^n - \<Psi>^n) / sqrt 5"
  by (rule Submission.binet)

lemma trisecting: "\<exists>xs ys zs . length xs = length as div 3 \<and> length ys = length as div 3 \<and> as = xs @ ys @ zs"
  by (rule Submission.trisecting)

end

Terms and Conditions