--- a/src/HOL/Library/Tree.thy Fri Jan 20 08:49:06 2017 +0100
+++ b/src/HOL/Library/Tree.thy Fri Jan 20 12:44:44 2017 +0100
@@ -72,6 +72,10 @@
"inorder2 \<langle>\<rangle> xs = xs" |
"inorder2 \<langle>l, x, r\<rangle> xs = inorder2 l (x # inorder2 r xs)"
+fun postorder :: "'a tree \<Rightarrow> 'a list" where
+"postorder \<langle>\<rangle> = []" |
+"postorder \<langle>l, x, r\<rangle> = postorder l @ postorder r @ [x]"
+
text\<open>Binary Search Tree:\<close>
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where
"bst \<langle>\<rangle> \<longleftrightarrow> True" |
@@ -372,18 +376,27 @@
lemma set_preorder[simp]: "set (preorder t) = set_tree t"
by (induction t) auto
+lemma set_postorder[simp]: "set (postorder 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 length_postorder[simp]: "length (postorder 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
+lemma postorder_map: "postorder (map_tree f t) = map f (postorder t)"
+by (induction t) auto
+
lemma inorder2_inorder: "inorder2 t xs = inorder t @ xs"
by (induction t arbitrary: xs) auto