Homework 5

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