Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Match exception in pat_completeness

Email Gateway (Aug 18 2022 at 15:43):

From: Lars Noschinski <noschinl@in.tum.de>
Hello,

the following code

function foo :: "'a list ⇒ nat" where
"foo (y # ys) = 0"
by pat_completeness termination sorry

raises a Match exception in pat_completeness (in Isabelle 2009-2):

*** exception Match raised (line 111 of
"/var/tmp/isabelle-makebin14768/Isabelle2009-2/src/HOL/Tools/Function/pat_completeness.ML")
*** At command "by".

-- Lars

Email Gateway (Aug 18 2022 at 15:43):

From: Alexander Krauss <krauss@in.tum.de>
Hi Lars,

the following code

function foo :: "'a list ⇒ nat" where
"foo (y # ys) = 0"
by pat_completeness termination sorry

raises a Match exception in pat_completeness (in Isabelle 2009-2):

*** exception Match raised (line 111 of
"/var/tmp/isabelle-makebin14768/Isabelle2009-2/src/HOL/Tools/Function/pat_completeness.ML")

pat_completeness is behaving badly here, and throws a low-level
exception. The correct behaviour would be

"empty result sequence"

since your patterns are indeed incomplete, and it wont be able to prove
completeness. (Look at the first subgoal that it is supposed to solve).
The function package can add the missing pattern automatically, if you
pass it the "(sequential)" option (which is also implicit when you use
the abbreviated form "fun". If your real problem is as simple as this
one, then you probably want to use "fun".

More explanations can be found in the tutorial for function definitions:
http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf

Alex

*** At command "by".

-- Lars

Email Gateway (Aug 18 2022 at 15:43):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Lars,

since you do not give all patterns (there is no case for the empty
list),
you have to pass the sequential argument to the definition.

function (sequential) foo :: "'a list ⇒ nat" where
"foo (y # ys) = 0"
by pat_completeness auto
termination ...

However, for such a simple function you can also directly use fun,
since it
will figure out the termination proof by itself.

fun foo :: "'a list ⇒ nat" where
"foo (y # ys) = 0"

Best regards,
René

Email Gateway (Aug 18 2022 at 15:44):

From: Lars Noschinski <noschinl@in.tum.de>
Dear René,

yes, this function definition is not complete, which is obvious here.
But it was far from obvious in my original function definition (from
which I extracted this toy example). Hence I would expect
pat_completeness to fail gracefully (or generate unsatisfiable
constraints), so the user can see that it is not a bug in Isabelle, but
his definition is wrong.

-- Lars

Last updated: Nov 21 2024 at 12:39 UTC