# HG changeset patch # User wenzelm # Date 1307380126 -7200 # Node ID 287182c2f23a980244acdd5c49d42e1c27d59ac1 # Parent 7860ffc5ec08fd3a396ff4a1290739568472df30 moved incr_boundvars; discontinued low-level term operations; diff -r 7860ffc5ec08 -r 287182c2f23a doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Jun 06 18:05:38 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Jun 06 19:08:46 2011 +0200 @@ -366,6 +366,7 @@ @{index_ML fastype_of: "term -> typ"} \\ @{index_ML lambda: "term -> term -> term"} \\ @{index_ML betapply: "term * term -> term"} \\ + @{index_ML incr_boundvars: "int -> term -> term"} \\ @{index_ML Sign.declare_const: "Proof.context -> (binding * typ) * mixfix -> theory -> term * theory"} \\ @{index_ML Sign.add_abbrev: "string -> binding * term -> @@ -414,6 +415,12 @@ "t u"}, with topmost @{text "\"}-conversion if @{text "t"} is an abstraction. + \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling + bound variables by the offset @{text "j"}. This is required when + moving a subterm into a context where it is enclosed by a different + number of abstractions. Bound variables with a matching abstraction + are unaffected. + \item @{ML Sign.declare_const}~@{text "ctxt ((c, \), mx)"} declares a new constant @{text "c :: \"} with optional mixfix syntax. diff -r 7860ffc5ec08 -r 287182c2f23a doc-src/IsarImplementation/Thy/document/Logic.tex --- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Jun 06 18:05:38 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Jun 06 19:08:46 2011 +0200 @@ -404,6 +404,7 @@ \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\ \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\ \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\ + \indexdef{}{ML}{incr\_boundvars}\verb|incr_boundvars: int -> term -> term| \\ \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline% \verb| (binding * typ) * mixfix -> theory -> term * theory| \\ \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline% @@ -444,6 +445,12 @@ \item \verb|betapply|~\isa{{\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}} produces an application \isa{t\ u}, with topmost \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion if \isa{t} is an abstraction. + \item \verb|incr_boundvars|~\isa{j} increments a term's dangling + bound variables by the offset \isa{j}. This is required when + moving a subterm into a context where it is enclosed by a different + number of abstractions. Bound variables with a matching abstraction + are unaffected. + \item \verb|Sign.declare_const|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax. diff -r 7860ffc5ec08 -r 287182c2f23a doc-src/Ref/Makefile --- a/doc-src/Ref/Makefile Mon Jun 06 18:05:38 2011 +0200 +++ b/doc-src/Ref/Makefile Mon Jun 06 19:08:46 2011 +0200 @@ -10,7 +10,7 @@ NAME = ref FILES = ref.tex introduction.tex tactic.tex tctical.tex thm.tex \ - theories.tex defining.tex syntax.tex substitution.tex \ + defining.tex syntax.tex substitution.tex \ simplifier.tex classical.tex ../proof.sty ../iman.sty \ ../extra.sty ../ttbox.sty ../manual.bib diff -r 7860ffc5ec08 -r 287182c2f23a doc-src/Ref/ref.tex --- a/doc-src/Ref/ref.tex Mon Jun 06 18:05:38 2011 +0200 +++ b/doc-src/Ref/ref.tex Mon Jun 06 19:08:46 2011 +0200 @@ -36,11 +36,9 @@ \subsubsection*{Acknowledgements} Tobias Nipkow, of T. U. Munich, wrote most of - Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}, - and part of - Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to - Chapter~\protect\ref{theories}. Markus Wenzel contributed to - Chapter~\protect\ref{chap:syntax}. Jeremy Dawson, Sara Kalvala, Martin + Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}. + Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}. + Jeremy Dawson, Sara Kalvala, Martin Simons and others suggested changes and corrections. The research has been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT @@ -53,7 +51,6 @@ \include{tactic} \include{tctical} \include{thm} -\include{theories} \include{defining} \include{syntax} \include{substitution} diff -r 7860ffc5ec08 -r 287182c2f23a doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Mon Jun 06 18:05:38 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ - -\chapter{Terms} - -\section{*Variable binding} -\begin{ttbox} -loose_bnos : term -> int list -incr_boundvars : int -> term -> term -abstract_over : term*term -> term -variant_abs : string * typ * term -> string * term -\end{ttbox} -These functions are all concerned with the de Bruijn representation of -bound variables. -\begin{ttdescription} -\item[\ttindexbold{loose_bnos} $t$] - returns the list of all dangling bound variable references. In - particular, \texttt{Bound~0} is loose unless it is enclosed in an - abstraction. Similarly \texttt{Bound~1} is loose unless it is enclosed in - at least two abstractions; if enclosed in just one, the list will contain - the number 0. A well-formed term does not contain any loose variables. - -\item[\ttindexbold{incr_boundvars} $j$] - increases a term's dangling bound variables by the offset~$j$. This is - required when moving a subterm into a context where it is enclosed by a - different number of abstractions. Bound variables with a matching - abstraction are unaffected. - -\item[\ttindexbold{abstract_over} $(v,t)$] - forms the abstraction of~$t$ over~$v$, which may be any well-formed term. - It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the - correct index. - -\item[\ttindexbold{variant_abs} $(a,T,u)$] - substitutes into $u$, which should be the body of an abstraction. - It replaces each occurrence of the outermost bound variable by a free - variable. The free variable has type~$T$ and its name is a variant - of~$a$ chosen to be distinct from all constants and from all variables - free in~$u$. - -\end{ttdescription} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "ref" -%%% End: