Email Gateway (Aug 18 2022 at 19:40): Email Gateway (Aug 18 2022 at 19:40):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
I was playing a bit with proofs with recursion induction in Isar and after
a while, it
became all too boring to type those long formulas so that I looked for some
ways of improving this
situation.
Pattern-matching with meta-variables as unknowns was a huge improvement.
But
I tried also pattern matching via case distinction and did not succeed.
Firstly, I thought case distinction
was only possible with structural induction. But in the new tutorial
(Programming and
Proving) one sees that proofs using rule induction can be done via case
distinction
with respect to the name (labels) of the rules.
Unfortunately, I did not succeed using this trick (of using a label) for
recursion induction.
Am I missing something very basic here?
Best!
Email Gateway (Aug 18 2022 at 19:41):From: Tobias Nipkow <nipkow@in.tum.de>
The names of the cases for recursive functions are 1, 2, ....
The reason is that fun may modify the input equations to disambiguate them. Thus
one equation may become two or more and one would need some clever naming scheme
to deal with that situation in inductions.
Tobias
Email Gateway (Aug 18 2022 at 19:41):From: Brian Huffman <huffman@in.tum.de>
On Tue, May 15, 2012 at 8:12 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:
The names of the cases for recursive functions are 1, 2, ....
The reason is that fun may modify the input equations to disambiguate them. Thus
one equation may become two or more and one would need some clever naming scheme
to deal with that situation in inductions.
Hi Alfio,
Note that if you don't like the default case names, you can rename
them using the "case_names" attribute on the induction rule. You can
use the "lemmas" command to save the updated rule for reuse. For
example:
fun fib :: "nat => nat" where
"fib 0 = 0" | "fib (Suc 0) = 1" | "fib n = fib (n - 1) + fib (n - 2)"
lemmas fib_induct = fib.induct [case_names 0 Suc_0 Suc_Suc]
lemma "fib n \<le> fib (Suc n)"
proof (induct n rule: fib_induct)
case 0 show ?case by simp
next
case Suc_0 show ?case by simp
next
case (Suc_Suc k) thus ?case by simp
qed
Am 14/05/2012 22:50, schrieb Alfio Martini:
Dear Isabelle Users,
I was playing a bit with proofs with recursion induction in Isar and after
a while, it
became all too boring to type those long formulas so that I looked for some
ways of improving this
situation.Pattern-matching with meta-variables as unknowns was a huge improvement.
But
I tried also pattern matching via case distinction and did not succeed.
Firstly, I thought case distinction
was only possible with structural induction. But in the new tutorial
(Programming and
Proving) one sees that proofs using rule induction can be done via case
distinction
with respect to the name (labels) of the rules.Unfortunately, I did not succeed using this trick (of using a label) for
recursion induction.
Am I missing something very basic here?Best!
Email Gateway (Aug 18 2022 at 19:41):From: Alfio Martini <alfio.martini@acm.org>
Dear Tobias,
Thank you for your reply. Now it works! However, when
using this I will always insert a comment next to
the corresponding case so as to avoid impairing the
clarity of the proof.
Best!
Email Gateway (Aug 18 2022 at 19:41):From: Alfio Martini <alfio.martini@acm.org>
Dear Brian,
That was really a great hint. Exactly what I wanted! I was not aware
of this "lemmas" command. I will look into into in more detail.
All the Best!
Email Gateway (Aug 18 2022 at 19:43):From: Makarius <makarius@sketis.net>
Comments can be very confusion, because they tend to diverge quickly from
the formally checked text, when that is changed a few times in its natural
life cycle.
Clarity of proofs means to put the right amount of explicit propositions
in the text, not too little, not too much. Isar allows some flexibilty
here. If you take a look at src/HOL/Induct/Command_Patterns.thy, for
example, there are some illustrative patterns that use symbolic 'case'
statements together with concrete propositions.
So an invocation of
case Foo
that introduces some local facts A and B and more in an opaque manner can
later be elucidated by saying
have "A" by fact
have "B" by fact
or
have "A" and "B" by fact+
or
note A and B
etc.
Makarius
Email Gateway (Aug 18 2022 at 19:43):From: Alfio Martini <alfio.martini@acm.org>
Dear Makarius,
That was very helpful. The theory "Common_Patterns.thy" is very
instructive! Especially
the "note" command when using "case" patterns in induction.
Best!
Last updated: Nov 21 2024 at 12:39 UTC