Email Gateway (Aug 18 2022 at 18:04): Email Gateway (Aug 18 2022 at 18:04):From: Victor Porton <porton@narod.ru>
After some experimentation I concluded that Isabelle 2011 does not support definitions of functions with pattern matching by a unique tag. For example the following does not work:
typedecl tag
consts t1::tag
consts t2::tag
definition "f (t1, x) = t1"
definition "f (t2, x) = t2"
I think it is a good idea to make this working in a future version of Isabelle (or in an entirely new proof assistant).
Email Gateway (Aug 18 2022 at 18:04):From: Tjark Weber <webertj@in.tum.de>
Victor,
The kind of "matching by constant" that you suggest may not be so useful
after all. Remember that t1 and t2 are just names for elements of tag.
We don't know whether the tag type has other elements (in which case f
would be underspecified), or whether t1 and t2 denote the same element
(in which case you are lucky that your definitions aren't inconsistent).
However, Isabelle/HOL does support pattern matching for datatype
constructors. For instance, you could define
datatype tag = t1 | t2
fun f where
"f (t1, x) = t1"
| "f (t2, x) = t2"
See the Isabelle documentation, specifically the Tutorial on Function
Definitions, for details.
Kind regards,
Tjark
Last updated: Apr 19 2024 at 20:15 UTC