summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 29 Oct 2021 11:57:49 +0200 | |

changeset 74619 | e495ab64c694 |

parent 74618 | 43142ac556e6 |

child 74620 | d622d1dce05c |

added Thm.instantiate_beta;
tuned;

--- a/NEWS Thu Oct 28 06:39:36 2021 +0000 +++ b/NEWS Fri Oct 29 11:57:49 2021 +0200 @@ -340,9 +340,39 @@ adoption; better use TVars.add, TVars.add_tfrees etc. for scalable accumulation of items. -* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to -corresponding functions for the object-logic of the ML compilation -context. This supersedes older mk_Trueprop / dest_Trueprop operations. +* Thm.instantiate_beta applies newly emerging abstractions to their +arguments in the term, but leaves other beta-redexes unchanged --- in +contrast to Drule.instantiate_normalize. + +* 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. + +Newly emerging abstractions are applied to their arguments in the term +(using Thm.instantiate_beta). + +Examples in HOL: + + fun make_assoc_type (A, B) = + \<^instantiate>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>; + + val make_assoc_list = + map (fn (x, y) => + \<^instantiate>\<open>'a = \<open>fastype_of x\<close> and 'b = \<open>fastype_of y\<close> and + x and y in term \<open>(x, y)\<close> for x :: 'a and y :: 'b\<close>); + + fun symmetry x y = + \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y in + lemma \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close> + + fun symmetry_schematic A = + \<^instantiate>\<open>'a = A in + lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close> * ML antiquotations for type constructors and term constants: @@ -373,31 +403,9 @@ fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>; val dest_eq = \<^Const_fn>\<open>HOL.eq T for t u => \<open>(T, (t, u))\<close>\<close>; -* 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>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>; - - val make_assoc_list = - map (fn (x, y) => - \<^instantiate>\<open>'a = \<open>fastype_of x\<close> and 'b = \<open>fastype_of y\<close> and - x and y in term \<open>(x, y)\<close> for x :: 'a and y :: 'b\<close>); - - fun symmetry x y = - \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y in - lemma \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close> - - fun symmetry_schematic A = - \<^instantiate>\<open>'a = A in - lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close> +* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to +corresponding functions for the object-logic of the ML compilation +context. This supersedes older mk_Trueprop / dest_Trueprop operations. * The "build" combinators of various data structures help to build content from bottom-up, by applying an "add" function the "empty" value.