src/HOL/Data_Structures/Tree2.thy

--- a/src/HOL/Data_Structures/Tree2.thy	Thu Sep 19 20:27:40 2019 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Sun Sep 22 16:25:09 2019 +0200
@@ -26,6 +26,10 @@
 "size1 \<langle>\<rangle> = 1" |
 "size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r"
 
+fun complete :: "('a,'b) tree \<Rightarrow> bool" where
+"complete Leaf = True" |
+"complete (Node l _ _ r) = (complete l \<and> complete r \<and> height l = height r)"
+
 lemma size1_size: "size1 t = size t + 1"
 by (induction t) simp_all