[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) Î =
datatype ('Ï) step =
| 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)))
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and