Re: [isabelle] feature request: defining tuples



Well, no, in general nothing exists. 

Of course I see that “fun” might be cumbersome in such a simple case.

Larry Paulson


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

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