Chris, > function > parse_len :: "prod => nat list => int" where > > "parse_len (PTrm tok) toks = (if ((hd toks) = tok) then 1 else -1)" > | "parse_len (Prod pl) toks = > last (sort (map (%p. foldl (% (len::int) (p, l). > if len = -1 then -1 > else len + parse_len p l) > 0 (zip p (powerlist toks))) > pl))" > by pat_completeness auto > termination > apply (relation "measure (%(p, l). size p)", auto) > apply (rename_tac pll toks pl len p l)
by (auto dest!: set_zip_leftD simp: termination_simp) zip was in the way, and set_zip_leftD is the lemma you need. You can also just do termination by (lexicographic_order dest!: set_zip_leftD) Alex
