--- a/Correctness.thy	Fri May 05 15:03:30 2017 +0100
+++ b/Correctness.thy	Fri May 12 14:55:35 2017 +0100
@@ -1283,11 +1283,21 @@
 
 fun postfixes where 
   "postfixes [] = []" |
-  "postfixes (x#xs) = (xs)#postfixes xs" 
+  "postfixes (x#xs) = xs # postfixes xs" 
 
 definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)"
 
+fun upto where
+  "upto s [] = []" |
+  "upto s (e # es) = (es @ s) # upto s es"
 
+value "up_to [s3, s2, s1] [e5, e4, e3, e2, e1] "
+value "upto [s3, s2, s1] [e5, e4, e3, e2, e1] "
+
+lemma "upto s t = up_to s t"
+apply(induct t arbitrary: s)
+apply(auto simp add: up_to_def)
+done
 
 
 definition "occs' Q tt = length (filter Q (postfixes tt))"