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 metalogic. 
362 more other theories, inheriting their types, constants, syntax, etc. The 

363 theory \thydx{Pure} contains nothing but Isabelle's metalogic. 
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:reloadingtheories}{the {\em Reference Manual\/}}% 
387 \iflabelundefined{sec:reloadingtheories}{the {\em Reference Manual\/}}% 
386 {\S\ref{sec:reloadingtheories}} 
388 {\S\ref{sec:reloadingtheories}} 
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 righthard side. 
422 is your responsibility to ensure that your definitions are conservative. 
424 Determined users can write nonconservative `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 firstorder 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 firstorder 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 leftassociating infix operators 
565 The constant declaration part declares two leftassociating 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 