# Re: [isabelle] Pattern splitting in "function"

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:

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

--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

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