# [isabelle] function with non-linear patterns

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] function with non-linear patterns
• From: Makarius <makarius at sketis.net>
• Date: Mon, 14 May 2012 19:29:48 +0200 (CEST)
• Cc: trung tran nguyen <ntrtrung at gmail.com>
• In-reply-to: <CAGxybBVf9oNkeNSjZSXJz=YqOW6sAETqkwUaP7jZ87VP-GKWNg@mail.gmail.com>
• References: <alpine.LNX.2.00.1205081143140.15872@macbroy21.informatik.tu-muenchen.de> <CAGxybBVf9oNkeNSjZSXJz=YqOW6sAETqkwUaP7jZ87VP-GKWNg@mail.gmail.com>
• User-agent: Alpine 2.00 (LNX 1167 2008-08-23)

```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_completeness
```
```
exception THM 1 raised (line 334 of "drule.ML"):
RSN: no unifiers
?t = ?t
_av3 = _av4 ⟹ P
[⋀xa xs. x = (Seq xa xs, xa) ⟹ P, x = (_av2, _av3),
_av2 = Seq _av4 _av5]

This is Isabelle2012-RC2.  The full example based an Main looks like this:

theory Scratch
imports Main
begin

datatype 'a seq = Empty | Seq 'a "'a seq"

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_completeness
apply auto

Is there anything fundamentally wrong with the idea of such non-linear
function patterns?

```
I am posting this on behalf of Trung, who is participating in our Isabelle/HOL tutorial today and tomorrow at Paris Sud.
```

Makarius```

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