--- a/src/HOL/Data_Structures/AA_Set.thy Sun Apr 08 12:14:00 2018 +0200
+++ b/src/HOL/Data_Structures/AA_Set.thy Sun Apr 08 12:31:08 2018 +0200
@@ -488,7 +488,7 @@
proof (standard, goal_cases)
case 1 show ?case by simp
next
- case 2 thus ?case by(simp add: isin_set)
+ case 2 thus ?case by(simp add: isin_set_inorder)
next
case 3 thus ?case by(simp add: inorder_insert)
next
--- a/src/HOL/Data_Structures/AVL_Set.thy Sun Apr 08 12:14:00 2018 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy Sun Apr 08 12:31:08 2018 +0200
@@ -129,7 +129,7 @@
proof (standard, goal_cases)
case 1 show ?case by simp
next
- case 2 thus ?case by(simp add: isin_set)
+ case 2 thus ?case by(simp add: isin_set_inorder)
next
case 3 thus ?case by(simp add: inorder_insert)
next
--- a/src/HOL/Data_Structures/Isin2.thy Sun Apr 08 12:14:00 2018 +0200
+++ b/src/HOL/Data_Structures/Isin2.thy Sun Apr 08 12:31:08 2018 +0200
@@ -17,7 +17,10 @@
EQ \<Rightarrow> True |
GT \<Rightarrow> isin r x)"
-lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
+lemma isin_set_inorder: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
by (induction t) (auto simp: isin_simps)
+lemma isin_set_tree: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t"
+by(induction t) auto
+
end
--- a/src/HOL/Data_Structures/RBT_Set.thy Sun Apr 08 12:14:00 2018 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sun Apr 08 12:31:08 2018 +0200
@@ -262,7 +262,7 @@
proof (standard, goal_cases)
case 1 show ?case by simp
next
- case 2 thus ?case by(simp add: isin_set)
+ case 2 thus ?case by(simp add: isin_set_inorder)
next
case 3 thus ?case by(simp add: inorder_insert)
next
--- a/src/HOL/Data_Structures/Set2_BST2_Join.thy Sun Apr 08 12:14:00 2018 +0200
+++ b/src/HOL/Data_Structures/Set2_BST2_Join.thy Sun Apr 08 12:31:08 2018 +0200
@@ -21,17 +21,6 @@
Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
and recursion operators on it.\<close>
-fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where
-"set_tree Leaf = {}" |
-"set_tree (Node _ l x r) = Set.insert x (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))"
-
-lemma isin_iff: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t"
-by(induction t) auto
-
locale Set2_BST2_Join =
fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
fixes inv :: "('a,'b) tree \<Rightarrow> bool"
@@ -326,7 +315,7 @@
proof (standard, goal_cases)
case 1 show ?case by (simp)
next
- case 2 thus ?case by(simp add: isin_iff)
+ case 2 thus ?case by(simp add: isin_set_tree)
next
case 3 thus ?case by (simp add: set_tree_insert)
next
--- a/src/HOL/Data_Structures/Tree2.thy Sun Apr 08 12:14:00 2018 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy Sun Apr 08 12:31:08 2018 +0200
@@ -14,6 +14,14 @@
"height Leaf = 0" |
"height (Node _ l a r) = max (height l) (height r) + 1"
+fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where
+"set_tree Leaf = {}" |
+"set_tree (Node _ l x r) = Set.insert x (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))"
+
definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
"size1 t = size t + 1"