*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] parse translations*From*: Matthias Schmalz <Matthias.Schmalz at inf.ethz.ch>*Date*: Sun, 16 Jan 2011 17:59:11 +0100*In-reply-to*: <alpine.LNX.1.10.1101161329480.6514@atbroy100.informatik.tu-muenchen.de>*References*: <4D30B401.8050002@inf.ethz.ch> <alpine.LNX.1.10.1101161329480.6514@atbroy100.informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.24 (X11/20101027)

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Makarius schrieb: > On Fri, 14 Jan 2011, Matthias Schmalz wrote: > >> 1. Consider the following contrieved parse translation translating >> "foo x. t" to "(\<forall> x. t) \<and> (\<forall> x. t)": >> >> term "foo x. True" >> (with show_types activated) I get >> "(\<forall> x::'a. True) \<and> (\<forall> x::'b. True)". >> (The two occurrences of x have different types.) >> >> Is it possible to change the parse translation so that >> term "foo x. True" >> yields "(\<forall> x::'a. True) \<and> (\<forall> x::'a. True)". >> (The two occurrences of x have the same type.) > > Not really, at least not at the raw parse tree level. Duplication of > subtrees as above (and likewise comparison of subtrees for printing) > looks suspicious. That is good to know. So I will stop trying. > Nonetheless, it should work by separating the concrete from the abstract > syntax. I.e. "foo" is like a regular binder, and there is an > abbreviation for the rest. Abbreviations work by higher-order rewriting > on fully-typed lambda terms. The binder(s) I actually want to define has the following characteristics: 1. binds several variables (like \<forall>, \<exists>, set comprehension) 2. no simple recursive definition (like set comprehension, unlike \<forall>, as \<forall> x xs. p == \<forall> x. \<forall> xs. p) 3. the right-hand side of the definition has an extra bound variable (like set comprehension: {t | xs. p} == {y. \<exists> xs. y = t \<and> p}) 4. the right-hand side binds the bound variables of the left-hand side several times such as in: foo xs. p == (\<forall> xs. p) \<and> (\<exists> xs. p) The multiple bound variables make it hard to work with abbreviations. I will try to cook something up with overloading (to cope with the arbitrary number of bound variables). If that does not work out, I will define (on demand) several constants foo1, foo2, ..., one for each number of bound variables. Maybe somebody on the list can point to a running example of a binder with the above properties? That would be helpful. Anyway, thanks for the explanations, Matthias -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFNMyPfczhznXSdWggRAlcOAJ99BjR5aGRtjitF4CoPNY4bvIv5eQCeLZoe /D5T7dSFzOeQlzXAEuswYxc= =2xd+ -----END PGP SIGNATURE-----

**Follow-Ups**:**Re: [isabelle] parse translations***From:*Makarius

**References**:**[isabelle] parse translations and lexical matters***From:*Matthias Schmalz

**Re: [isabelle] parse translations***From:*Makarius

- Previous by Date: Re: [isabelle] lexical matters
- Next by Date: Re: [isabelle] lexical matters
- Previous by Thread: Re: [isabelle] parse translations
- Next by Thread: Re: [isabelle] parse translations
- Cl-isabelle-users January 2011 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