*To*: Lars Hupel <hupel at in.tum.de>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Splicing runtime ML values into Isar*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 10 Jun 2015 09:44:10 +0200*In-reply-to*: <5577588F.5070507@in.tum.de>*References*: <5577588F.5070507@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Dear Lars,

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-September/msg00056.html Andreas 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)â" oops ... 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 Ctrl-clicked. Disclaimer: Do not use this for production purposes. Comments welcome! Cheers Lars

**Follow-Ups**:**Re: [isabelle] Splicing runtime ML values into Isar***From:*Lars Hupel

**Re: [isabelle] Splicing runtime ML values into Isar***From:*Makarius

**References**:**[isabelle] Splicing runtime ML values into Isar***From:*Lars Hupel

- Previous by Date: Re: [isabelle] No warning for non-exhaustive case
- Next by Date: Re: [isabelle] Splicing runtime ML values into Isar
- Previous by Thread: [isabelle] Splicing runtime ML values into Isar
- Next by Thread: Re: [isabelle] Splicing runtime ML values into Isar
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list