[isabelle] Pattern Matching Problem

Hello all,
I need to define a function (say g) that involves non-constructor pattern
matching. Say S, C, and A are datatype constructors and f is a
function(f:: “a => nat”), I want to see if the argument of g matches with
the pattern “ S (C f(A 0))” or not, but it fails because f is not a
datatype constructor. How can I define such a function in HOL?

Any help would be appreciated.


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