291 declaration forms are discussed below. There are some more sections |
291 declaration forms are discussed below. There are some more sections |
292 not presented here, the full syntax can be found in |
292 not presented here, the full syntax can be found in |
293 \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference |
293 \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference |
294 Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that |
294 Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that |
295 object-logics may add further theory sections, for example |
295 object-logics may add further theory sections, for example |
296 \texttt{typedef}, \texttt{datatype} in \HOL. |
296 \texttt{typedef}, \texttt{datatype} in HOL. |
297 |
297 |
298 All the declaration parts can be omitted or repeated and may appear in |
298 All the declaration parts can be omitted or repeated and may appear in |
299 any order, except that the {\ML} section must be last (after the {\tt |
299 any order, except that the {\ML} section must be last (after the {\tt |
300 end} keyword). In the simplest case, $T$ is just the union of |
300 end} keyword). In the simplest case, $T$ is just the union of |
301 $S@1$,~\ldots,~$S@n$. New theories always extend one or more other |
301 $S@1$,~\ldots,~$S@n$. New theories always extend one or more other |
302 theories, inheriting their types, constants, syntax, etc. The theory |
302 theories, inheriting their types, constants, syntax, etc. The theory |
303 \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant |
303 \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant |
304 \thydx{CPure} offers the more usual higher-order function application |
304 \thydx{CPure} offers the more usual higher-order function application |
305 syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure. |
305 syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure. |
306 |
306 |
307 Each theory definition must reside in a separate file, whose name is |
307 Each theory definition must reside in a separate file, whose name is |
308 the theory's with {\tt.thy} appended. Calling |
308 the theory's with {\tt.thy} appended. Calling |
309 \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it |
309 \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it |
310 T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it |
310 T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it |
962 \iflabelundefined{simp-chap}% |
962 \iflabelundefined{simp-chap}% |
963 {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}. |
963 {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}. |
964 |
964 |
965 \index{simplification}\index{examples!of simplification} |
965 \index{simplification}\index{examples!of simplification} |
966 |
966 |
967 Isabelle's simplification tactics repeatedly apply equations to a |
967 Isabelle's simplification tactics repeatedly apply equations to a subgoal, |
968 subgoal, perhaps proving it. For efficiency, the rewrite rules must |
968 perhaps proving it. For efficiency, the rewrite rules must be packaged into a |
969 be packaged into a {\bf simplification set},\index{simplification |
969 {\bf simplification set},\index{simplification sets} or {\bf simpset}. We |
970 sets} or {\bf simpset}. We augment the implicit simpset of {\FOL} |
970 augment the implicit simpset of FOL with the equations proved in the previous |
971 with the equations proved in the previous section, namely $0+n=n$ and |
971 section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$: |
972 $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$: |
|
973 \begin{ttbox} |
972 \begin{ttbox} |
974 Addsimps [add_0, add_Suc]; |
973 Addsimps [add_0, add_Suc]; |
975 \end{ttbox} |
974 \end{ttbox} |
976 We state the goal for associativity of addition, and |
975 We state the goal for associativity of addition, and |
977 use \ttindex{res_inst_tac} to invoke induction on~$k$: |
976 use \ttindex{res_inst_tac} to invoke induction on~$k$: |