From: Makarius <makarius@sketis.net>

*** ML ***

- ML antiquotations for type constructors and term constants:
\<^Type>‹c›

\<^Type>‹c T …› ― ‹same with type arguments›

\<^Type>_fn‹c T …› ― ‹fn abstraction, failure via exception TYPE›

\<^Const>‹c›

\<^Const>‹c T …› ― ‹same with type arguments›

\<^Const>‹c for t …› ― ‹same with term arguments›

\<^Const_>‹c …› ― ‹same for patterns: case, let, fn›

\<^Const>_fn‹c T …› ― ‹fn abstraction, failure via exception TERM›

Examples in HOL:

val natT = \<^Type>‹nat›;

fun mk_funT (A, B) = \<^Type>‹fun A B›;

val dest_funT = fn \<^Type>‹fun A B› => (A, B);

fun mk_conj (A, B) = \<^Const>‹conj for A B›;

val dest_conj = fn \<^Const_>‹conj for A B› => (A, B);

fun mk_eq T (t, u) = \<^Const>‹HOL.eq T for t u›;

val dest_eq = fn \<^Const_>‹HOL.eq T for t u› => (T, (t, u));

This refers to Isabelle/4974c3697fee.

The question of how to represent outlines for type and term expressions

adequately and robustly in Isabelle/ML has remained open for a long time.

After 2007/2008, I always thought that we should use more concrete syntax

(namely inner syntax).

After rethinking it thoroughly, the outcome is now as above. The key idea is

to nest ML source inside antiquotations: this has become possible in recent

antiquotations \<^try>‹expr› and \<^can>‹expr›.

The result looks a bit like enhanced S-expressions from the old LISP days:

this fits perfectly well into the idea of antiquotations and nesting of

sublanguages via cartouches --- instead of lots of silly parentheses.

Another motivation: the Const antiquotations already use "typargs", e.g. just

one type T for overloaded "plus", instead of "T => T => T". When all

Isabelle/ML have been upgraded to use that form, we may have a chance to trim

down the redundant type information in datatype term for Const (within a few

years).

This has the potential to speed-up term/type

instantiation/matching/unification considerably: profiles always show a lot of

activity on types, rather than actual term structure.

Makarius

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Peter Lammich <lammich@in.tum.de>

Hi,

nice that term handling from ML gets some attention now.Just as a

remark, and maybe "feature request" of what I would like to see, I'm

using the following antiquotations for several years now. They are in

the AFP.

https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mpat_Antiquot.html

https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mk_Term_Antiquot.html

There is an antiquotation @{mpat} that generates a ML matching pattern

from a term, and one @{mk_term} that constructs a term. mk_term also

tries hard to infer types from the arguments (examples below).

These are definitely not include-in-distribution quality yet, as they

use a hack of identifying term-variables (?x) with ML variables.

However, I use them a lot, and would like to ultimately see robust and

clean means to efficiently match against and constructs complex terms

from ML level in a readable way.

-- Peter

Examples to generate matching patterns from terms:

fun dest_pair_singleton @{mpat "{(?a,_)}"} = (a)

| dest_pair_singleton t = raise TERM ("dest_pair_singleton",[t])

fun dest_nat_pair_singleton @{mpat (typs) "{(?a::nat,?b::nat)}"} =

(a,b)

| dest_nat_pair_singleton t = raise TERM

("dest_nat_pair_singleton",[t])

fun dest_pair_singleton_T @{mpat (typs) "{(?a::_ ⇒

?'v_Ta,?b::?'v_Tb)}"} =

((a,Ta),(b,Tb))

| dest_pair_singleton_T t = raise TERM

("dest_pair_singleton_T",[t])

fun dest_pair_lambda @{mpat "{(λa _ _. ?Ta, λb. ?Tb)}"} =

(a,a_T,b,b_T,Ta,Tb)

| dest_pair_lambda t = raise TERM ("dest_pair_lambda",[t])

fun foo @{mpat "[?a,?b AS⇩s mpaq_Bound ?i,?c AS⇩p [?n]]"} =

(a,b,i,c,n)

| foo t = raise TERM ("foo",[t])

Examples to generate term templates: fun mk_2elem_list a b = @{mk_term

"[?a,?b]"}

fun mk_compr s P = @{mk_term "{ x∈?s. ?P x}"}

