Re: [isabelle] parse translations



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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

Yes and no. It is some standard Event-B notation (set comprehension) but
I am not aware of an explanation in the literature. I have thus written
my own specification documentation:
ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf

Avoiding auxiliary notation, the Event-B set comprehension
"{x y. phi x y .| t x y}"
stands for
"(if
  \<forall> phi x y.
    phi x y \<noteq> None \<and> (the (phi x y) --> t x y \<noteq> None)
then Some {the (t x y) | x y. the (phi x y)}
else None)"

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

I think this is the missing piece of the puzzle. I have been unaware
that I can install transformations after type checking.

Thanks,
Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFNQFuwczhznXSdWggRAhRmAJ9XkaiVKy2RkFHSm7eYLGrzFCmyOACfWgbC
ETux71Xyh2E/whWf0IQgd48=
=KMHG
-----END PGP SIGNATURE-----





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