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.


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