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.
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
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
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