# HG changeset patch
# User nipkow
# Date 1438081254 -7200
# Node ID fd26519b1a6a0d03b1622190d4d604910baf2ca9
# Parent  d7e6c7760db5eab0d615032b5a24a4e78fdbf7eb
depth -> height; removed del_rightmost (too specifi)

diff -r d7e6c7760db5 -r fd26519b1a6a src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Mon Jul 27 23:56:11 2015 +0200
+++ b/src/HOL/Library/Tree.thy	Tue Jul 28 13:00:54 2015 +0200
@@ -40,21 +40,30 @@
 by (simp add: size1_def)
 
 
-subsection "The depth"
+subsection "The Height"
+
+class height = fixes height :: "'a \<Rightarrow> nat"
+
+instantiation tree :: (type)height
+begin
 
-fun depth :: "'a tree => nat" where
-"depth Leaf = 0" |
-"depth (Node t1 a t2) = Suc (max (depth t1) (depth t2))"
+fun height_tree :: "'a tree => nat" where
+"height Leaf = 0" |
+"height (Node t1 a t2) = max (height t1) (height t2) + 1"
 
-lemma depth_map_tree[simp]: "depth (map_tree f t) = depth t"
+instance ..
+
+end
+
+lemma height_map_tree[simp]: "height (map_tree f t) = height t"
 by (induction t) auto
 
 
 subsection "The set of subtrees"
 
 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
-  "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
-  "subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)"
+"subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
+"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)"
 
 lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
 by (induction t)(auto)
@@ -152,7 +161,7 @@
 lemma size1_mirror[simp]: "size1(mirror t) = size1 t"
 by (simp add: size1_def)
 
-lemma depth_mirror[simp]: "depth(mirror t) = depth t"
+lemma height_mirror[simp]: "height(mirror t) = height t"
 by (induction t) simp_all
 
 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
@@ -164,49 +173,4 @@
 lemma mirror_mirror[simp]: "mirror(mirror t) = t"
 by (induction t) simp_all
 
-
-subsection "Deletion of the rightmost entry"
-
-fun del_rightmost :: "'a tree \<Rightarrow> 'a tree * 'a" where
-"del_rightmost \<langle>l, a, \<langle>\<rangle>\<rangle> = (l,a)" |
-"del_rightmost \<langle>l, a, r\<rangle> = (let (r',x) = del_rightmost r in (\<langle>l, a, r'\<rangle>, x))"
-
-lemma del_rightmost_set_tree_if_bst:
-  "\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk>
-  \<Longrightarrow> x \<in> set_tree t \<and> set_tree t' = set_tree t - {x}"
-apply(induction t arbitrary: t' rule: del_rightmost.induct)
-  apply (fastforce simp: ball_Un split: prod.splits)+
-done
-
-lemma del_rightmost_set_tree:
-  "\<lbrakk> del_rightmost t = (t',x);  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> set_tree t = insert x (set_tree t')"
-apply(induction t arbitrary: t' rule: del_rightmost.induct)
-by (auto split: prod.splits) auto
-
-lemma del_rightmost_bst:
-  "\<lbrakk> del_rightmost t = (t',x);  bst t;  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> bst t'"
-proof(induction t arbitrary: t' rule: del_rightmost.induct)
-  case (2 l a rl b rr)
-  let ?r = "Node rl b rr"
-  from "2.prems"(1) obtain r' where 1: "del_rightmost ?r = (r',x)" and [simp]: "t' = Node l a r'"
-    by(simp split: prod.splits)
-  from "2.prems"(2) 1 del_rightmost_set_tree[OF 1] show ?case by(auto)(simp add: "2.IH")
-qed auto
-
-
-lemma del_rightmost_greater: "\<lbrakk> del_rightmost t = (t',x);  bst t;  t \<noteq> \<langle>\<rangle> \<rbrakk>
-  \<Longrightarrow> \<forall>a\<in>set_tree t'. a < x"
-proof(induction t arbitrary: t' rule: del_rightmost.induct)
-  case (2 l a rl b rr)
-  from "2.prems"(1) obtain r'
-  where dm: "del_rightmost (Node rl b rr) = (r',x)" and [simp]: "t' = Node l a r'"
-    by(simp split: prod.splits)
-  show ?case using "2.prems"(2) "2.IH"[OF dm] del_rightmost_set_tree_if_bst[OF dm]
-    by (fastforce simp add: ball_Un)
-qed simp_all
-
-lemma del_rightmost_Max:
-  "\<lbrakk> del_rightmost t = (t',x);  bst t;  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> x = Max(set_tree t)"
-by (metis Max_insert2 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le)
-
 end
diff -r d7e6c7760db5 -r fd26519b1a6a src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Mon Jul 27 23:56:11 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Tue Jul 28 13:00:54 2015 +0200
@@ -35,9 +35,4 @@
 lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
 by (induction t) (simp_all add: ac_simps)
 
-lemma del_rightmost_mset_tree:
-  "\<lbrakk> del_rightmost t = (t',x);  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
-apply(induction t arbitrary: t' rule: del_rightmost.induct)
-by (auto split: prod.splits) (auto simp: ac_simps)
-
 end