# HG changeset patch # User wenzelm # Date 1427119012 -3600 # Node ID a71dbf3481a2035b454347e4bba47117a5be6303 # Parent 23b67731f4f09592dbed585f6d22816f58849a56 tuned; diff -r 23b67731f4f0 -r a71dbf3481a2 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Mar 23 13:30:59 2015 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Mar 23 14:56:52 2015 +0100 @@ -4,21 +4,18 @@ chapter \Specifications\ -text \ - The Isabelle/Isar theory format integrates specifications and - proofs, supporting interactive development with unlimited undo - operation. There is an integrated document preparation system (see - \chref{ch:document-prep}), for typesetting formal developments - together with informal text. The resulting hyper-linked PDF - documents can be used both for WWW presentation and printed copies. +text \The Isabelle/Isar theory format integrates specifications and proofs, + with support for interactive development by continuous document editing. + There is a separate document preparation system (see + \chref{ch:document-prep}), for typesetting formal developments together + with informal text. The resulting hyper-linked PDF documents can be used + both for WWW presentation and printed copies. The Isar proof language (see \chref{ch:proofs}) is embedded into the theory language as a proper sub-language. Proof mode is entered by stating some @{command theorem} or @{command lemma} at the theory level, and left again with the final conclusion (e.g.\ via @{command - qed}). Some theory specification mechanisms also require a proof, - such as @{command typedef} in HOL, which demands non-emptiness of - the representing sets. + qed}). \ @@ -30,28 +27,36 @@ @{command_def (global) "end"} & : & @{text "theory \ toplevel"} \\ \end{matharray} - Isabelle/Isar theories are defined via theory files, which may - contain both specifications and proofs; occasionally definitional - mechanisms also require some explicit proof. The theory body may be - sub-structured by means of \emph{local theory targets}, such as - @{command "locale"} and @{command "class"}. + Isabelle/Isar theories are defined via theory files, which consist of an + outermost sequence of definition--statement--proof elements. Some + definitions are self-sufficient (e.g.\ @{command fun} in Isabelle/HOL), + with foundational proofs performed internally. Other definitions require + an explicit proof as justification (e.g.\ @{command function} and + @{command termination} in Isabelle/HOL). Plain statements like @{command + theorem} or @{command lemma} are merely a special case of that, defining a + theorem from a given proposition and its proof. - The first proper command of a theory is @{command "theory"}, which - indicates imports of previous theories and optional dependencies on - other source files (usually in ML). Just preceding the initial - @{command "theory"} command there may be an optional @{command - "header"} declaration, which is only relevant to document - preparation: see also the other section markup commands in - \secref{sec:markup}. + The theory body may be sub-structured by means of \emph{local theory + targets}, such as @{command "locale"} and @{command "class"}. It is also + possible to use @{command context}~@{keyword "begin"}~\dots~@{command end} + blocks to delimited a local theory context: a \emph{named context} to + augment a locale or class specification, or an \emph{unnamed context} to + refer to local parameters and assumptions that are discharged later. See + \secref{sec:target} for more details. - A theory is concluded by a final @{command (global) "end"} command, - one that does not belong to a local theory target. No further - commands may follow such a global @{command (global) "end"}, - although some user-interfaces might pretend that trailing input is - admissible. + \medskip A theory is commenced by the @{command "theory"} command, which + indicates imports of previous theories, according to an acyclic + foundational order. Before the initial @{command "theory"} command, there + may be optional document header material (like @{command section} or + @{command text}, see \secref{sec:markup}). The document header is outside + of the formal theory context, though. + + A theory is concluded by a final @{command (global) "end"} command, one + that does not belong to a local theory target. No further commands may + follow such a global @{command (global) "end"}. @{rail \ - @@{command theory} @{syntax name} imports keywords? \ @'begin' + @@{command theory} @{syntax name} imports? keywords? \ @'begin' ; imports: @'imports' (@{syntax name} +) ; @@ -72,6 +77,11 @@ up-to-date: changed files are automatically rechecked whenever a theory header specification is processed. + Empty imports are only allowed in the bootstrap process of the special + theory @{theory Pure}, which is the start of any other formal development + based on Isabelle. Regular user theories usually refer to some more + complex entry point, such as theory @{theory Main} in Isabelle/HOL. + The optional @{keyword_def "keywords"} specification declares outer syntax (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare in end-user applications). Both minor keywords and @@ -85,8 +95,8 @@ with and without proof, respectively. Additional @{syntax tags} provide defaults for document preparation (\secref{sec:tags}). - It is possible to specify an alternative completion via @{text "== - text"}, while the default is the corresponding keyword name. + It is possible to specify an alternative completion via @{verbatim + "=="}~@{text "text"}, while the default is the corresponding keyword name. \item @{command (global) "end"} concludes the current theory definition. Note that some other commands, e.g.\ local theory @@ -106,9 +116,9 @@ @{command_def (local) "end"} & : & @{text "local_theory \ theory"} \\ \end{matharray} - A local theory target is a context managed separately within the - enclosing theory. Contexts may introduce parameters (fixed - variables) and assumptions (hypotheses). Definitions and theorems + A local theory target is a specification context that is managed + separately within the enclosing theory. Contexts may introduce parameters + (fixed variables) and assumptions (hypotheses). Definitions and theorems depending on the context may be added incrementally later on. \emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or