moved and renamed lemmas
authornipkow
Sun Apr 08 12:31:08 2018 +0200 (13 months ago)
changeset 679675a4280946a25
parent 67966 f13796496e82
child 67968 a5ad4c015d1c
child 67969 83c8cafdebe8
moved and renamed lemmas
src/HOL/Data_Structures/AA_Set.thy
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/Isin2.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Set2_BST2_Join.thy
src/HOL/Data_Structures/Tree2.thy
     1.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Sun Apr 08 12:14:00 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Sun Apr 08 12:31:08 2018 +0200
     1.3 @@ -488,7 +488,7 @@
     1.4  proof (standard, goal_cases)
     1.5    case 1 show ?case by simp
     1.6  next
     1.7 -  case 2 thus ?case by(simp add: isin_set)
     1.8 +  case 2 thus ?case by(simp add: isin_set_inorder)
     1.9  next
    1.10    case 3 thus ?case by(simp add: inorder_insert)
    1.11  next
     2.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Sun Apr 08 12:14:00 2018 +0200
     2.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Sun Apr 08 12:31:08 2018 +0200
     2.3 @@ -129,7 +129,7 @@
     2.4  proof (standard, goal_cases)
     2.5    case 1 show ?case by simp
     2.6  next
     2.7 -  case 2 thus ?case by(simp add: isin_set)
     2.8 +  case 2 thus ?case by(simp add: isin_set_inorder)
     2.9  next
    2.10    case 3 thus ?case by(simp add: inorder_insert)
    2.11  next
     3.1 --- a/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 12:14:00 2018 +0200
     3.2 +++ b/src/HOL/Data_Structures/Isin2.thy	Sun Apr 08 12:31:08 2018 +0200
     3.3 @@ -17,7 +17,10 @@
     3.4       EQ \<Rightarrow> True |
     3.5       GT \<Rightarrow> isin r x)"
     3.6  
     3.7 -lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
     3.8 +lemma isin_set_inorder: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
     3.9  by (induction t) (auto simp: isin_simps)
    3.10  
    3.11 +lemma isin_set_tree: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t"
    3.12 +by(induction t) auto
    3.13 +
    3.14  end
     4.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sun Apr 08 12:14:00 2018 +0200
     4.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Apr 08 12:31:08 2018 +0200
     4.3 @@ -262,7 +262,7 @@
     4.4  proof (standard, goal_cases)
     4.5    case 1 show ?case by simp
     4.6  next
     4.7 -  case 2 thus ?case by(simp add: isin_set)
     4.8 +  case 2 thus ?case by(simp add: isin_set_inorder)
     4.9  next
    4.10    case 3 thus ?case by(simp add: inorder_insert)
    4.11  next
     5.1 --- a/src/HOL/Data_Structures/Set2_BST2_Join.thy	Sun Apr 08 12:14:00 2018 +0200
     5.2 +++ b/src/HOL/Data_Structures/Set2_BST2_Join.thy	Sun Apr 08 12:31:08 2018 +0200
     5.3 @@ -21,17 +21,6 @@
     5.4  Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
     5.5  and recursion operators on it.\<close>
     5.6  
     5.7 -fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where
     5.8 -"set_tree Leaf = {}" |
     5.9 -"set_tree (Node _ l x r) = Set.insert x (set_tree l \<union> set_tree r)"
    5.10 -
    5.11 -fun bst :: "('a::linorder,'b) tree \<Rightarrow> bool" where
    5.12 -"bst Leaf = True" |
    5.13 -"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))"
    5.14 -
    5.15 -lemma isin_iff: "bst t \<Longrightarrow> isin t x \<longleftrightarrow> x \<in> set_tree t"
    5.16 -by(induction t) auto
    5.17 -
    5.18  locale Set2_BST2_Join =
    5.19  fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
    5.20  fixes inv :: "('a,'b) tree \<Rightarrow> bool"
    5.21 @@ -326,7 +315,7 @@
    5.22  proof (standard, goal_cases)
    5.23    case 1 show ?case by (simp)
    5.24  next
    5.25 -  case 2 thus ?case by(simp add: isin_iff)
    5.26 +  case 2 thus ?case by(simp add: isin_set_tree)
    5.27  next
    5.28    case 3 thus ?case by (simp add: set_tree_insert)
    5.29  next
     6.1 --- a/src/HOL/Data_Structures/Tree2.thy	Sun Apr 08 12:14:00 2018 +0200
     6.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Sun Apr 08 12:31:08 2018 +0200
     6.3 @@ -14,6 +14,14 @@
     6.4  "height Leaf = 0" |
     6.5  "height (Node _ l a r) = max (height l) (height r) + 1"
     6.6  
     6.7 +fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where
     6.8 +"set_tree Leaf = {}" |
     6.9 +"set_tree (Node _ l x r) = Set.insert x (set_tree l \<union> set_tree r)"
    6.10 +
    6.11 +fun bst :: "('a::linorder,'b) tree \<Rightarrow> bool" where
    6.12 +"bst Leaf = True" |
    6.13 +"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))"
    6.14 +
    6.15  definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
    6.16  "size1 t = size t + 1"
    6.17