[isabelle] Doing induction on lists "backwards"



Hi, Iâm fairly new to Isabelle/HOL so please bear with me if this is obvious. 

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? I can obviously prove the base case, but the inductive step doesnât match the correct pattern. 

datatype  ('a) Î = 
   state 'a
|   abortState

datatype ('Ï) step = 
   stop
|   pgm 'Ï
|   env 'Ï

function (sequential, domintros) laststate_seq :: "('Ï Ã ('Ï Î step list)) â ('Ï Î)" where 
 "laststate_seq (Ï, []) = state Ï"
| "laststate_seq (Ï, xs) = (case last (xs) of 
                                   pgm Ï' â Ï'|
                                   env Ï' â Ï'|
                                   stop   â (laststate_seq (Ï, butlast (xs)))
                                )"
 apply auto
 by (metis neq_Nil_conv)

lemma laststate_seq_stop: "last t = stop â laststate_seq (Ï, t) = laststate_seq (Ï, (butlast t))"
apply (induct t)
apply (metis butlast.simps(1))
?????

Any help with this would be very much appreciated.

Thanks,
Julian.


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