Re: [isabelle] feature request: defining tuples



Am 28/11/2013 21:35, schrieb Michael Norrish:
> HOL4 does support this for its new_definition "primitive". Later theories can interpose pre and post transformations on the input term and the output theorem so that definitions appearing to be on tuples get turned into "real" definitions of the form `var = rhs`, and then turned back into the characterising theorem that the user expects.  (Even handling `f x = x + 1` uses this machinery.)

Thanks, I thought so. Awesome how you manage to support all this complexity!

Tobias

> Michael
> 
>> On 29 Nov 2013, at 2:20, "Tobias Nipkow" <nipkow at in.tum.de> wrote:
>>
>> That would indeed be convenient and I have frequently felt like adding it to
>> Isabelle/HOL. HOL Light supports this, and maybe HOL4 too.
>>
>> Tobias
>>
>> Am 28/11/2013 15:55, schrieb John Wickerson:
>>> 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
>>
> 
> ________________________________
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
> 




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