Re: [isabelle] Pattern Matching Problem



Something to note: an alternative to this case matching can be done in pure logic.

Instead of "case v of S (C (f A 0)) => a | _ => b" I could type "if v = S (C (f A 0))) then a else b". This turns out to be an especially simple example, since f was applied to constant arguments (if I understood correctly).

A more involved example is "case v of S (C (f x)) => a x | _ => b", which I might write as "if EX x. v = S (C (f x)) then a (SOME x. v = S (C (f x))) else b", or maybe better "if v : range (S o C o f) then a (inv (S o C o f) v) else b". The latter assumes that f is sufficiently injective for the inverse of that function to be well defined.

Yours,
    Thomas.
________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Alexander Krauss [krauss at in.tum.de]
Sent: Monday, November 22, 2010 7:54 PM
To: attarzadeh at ee.sharif.ir
Cc: isabelle-users at cl.cam.ac.uk
Subject: 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


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





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