Re: [isabelle] function with non-linear patterns



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_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.

We have tried the precondition later, but it also produced a low-level exception (in Isabelle2012-RC2):

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 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.

This was also my conclusion: it falls into the "don't do it then" category.


	Makarius





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