Re: [isabelle] Case distinction with Recursion Induction



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!

On Tue, May 15, 2012 at 3: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.
>
> Tobias
>
> 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!
> >
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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