> On 29. Sep 2021, at 12:19, Makarius <[email protected]> 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. Regards, Norbert -- Norbert Schirmer ([email protected]) SEG Formal Verification
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
