[isabelle-dev] Declaration depending on user proofs

[Lukas Bulwahn]

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

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 at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>    

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101007/d2e6905a/attachment-0002.html>