<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><div><br class=""></div>
</div>
<div><br class=""><blockquote type="cite" class=""><div class="">On 29. Sep 2021, at 12:19, Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">Are there any remaining uses of your alternative antiquotations that are not</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">covered properly by the new official scheme?</span></div></blockquote></div><br class=""><div class=""><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">In AutoCorres there are also alternative antiquotations for matching and building terms, similar to the ones presented by Peter:</div><div><font color="#000000" class=""><span style="caret-color: rgb(0, 0, 0);" class=""><a href="https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy" class="">https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote.thy</a></span></font></div><div><font color="#000000" class=""><a href="https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy" class="">https://github.com/seL4/l4v/blob/master/lib/ml-helpers/MkTermAntiquote_Tests.thy</a></font></div><div><font color="#000000" class=""><a href="https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy" class="">https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote.thy</a></font></div><div><a href="https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy" class="">https://github.com/seL4/l4v/blob/master/lib/ml-helpers/TermPatternAntiquote_Tests.thy</a></div><div><br class=""></div><div><br class=""></div><div>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.</div><div><br class=""></div><div>In my experience recertifying cterms in proof tools like simprocs or tactics can easily become a performance hot-spot when terms become large.</div><div><br class=""></div><div>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. </div><div><br class=""></div><div>Having antiquotations for cterms can be a powerful show-case for the potential of antiquotations, bringing together readability / conciseness as well as scalability.</div><div><font color="#000000" class=""><br class=""></font></div><div><font color="#000000" class=""><span style="caret-color: rgb(0, 0, 0);" class=""><br class=""></span></font></div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Regards,</div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Norbert</div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">--</div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Norbert Schirmer (<a href="mailto:nschirmer@apple.com" class="">nschirmer@apple.com</a>)</div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"> SEG Formal Verification</div></div><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br class=""></div></body></html>