1 |
1 |
2 The next examples illustrate advanced features of inductive definitions. |
2 This section describes advanced features of inductive definitions. |
3 The premises of introduction rules may contain universal quantifiers and |
3 The premises of introduction rules may contain universal quantifiers and |
4 monotonic functions. Theorems may be proved by rule inversion. |
4 monotonic functions. Theorems may be proved by rule inversion. |
5 |
5 |
6 \subsection{Universal quantifiers in introduction rules} |
6 \subsection{Universal quantifiers in introduction rules} |
7 \label{sec:gterm-datatype} |
7 \label{sec:gterm-datatype} |
8 |
8 |
9 A \textbf{ground} term is a term constructed from constant and function |
9 As a running example, this section develops the theory of \textbf{ground |
10 symbols alone: no variables. To simplify matters further, |
10 terms}: terms constructed from constant and function |
11 we regard a constant as a function applied to the null argument |
11 symbols but not variables. To simplify matters further, we regard a |
12 list. Let us declare a datatype \isa{gterm} for the type of ground |
12 constant as a function applied to the null argument list. Let us declare a |
13 terms. It is a type constructor whose argument is a type of |
13 datatype \isa{gterm} for the type of ground terms. It is a type constructor |
14 function symbols. |
14 whose argument is a type of function symbols. |
15 \begin{isabelle} |
15 \begin{isabelle} |
16 \isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list" |
16 \isacommand{datatype}\ 'f\ gterm\ =\ Apply\ 'f\ "'f\ gterm\ list" |
17 \end{isabelle} |
17 \end{isabelle} |
18 To try it out, we declare a datatype of some integer operations: |
18 To try it out, we declare a datatype of some integer operations: |
19 integer constants, the unary minus operator and the addition |
19 integer constants, the unary minus operator and the addition |