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 definition "occs' Q tt = length (filter Q (postfixes tt))"

  1293 definition "occs' Q tt = length (filter Q (postfixes tt))"

  1291 

  1294 

  1292 lemma occs'_nil [simp]: "occs' Q [] = 0"

  1295 lemma occs'_nil [simp]: "occs' Q [] = 0"

  1293         by (unfold occs'_def, simp)

  1296         by (unfold occs'_def, simp)

  1294 

  1297