49 |
49 |
50 \begin{descr} |
50 \begin{descr} |
51 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] |
51 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] |
52 defines extensible record type $(\vec\alpha)t$, derived from the optional |
52 defines extensible record type $(\vec\alpha)t$, derived from the optional |
53 parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. |
53 parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. |
54 See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only |
|
55 simply-typed extensible records. |
|
56 \end{descr} |
54 \end{descr} |
|
55 |
|
56 See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information only |
|
57 simply-typed extensible records. |
57 |
58 |
58 |
59 |
59 \section{Datatypes}\label{sec:datatype} |
60 \section{Datatypes}\label{sec:datatype} |
60 |
61 |
61 \indexisarcmd{datatype}\indexisarcmd{rep-datatype} |
62 \indexisarcmd{datatype}\indexisarcmd{rep-datatype} |
76 constructor: name (type * ) mixfix? comment? |
77 constructor: name (type * ) mixfix? comment? |
77 ; |
78 ; |
78 \end{rail} |
79 \end{rail} |
79 |
80 |
80 \begin{descr} |
81 \begin{descr} |
81 \item [$\isarkeyword{datatype}$] FIXME |
82 \item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. |
82 \item [$\isarkeyword{rep_datatype}$] FIXME |
83 \item [$\isarkeyword{rep_datatype}$] represents existing types as inductive |
|
84 ones, generating the standard infrastructure of derived concepts (primitive |
|
85 recursion etc.). |
83 \end{descr} |
86 \end{descr} |
|
87 |
|
88 See \cite{isabelle-HOL} for more details on datatypes. Note that the theory |
|
89 syntax above has been slightly simplified over the old version. |
84 |
90 |
85 |
91 |
86 \section{Recursive functions} |
92 \section{Recursive functions} |
87 |
93 |
88 \indexisarcmd{primrec}\indexisarcmd{recdef} |
94 \indexisarcmd{primrec}\indexisarcmd{recdef} |
99 'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)? |
105 'recdef' name term (term comment? +) \\ ('congs' thmrefs)? ('simpset' name)? |
100 ; |
106 ; |
101 \end{rail} |
107 \end{rail} |
102 |
108 |
103 \begin{descr} |
109 \begin{descr} |
104 \item [$\isarkeyword{primrec}$] FIXME |
110 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over |
105 \item [$\isarkeyword{recdef}$] FIXME |
111 datatypes. |
|
112 \item [$\isarkeyword{recdef}$] defines general well-founded recursive |
|
113 functions (using the TFL package). |
106 \end{descr} |
114 \end{descr} |
|
115 |
|
116 See \cite{isabelle-HOL} for more information. |
107 |
117 |
108 |
118 |
109 \section{(Co)Inductive sets} |
119 \section{(Co)Inductive sets} |
110 |
120 |
111 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases} |
121 \indexisarcmd{inductive}\indexisarcmd{coinductive}\indexisarcmd{inductive-cases} |
127 indcases thmdef? nameref ':' \\ (prop +) comment? |
137 indcases thmdef? nameref ':' \\ (prop +) comment? |
128 ; |
138 ; |
129 \end{rail} |
139 \end{rail} |
130 |
140 |
131 \begin{descr} |
141 \begin{descr} |
132 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] FIXME |
142 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define |
133 \item [$\isarkeyword{inductive_cases}$] FIXME |
143 (co)inductive sets from the given introduction rules. |
|
144 \item [$\isarkeyword{inductive_cases}$] creates simplified instances of |
|
145 elimination rules of (co)inductive sets. |
134 \end{descr} |
146 \end{descr} |
|
147 |
|
148 See \cite{isabelle-HOL} for more information. Note that |
|
149 $\isarkeyword{inductive_cases}$ corresponds to the ML function |
|
150 \texttt{mk_cases}. |
135 |
151 |
136 |
152 |
137 \section{Proof by induction} |
153 \section{Proof by induction} |
138 |
154 |
139 FIXME induct proof method |
155 \indexisarmeth{induct} |
|
156 \begin{matharray}{rcl} |
|
157 induct & : & \isarmeth \\ |
|
158 \end{matharray} |
|
159 |
|
160 The $induct$ method provides a uniform interface to induction over datatypes, |
|
161 inductive sets, and recursive functions. Basically, it is just an interface |
|
162 to the $rule$ method applied to appropriate instances of the corresponding |
|
163 induction rules. |
|
164 |
|
165 \begin{rail} |
|
166 'induct' (inst * 'and') kind? |
|
167 ; |
|
168 |
|
169 inst: term term? |
|
170 ; |
|
171 kind: ('type' | 'set' | 'function') ':' nameref |
|
172 ; |
|
173 \end{rail} |
|
174 |
|
175 \begin{descr} |
|
176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the |
|
177 induction rule of the type/set/function specified by $kind$ and instantiated |
|
178 by $insts$. The latter either consists of pairs $P$ $x$ (induction |
|
179 predicate and variable), where $P$ is optional. If $kind$ is omitted, the |
|
180 default is to pick a datatype induction rule according to the type of some |
|
181 induction variable (at least one has to be given in that case). |
|
182 \end{descr} |
140 |
183 |
141 |
184 |
142 %%% Local Variables: |
185 %%% Local Variables: |
143 %%% mode: latex |
186 %%% mode: latex |
144 %%% TeX-master: "isar-ref" |
187 %%% TeX-master: "isar-ref" |