*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Pattern Matching Problem*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Wed, 24 Nov 2010 10:37:00 +1100*Accept-language*: en-US*Acceptlanguage*: en-US*In-reply-to*: <4CEA2FAC.1010209@in.tum.de>*References*: <450804ea6783913128cf6e9ff25a8b1e.squirrel@ee.sharif.ir>, <4CEA2FAC.1010209@in.tum.de>*Thread-index*: AcuKI4MZQbZM03lHRymOcM0rb6q3sgBQsBuI*Thread-topic*: [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.

**References**:**[isabelle] Pattern Matching Problem***From:*attarzadeh

**Re: [isabelle] Pattern Matching Problem***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Huanhuan Zhang
- Next by Date: Re: [isabelle] A beginner's questionu
- Previous by Thread: Re: [isabelle] Pattern Matching Problem
- Next by Thread: [isabelle] A beginner's questionu
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list