changeset 1084 502a61cbf37b parent 841 14b96e3bd4ab child 1185 9968989790e2
equal inserted replaced
1083:53a0667e1cd2 1084:502a61cbf37b
   337 default      {\it sort}
   337 default      {\it sort}
   338 types        {\it type declarations and synonyms}
   338 types        {\it type declarations and synonyms}
   339 arities      {\it arity declarations}
   339 arities      {\it arity declarations}
   340 consts       {\it constant declarations}
   340 consts       {\it constant declarations}
   341 translations {\it translation declarations}
   341 translations {\it translation declarations}

   342 defs         {\it constant definitions}
   342 rules        {\it rule declarations}
   343 rules        {\it rule declarations}
   343 end
   344 end
   344 ML           {\it ML code}
   345 ML           {\it ML code}
   345 \end{ttbox}
   346 \end{ttbox}
   346 This declares the theory $T$ to extend the existing theories
   347 This declares the theory $T$ to extend the existing theories
   353 The {\tt ML} section contains code to perform arbitrary syntactic
   354 The {\tt ML} section contains code to perform arbitrary syntactic
   354 transformations.  The main declaration forms are discussed below.
   355 transformations.  The main declaration forms are discussed below.
   355 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
   356 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
   356   appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
   357   appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
   357
   358
   358 All the declaration parts can be omitted.  In the simplest case, $T$ is
   359 All the declaration parts can be omitted or repeated and may appear in any
   359 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
   360 order, except that the {\ML} section must be last.  In the simplest case, $T$
   360 or more other theories, inheriting their types, constants, syntax, etc.
   361 is just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one or
   361 The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
   362 more other theories, inheriting their types, constants, syntax, etc.  The

   363 theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
   362
   364
   363 Each theory definition must reside in a separate file, whose name is the
   365 Each theory definition must reside in a separate file, whose name is the
   364 theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
   366 theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
   365 on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
   367 on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
   366 file containing a given theory; \ttindexbold{use_thy} automatically loads a
   368 file containing a given theory; \ttindexbold{use_thy} automatically loads a
   385 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
   387 \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
   386                  {\S\ref{sec:reloading-theories}}
   388                  {\S\ref{sec:reloading-theories}}
   387 for more details.
   389 for more details.
   388
   390
   389
   391
   390 \subsection{Declaring constants and rules}
   392 \subsection{Declaring constants, definitions and rules}
   391 \indexbold{constants!declaring}\index{rules!declaring}
   393 \indexbold{constants!declaring}\index{rules!declaring}
   392
   394
   393 Most theories simply declare constants and rules.  The {\bf constant
   395 Most theories simply declare constants, definitions and rules.  The {\bf
   394 declaration part} has the form
   396   constant declaration part} has the form
   395 \begin{ttbox}
   397 \begin{ttbox}
   396 consts  $$c@1$$ :: "$$\tau@1$$"
   398 consts  $$c@1$$ :: "$$\tau@1$$"
   397         \vdots
   399         \vdots
   398         $$c@n$$ :: "$$\tau@n$$"
   400         $$c@n$$ :: "$$\tau@n$$"
   399 \end{ttbox}
   401 \end{ttbox}
   413 \end{ttbox}
   415 \end{ttbox}
   414 where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
   416 where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
   415 $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
   417 $rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
   416 enclosed in quotation marks.
   418 enclosed in quotation marks.
   417
   419
   418 \indexbold{definitions}
   420 \indexbold{definitions} The {\bf definition part} is similar, but with the
   419 {\bf Definitions} are rules of the form $t\equiv u$.  Normally definitions
   421 keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are rules of the
   420 should be conservative, serving only as abbreviations.  As of this writing,
   422 form $t\equiv u$, and should serve only as abbreviations.  Isabelle checks for
   421 Isabelle does not provide a separate declaration part for definitions; it
   423 common errors in definitions, such as extra variables on the right-hard side.
   422 is your responsibility to ensure that your definitions are conservative.
   424 Determined users can write non-conservative definitions' by using mutual
   423 However, Isabelle's rewriting primitives will reject $t\equiv u$ unless all
   425 recursion, for example; the consequences of such actions are their
   424 variables free in~$u$ are also free in~$t$.
   426 responsibility.
   425 
   427 
   426 \index{examples!of theories}
   428 
   427 This theory extends first-order logic with two constants {\em nand} and
   429 \index{examples!of theories} 
   428 {\em xor}, and declares rules to define them:
   430 This theory extends first-order logic by declaring and defining two constants,
       
   431 {\em nand} and {\em xor}:
   429 \begin{ttbox}
   432 \begin{ttbox}
   430 Gate = FOL +
   433 Gate = FOL +
   431 consts  nand,xor :: "[o,o] => o"
   434 consts  nand,xor :: "[o,o] => o"
   432 rules   nand_def "nand(P,Q) == ~(P & Q)"
   435 defs    nand_def "nand(P,Q) == ~(P & Q)"
   433         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   436         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   434 end
   437 end
   435 \end{ttbox}
   438 \end{ttbox}
   436 
   439 
   437 
   440 
   553 following theory:
   556 following theory:
   554 \begin{ttbox}
   557 \begin{ttbox}
   555 Gate2 = FOL +
   558 Gate2 = FOL +
   556 consts  "~&"     :: "[o,o] => o"         (infixl 35)
   559 consts  "~&"     :: "[o,o] => o"         (infixl 35)
   557         "#"      :: "[o,o] => o"         (infixl 30)
   560         "#"      :: "[o,o] => o"         (infixl 30)
   558 rules   nand_def "P ~& Q == ~(P & Q)"    
   561 defs    nand_def "P ~& Q == ~(P & Q)"    
   559         xor_def  "P # Q  == P & ~Q | ~P & Q"
   562         xor_def  "P # Q  == P & ~Q | ~P & Q"
   560 end
   563 end
   561 \end{ttbox}
   564 \end{ttbox}
   562 The constant declaration part declares two left-associating infix operators
   565 The constant declaration part declares two left-associating infix operators
   563 with their priorities, or precedences; they are $\nand$ of priority~35 and
   566 with their priorities, or precedences; they are $\nand$ of priority~35 and
   612 because expressions in parentheses have maximal priority.  
   615 because expressions in parentheses have maximal priority.  
   613 
   616 
   614 Binary type constructors, like products and sums, may also be declared as
   617 Binary type constructors, like products and sums, may also be declared as
   615 infixes.  The type declaration below introduces a type constructor~$*$ with
   618 infixes.  The type declaration below introduces a type constructor~$*$ with
   616 infix notation $\alpha*\beta$, together with the mixfix notation
   619 infix notation $\alpha*\beta$, together with the mixfix notation
   617 ${<}\_,\_{>}$ for pairs.  
   620 ${<}\_,\_{>}$ for pairs.  We also see a rule declaration part.
   618 \index{examples!of theories}\index{mixfix declarations}
   621 \index{examples!of theories}\index{mixfix declarations}
   619 \begin{ttbox}
   622 \begin{ttbox}
   620 Prod = FOL +
   623 Prod = FOL +
   621 types   ('a,'b) "*"                           (infixl 20)
   624 types   ('a,'b) "*"                           (infixl 20)
   622 arities "*"     :: (term,term)term
   625 arities "*"     :: (term,term)term`