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"
"contains Empty x = False"
|"contains (Seq x xs) x = True"
|"contains (Seq y xs) x = contains(xs) x"
exception THM 1 raised (line 334 of "drule.ML"):
Is there anything fundamentally wrong with the idea of such non-linear
No, but it is outside the scope of pat_completeness (for mere syntactic
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and