[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)

  *types
*  k = nat

*datatype*

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

*datatype*

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

*consts*

  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
"if")?

 Any suggestions would be of a really great help.

 Kind Regards


 --Mir




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