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

[Peter Lammich]

> 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'.

--
  Peter


> Most other uses will be even easier to rephrase.
> 
> 
> 	Makarius