# [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.*