[isabelle] not a datatype constructor err

Dear all,

I am a beginner in Isabelle and have faced some problems in writing a case
expression. I've defined the bellow primitives: (e and a are datatypes, S
and F are datatype constructors, and f1, f2 and g are functions)

*  k = nat


  e *=* S k a*|* ...


  a *=* F nat *|* ...


  f1 *::* "a => k"

  f2 *::* "a => k"

  I want to write a case expression that if e1(of type e) has the pattern "S
f1(F 0) a' " do something with a' :

 case e1 of S (f1(F 0)) a' => g(a')

 , but I get the "f1 is not a datatype constructor" error. How can I fix the
error? Is there another way to write the case expression (for example using

 Any suggestions would be of a really great help.

 Kind Regards


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