# HG changeset patch
# User nipkow
# Date 1472798066 -7200
# Node ID e60020520b1501af9ad6cd85389e155d89da1d08
# Parent  f3ad26c4b2d9e3f18c6a36e22d463fe79b05380c
added inorder2

diff -r f3ad26c4b2d9 -r e60020520b15 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Sep 01 21:28:55 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Sep 02 08:34:26 2016 +0200
@@ -269,6 +269,12 @@
 "inorder \<langle>\<rangle> = []" |
 "inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r"
 
+text\<open>A linear version avoiding append:\<close>
+fun inorder2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"inorder2 \<langle>\<rangle> xs = xs" |
+"inorder2 \<langle>l, x, r\<rangle> xs = inorder2 l (x # inorder2 r xs)"
+
+
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
@@ -287,6 +293,9 @@
 lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)"
 by (induction t) auto
 
+lemma inorder2_inorder: "inorder2 t xs = inorder t @ xs"
+by (induction t arbitrary: xs) auto
+
 
 subsection \<open>Binary Search Tree predicate\<close>