Re: [isabelle] Pattern Matching Problem
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?
The "fun" command requires all patterns to be datatype constructors.
The more general "function" command can handle non-constructor patterns,
but you must prove that your patterns are used consistently. Moreover,
you can no longer use the code generator for such definitions, since
they are not programs. Section 6.2 of the function tutorial explains how
to do this:
The proof obligations arising from this sort of definition can be hard
to solve. Often it is easier to rewrite the definition such that it does
not use such patterns.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and