equal
deleted
inserted
replaced
1281 |
1281 |
1282 (* ccc *) |
1282 (* ccc *) |
1283 |
1283 |
1284 fun postfixes where |
1284 fun postfixes where |
1285 "postfixes [] = []" | |
1285 "postfixes [] = []" | |
1286 "postfixes (x#xs) = (xs)#postfixes xs" |
1286 "postfixes (x#xs) = xs # postfixes xs" |
1287 |
1287 |
1288 definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)" |
1288 definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)" |
1289 |
1289 |
1290 |
1290 fun upto where |
|
1291 "upto s [] = []" | |
|
1292 "upto s (e # es) = (es @ s) # upto s es" |
|
1293 |
|
1294 value "up_to [s3, s2, s1] [e5, e4, e3, e2, e1] " |
|
1295 value "upto [s3, s2, s1] [e5, e4, e3, e2, e1] " |
|
1296 |
|
1297 lemma "upto s t = up_to s t" |
|
1298 apply(induct t arbitrary: s) |
|
1299 apply(auto simp add: up_to_def) |
|
1300 done |
1291 |
1301 |
1292 |
1302 |
1293 definition "occs' Q tt = length (filter Q (postfixes tt))" |
1303 definition "occs' Q tt = length (filter Q (postfixes tt))" |
1294 |
1304 |
1295 lemma occs'_nil [simp]: "occs' Q [] = 0" |
1305 lemma occs'_nil [simp]: "occs' Q [] = 0" |