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.