# HG changeset patch
# User nipkow
# Date 1569162309 -7200
# Node ID e21c6b677c79bc47b257ac96fc3f54ef2def103a
# Parent  49ae62f849017ceef7ad7da12e8f824487672152
added function

diff -r 49ae62f84901 -r e21c6b677c79 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