[isabelle-dev] recursive datatype measure

[Alexander Krauss]

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