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



Dear Julian,

if you want to use a different induction schema, you have to provide induct the name of the induction schema you want. For backwards structural induction over lists, there is already the theorem rev_induct. So you might try apply(induct t rule: rev_induct)

Best,
Andreas

On 03/06/15 09:34, Mr Julian Fell wrote:
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.