val test1 = mk_2elem_list @{term "1::nat"} @{term "2::nat"} |>

Thm.cterm_of @{context}

val test2 = mk_compr @{term "{1,2,3::nat}"} @{term "(<) (2::nat)"} |>

Thm.cterm_of @{context}

val test3 = let

val x = Bound 0

val env = [@{typ nat}]

in

@{mk_term env: "?x+?x"}

end

From: Makarius <makarius@sketis.net>

On 22/09/2021 13:16, Peter Lammich wrote:

Just as a remark, and maybe "feature request" of what I would like to see, I'm

using the following antiquotations for several years now. They are in the AFP.

https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mpat_Antiquot.html

https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mk_Term_Antiquot.htmlThere is an antiquotation @{mpat} that generates a ML matching pattern from a

term, and one @{mk_term} that constructs a term.

mk_term also tries hard to infer types from the arguments (examples below).These are definitely not include-in-distribution quality yet, as they use a

hack of identifying term-variables (?x) with ML variables. However, I use them

a lot, and would like to

ultimately see robust and clean means to efficiently match against and

constructs complex terms from ML level in a readable way.

This looks like enormous complexity, with remaining open questions and

problems. It is like an attempt to implement my postulates from many years

ago, to connect inner syntax somehow to ML.

My current move deviates from that, returning to a more basic and more robust

scheme. Recall these explanations:

On Wed, 2021-09-22 at 12:50 +0200, Makarius wrote:

The question of how to represent outlines for type and term expressions

adequately and robustly in Isabelle/ML has remained open for a long time.

After 2007/2008, I always thought that we should use more concrete syntax

(namely inner syntax).After rethinking it thoroughly, the outcome is now as above. The key idea is

to nest ML source inside antiquotations: this has become possible in recent

antiquotations \<^try>‹expr› and \<^can>‹expr›.The result looks a bit like enhanced S-expressions from the old LISP days:

this fits perfectly well into the idea of antiquotations and nesting of

sublanguages via cartouches --- instead of lots of silly parentheses.

So my counter feature request: Can you upgrade your applications to the new ML

antiquotations, and remove your attempt?

Looking briefly at actual uses of @{mpat} in AFP, most of them look very basic.

Here is an example at the upper end in complexity, translated into the new

Type/Const/Const_ scheme:

ML ‹

(*

fun constraints_of_goal i st =

case Logic.concl_of_goal (Thm.prop_of st) i of

@{mpat "Trueprop ((_,?a)∈_)"} => constraints_of_term a

| _ => raise THM ("constraints_of_goal",i,[st])

*)

val constraints_of_term: term -> (term * term) list = undefined;

fun constraints_of_goal i st =

case Logic.concl_of_goal (Thm.prop_of st) i of

\<^Const_>‹Trueprop for ‹\<^Const_>‹Set.member _ for ‹\<^Const_>‹Pair _
_ for _ a›› _››› =>

constraints_of_term a

| _ => raise THM ("constraints_of_goal",i,[st])

›

Most other uses will be even easier to rephrase.

Makarius

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Peter Lammich <lammich@in.tum.de>

Here is an example at the upper end in complexity, translated into

the new

Type/Const/Const_ scheme:ML ‹

(*

fun constraints_of_goal i st =

case Logic.concl_of_goal (Thm.prop_of st) i of

@{mpat "Trueprop ((_,?a)∈_)"} => constraints_of_term a

| _ => raise THM ("constraints_of_goal",i,[st])

*)val constraints_of_term: term -> (term * term) list = undefined;

fun constraints_of_goal i st =

case Logic.concl_of_goal (Thm.prop_of st) i of

\<^Const_>‹Trueprop for ‹\<^Const_>‹Set.member _ for

‹\<^Const_>‹Pair _ _ for _ a›› _››› =>

constraints_of_term a

| _ => raise THM ("constraints_of_goal",i,[st])

›

Unfortunately, the translation sacrifices quite some readability. In my

latest developments (not yet in AFP), I'd use @{mprop "(_,?a)∈_"} for

the above pattern, which is even more concise.

Btw, the upper end of complexity for term creation @{mk_term} is

something like:

@{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}

which looks like a lot of effort to write down in plain ML, or with

basic Const antiquotations. In particular, note that all types in the

