Exercise 1

Definitions File

theory Defs
  imports "HOL-Data_Structures.Leftist_Heap"
begin

fun rank :: "'a tree \<Rightarrow> nat" where
"rank Leaf = 0" |
"rank (Node l x r) = rank r + 1"

fun ltree_by :: "('a tree \<Rightarrow> nat) \<Rightarrow> 'a tree \<Rightarrow> bool" where
"ltree_by f Leaf = True" |
"ltree_by f (Node l _ r) = (f l \<ge> f r \<and> ltree_by f l \<and> ltree_by f r)"

end

Template File

theory Submission
  imports Defs
begin

lemma ltree_by_rank_iff_mh: "ltree_by rank t \<longleftrightarrow> ltree_by min_height t"
  sorry


end

Check File

theory Check
  imports Submission
begin

lemma ltree_by_rank_iff_mh: "ltree_by rank t \<longleftrightarrow> ltree_by min_height t"
  by (rule Submission.ltree_by_rank_iff_mh)

end