Re: [isabelle] feature request: defining tuples



I feel uneasy about this idea, because “definition” is the low-level definitional mechanism of Isabelle, which doesn’t presume the existence of such things as ordered pairs. Your suggestion makes sense for Isabelle/HOL, but not in the wider context of generic theories, where ordered pairs may not exist. One of the specific purposes of “fun” is to support pattern matching.

Larry Paulson


On 28 Nov 2013, at 14:55, John Wickerson <johnwickerson at cantab.net> wrote:

> Hi,
> 
> Could I make a feature request regarding the "definition" package?
> 
> Current status
> --------------
> 
> Statements like { definition "foo (a,b) == blah /\ bleh" } are not accepted, since the definition package does not support tupled arguments. 
> 
> Proposal
> --------
> 
> That the definition package allows tupled arguments. Slightly more generally, since (a,b) is just shorthand for the constructed term "Pair a b", I propose that the definition package should support pattern-matching of arguments whenever the types of those arguments have exactly *one* constructor. For instance, I could then write { datatype proc = Procedure string command } and { definition "exec (Procedure s c) == ..." }.
> 
> Current workarounds
> -------------------
> 
> 1. Write { definition "foo == %(a,b). blah /\ bleh" }. But this changes the foo_def theorem, and doesn't look so visually nice.
> 
> 2. Write { fun foo where "foo (a,b) = (blah /\ bleh)" }. But this changes the foo_def theorem, and I have to remember to use foo.simps instead. And I have to put extra parentheses around the definiens, because "=" has different precedence to "==". And I have to remove foo.simps from the simplifier if I don't want foo expanding all the time. And I prefer to reserve "fun" for proper recursive functions, which foo isn't.
> 
> 3. Write { definition "foo a b == blah /\ bleh" }. But there are times when it's more idiomatic to tuple than to curry.
> 
> 
> cheers,
> John





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