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