Email Gateway (Aug 18 2022 at 16:30): Email Gateway (Aug 18 2022 at 16:30):From: attarzadeh@ee.sharif.ir
Hello all,
I need to define a function (say g) that involves non-constructor pattern
matching. Say S, C, and A are datatype constructors and f is a
function(f:: “a => nat”), I want to see if the argument of g matches with
the pattern “ S (C f(A 0))” or not, but it fails because f is not a
datatype constructor. How can I define such a function in HOL?
Any help would be appreciated.
Regards,
Hoorie
Email Gateway (Aug 18 2022 at 16:31):From: Alexander Krauss <krauss@in.tum.de>
Dear Hoorie,
The "fun" command requires all patterns to be datatype constructors.
The more general "function" command can handle non-constructor patterns,
but you must prove that your patterns are used consistently. Moreover,
you can no longer use the code generator for such definitions, since
they are not programs. Section 6.2 of the function tutorial explains how
to do this:
http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf
The proof obligations arising from this sort of definition can be hard
to solve. Often it is easier to rewrite the definition such that it does
not use such patterns.
Hope this helps,
Alex
Email Gateway (Aug 18 2022 at 16:31):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Something to note: an alternative to this case matching can be done in pure logic.
Instead of "case v of S (C (f A 0)) => a | _ => b" I could type "if v = S (C (f A 0))) then a else b". This turns out to be an especially simple example, since f was applied to constant arguments (if I understood correctly).
A more involved example is "case v of S (C (f x)) => a x | _ => b", which I might write as "if EX x. v = S (C (f x)) then a (SOME x. v = S (C (f x))) else b", or maybe better "if v : range (S o C o f) then a (inv (S o C o f) v) else b". The latter assumes that f is sufficiently injective for the inverse of that function to be well defined.
Yours,
Thomas.
Last updated: Apr 26 2024 at 20:16 UTC