[isabelle-dev] Declaration depending on user proofs

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 7 09:11:52 CEST 2010

I'm currently working on a package for generic type mappers.  Leaving
aside matters like contravariance and such, a type mapper

  map_k :: ('a_1 => 'b_1) => ... => ('a_n => 'b_n)
    => ('a_1, ..., 'a_n) k is => ('b_1, ..., 'b_n) k

for an n-ary type ('a_1, ..., 'a_n) k must satisfy some characteristic
properties like

  map_k f_1 ... f_n o map_k g_1 ... g_n =
    map_k (f_1 o g_1) ... (f_n o g_n)

To declare something as a type mapper, the following command could be

  type_mapper map_k

which would issue an appropriate declaration.  Attributes are
inappropriate here since the user cannot be expected to write down the
theorems to prove explicitly.

However I am always reluctant to introduce new keywords, both for
aesthetic and technical reasons.  So I am asking myself whether we
should introduce a command for generic user-proof-dependent
declarations, e.g.

  prove <args>

Here different parsers could be registered under the umbrella of the
same command.  Some possible instances:

  prove type_mapper: map_l

  prove isomorphism: Fset.Fset Fset.member

Any opinions?




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101007/3e6f4632/attachment.sig>

More information about the isabelle-dev mailing list