[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

Norbert Schirmer nschirmer at apple.com
Sat Oct 2 10:51:11 CEST 2021

> On 29. Sep 2021, at 12:19, Makarius <makarius at sketis.net> wrote:
> Are there any remaining uses of your alternative antiquotations that are not
> covered properly by the new official scheme?

In AutoCorres there are also alternative antiquotations for matching and building terms, similar to the ones presented by Peter:
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy>
https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy <https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy>

Also I see great potential for providing similar antiquotations also for cterms, offering the possibility to ‘match’ sub-cterms and build cterms from certified sub-cterms. In contrast to terms also the matching part will result in a matching function, as cterms are an abstract data type.

In my experience recertifying cterms in proof tools like simprocs or tactics can easily become a performance hot-spot when terms become large.

As taking apart and recombining cterms manually with functions like Thm.dest_comb / Thm.apply is quite verbose and hard to maintain it rarely is used in practise. Instead terms are decomposed by ML-matching, recombined and recertified. In the presence of your new antiquotations this idiom is likely to become even more attractive and commonplace. 

Having antiquotations for cterms can be a powerful show-case for the potential of antiquotations, bringing together readability / conciseness as well as scalability.



Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211002/6080b9b1/attachment.htm>

More information about the isabelle-dev mailing list