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"
"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.
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"):
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and