Re: [isabelle] feature request: defining tuples



Hi Larry,

I see, yes, that sounds sensible. What about my slight generalisation, of pattern-matching an argument whenever its type has just one constructor? Ordered pairs don't always exist, but do datatypes always exist?

John

On 28 Nov 2013, at 16:26, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> 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.