# HG changeset patch # User lcp # Date 799495461 -7200 # Node ID 502a61cbf37b1c32353c4a55987d62e160403750 # Parent 53a0667e1cd228b27c313803174b76188bdc9a01 Covers defs and re-ordering of theory sections diff -r 53a0667e1cd2 -r 502a61cbf37b doc-src/Intro/advanced.tex --- a/doc-src/Intro/advanced.tex Wed May 03 11:58:40 1995 +0200 +++ b/doc-src/Intro/advanced.tex Wed May 03 12:04:21 1995 +0200 @@ -339,6 +339,7 @@ arities {\it arity declarations} consts {\it constant declarations} translations {\it translation declarations} +defs {\it constant definitions} rules {\it rule declarations} end ML {\it ML code} @@ -355,10 +356,11 @@ The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. -All the declaration parts can be omitted. In the simplest case, $T$ is -just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one -or more other theories, inheriting their types, constants, syntax, etc. -The theory \thydx{Pure} contains nothing but Isabelle's meta-logic. +All the declaration parts can be omitted or repeated and may appear in any +order, except that the {\ML} section must be last. In the simplest case, $T$ +is just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one or +more other theories, inheriting their types, constants, syntax, etc. The +theory \thydx{Pure} contains nothing but Isabelle's meta-logic. Each theory definition must reside in a separate file, whose name is the theory's with {\tt.thy} appended. For example, theory {\tt ListFn} resides @@ -387,11 +389,11 @@ for more details. -\subsection{Declaring constants and rules} +\subsection{Declaring constants, definitions and rules} \indexbold{constants!declaring}\index{rules!declaring} -Most theories simply declare constants and rules. The {\bf constant -declaration part} has the form +Most theories simply declare constants, definitions and rules. The {\bf + constant declaration part} has the form \begin{ttbox} consts \(c@1\) :: "\(\tau@1\)" \vdots @@ -415,21 +417,22 @@ $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be enclosed in quotation marks. -\indexbold{definitions} -{\bf Definitions} are rules of the form $t\equiv u$. Normally definitions -should be conservative, serving only as abbreviations. As of this writing, -Isabelle does not provide a separate declaration part for definitions; it -is your responsibility to ensure that your definitions are conservative. -However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all -variables free in~$u$ are also free in~$t$. +\indexbold{definitions} The {\bf definition part} is similar, but with the +keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are rules of the +form $t\equiv u$, and should serve only as abbreviations. Isabelle checks for +common errors in definitions, such as extra variables on the right-hard side. +Determined users can write non-conservative `definitions' by using mutual +recursion, for example; the consequences of such actions are their +responsibility. -\index{examples!of theories} -This theory extends first-order logic with two constants {\em nand} and -{\em xor}, and declares rules to define them: + +\index{examples!of theories} +This theory extends first-order logic by declaring and defining two constants, +{\em nand} and {\em xor}: \begin{ttbox} Gate = FOL + consts nand,xor :: "[o,o] => o" -rules nand_def "nand(P,Q) == ~(P & Q)" +defs nand_def "nand(P,Q) == ~(P & Q)" xor_def "xor(P,Q) == P & ~Q | ~P & Q" end \end{ttbox} @@ -555,7 +558,7 @@ Gate2 = FOL + consts "~&" :: "[o,o] => o" (infixl 35) "#" :: "[o,o] => o" (infixl 30) -rules nand_def "P ~& Q == ~(P & Q)" +defs nand_def "P ~& Q == ~(P & Q)" xor_def "P # Q == P & ~Q | ~P & Q" end \end{ttbox} @@ -614,7 +617,7 @@ Binary type constructors, like products and sums, may also be declared as infixes. The type declaration below introduces a type constructor~$*$ with infix notation $\alpha*\beta$, together with the mixfix notation -${<}\_,\_{>}$ for pairs. +${<}\_,\_{>}$ for pairs. We also see a rule declaration part. \index{examples!of theories}\index{mixfix declarations} \begin{ttbox} Prod = FOL +