Homework 8_1

Definitions File

theory Defs
  imports Complex_Main "HOL-Data_Structures.Tree23_Set"
begin

lemma height_bound_upper: "complete t \<Longrightarrow> height t \<le> log 2 (size t + 1)"
  using ht_sz_if_complete le_log2_of_power by blast

lemma height_bound_lower_aux:
  assumes "complete t"
  shows "size t + 1 \<le> 3^(height t)"
  using assms
  by (induction t) auto

lemma height_bound_lower: assumes "complete t"
   shows "log 3 (size t + 1) \<le> height t"
proof -
  from log_le_cancel_iff[of 3 "size t + 1" "3^height t"]
    and height_bound_lower_aux[OF assms]
  have "log 3 (size t + 1) \<le> log 3 (3 ^ height t)"
    using of_nat_mono
    by fastforce
  also have "\<dots> = height t"
    by (simp add: log_nat_power)
  finally show ?thesis .
qed


consts num_leaves :: "'a' tree23 \<Rightarrow> nat"

consts is_2_tree :: "'a tree23 \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

fun num_leaves :: "'a tree23 \<Rightarrow> nat"  where
  "num_leaves _ = undefined"

fun is_2_tree :: "'a tree23 \<Rightarrow> bool"  where
  "is_2_tree _ = undefined"

theorem complete_2_tree_height: "complete t \<Longrightarrow> is_2_tree t \<longleftrightarrow> num_leaves t = 2^height t"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem complete_2_tree_height: "complete t \<Longrightarrow> is_2_tree t \<longleftrightarrow> num_leaves t = 2^height t"
  by (rule Submission.complete_2_tree_height)

end