[isabelle] Pattern splitting in "function"



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





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