# HG changeset patch
# User nipkow
# Date 1523183468 -7200
# Node ID 5a4280946a256bf30da3d37804e6411846033f01
# Parent  f13796496e82379b75be180ffb2d3f3cdc01cae0
moved and renamed lemmas

diff -r f13796496e82 -r 5a4280946a25 src/HOL/Data_Structures/AA_Set.thy
--- 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
diff -r f13796496e82 -r 5a4280946a25 src/HOL/Data_Structures/AVL_Set.thy
--- 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
diff -r f13796496e82 -r 5a4280946a25 src/HOL/Data_Structures/Isin2.thy
--- 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
diff -r f13796496e82 -r 5a4280946a25 src/HOL/Data_Structures/RBT_Set.thy
--- 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
diff -r f13796496e82 -r 5a4280946a25 src/HOL/Data_Structures/Set2_BST2_Join.thy
--- 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
diff -r f13796496e82 -r 5a4280946a25 src/HOL/Data_Structures/Tree2.thy
--- 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"