Email Gateway (Aug 19 2022 at 08:43): Email Gateway (Aug 19 2022 at 08:43):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Hello all:
I have a function that I have defined like this:
fun sv2vl :: "nat 'a::scalar list 'a::scalar list 'a::scalar list" where
"sv2vl 0 orig lst = []"
| "sv2vl cnt [] [] = (replicate cnt fill)"
| "sv2vl (Suc cnt) (oel # ors) [] = (oel # (sv2vl cnt (oel # ors) ors))"
| "sv2vl (Suc cnt) orig (elm # rst) = (elm # (sv2vl cnt orig rst))"
And I am trying to prove that the length of the result of this function
is equal to the first argument. However, unlike with primrec or
some other elements, I am having a hard time figuring out how to
express the various cases of the body to Isabelle. That is, I am thinking
that you would prove this inductively by showing the base case
trivially, and then showing that for the case (Suc n) you have three
cases where this could be true, and in each one of them, the length
is what I want.
However, how do I say this in Isar or whatever else I am doing?
Yours truly,
Aaron W. Hsu
Email Gateway (Aug 19 2022 at 08:43):From: Tobias Nipkow <nipkow@in.tum.de>
Because fun generates the right induction principle, the proof is a one-liner:
by (induct n xs ys rule: sv2vl.induct) auto
See the documentation (eg Tutorial on Function Definitions or the new
Programming and Proving tutorial) for more info.
Of course you can also use this induction rule in more verbose Isar proofs.
Tobias
Email Gateway (Aug 19 2022 at 08:44):From: "Aaron W. Hsu" <arcfide@sacrideo.us>
Tobias Nipkow <nipkow@in.tum.de> writes:
Thanks so much! I took a look at the documentation in question and
that clears things up, though I do not understand why the explicit
"rule" part is necessary. Why would it not automatically choose that
rule? Do you normally want the other induction rules instead of this
one in proofs?
Email Gateway (Aug 19 2022 at 08:45):From: Tobias Nipkow <nipkow@in.tum.de>
There needs to be some indication which induction principle is wanted. Just
giving variable names indicates structural induction. Other induction principles
would need other hints. One could imagine writing something like "sv2vl n xs ys"
to indicate that, but that would be a significant extension of induction, and it
is already too complicated as it is.
Moreover you will find that the limiting factor in writing proofs is not stating
an induction rule.
Tobias
Last updated: Apr 30 2024 at 12:28 UTC