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,

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.


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