FDS Week 5 homework

Definitions File

theory Defs
  imports Main
begin

end

Template File

theory Submission
  imports Defs
begin

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)

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"
proof(induction xs rule: induct_pcpl)
  case 1
  show ?case
    sorry
next
  case (2 x)
  show ?case
    sorry
next
  case (3 y z xs)
  show ?case
    sorry
qed

lemma eq_identiy:
  fixes f :: "nat \<Rightarrow> nat"
  assumes "\<forall>n. f(Suc n) = f(n)^2"
  shows "f(n) = f(0)^(2^n)"
  sorry

end

Check File

theory Check
  imports Submission
begin

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 split_splice)

lemma eq_identiy:
  fixes f :: "nat \<Rightarrow> nat"
  assumes "\<forall>n. f(Suc n) = f(n)^2"
  shows "f(n) = f(0)^(2^n)"
  by(rule eq_identiy[OF assms])

end