Re: [isabelle] Match exception in pat_completeness



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






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