Homework 5

Definitions File

theory Defs
  imports Main
begin

definition \<O> :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) set" where 
  "\<O>(g) = {f. \<exists>c>0. \<exists>x\<^sub>0. \<forall>x \<ge> x\<^sub>0. f(x) \<le> c * g(x)}"

lemma induct_pcpl:
  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P zs \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
by induction_schema (pat_completeness, lexicographic_order)




end

Template File

theory Submission
  imports Defs
begin

lemma lin_in_square: "(\<lambda>n. 2*n) \<in> \<O> (\<lambda>n. n^2)"
  unfolding \<O>_def
sorry
qed

lemma square_notin_lin: "(\<lambda>n. n^2) \<notin> \<O> (\<lambda>n. 2*n)"
  sorry

thm splice.simps

lemma split_splice:
  "\<exists>ys zs. xs = splice ys zs \<and> length ys \<ge> (length xs) div 2 \<and> length zs \<ge> (length xs) div 2"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma lin_in_square: "(\<lambda>n. 2*n) \<in> \<O> (\<lambda>n. n^2)"
  by (rule Submission.lin_in_square)

lemma square_notin_lin: "(\<lambda>n. n^2) \<notin> \<O> (\<lambda>n. 2*n)"
  by (rule Submission.square_notin_lin)

lemma split_splice: "\<exists>ys zs. xs = splice ys zs \<and> length ys \<ge> (length xs) div 2 \<and> length zs \<ge> (length xs) div 2"
  by (rule Submission.split_splice)

end