Homework 8

Definitions File

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

fun size1 :: "'a tree23 \<Rightarrow> nat" where
  "size1 \<langle>\<rangle> = 1"
| "size1 \<langle>l,_,r\<rangle> = size1 l + size1 r"
| "size1 \<langle>l,_,m,_,r\<rangle> = size1 l + size1 m + size1 r"

fun is_3_tree :: "'a tree23 \<Rightarrow> bool" where
  "is_3_tree \<langle>\<rangle> = True"
| "is_3_tree \<langle>l,_,m,_,r\<rangle> = (is_3_tree l \<and> is_3_tree m \<and> is_3_tree r)"  
| "is_3_tree _ = False"  

type_synonym bv = "bool list"

definition bv_set :: "bv \<Rightarrow> nat set"
  where "bv_set l = { i. i<length l \<and> l!i }"



end

Template File

theory Submission
  imports Defs
begin

theorem complete_3_tree_height: "complete t \<Longrightarrow> is_3_tree t \<longleftrightarrow> size1 t = 3^height t"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem complete_3_tree_height: "complete t \<Longrightarrow> is_3_tree t \<longleftrightarrow> size1 t = 3^height t"
  by (rule Submission.complete_3_tree_height)

end