[isabelle] function with non-linear patterns



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.