Re: [isabelle] Case distinction with Recursion Induction
On Tue, May 15, 2012 at 8:12 AM, Tobias Nipkow <nipkow at 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.
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
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
case Suc_0 show ?case by simp
case (Suc_Suc k) thus ?case by simp
> 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
>> Pattern-matching with meta-variables as unknowns was a huge improvement.
>> 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
>> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and