<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html; charset=ISO-8859-15"
 http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#ffffff">
On 10/07/2010 09:11 AM, Florian Haftmann wrote:
<blockquote cite="mid:4CAD72B8.1010009@informatik.tu-muenchen.de"
 type="cite">
  <pre wrap="">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

  </pre>
</blockquote>
<br>
The code_pred command for the invocation of the predicate compiler
could also fit under this umbrella.<br>
<br>
So the syntax would change from "code_pred" to "prove code_pred" which
is actually better, because then users are not surprised<br>
that the command sets up some goal state (in most cases the empty goal)
for the user to prove.<br>
<br>
<br>
Lukas<br>
<br>
<br>
<blockquote cite="mid:4CAD72B8.1010009@informatik.tu-muenchen.de"
 type="cite">
  <pre wrap=""></pre>
  <pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
Isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Isabelle-dev@mailbroy.informatik.tu-muenchen.de">Isabelle-dev@mailbroy.informatik.tu-muenchen.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
  </pre>
</blockquote>
<br>
</body>
</html>