Re: [isabelle] Feature suggestion: matching arguments by a unique tag



Victor,

On Sat, 2011-07-09 at 18:34 +0400, Victor Porton wrote:
> 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).

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







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