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

```Consider:

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)

*** Prove termination of your function ***
termination
apply (relation "{} <*lex*> measure length")
by auto

*** Prove a usable simplification rule ***
lemma [simp]: "xs â[] â laststate_seq (Ï, xs) = (case last (xs) of
pgm Ï' â Ï'|
env Ï' â Ï'|
stop   â (laststate_seq (Ï, butlast
(xs)))
)"
apply (cases xs) apply auto done

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

*** And your lemma is straightforward ***
apply auto
done

Cheers,
Peter

On Mi, 2015-06-03 at 07:34 +0000, 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.