--- 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"
--- 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+
--- 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
--- 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
--- 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>