term need to be inferred from the types of ?p and ?t'.

From: Makarius <makarius@sketis.net>

Here is the direct correspondence to the new antiquotations:

theory Scratch

imports Refine_Imperative_HOL.Sepref_Rules Refine_Imperative_HOL.Sepref_Monadify

begin

ML ‹

fn p => fn t' =>

@{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}›

ML ‹

fn A => fn B => fn p => fn t' =>

\<^Const>‹Refine_Basic.bind A B for

‹\<^Const>‹RETURN A for ‹\<^Const>‹COPY A for p›››› t'›

›

end

Of course, this needs to be viewed in Isabelle/jEdit, to make the \<^Const>

symbol look nice.

Note that the explicit data-flow concerning the type parameters (for Type and

Const likewise) is intentional: it is the key information without extra

redundancy; it is provided statically from the program structure, instead of

doing Term.fastype_of again at run-time (like your mk_term antiquotation).

That operation is actually called "fastype_of", because re-checking the type

of a term is very slow, but here a few extra checks are omitted compared to

full Term.type_of (this works under the assumption that the term is well-typed).

If we do manage to brush-up our thinking and working with types and terms, we

could get a somewhat smoother system within a few years. See also the thread

on locale performance opened by Norber Schirmer

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-September/msg00034.html

Makarius

isabelle-dev mailing list

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

Excellent!

The abstraction form syntax is not so trivial to grasp, maybe one

example coulde be added to the NEWS, e. g.

val dest_add_nat = \<^Const_fn>‹Groups.plus \<^Type>‹nat› for a b =>

‹(a, b)››

Florian

OpenPGP_signature

From: Makarius <makarius@sketis.net>

In Isabelle/b9331caf92c3, I have updated the above examples using

Type_fn/Const_fn (they were from an earlier stage, before these extra

antiquotations).

Also note that in Isabelle/e585e5a906ba, I have tune the syntax to allow the

\<^Type>‹nat› in your example stand on its own, without an extra cartouche

around it.

Makarius

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Makarius <makarius@sketis.net>

Update for Isabelle/e585e5a906ba:

theory Scratch

imports Refine_Imperative_HOL.Sepref_Rules Refine_Imperative_HOL.Sepref_Monadify

begin

ML ‹

fn p => fn t' =>

@{mk_term "Refine_Basic.bind$(RETURN$(COPY$?p))$?t'"}›

ML ‹

fn A => fn B => fn p => fn t' =>

\<^Const>‹Refine_Basic.bind A B for

\<^Const>‹RETURN A for \<^Const>‹COPY A for p›› t'›

›

end

Thus it is a bit more concise and to the point: no extra nesting of cartouches.

Are there any remaining uses of your alternative antiquotations that are not

covered properly by the new official scheme?

Makarius

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Norbert Schirmer <nschirmer@apple.com>

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

From: Makarius <makarius@sketis.net>

On 02/10/2021 10:51, Norbert Schirmer wrote:

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_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_Tests.thy

I have looked through this a bit, with the same questions in mind: What are

the remaining uses of these @{mk_term} and @{term_pat} antiquotations? Would

these antiquotations be introduced today, as replacement or improvement over

the new \<^Type> and \<^Const> forms?

My impressions so far:

* @{term_pat} is potentially more relevant, but hardly used in that code

base at all. Most applications are actually tests, to demonstrate what it is

supposed to be. It could be very easily eliminated and simplified, using the

new antiquotations from Isabelle2021-1.

* @{mk_term} has more actual applications, but about 30% very basic that

could be done with the same amount of text with \<^Type> and \<^Const>; 30%

involve relatively complex terms like this:

