Re: [isabelle] function with non-linear patterns



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_completeness

exception 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 syntactic reasons).

With the definition above, while you can prove completeness manually, the other goals (compatibility) will be unsolvable, since the third equation is inconsistent with the second one. Note that when using "function", the automatic disambiguation for pattern overlaps is disabled, which means that you have to write what you mean, e.g. by adding a precondition "y ~= x" to the third equation.

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

Alex





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