Re: [isabelle] Pattern Matching Problem



Dear Hoorie,

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:
http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf

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,
Alex





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