Manual/Logic/syntax.tex

22 that because of context, no confusion results from these two uses of
291 type-in-context.
293 A {\em type context}\index{type context}, $\alpha\!s$, is simply a
296 type-in-context\/}\index{type-in-context} is a pair, written
297 $\alpha\!s.\sigma$, where $\alpha\!s$ is a type context, $\sigma$ is a
304 $\alpha\!s.\sigma$ is a type-in-context, which only differ by the order
306 order to select one such context, let us assume that  {\sf TyVars}
308 canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of types} context of the type $\sigma$ to consist of
316 type-in-context
321 (where $n$ is the length of the context) by induction on the structure
349 canonical context of $\sigma$. If $\sigma$ is monomorphic, then $n=0$
352 clear from the context, $\den{\_}_{M}$ will be written $\den{\_}$.
385 just that the context ties down the admissible domain to a particular
423 \noindent{\bf Lemma 2\ }{\it Given types-in-context $\beta\!s.\sigma$ and
427 type-in-context and its meaning in any model $M$ is related to that of
522 is clear from the context that $x$ is a variable rather than a
544 structure of the term or the context in which it occurs what its type
570 \subsection{Terms-in-context}
571 \label{terms-in-context}
573 A {\em context\/}\index{contexts, in semantics of HOL logic@contexts, in semantics of \HOL{} logic} $\alpha\!s,\!x\!s$ consists of a type
574 context $\alpha\!s$ together with a list $x\!s=x_{1},\ldots,x_{m}$ of
588 A {\em term-in-context\/}\index{term-in-context}
589 $\alpha\!s,\!x\!s.t$ consists of a context together with a term
601 The context $\alpha\!s,\!x\!s$ may contain (type) variables which do
613 for such a term there is a minimal context $\alpha\!s,\!x\!s$, unique
615 $\alpha\!s,\!x\!s.t$ is a term-in-context. As for type variables, we
617 minimal context with variables listed in order will be called the {\em
618 canonical}\index{canonical contexts, in HOL logic@canonical contexts, in \HOL{} logic!of terms} context of the term $t$.
648 U}$ is derived from the type of the term (in a type context derived
668 variables and the type of the term (in a type context derived from the
671 More precisely, given a term-in-context $\alpha\!s,\!x\!s.t$
682 Then since $\alpha\!s,\!x\!s.t$ is a term-in-context, $\alpha\!s.\tau$
683 and $\alpha\!s.\sigma_{j}$ are types-in-context, and hence give rise
704 clear from the context.)
745 $\alpha\!s,\!x\!s.t$ is a term-in-context, by convention the bound
747 $\alpha\!s,\!x\!s,\!x.t_{2}$ is also a term-in-context.)
756 canonical context of $t_{\tau}$. So $n$ is the number of type variables in
761 $\alpha\!s$, which is part of the canonical context of $t$, may be strictly
795 Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say,
799 types-in-context, then substituting\index{type substitution, in HOL logic@type substitution, in \HOL{} logic!formal semantics of} the types
811 This condition ensures that $\alpha\!s',x\!s'$ really is a context. Then
812 one obtains a new term-in-context $\alpha\!s',\!x\!s'.t'$ by
844 Suppose $t$ is a term, with canonical context $\alpha\!s,\!x\!s$ say,
847 $\sigma_j$. If one has terms-in-context $\alpha\!s,\!x\!s'.t_{j}$ for
849 $\sigma_{j}$, then one obtains a new term-in-context