Email Gateway (Aug 18 2022 at 19:40): Email Gateway (Aug 18 2022 at 19:40):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 19:40):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:43):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 19 2024 at 08:19 UTC