*To*: Alexander Krauss <krauss at in.tum.de>, trung tran nguyen <ntrtrung at gmail.com>*Subject*: Re: [isabelle] function with non-linear patterns*From*: Makarius <makarius at sketis.net>*Date*: Wed, 16 May 2012 15:02:40 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4FB17B77.30500@in.tum.de>*References*: <alpine.LNX.2.00.1205081143140.15872@macbroy21.informatik.tu-muenchen.de> <CAGxybBVf9oNkeNSjZSXJz=YqOW6sAETqkwUaP7jZ87VP-GKWNg@mail.gmail.com> <alpine.LNX.2.00.1205141923310.3781@macbroy21.informatik.tu-muenchen.de> <4FB17B77.30500@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 14 May 2012, Alexander Krauss wrote:

On 05/14/2012 07:29 PM, Makarius wrote:On Mon, 14 May 2012, trung tran nguyen wrote:function contains ::"'a seq => 'a => bool" where "contains Empty x = False" |"contains (Seq x xs) x = True" |"contains (Seq y xs) x = contains(xs) x" apply pat_completenessexception THM 1 raised (line 334 of "drule.ML"):[...]Is there anything fundamentally wrong with the idea of such non-linear function patterns?No, but it is outside the scope of pat_completeness (for mere syntacticreasons).With the definition above, while you can prove completeness manually, theother goals (compatibility) will be unsolvable, since the third equation isinconsistent with the second one. Note that when using "function", theautomatic disambiguation for pattern overlaps is disabled, which means thatyou have to write what you mean, e.g. by adding a precondition "y ~= x" tothe third equation.

exception TERM raised (line 256 of "~~/src/HOL/Tools/hologic.ML"): dest_eq xa ~= x

However, I generally do not recommend this, since you are then leavingthe area of functional programming, which means that you lose quite abit of tool support (simplifier, code generation, quickcheck, etc.).Writing "if" is usually better.

Makarius

**References**:**[isabelle] function with non-linear patterns***From:*Makarius

**Re: [isabelle] function with non-linear patterns***From:*Alexander Krauss

- Previous by Date: [isabelle] CFP ICTSS 2012
- Next by Date: Re: [isabelle] Case distinction with Recursion Induction
- Previous by Thread: Re: [isabelle] function with non-linear patterns
- Next by Thread: [isabelle] Case distinction with Recursion Induction
- Cl-isabelle-users May 2012 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