Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pattern splitting in "function"

Email Gateway (Aug 18 2022 at 17:44):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
I'm running the Nominal2 bundle from Christian Urban's webpage
(Nominal2 and Isabelle 2011, February 2011), but the question arises
from theory Main of this bundle.

In sect. 6.1 of the tutorial on function definition we have datatype
P3 and function And2, which avoids the automatic pattern splitting of
"fun". I understood that the point was to have the recursion
equations of the definition of And2 as written. However when I do the
function definition as in the tutorial I get psimp equations guarded
by "And2_dom". How can I use these recursion equations?

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 is not what the tutorial led me to expect.

Thanks,
Randy

Email Gateway (Aug 18 2022 at 17:45):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Randy,

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. After showing pattern completeness and consistency as
described in Section 6.1, i.e. "by pat_completeness auto", you want to show
termination before working with your function. For the example in the tutorial,
you need

termination by lexicographic_order

Then, you get the simp rules you would expect under the name And2.simps.
Section 4 of the tutorial explains termination proofs in more detail.

Hope this helps,
Andreas

Randy Pollack schrieb:

Email Gateway (Aug 18 2022 at 17:45):

From: Alexander Krauss <krauss@in.tum.de>
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

Last updated: Apr 26 2024 at 08:19 UTC