moved incr_boundvars;
authorwenzelm
Mon Jun 06 19:08:46 2011 +0200 (2011-06-06)
changeset 42934287182c2f23a
parent 42933 7860ffc5ec08
child 42935 e68c3861b8db
moved incr_boundvars;
discontinued low-level term operations;
doc-src/IsarImplementation/Thy/Logic.thy
doc-src/IsarImplementation/Thy/document/Logic.tex
doc-src/Ref/Makefile
doc-src/Ref/ref.tex
doc-src/Ref/theories.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Mon Jun 06 18:05:38 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Jun 06 19:08:46 2011 +0200
     1.3 @@ -366,6 +366,7 @@
     1.4    @{index_ML fastype_of: "term -> typ"} \\
     1.5    @{index_ML lambda: "term -> term -> term"} \\
     1.6    @{index_ML betapply: "term * term -> term"} \\
     1.7 +  @{index_ML incr_boundvars: "int -> term -> term"} \\
     1.8    @{index_ML Sign.declare_const: "Proof.context ->
     1.9    (binding * typ) * mixfix -> theory -> term * theory"} \\
    1.10    @{index_ML Sign.add_abbrev: "string -> binding * term ->
    1.11 @@ -414,6 +415,12 @@
    1.12    "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
    1.13    abstraction.
    1.14  
    1.15 +  \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling
    1.16 +  bound variables by the offset @{text "j"}.  This is required when
    1.17 +  moving a subterm into a context where it is enclosed by a different
    1.18 +  number of abstractions.  Bound variables with a matching abstraction
    1.19 +  are unaffected.
    1.20 +
    1.21    \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
    1.22    a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    1.23  
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Jun 06 18:05:38 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Jun 06 19:08:46 2011 +0200
     2.3 @@ -404,6 +404,7 @@
     2.4    \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
     2.5    \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
     2.6    \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
     2.7 +  \indexdef{}{ML}{incr\_boundvars}\verb|incr_boundvars: int -> term -> term| \\
     2.8    \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline%
     2.9  \verb|  (binding * typ) * mixfix -> theory -> term * theory| \\
    2.10    \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
    2.11 @@ -444,6 +445,12 @@
    2.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
    2.13    abstraction.
    2.14  
    2.15 +  \item \verb|incr_boundvars|~\isa{j} increments a term's dangling
    2.16 +  bound variables by the offset \isa{j}.  This is required when
    2.17 +  moving a subterm into a context where it is enclosed by a different
    2.18 +  number of abstractions.  Bound variables with a matching abstraction
    2.19 +  are unaffected.
    2.20 +
    2.21    \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
    2.22    a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax.
    2.23  
     3.1 --- a/doc-src/Ref/Makefile	Mon Jun 06 18:05:38 2011 +0200
     3.2 +++ b/doc-src/Ref/Makefile	Mon Jun 06 19:08:46 2011 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  NAME = ref
     3.6  FILES = ref.tex introduction.tex tactic.tex tctical.tex thm.tex	\
     3.7 -	theories.tex defining.tex syntax.tex substitution.tex	\
     3.8 +	defining.tex syntax.tex substitution.tex	\
     3.9  	simplifier.tex classical.tex ../proof.sty ../iman.sty	\
    3.10  	../extra.sty ../ttbox.sty ../manual.bib
    3.11  
     4.1 --- a/doc-src/Ref/ref.tex	Mon Jun 06 18:05:38 2011 +0200
     4.2 +++ b/doc-src/Ref/ref.tex	Mon Jun 06 19:08:46 2011 +0200
     4.3 @@ -36,11 +36,9 @@
     4.4  
     4.5  \subsubsection*{Acknowledgements} 
     4.6  Tobias Nipkow, of T. U. Munich, wrote most of
     4.7 -  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
     4.8 -  and part of
     4.9 -  Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
    4.10 -  Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
    4.11 -  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
    4.12 +  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification}.
    4.13 +  Markus Wenzel contributed to Chapter~\protect\ref{chap:syntax}.
    4.14 +  Jeremy Dawson, Sara Kalvala, Martin
    4.15    Simons  and others suggested changes
    4.16    and corrections.  The research has been funded by the EPSRC (grants
    4.17    GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
    4.18 @@ -53,7 +51,6 @@
    4.19  \include{tactic}
    4.20  \include{tctical}
    4.21  \include{thm}
    4.22 -\include{theories}
    4.23  \include{defining}
    4.24  \include{syntax}
    4.25  \include{substitution}
     5.1 --- a/doc-src/Ref/theories.tex	Mon Jun 06 18:05:38 2011 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,44 +0,0 @@
     5.4 -
     5.5 -\chapter{Terms}
     5.6 -
     5.7 -\section{*Variable binding}
     5.8 -\begin{ttbox}
     5.9 -loose_bnos     : term -> int list
    5.10 -incr_boundvars : int -> term -> term
    5.11 -abstract_over  : term*term -> term
    5.12 -variant_abs    : string * typ * term -> string * term
    5.13 -\end{ttbox}
    5.14 -These functions are all concerned with the de Bruijn representation of
    5.15 -bound variables.
    5.16 -\begin{ttdescription}
    5.17 -\item[\ttindexbold{loose_bnos} $t$]
    5.18 -  returns the list of all dangling bound variable references.  In
    5.19 -  particular, \texttt{Bound~0} is loose unless it is enclosed in an
    5.20 -  abstraction.  Similarly \texttt{Bound~1} is loose unless it is enclosed in
    5.21 -  at least two abstractions; if enclosed in just one, the list will contain
    5.22 -  the number 0.  A well-formed term does not contain any loose variables.
    5.23 -
    5.24 -\item[\ttindexbold{incr_boundvars} $j$]
    5.25 -  increases a term's dangling bound variables by the offset~$j$.  This is
    5.26 -  required when moving a subterm into a context where it is enclosed by a
    5.27 -  different number of abstractions.  Bound variables with a matching
    5.28 -  abstraction are unaffected.
    5.29 -
    5.30 -\item[\ttindexbold{abstract_over} $(v,t)$]
    5.31 -  forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
    5.32 -  It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the
    5.33 -  correct index.
    5.34 -
    5.35 -\item[\ttindexbold{variant_abs} $(a,T,u)$]
    5.36 -  substitutes into $u$, which should be the body of an abstraction.
    5.37 -  It replaces each occurrence of the outermost bound variable by a free
    5.38 -  variable.  The free variable has type~$T$ and its name is a variant
    5.39 -  of~$a$ chosen to be distinct from all constants and from all variables
    5.40 -  free in~$u$.
    5.41 -
    5.42 -\end{ttdescription}
    5.43 -
    5.44 -%%% Local Variables: 
    5.45 -%%% mode: latex
    5.46 -%%% TeX-master: "ref"
    5.47 -%%% End: