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.

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

- Brian

> 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!
>>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.