Homework 5

Definitions File

theory Defs
  imports "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)"


consts num_leafs :: "'a tree \<Rightarrow> nat"


end

Template File

theory Submission
  imports Defs
begin

lemma sum_ident: 
  "sumto (\<lambda>i. i* 2 ^ i) n = n * 2 ^ (n + 1) - (2 ^ (n + 1) - 2)"
  sorry

fun num_leafs :: "'a tree \<Rightarrow> nat"  where
  "num_leafs _ = 0"

lemma auxl:
    assumes IHl: "num_leafs l \<le> 2 ^ height l"
      and IHr: "num_leafs r \<le> 2 ^ height r"
      and lr: "height l \<le> height r"
  shows "num_leafs(Node l x r) \<le> 2 ^ height(Node l x r)"
  sorry

lemma auxr:
    assumes IHl: "num_leafs l \<le> 2 ^ height l"
      and IHr: "num_leafs r \<le> 2 ^ height r"
      and rl: "\<not> height l \<le> height r"
  shows "num_leafs(Node l x r) \<le> 2 ^ height(Node l x r)"
  sorry

theorem num_leafs_est: "num_leafs t \<le> 2^height t"
proof (induction t)
  case Leaf show ?case by auto
next
  case (Node l x r)
  assume IHl: "num_leafs l \<le> 2 ^ height l"  
  assume IHr: "num_leafs r \<le> 2 ^ height r"  
  show "num_leafs \<langle>l, x, r\<rangle> \<le> 2 ^ height \<langle>l, x, r\<rangle>"
    sorry
qed

end

Check File

theory Check
  imports Submission
begin

lemma sum_ident: "sumto (\<lambda>i. i* 2 ^ i) n = n * 2 ^ (n + 1) - (2 ^ (n + 1) - 2)"
  by (rule Submission.sum_ident)

lemma auxl: "(num_leafs l \<le> 2 ^ height l) \<Longrightarrow> (num_leafs r \<le> 2 ^ height r) \<Longrightarrow> (height l \<le> height r) \<Longrightarrow> num_leafs(Node l x r) \<le> 2 ^ height(Node l x r)"
  by (rule Submission.auxl)

lemma auxr: "(num_leafs l \<le> 2 ^ height l) \<Longrightarrow> (num_leafs r \<le> 2 ^ height r) \<Longrightarrow> (\<not> height l \<le> height r) \<Longrightarrow> num_leafs(Node l x r) \<le> 2 ^ height(Node l x r)"
  by (rule Submission.auxr)

theorem num_leafs_est: "num_leafs t \<le> 2^height t"
  by (rule Submission.num_leafs_est)

end