From: Makarius <makarius@sketis.net>

*** ML ***

- ML antiquotation "instantiate" allows to instantiate formal entities

(types, terms, theorems) with values given ML. This works uniformly for

"typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a

keyword after the instantiation. A mode "(schematic)" behind the keyword

means that some variables may remain uninstantiated (fixed in the

specification and schematic in the result); by default, all variables

need to be instantiated.

Examples in HOL:

fun make_assoc_type (A, B) =

\<^instantiate>‹'a = A and 'b = B in typ ‹('a × 'b) list››;

val make_assoc_list =

map (fn (x, y) =>

\<^instantiate>‹'a = ‹fastype_of x› and 'b = ‹fastype_of y› and

x and y in term ‹(x, y)› for x :: 'a and y :: 'b›);

fun symmetry x y =

\<^instantiate>‹'a = ‹Thm.ctyp_of_cterm x› and x and y in

lemma ‹x = y ⟹ y = x› for x y :: 'a by simp›

fun symmetry_schematic A =

\<^instantiate>‹'a = A in

lemma (schematic) ‹x = y ⟹ y = x› for x y :: 'a by simp›

This refers to Isabelle/54085e37ce4d. Some applications are in the preceeding

changesets.

Proper documentation will follow shortly after Isabelle2021-1-RC1 (start of

next week).

Makarius

isabelle-dev mailing list

isabelle-dev@in.tum.de

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

Last updated: Mar 04 2024 at 10:08 UTC