Intro/document/foundations.tex

66 \index{types!syntax of}\index{types!function}\index{*fun type}
68 Isabelle has \ML-style polymorphic types such as~$(\alpha)list$, where
70 $(bool)list$ is the type of lists of booleans.  Function types have the
72 types.  Curried function types may be abbreviated:
94 \subsection{Simple types and constants}\index{types!simple|bold}
100 how to admit terms of other types.
103 After declaring the types~$o$ and~$nat$, we may declare constants for the
128 \subsection{Polymorphic types and constants} \label{polymorphic}
129 \index{types!polymorphic|bold}
140 where the type variable~$\alpha$ ranges over all types.
142 includes types like~$o$ and $nat\To nat$.  Thus, it admits
148 class, which denotes a set of types.  Classes are partially ordered by the
150 types.  They closely resemble the classes of the functional language
155 types: the ones we want to reason about.  Let us declare a class $term$, to
156 consist of all legal types of terms in our logic.  The subclass structure
169 We give~$o$ and function types the class $logic$ rather than~$term$, since
170 they are not legal types for terms.  We may introduce new types of class
183 (Recall that $fun$ is the type constructor for function types.)
188 subclass of $term$ consisting of the `arithmetic' types, such as~$nat$.
193 If we declare new types $real$ and $complex$ of class $arith$, then we
210 `ordered' types, and a constant
217 intersection of the sets of types represented by $arith$ and $ord$.  Such
219 intersection of classes, $\{\}$, contains all types and is thus the {\bf
230 \subsection{Higher types and quantifiers}
231 \index{types!higher|bold}\index{quantifiers}
252 all legal types of terms, not just the natural numbers, and
253 allow summations over all arithmetic types:
290 and $\tau$ do.  Here are the types of the built-in connectives:
298 certain types, those used just for parsing.  The type variable
303 we declared the object-level connectives to have types such as
305 meta-level formulae.  Keeping $prop$ and $o$ as separate types maintains
332 types denote sets and $\Forall$ really means `for all.'
434 relationships, types and their arities, constants and their types, etc.  It
438 they must not, for example, assign different types to the same constant.
446 types, constants and mixfix declarations --- plus lists of axioms and
578 are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be