--- a/src/HOL/Library/Tree.thy Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Library/Tree.thy Thu Nov 12 12:44:17 2020 +0100
@@ -28,7 +28,7 @@
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
"subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
-"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)"
+"subtrees (\<langle>l, a, r\<rangle>) = {\<langle>l, a, r\<rangle>} \<union> subtrees l \<union> subtrees r"
fun mirror :: "'a tree \<Rightarrow> 'a tree" where
"mirror \<langle>\<rangle> = Leaf" |
@@ -53,7 +53,7 @@
fun complete :: "'a tree \<Rightarrow> bool" where
"complete Leaf = True" |
-"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
+"complete (Node l x r) = (height l = height r \<and> complete l \<and> complete r)"
text \<open>Almost complete:\<close>
definition acomplete :: "'a tree \<Rightarrow> bool" where
@@ -90,7 +90,7 @@
fun bst_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" where
"bst_wrt P \<langle>\<rangle> \<longleftrightarrow> True" |
"bst_wrt P \<langle>l, a, r\<rangle> \<longleftrightarrow>
- bst_wrt P l \<and> bst_wrt P r \<and> (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x)"
+ (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x) \<and> bst_wrt P l \<and> bst_wrt P r"
abbreviation bst :: "('a::linorder) tree \<Rightarrow> bool" where
"bst \<equiv> bst_wrt (<)"
@@ -98,7 +98,7 @@
fun (in linorder) heap :: "'a tree \<Rightarrow> bool" where
"heap Leaf = True" |
"heap (Node l m r) =
- (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
+ ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"
subsection \<open>\<^const>\<open>map_tree\<close>\<close>