src/HOL/Library/Tree.thy

--- a/src/HOL/Library/Tree.thy	Sun Mar 22 13:10:34 2015 +0100
+++ b/src/HOL/Library/Tree.thy	Mon Mar 23 07:36:27 2015 +0100
@@ -30,6 +30,22 @@
 lemma finite_set_tree[simp]: "finite(set_tree t)"
 by(induction t) auto
 
+lemma size_map_tree[simp]: "size (map_tree f t) = size t"
+by (induction t) auto
+
+lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t"
+by (simp add: size1_def)
+
+
+subsection "The depth"
+
+fun depth :: "'a tree => nat" where
+"depth Leaf = 0" |
+"depth (Node t1 a t2) = Suc (max (depth t1) (depth t2))"
+
+lemma depth_map_tree[simp]: "depth (map_tree f t) = depth t"
+by (induction t) auto
+
 
 subsection "The set of subtrees"
 
@@ -47,7 +63,11 @@
 by (metis Node_notin_subtrees_if)
 
 
-subsection "Inorder list of entries"
+subsection "List of entries"
+
+fun preorder :: "'a tree \<Rightarrow> 'a list" where
+"preorder \<langle>\<rangle> = []" |
+"preorder \<langle>l, x, r\<rangle> = x # preorder l @ preorder r"
 
 fun inorder :: "'a tree \<Rightarrow> 'a list" where
 "inorder \<langle>\<rangle> = []" |
@@ -56,6 +76,21 @@
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
+lemma set_preorder[simp]: "set (preorder t) = set_tree t"
+by (induction t) auto
+
+lemma length_preorder[simp]: "length (preorder t) = size t"
+by (induction t) auto
+
+lemma length_inorder[simp]: "length (inorder t) = size t"
+by (induction t) auto
+
+lemma preorder_map: "preorder (map_tree f t) = map f (preorder t)"
+by (induction t) auto
+
+lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)"
+by (induction t) auto
+
 
 subsection {* Binary Search Tree predicate *}
 
@@ -78,6 +113,7 @@
  apply(simp)
 by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans)
 
+
 subsection "Function @{text mirror}"
 
 fun mirror :: "'a tree \<Rightarrow> 'a tree" where
@@ -93,6 +129,15 @@
 lemma size1_mirror[simp]: "size1(mirror t) = size1 t"
 by (simp add: size1_def)
 
+lemma depth_mirror[simp]: "depth(mirror t) = depth t"
+by (induction t) simp_all
+
+lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
+by (induction t) simp_all
+
+lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)"
+by (induction t) simp_all
+
 lemma mirror_mirror[simp]: "mirror(mirror t) = t"
 by (induction t) simp_all