ML antiquotation "instantiate"
- 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.
Written by makarius on Oct 28 2021, 9:50 PM.