# Re: [isabelle] parse translations

On Sun, 16 Jan 2011, Matthias Schmalz wrote:

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

`Is this some standard notion of Event-B explained in the literature
``somewhere?
`

`Anyway, the aforementioned idea of separating the concrete syntax (with
``the binding) from the abstract syntax (with the duplication of subterms)
``works along these lines:
`
abbreviation Foo :: "('a => bool) => bool" (binder "FOO " 10)
where "Foo b == (ALL x. b x) & (EX x. b x)"

`There are two syntax layers involved here: the "binder" annotation
``produces some standard parse/print translation for iterated binders; the
``rewrite rule operates on fully type-checked lambda terms -- when the
``regular type-inference is already finished.
`

`At both layers you can install your own ML function to operate on parse
``terms and typed lambda terms, respectively. You merely declare an
``uninterpreted constant like this:
`
axiomatization Foo :: "('a => bool) => bool"

`or any other type scheme that fits for your application. Note that
``'axiomatization' instead of 'consts' ensures that the user cannot
``accidentally define Foo later on.
`

`You then provide ML 'parse_translation' and 'print_translation' in the
``known manner. Moreover, the inner check/uncheck phase is configured like
``this:
`
declaration {* K (Syntax.add_term_check 0 "my_check" my_check) *}

`Here my_check is your function to operate on simultatenously on a given
``input or output situation (consiting of terms). It returns either SOME
``changed result, or NONE for identity. See also e.g. see
``src/Pure/Isar/proof_context.ML how expand_abbrevs and contract_abbrevs are
``done. This is really a user-space mechanism.
`
Makarius

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