@{mk_term "ran (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const

|> Thm.cterm_of ctxt

It might be actually better to produce a closed @{cterm} with lambdas inside,

and use cterm application in ML --- it would avoid rechecking the whole cterm.

Moreover, the antiquotation itself contains hidden Term.fastype_of: another

relatively costly operation (for complex terms).

The whole point of the new \<^Const> antiquotation is to cultivate a view of

Consts.typargs almost everywhere, with very little recomputation of types for

subterms (no more Term.fastype_of).

This technique also has the potential to simplify the ML source complexity, at

least in the most common cases. Sometimes there are tough situations seen in

the wild, where ML operates in rather non-standard ways on terms, like working

morally ill-typed constants.

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.

That is a separate concern, independent of the question of concrete term

syntax vs. abstract ML syntax.

We do waste a lot in frequent ctyp_of/cterm_of operations, but doing it

differently is quite a lot of work.

Also note that the cterm destructors are not for free either. In particular,

Thm.dest_abs needs to replace a de-Bruijn Bound by a fresh Free. Over the

years I have fine-tuned this a lot, with measurable impact; the latest update

is here:

https://isabelle.sketis.net/repos/isabelle/annotate/21a20b990724/src/Pure/term.ML#l966

(Staring at this again, I immediately see further potential for improvement,

like an explicit Name.context as argument, taken from the implicit

Proof.context of the application.)

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.

The state-of-the art is to decompose the Thm.term_of view of cterms and

re-certify. The cost for that is well-known, but could be trimmed down a bit

by treating the types within terms more carefully (or by reducing them via

Consts.typargs as hinted above).

Having antiquotations for cterms can be a powerful show-case for the potential

of antiquotations, bringing together readability / conciseness as well as

scalability.

This sounds like marketing-speak.

Note that too much complexity in ML antiquotations can degrade the robustness

and maintainability of ML tools. For example, too much concrete syntax will

lead to surprises after inevitable changes of abbreviations, translations etc.

over the years / decades.

With \<^Type> / \<^Const> everything is clear and well-defined.

Makarius

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Norbert Schirmer <nschirmer@apple.com>

On 13. Oct 2021, at 23:05, Makarius <makarius@sketis.net> wrote:

My impressions so far:

@{term_pat} is potentially more relevant, but hardly used in that code

base at all. Most applications are actually tests, to demonstrate what it is

supposed to be. It could be very easily eliminated and simplified, using the

new antiquotations from Isabelle2021-1.@{mk_term} has more actual applications, but about 30% very basic that

could be done with the same amount of text with \<^Type> and \<^Const>; 30%

involve relatively complex terms like this:@{mk_term "ran (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const

|> Thm.cterm_of ctxtIt might be actually better to produce a closed @{cterm} with lambdas inside,

and use cterm application in ML --- it would avoid rechecking the whole cterm.Moreover, the antiquotation itself contains hidden Term.fastype_of: another

relatively costly operation (for complex terms).

Meanwhile there are many more applications of the two antiquotations.

We plan to release these extensions of the AutoCorres code-base following Isabelle2021-1.

The whole point of the new \<^Const> antiquotation is to cultivate a view of

Consts.typargs almost everywhere, with very little recomputation of types for

subterms (no more Term.fastype_of).You are right with the cost of Term.fastype_of. But many use-cases of

@{mk_term} are situations where the term size is under control of the actual code.

There is no additional user-space input coming in. E.g. think of something like the

@{command record} where you have to generate lots of lemmas about

field lookup / update etc. There something like @{mk_term} leads to very readable and compact code

to generate the terms for the propositions.

Having antiquotations for cterms can be a powerful show-case for the potential

of antiquotations, bringing together readability / conciseness as well as

scalability.This sounds like marketing-speak.

What I like about the application here is that the antiquation in a sense stretches the type-system of ML.

What results in a sequence of combinator applications becomes an atomic entity.

Note that too much complexity in ML antiquotations can degrade the robustness

and maintainability of ML tools. For example, too much concrete syntax will

lead to surprises after inevitable changes of abbreviations, translations etc.

over the years / decades.With \<^Type> / \<^Const> everything is clear and well-defined.

That is certainly true. The more syntax is involved the more can go wrong. But in my experience with these antiquotation so far this

falls in the category of “benign” issues. Meaning that you will hit the problem quite early. In the best case

already at compile time. Or if that does not work the problem manifests upon every and thus already the first actual usage of the antiquotation.

In those situations the benefits of a readable and concise term overweight.

Norbert

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Peter Lammich <lammich@in.tum.de>

Hi all.

The whole point of the new \<^Const> antiquotation is to cultivate

a view of

Consts.typargs almost everywhere, with very little recomputation of

types for

subterms (no more Term.fastype_of).You are right with the cost of Term.fastype_of. But many use-cases of

@{mk_term} are situations where the term size is under control of the

actual code.

There is no additional user-space input coming in. E.g. think of

something like the

@{command record} where you have to generate lots of lemmas about

field lookup / update etc. There something like @{mk_term} leads to

very readable and compact code

to generate the terms for the propositions.

I'm also, in many cases, in favour of clear and readable code over

efficient and less readable. (That's the reason why we use functional

programming for Isabelle, in first place!)

the potential

of antiquotations, bringing together readability / conciseness as

well as

scalability.This sounds like marketing-speak.

What I like about the application here is that the antiquation in a

sense stretches the type-system of ML.

What results in a sequence of combinator applications becomes an

atomic entity.Note that too much complexity in ML antiquotations can degrade the

robustness

and maintainability of ML tools. For example, too much concrete

syntax will

lead to surprises after inevitable changes of abbreviations,

translations etc.

over the years / decades.With \<^Type> / \<^Const> everything is clear and well-defined.

That is certainly true. The more syntax is involved the more can go

wrong. But in my experience with these antiquotation so far this

falls in the category of “benign” issues. Meaning that you will hit

the problem quite early. In the best case

already at compile time. Or if that does not work the problem

manifests upon every and thus already the first actual usage of the

antiquotation.

In those situations the benefits of a readable and concise term

overweight.

I agree here.

Me, personally, am not yet convinced to switch from the very consise

and high-level mk_term / mpat to the still more verbose and low-level

Type/Const. Obviously, I would like to improve these high-level

concepts, but not at the cost of readability or conciseness, which is

exactly what makes them so appealing.

Peter

Norbert

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Makarius <makarius@sketis.net>

The new \<^Type> / \<^Const> antiquotations are designed to be both

efficient in the runtime, and efficient in the source text (readable,

maintainable).

As usual, it is just a matter to get used to a new way of thinking,

which is actually closer to the old way of direct use of datatype

constructors.

Moreover, the treatment of type arguments is much more concise: the term

(patterns) are rather awkward in that respect: both in the text and at

runtime (fastype_of).

This thread was mainly meant to figure out shortcomings that can be

improved further: this often becomes apparent in concrete use, e.g.

while converting an application to the new format.

(Doing that here and there, I did already see another are of reform,

namely "instantiate" forms for thm, cterm, maybe even term.)

Makarius

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

From: Peter Lammich <lammich@in.tum.de>

On Thu, 2021-10-14 at 10:06 +0200, Makarius wrote:

On 14.10.21 09:49, Peter Lammich wrote:

I'm also, in many cases, in favour of clear and readable code over

efficient and less readable. (That's the reason why we use

functional

programming for Isabelle, in first place!)The new \<^Type> / \<^Const> antiquotations are designed to be both

efficient in the runtime, and efficient in the source text (readable,

maintainable).

but they are clearly less concise than mk_term/pat, at least for some

applications.

The usage of mk_term/pat, and the fact that it has been invented at

least twice independently, indicates that there is some sweet spot

here, which, at least for some use cases, allows a very concise

notation.

This still has some problems in other cases (e.g., treatment of types).

However, this should not be a reason for abandoning this promising

find, but to try to understand it further: in what cases is use of

mk_term/pat adequate, and in what cases do we have to fall back to the

more low-level but robust/general Type/Const. Can we even have both:

the benefit of concise treatment of type arguments AND the benefit of

concise, high-level notation?

From: Makarius <makarius@sketis.net>

All these attempts are rather fragile and incomplete. Over a long time, I used

to tell the story myself, that we should use inner syntax for term patterns

and it never quite worked out.

There are various dimensions in the problem that should not be collapsed:

* Patterns should be considered separately from expressions (but: the new

\<^Type>/\<^Const> antiquotations are so elementary and close to ML that they

can do both).

* Expressions can be easily used with concrete syntax, e.g. a version of

@{term} / @{cterm} / @{thm} combined with instantiation (Thm.instantiate): I

have started to think about that some weeks ago, and might manage to do

something for the release. This will supersede earlier attempts like @{mk_term}.

* Genuine cterms are probably better treated like the core logic does, e.g.

with Thm.match / Thm.first_order_match. Instead of raw decomposition of cterms

(with awkward invention of frees for bounds), regular matching can treat

binders directly.

Makarius

isabelle-dev@in.tum.de

https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Sep 09 2024 at 08:25 UTC