[isabelle] Case distinction with Recursion Induction

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?


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.