# HG changeset patch
# User nipkow
# Date 1605181457 -3600
# Node ID e3ba2578ad9dd69a8865b5bfe9e0cae143a18603
# Parent  4ea19e5dc67e591c7f310baac8643d24c298434d
tuned

diff -r 4ea19e5dc67e -r e3ba2578ad9d src/HOL/Data_Structures/Interval_Tree.thy
--- a/src/HOL/Data_Structures/Interval_Tree.thy	Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Data_Structures/Interval_Tree.thy	Thu Nov 12 12:44:17 2020 +0100
@@ -78,7 +78,7 @@
 
 fun inv_max_hi :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where
 "inv_max_hi Leaf \<longleftrightarrow> True" |
-"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (inv_max_hi l \<and> inv_max_hi r \<and> m = max3 a (max_hi l) (max_hi r))"
+"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (m = max3 a (max_hi l) (max_hi r) \<and> inv_max_hi l \<and> inv_max_hi r)"
 
 lemma max_hi_is_max:
   "inv_max_hi t \<Longrightarrow> a \<in> set_tree t \<Longrightarrow> high a \<le> max_hi t"
diff -r 4ea19e5dc67e -r e3ba2578ad9d src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 12 12:44:17 2020 +0100
@@ -108,7 +108,7 @@
 fun invc :: "'a rbt \<Rightarrow> bool" where
 "invc Leaf = True" |
 "invc (Node l (a,c) r) =
-  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
+  ((c = Red \<longrightarrow> color l = Black \<and> color r = Black) \<and> invc l \<and> invc r)"
 
 text \<open>Weaker version:\<close>
 abbreviation invc2 :: "'a rbt \<Rightarrow> bool" where
@@ -116,7 +116,7 @@
 
 fun invh :: "'a rbt \<Rightarrow> bool" where
 "invh Leaf = True" |
-"invh (Node l (x, c) r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
+"invh (Node l (x, c) r) = (bheight l = bheight r \<and> invh l \<and> invh r)"
 
 lemma invc2I: "invc t \<Longrightarrow> invc2 t"
 by (cases t rule: tree2_cases) simp+
diff -r 4ea19e5dc67e -r e3ba2578ad9d src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Thu Nov 12 12:44:17 2020 +0100
@@ -21,11 +21,11 @@
 
 fun set_tree :: "('a*'b) tree \<Rightarrow> 'a set" where
 "set_tree Leaf = {}" |
-"set_tree (Node l (a,_) r) = Set.insert a (set_tree l \<union> set_tree r)"
+"set_tree (Node l (a,_) r) = {a} \<union> set_tree l \<union> set_tree r"
 
 fun bst :: "('a::linorder*'b) tree \<Rightarrow> bool" where
 "bst Leaf = True" |
-"bst (Node l (a, _) r) = (bst l \<and> bst r \<and> (\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x))"
+"bst (Node l (a, _) r) = ((\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x) \<and> bst l \<and> bst r)"
 
 lemma finite_set_tree[simp]: "finite(set_tree t)"
 by(induction t) auto
diff -r 4ea19e5dc67e -r e3ba2578ad9d src/HOL/Data_Structures/Tree23.thy
--- a/src/HOL/Data_Structures/Tree23.thy	Thu Oct 22 15:18:08 2020 +0200
+++ b/src/HOL/Data_Structures/Tree23.thy	Thu Nov 12 12:44:17 2020 +0100
@@ -36,9 +36,9 @@
 
 fun complete :: "'a tree23 \<Rightarrow> bool" where
 "complete Leaf = True" |
-"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
+"complete (Node2 l _ r) = (height l = height r \<and> complete l & complete r)" |
 "complete (Node3 l _ m _ r) =
-  (complete l & complete m & complete r & height l = height m & height m = height r)"
+  (height l = height m & height m = height r & complete l & complete m & complete r)"
 
 lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
 by (induction t) auto
diff -r 4ea19e5dc67e -r e3ba2578ad9d src/HOL/Library/Tree.thy
--- 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>