Re: [isabelle] Pattern splitting in "function"
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,
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,
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
Is this the intended behavior? It is not what the tutorial led me to expect.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 023
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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