diff -r 14582233d36b -r 3d3e6e07b931 doc-src/IsarRef/Thy/pure.thy --- a/doc-src/IsarRef/Thy/pure.thy Mon Jun 02 22:50:21 2008 +0200 +++ b/doc-src/IsarRef/Thy/pure.thy Mon Jun 02 22:50:23 2008 +0200 @@ -6,629 +6,6 @@ chapter {* Basic language elements \label{ch:pure-syntax} *} -text {* - Subsequently, we introduce the main part of Pure theory and proof - commands, together with fundamental proof methods and attributes. - \Chref{ch:gen-tools} describes further Isar elements provided by - generic tools and packages (such as the Simplifier) that are either - part of Pure Isabelle or pre-installed in most object logics. - Specific language elements introduced by the major object-logics are - described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf} - (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless, - examples given in the generic parts will usually refer to - Isabelle/HOL as well. - - \medskip Isar commands may be either \emph{proper} document - constructors, or \emph{improper commands}. Some proof methods and - attributes introduced later are classified as improper as well. - Improper Isar language elements, which are subsequently marked by - ``@{text "\<^sup>*"}'', are often helpful when developing proof - documents, while their use is discouraged for the final - human-readable outcome. Typical examples are diagnostic commands - that print terms or theorems according to the current context; other - commands emulate old-style tactical theorem proving. -*} - - -section {* Theory commands *} - -subsection {* Markup commands \label{sec:markup-thy} *} - -text {* - \begin{matharray}{rcl} - @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\ - \end{matharray} - - Apart from formal comments (see \secref{sec:comments}), markup - commands provide a structured way to insert text into the document - generated from a theory (see \cite{isabelle-sys} for more - information on Isabelle's document preparation tools). - - \begin{rail} - ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text - ; - 'text\_raw' text - ; - \end{rail} - - \begin{descr} - - \item [@{command "chapter"}, @{command "section"}, @{command - "subsection"}, and @{command "subsubsection"}] mark chapter and - section headings. - - \item [@{command "text"}] specifies paragraphs of plain text. - - \item [@{command "text_raw"}] inserts {\LaTeX} source into the - output, without additional markup. Thus the full range of document - manipulations becomes available. - - \end{descr} - - The @{text "text"} argument of these markup commands (except for - @{command "text_raw"}) may contain references to formal entities - (``antiquotations'', see also \secref{sec:antiq}). These are - interpreted in the present theory context, or the named @{text - "target"}. - - Any of these markup elements corresponds to a {\LaTeX} command with - the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning - commands this is a plain macro with a single argument, e.g.\ - @{verbatim "\\isamarkupchapter{"}@{text "\"}@{verbatim "}"} for - @{command "chapter"}. The @{command "text"} markup results in a - {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text - "\"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"} - causes the text to be inserted directly into the {\LaTeX} source. - - \medskip Additional markup commands are available for proofs (see - \secref{sec:markup-prf}). Also note that the @{command_ref - "header"} declaration (see \secref{sec:begin-thy}) admits to insert - section markup just preceding the actual theory definition. -*} - - -subsection {* Type classes and sorts \label{sec:classes} *} - -text {* - \begin{matharray}{rcll} - @{command_def "classes"} & : & \isartrans{theory}{theory} \\ - @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\ - @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\ - \end{matharray} - - \begin{rail} - 'classes' (classdecl +) - ; - 'classrel' (nameref ('<' | subseteq) nameref + 'and') - ; - 'defaultsort' sort - ; - \end{rail} - - \begin{descr} - - \item [@{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"}] - declares class @{text c} to be a subclass of existing classes @{text - "c\<^sub>1, \, c\<^sub>n"}. Cyclic class structures are not permitted. - - \item [@{command "classrel"}~@{text "c\<^sub>1 \ c\<^sub>2"}] states - subclass relations between existing classes @{text "c\<^sub>1"} and - @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref - "instance"} command (see \secref{sec:axclass}) provides a way to - introduce proven class relations. - - \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the - new default sort for any type variables given without sort - constraints. Usually, the default sort would be only changed when - defining a new object-logic. - - \item [@{command "class_deps"}] visualizes the subclass relation, - using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - - \end{descr} -*} - - -subsection {* Primitive types and type abbreviations \label{sec:types-pure} *} - -text {* - \begin{matharray}{rcll} - @{command_def "types"} & : & \isartrans{theory}{theory} \\ - @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\ - @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\ - @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - \end{matharray} - - \begin{rail} - 'types' (typespec '=' type infix? +) - ; - 'typedecl' typespec infix? - ; - 'nonterminals' (name +) - ; - 'arities' (nameref '::' arity +) - ; - \end{rail} - - \begin{descr} - - \item [@{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"}] - introduces \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} - for existing type @{text "\"}. Unlike actual type definitions, as - are available in Isabelle/HOL for example, type synonyms are just - purely syntactic abbreviations without any logical significance. - Internally, type synonyms are fully expanded. - - \item [@{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"}] - declares a new type constructor @{text t}, intended as an actual - logical type (of the object-logic, if available). - - \item [@{command "nonterminals"}~@{text c}] declares type - constructors @{text c} (without arguments) to act as purely - syntactic types, i.e.\ nonterminal symbols of Isabelle's inner - syntax of terms or types. - - \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) - s"}] augments Isabelle's order-sorted signature of types by new type - constructor arities. This is done axiomatically! The @{command_ref - "instance"} command (see \S\ref{sec:axclass}) provides a way to - introduce proven type arities. - - \end{descr} -*} - - -subsection {* Primitive constants and definitions \label{sec:consts} *} - -text {* - Definitions essentially express abbreviations within the logic. The - simplest form of a definition is @{text "c :: \ \ t"}, where @{text - c} is a newly declared constant. Isabelle also allows derived forms - where the arguments of @{text c} appear on the left, abbreviating a - prefix of @{text \}-abstractions, e.g.\ @{text "c \ \x y. t"} may be - written more conveniently as @{text "c x y \ t"}. Moreover, - definitions may be weakened by adding arbitrary pre-conditions: - @{text "A \ c x y \ t"}. - - \medskip The built-in well-formedness conditions for definitional - specifications are: - - \begin{itemize} - - \item Arguments (on the left-hand side) must be distinct variables. - - \item All variables on the right-hand side must also appear on the - left-hand side. - - \item All type variables on the right-hand side must also appear on - the left-hand side; this prohibits @{text "0 :: nat \ length ([] :: - \ list)"} for example. - - \item The definition must not be recursive. Most object-logics - provide definitional principles that can be used to express - recursion safely. - - \end{itemize} - - Overloading means that a constant being declared as @{text "c :: \ - decl"} may be defined separately on type instances @{text "c :: - (\\<^sub>1, \, \\<^sub>n) t decl"} for each type constructor @{text - t}. The right-hand side may mention overloaded constants - recursively at type instances corresponding to the immediate - argument types @{text "\\<^sub>1, \, \\<^sub>n"}. Incomplete - specification patterns impose global constraints on all occurrences, - e.g.\ @{text "d :: \ \ \"} on the left-hand side means that all - corresponding occurrences on some right-hand side need to be an - instance of this, general @{text "d :: \ \ \"} will be disallowed. - - \begin{matharray}{rcl} - @{command_def "consts"} & : & \isartrans{theory}{theory} \\ - @{command_def "defs"} & : & \isartrans{theory}{theory} \\ - @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - 'consts' ((name '::' type mixfix?) +) - ; - 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) - ; - \end{rail} - - \begin{rail} - 'constdefs' structs? (constdecl? constdef +) - ; - - structs: '(' 'structure' (vars + 'and') ')' - ; - constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' - ; - constdef: thmdecl? prop - ; - \end{rail} - - \begin{descr} - - \item [@{command "consts"}~@{text "c :: \"}] declares constant - @{text c} to have any instance of type scheme @{text \}. The - optional mixfix annotations may attach concrete syntax to the - constants declared. - - \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn} - as a definitional axiom for some existing constant. - - The @{text "(unchecked)"} option disables global dependency checks - for this definition, which is occasionally useful for exotic - overloading. It is at the discretion of the user to avoid malformed - theory specifications! - - The @{text "(overloaded)"} option declares definitions to be - potentially overloaded. Unless this option is given, a warning - message would be issued for any definitional equation with a more - special type than that of the corresponding constant declaration. - - \item [@{command "constdefs"}] provides a streamlined combination of - constants declarations and definitions: type-inference takes care of - the most general typing of the given specification (the optional - type constraint may refer to type-inference dummies ``@{text - _}'' as usual). The resulting type declaration needs to agree with - that of the specification; overloading is \emph{not} supported here! - - The constant name may be omitted altogether, if neither type nor - syntax declarations are given. The canonical name of the - definitional axiom for constant @{text c} will be @{text c_def}, - unless specified otherwise. Also note that the given list of - specifications is processed in a strictly sequential manner, with - type-checking being performed independently. - - An optional initial context of @{text "(structure)"} declarations - admits use of indexed syntax, using the special symbol @{verbatim - "\"} (printed as ``@{text "\"}''). The latter concept is - particularly useful with locales (see also \S\ref{sec:locale}). - - \end{descr} -*} - - -subsection {* Syntax and translations \label{sec:syn-trans} *} - -text {* - \begin{matharray}{rcl} - @{command_def "syntax"} & : & \isartrans{theory}{theory} \\ - @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\ - @{command_def "translations"} & : & \isartrans{theory}{theory} \\ - @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - ('syntax' | 'no\_syntax') mode? (constdecl +) - ; - ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) - ; - - mode: ('(' ( name | 'output' | name 'output' ) ')') - ; - transpat: ('(' nameref ')')? string - ; - \end{rail} - - \begin{descr} - - \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to - @{command "consts"}~@{text decls}, except that the actual logical - signature extension is omitted. Thus the context free grammar of - Isabelle's inner syntax may be augmented in arbitrary ways, - independently of the logic. The @{text mode} argument refers to the - print mode that the grammar rules belong; unless the @{keyword_ref - "output"} indicator is given, all productions are added both to the - input and output grammar. - - \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes - grammar declarations (and translations) resulting from @{text - decls}, which are interpreted in the same manner as for @{command - "syntax"} above. - - \item [@{command "translations"}~@{text rules}] specifies syntactic - translation rules (i.e.\ macros): parse~/ print rules (@{text "\"}), - parse rules (@{text "\"}), or print rules (@{text "\"}). - Translation patterns may be prefixed by the syntactic category to be - used for parsing; the default is @{text logic}. - - \item [@{command "no_translations"}~@{text rules}] removes syntactic - translation rules, which are interpreted in the same manner as for - @{command "translations"} above. - - \end{descr} -*} - - -subsection {* Axioms and theorems \label{sec:axms-thms} *} - -text {* - \begin{matharray}{rcll} - @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\ - @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\ - \end{matharray} - - \begin{rail} - 'axioms' (axmdecl prop +) - ; - ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') - ; - \end{rail} - - \begin{descr} - - \item [@{command "axioms"}~@{text "a: \"}] introduces arbitrary - statements as axioms of the meta-logic. In fact, axioms are - ``axiomatic theorems'', and may be referred later just as any other - theorem. - - Axioms are usually only introduced when declaring new logical - systems. Everyday work is typically done the hard way, with proper - definitions and proven theorems. - - \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] - retrieves and stores existing facts in the theory context, or the - specified target context (see also \secref{sec:target}). Typical - applications would also involve attributes, to declare Simplifier - rules, for example. - - \item [@{command "theorems"}] is essentially the same as @{command - "lemmas"}, but marks the result as a different kind of facts. - - \end{descr} -*} - - -subsection {* Name spaces *} - -text {* - \begin{matharray}{rcl} - @{command_def "global"} & : & \isartrans{theory}{theory} \\ - @{command_def "local"} & : & \isartrans{theory}{theory} \\ - @{command_def "hide"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - 'hide' ('(open)')? name (nameref + ) - ; - \end{rail} - - Isabelle organizes any kind of name declarations (of types, - constants, theorems etc.) by separate hierarchically structured name - spaces. Normally the user does not have to control the behavior of - name spaces by hand, yet the following commands provide some way to - do so. - - \begin{descr} - - \item [@{command "global"} and @{command "local"}] change the - current name declaration mode. Initially, theories start in - @{command "local"} mode, causing all names to be automatically - qualified by the theory name. Changing this to @{command "global"} - causes all names to be declared without the theory prefix, until - @{command "local"} is declared again. - - Note that global names are prone to get hidden accidently later, - when qualified names of the same base name are introduced. - - \item [@{command "hide"}~@{text "space names"}] fully removes - declarations from a given name space (which may be @{text "class"}, - @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text - "(open)"} option, only the base name is hidden. Global - (unqualified) names may never be hidden. - - Note that hiding name space accesses has no impact on logical - declarations -- they remain valid internally. Entities that are no - longer accessible to the user are printed with the special qualifier - ``@{text "??"}'' prefixed to the full internal name. - - \end{descr} -*} - - -subsection {* Incorporating ML code \label{sec:ML} *} - -text {* - \begin{matharray}{rcl} - @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ - @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ - @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\ - @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\ - @{command_def "setup"} & : & \isartrans{theory}{theory} \\ - @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - 'use' name - ; - ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text - ; - 'method\_setup' name '=' text text - ; - \end{rail} - - \begin{descr} - - \item [@{command "use"}~@{text "file"}] reads and executes ML - commands from @{text "file"}. The current theory context is passed - down to the ML toplevel and may be modified, using @{ML - "Context.>>"} or derived ML commands. The file name is checked with - the @{keyword_ref "uses"} dependency declaration given in the theory - header (see also \secref{sec:begin-thy}). - - \item [@{command "ML"}~@{text "text"}] is similar to @{command - "use"}, but executes ML commands directly from the given @{text - "text"}. - - \item [@{command "ML_val"} and @{command "ML_command"}] are - diagnostic versions of @{command "ML"}, which means that the context - may not be updated. @{command "ML_val"} echos the bindings produced - at the ML toplevel, but @{command "ML_command"} is silent. - - \item [@{command "setup"}~@{text "text"}] changes the current theory - context by applying @{text "text"}, which refers to an ML expression - of type @{ML_type "theory -> theory"}. This enables to initialize - any object-logic specific tools and packages written in ML, for - example. - - \item [@{command "method_setup"}~@{text "name = text description"}] - defines a proof method in the current theory. The given @{text - "text"} has to be an ML expression of type @{ML_type "Args.src -> - Proof.context -> Proof.method"}. Parsing concrete method syntax - from @{ML_type Args.src} input can be quite tedious in general. The - following simple examples are for methods without any explicit - arguments, or a list of theorems, respectively. - -%FIXME proper antiquotations -{\footnotesize -\begin{verbatim} - Method.no_args (Method.METHOD (fn facts => foobar_tac)) - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) - Method.thms_ctxt_args (fn thms => fn ctxt => - Method.METHOD (fn facts => foobar_tac)) -\end{verbatim} -} - - Note that mere tactic emulations may ignore the @{text facts} - parameter above. Proper proof methods would do something - appropriate with the list of current facts, though. Single-rule - methods usually do strict forward-chaining (e.g.\ by using @{ML - Drule.multi_resolves}), while automatic ones just insert the facts - using @{ML Method.insert_tac} before applying the main tactic. - - \end{descr} -*} - - -subsection {* Syntax translation functions *} - -text {* - \begin{matharray}{rcl} - @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\ - @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - \begin{rail} - ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | - 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text - ; - - 'token\_translation' text - ; - \end{rail} - - Syntax translation functions written in ML admit almost arbitrary - manipulations of Isabelle's inner syntax. Any of the above commands - have a single \railqtok{text} argument that refers to an ML - expression of appropriate type, which are as follows by default: - -%FIXME proper antiquotations -\begin{ttbox} -val parse_ast_translation : (string * (ast list -> ast)) list -val parse_translation : (string * (term list -> term)) list -val print_translation : (string * (term list -> term)) list -val typed_print_translation : - (string * (bool -> typ -> term list -> term)) list -val print_ast_translation : (string * (ast list -> ast)) list -val token_translation : - (string * string * (string -> string * real)) list -\end{ttbox} - - If the @{text "(advanced)"} option is given, the corresponding - translation functions may depend on the current theory or proof - context. This allows to implement advanced syntax mechanisms, as - translations functions may refer to specific theory declarations or - auxiliary proof data. - - See also \cite[\S8]{isabelle-ref} for more information on the - general concept of syntax transformations in Isabelle. - -%FIXME proper antiquotations -\begin{ttbox} -val parse_ast_translation: - (string * (Context.generic -> ast list -> ast)) list -val parse_translation: - (string * (Context.generic -> term list -> term)) list -val print_translation: - (string * (Context.generic -> term list -> term)) list -val typed_print_translation: - (string * (Context.generic -> bool -> typ -> term list -> term)) list -val print_ast_translation: - (string * (Context.generic -> ast list -> ast)) list -\end{ttbox} -*} - - -subsection {* Oracles *} - -text {* - \begin{matharray}{rcl} - @{command_def "oracle"} & : & \isartrans{theory}{theory} \\ - \end{matharray} - - The oracle interface promotes a given ML function @{ML_text - "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some - type @{ML_text T} given by the user. This acts like an infinitary - specification of axioms -- there is no internal check of the - correctness of the results! The inference kernel records oracle - invocations within the internal derivation object of theorems, and - the pretty printer attaches ``@{text "[!]"}'' to indicate results - that are not fully checked by Isabelle inferences. - - \begin{rail} - 'oracle' name '(' type ')' '=' text - ; - \end{rail} - - \begin{descr} - - \item [@{command "oracle"}~@{text "name (type) = text"}] turns the - given ML expression @{text "text"} of type - @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an - ML function of type - @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is - bound to the global identifier @{ML_text name}. - - \end{descr} -*} - - -section {* Proof commands *} - -subsection {* Markup commands \label{sec:markup-prf} *} - -text {* - \begin{matharray}{rcl} - @{command_def "sect"} & : & \isartrans{proof}{proof} \\ - @{command_def "subsect"} & : & \isartrans{proof}{proof} \\ - @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\ - @{command_def "txt"} & : & \isartrans{proof}{proof} \\ - @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\ - \end{matharray} - - These markup commands for proof mode closely correspond to the ones - of theory mode (see \S\ref{sec:markup-thy}). - - \begin{rail} - ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text - ; - \end{rail} -*} - - section {* Other commands *} subsection {* Diagnostics *} @@ -846,15 +223,11 @@ @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ \end{matharray} \begin{rail} ('cd' | 'use\_thy' | 'update\_thy') name ; - ('display\_drafts' | 'print\_drafts') (name +) - ; \end{rail} \begin{descr} @@ -868,12 +241,6 @@ These system commands are scarcely used when working interactively, since loading of theories is done automatically as required. - \item [@{command "display_drafts"}~@{text paths} and @{command - "print_drafts"}~@{text paths}] perform simple output of a given list - of raw source files. Only those symbols that do not require - additional {\LaTeX} packages are displayed properly, everything else - is left verbatim. - \end{descr} *}