On 10/07/2010 09:11 AM, Florian Haftmann wrote:
I'm currently working on a package for generic type mappers. Leaving aside matters like contravariance and such, a type mappermap_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
The code_pred command for the invocation of the predicate compiler could also fit under this umbrella.
So the syntax would change from "code_pred" to "prove code_pred" which is actually better, because then users are not surprised that the command sets up some goal state (in most cases the empty goal) for the user to prove.
Lukas
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
