Re: [isabelle] Pattern splitting in "function"



On 05/27/2011 04:25 PM, Andreas Lochbihler wrote:
No, this is not the intended usage. According to Section 3, function
does not attempt to prove termination of the defintion like fun does.
Hence, you only get the psimps equations.

Yes. "function" always needs an explicit termination proof.


reading further and experimenting, I find that function And2 can be
defined with the (domintros) attribute, and then the definition works

lemma "And2 T T = T"
using And2.domintros And2.psimps
by (simp)

Is this the intended behavior?

It works by pure luck here, or rather the fact that the function is not recursive, so And2.domintros is rather trivial.

I admit that omitting the "termination by ..." is a bit confusing, so I now added that line to the tutorial.

Alex





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