Re: [isabelle] Doing induction on lists "backwards"



Hi Julian,

> Is there any way to use an inductive method to prove 
> laststate_seq_stop despite it being defined going backwards over the 
> list, rather than forwards as per the list definition?

this occurs from time to time. I haven't tried out your concrete
example, but there's a rule which could work for your case:
'rev_induct'. You can use it like this:

  apply (induction t rule: rev_induct)

Hope that helps.

Cheers
Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.