*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] feature request: defining tuples*From*: John Wickerson <johnwickerson at cantab.net>*Date*: Mon, 2 Dec 2013 16:23:46 +0000*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1312021625170.32036@lxbroy10.informatik.tu-muenchen.de>*References*: <82C43CB8-FAB8-4257-99AE-1ABDF8E19AE1@cantab.net> <alpine.LNX.2.00.1312021625170.32036@lxbroy10.informatik.tu-muenchen.de>

Thanks Makarius, particularly for the "where [simp del]" tip. That's much nicer than having to issue a separate "declare" instruction. John On 2 Dec 2013, at 16:06, Makarius <makarius at sketis.net> wrote: > On Thu, 28 Nov 2013, John Wickerson wrote: > >> 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. > >> From these usage patterns, the mental model of the essense of 'definition' > vs. 'fun' / 'function' is not fully clear. > > The 'definition' package is for "simple definitions". It wraps up the basic Local_Theory.define concept, which in turn goes releatively straight to primitive definitions of the logical core (which are not accessible to users these days). It presents itself in an object-logic friendly manner, to allow writing "f x y = rhs" (with HOL equality). The Pure form "f x y == rhs" or even "f == %x y. rhs" is mostly historic -- it is only required for object-logics like ZF that cannot internalize all forms of definition. The conversion of the user specification is represented as higher-order rewrite system via 'defn' rules -- whatever works here works, what doesn't work doesn't. > > The 'function' package is somehow dual: it incorporates as many features as possible, just before gravitational collapse. Pattern matching probably even outweighs the recursion / termination aspect. (Interestingly, Scala is a higher-order functional language, where recursion and pattern matching are separate. Odersky then uses his remaining complexity budget elsewhere to make it more sophisticated than ML or Haskell.) > > > The practical situation can be improved in a simple manner like this: > > * Refrain from using == in definitions. Uniform = simplifies theories > and allows to move specifications between different tools and packages > more easily: 'theorem', 'definition', 'primrec', 'fun', 'function' etc. > > * The function package could refrain from exposing its internal > construction of f as f_def. This was technically not possible when > first implemented, but is now just a matter how Local_Theory.define is > invoked. This also avoids well-known confusion due to unintended > "unfold f_def" seen routinely with fresh users. > > Then the difference is just implicit simplification or not, and you write something like: > > fun f where [simp del]: "f (x, y, z) ((a, b), (u, v, w)) = rhs" > > and make patterns as complex as the function package allows. Later you simplify with f.simps as usual. > > > A side-alley of this thread is the old question, what the "unfold" proof method or 'unfolding' command should really do. There are various well-known anomalies in its wording and technical snags of "unfolding f_def" where the equation does not always apply (because patterns don't match). > > So far I always considered a puristic approach more desirable (at least in theory): reconstruct a precise equation "f == %x y z. rhs" from the user-space equation f x y z = rhs. Really *unfold* that, and don't rewrite with arbitray rules. Any such change and clarification is apt to break existing applications, as usual. > > An alternative speculation is this: "unfold f" takes a term f and looks up its equational "Spec_Rules", which is a new concept from some years ago. It then just rewrites with them by simplification, like the present f_def or f.simps would do. This unifies 'definition' and 'fun' in that respect, and makes the system appear more like Coq, where terms have canonical "computation rules". > > > Makarius >

**References**:**Re: [isabelle] feature request: defining tuples***From:*Makarius

- Previous by Date: Re: [isabelle] feature request: defining tuples
- Next by Date: Re: [isabelle] feature request: defining tuples
- Previous by Thread: Re: [isabelle] feature request: defining tuples
- Next by Thread: Re: [isabelle] feature request: defining tuples
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list