Re: [isabelle] feature request: defining tuples



Handling tuples in the input to the HOL4 definition mechanism
was definitely annoying. (Bear in mind that tuples would also
have to be handled for the derived induction theorem.) I think the
HOL4 implementation tries to handle arbitrarily nested tuple arguments,
but that is probably overkill.

Konrad.



On Thu, Nov 28, 2013 at 2:45 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:

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