# 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 \ True | GT \ isin r x)" -lemma isin_set: "sorted(inorder t) \ isin t x = (x \ set(inorder t))" +lemma isin_set_inorder: "sorted(inorder t) \ isin t x = (x \ set(inorder t))" by (induction t) (auto simp: isin_simps) +lemma isin_set_tree: "bst t \ isin t x \ x \ 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.\ -fun set_tree :: "('a,'b) tree \ 'a set" where -"set_tree Leaf = {}" | -"set_tree (Node _ l x r) = Set.insert x (set_tree l \ set_tree r)" - -fun bst :: "('a::linorder,'b) tree \ bool" where -"bst Leaf = True" | -"bst (Node _ l a r) = (bst l \ bst r \ (\x \ set_tree l. x < a) \ (\x \ set_tree r. a < x))" - -lemma isin_iff: "bst t \ isin t x \ x \ set_tree t" -by(induction t) auto - locale Set2_BST2_Join = fixes join :: "('a::linorder,'b) tree \ 'a \ ('a,'b) tree \ ('a,'b) tree" fixes inv :: "('a,'b) tree \ 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 \ 'a set" where +"set_tree Leaf = {}" | +"set_tree (Node _ l x r) = Set.insert x (set_tree l \ set_tree r)" + +fun bst :: "('a::linorder,'b) tree \ bool" where +"bst Leaf = True" | +"bst (Node _ l a r) = (bst l \ bst r \ (\x \ set_tree l. x < a) \ (\x \ set_tree r. a < x))" + definition size1 :: "('a,'b) tree \ nat" where "size1 t = size t + 1"