diff -r c5232e6fb10b -r 3fb16bed5d6c src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Tue Sep 24 17:36:14 2019 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Wed Sep 25 17:22:57 2019 +0200
@@ -1,40 +1,29 @@
 theory Tree2
-imports Main
+imports "HOL-Library.Tree"
 begin
 
-datatype ('a,'b) tree =
-  Leaf ("\<langle>\<rangle>") |
-  Node "('a,'b)tree" 'a 'b "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
-
-fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
-"inorder Leaf = []" |
-"inorder (Node l a _ r) = inorder l @ a # inorder r"
+text \<open>This theory provides the basic infrastructure for the type @{typ \<open>('a * 'b) tree\<close>}
+of augmented trees where @{typ 'a} is the key and @{typ 'b} some additional information.\<close>
 
-fun height :: "('a,'b) tree \<Rightarrow> nat" where
-"height Leaf = 0" |
-"height (Node l a _ r) = max (height l) (height r) + 1"
+text \<open>IMPORTANT: Inductions and cases analyses on augmented trees need to use the following
+two rules explicitly. They generate nodes of the form @{term "Node l (a,b) r"}
+rather than @{term "Node l a r"} for trees of type @{typ "'a tree"}.\<close>
 
-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)"
+lemmas tree2_induct = tree.induct[where 'a = "'a * 'b", split_format(complete)]
+
+lemmas tree2_cases = tree.exhaust[where 'a = "'a * 'b", split_format(complete)]
 
-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))"
-
-fun size1 :: "('a,'b) tree \<Rightarrow> nat" where
-"size1 \<langle>\<rangle> = 1" |
-"size1 \<langle>l, _, _, r\<rangle> = size1 l + size1 r"
+fun inorder :: "('a*'b)tree \<Rightarrow> 'a list" where
+"inorder Leaf = []" |
+"inorder (Node l (a,_) r) = inorder l @ a # inorder r"
 
-fun complete :: "('a,'b) tree \<Rightarrow> bool" where
-"complete Leaf = True" |
-"complete (Node l _ _ r) = (complete l \<and> complete r \<and> height l = height r)"
+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)"
 
-lemma size1_size: "size1 t = size t + 1"
-by (induction t) simp_all
-
-lemma size1_ge0[simp]: "0 < size1 t"
-by (simp add: size1_size)
+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 finite_set_tree[simp]: "finite(set_tree t)"
 by(induction t) auto