Re: [isabelle] Case distinction with Recursion Induction
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.
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
> to deal with that situation in inductions.
> 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
> > a while, it
> > became all too boring to type those long formulas so that I looked for
> > 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