Re: [isabelle] Case distinction with Recursion Induction



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





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