Re: [isabelle] Splicing runtime ML values into Isar

Dear Lars,

This looks like an interesting experiment. Do you think that something similar could be done for formal comments inside types and terms, i.e., to change from the term language to the language context "document", as discussed in a thread from last year?


On 09/06/15 23:20, Lars Hupel wrote:
Dear list,

we've had antiquotations for a while now -- a syntactic method to embed
formal entities into ML code. I've been wondering about the opposite
direction -- embedding (properly typed) ML values into a formal context.
With the arrival of cartouches, this is actually possible now. The
attached theory allows one to write:

   term "(Îx. SPLICE âBound 0â)"

... which results in a formal expression logically equivalent to

   term "(Îx. x)"

This also works with theorems:

   MLâval mythm = @{thm conjI[where P = True]}â
   lemmas mythm = [[splice âmythmâ]]

Of course, this is not very useful by itself. But it can also be used to
compute larger terms using ML, e.g. for lemma statements:

   lemma "0 < SPLICE âHOLogic.mk_number @{typ nat} (1+1)â"

... produces the goal "0 < 2". There might be use cases in program
synthesis here.

A nice side effect of using cartouches is that markup works out of the
box, i.e. all the ML entities (and embedded antiquotations) can be

Disclaimer: Do not use this for production purposes.

Comments welcome!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.