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
introduced
type_mapper map_k
<proof>
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>
<proof>
Here different parsers could be registered under the umbrella of the
same command. Some possible instances:
prove type_mapper: map_l
<proof>
prove isomorphism: Fset.Fset Fset.member
<proof>
Any opinions?
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
