Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 10:28):

From: Mr Julian Fell <julian.fell@uq.net.au>
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.

Email Gateway (Aug 22 2022 at 10:28):

From: Lars Hupel <hupel@in.tum.de>
Hi Julian,

this occurs from time to time. I haven't tried out your concrete
example, but there's a rule which could work for your case:
'rev_induct'. You can use it like this:

apply (induction t rule: rev_induct)

Hope that helps.

Cheers
Lars

Email Gateway (Aug 22 2022 at 10:29):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 10:29):

From: Peter Lammich <lammich@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC