# HG changeset patch # User wenzelm # Date 1226609026 -3600 # Node ID cbc435f7b16b5c7b19fd12c245141c2a384b2b04 # Parent 8358fabeea9546bbf37b0709dcf4228517b98c57 unified use of declaration environment with IsarImplementation; tuned ML decls; diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Thu Nov 13 21:43:46 2008 +0100 @@ -90,36 +90,36 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command header}] provides plain text markup just preceding + \item @{command header} provides plain text markup just preceding the formal beginning of a theory. The corresponding {\LaTeX} macro is @{verbatim "\\isamarkupheader"}, which acts like @{command section} by default. - \item [@{command chapter}, @{command section}, @{command - subsection}, and @{command subsubsection}] mark chapter and section - headings within the main theory body or local theory targets. The + \item @{command chapter}, @{command section}, @{command subsection}, + and @{command subsubsection} mark chapter and section headings + within the main theory body or local theory targets. The corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"}, @{verbatim "\\isamarkupsection"}, @{verbatim "\\isamarkupsubsection"} etc. - \item [@{command sect}, @{command subsect}, and @{command - subsubsect}] mark section headings within proofs. The corresponding - {\LaTeX} macros are @{verbatim "\\isamarkupsect"}, @{verbatim + \item @{command sect}, @{command subsect}, and @{command subsubsect} + mark section headings within proofs. The corresponding {\LaTeX} + macros are @{verbatim "\\isamarkupsect"}, @{verbatim "\\isamarkupsubsect"} etc. - \item [@{command text} and @{command txt}] specify paragraphs of - plain text. This corresponds to a {\LaTeX} environment @{verbatim + \item @{command text} and @{command txt} specify paragraphs of plain + text. This corresponds to a {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text "\"} @{verbatim "\\end{isamarkuptext}"} etc. - \item [@{command text_raw} and @{command txt_raw}] insert {\LaTeX} + \item @{command text_raw} and @{command txt_raw} insert {\LaTeX} source into the output, without additional markup. Thus the full range of document manipulations becomes available, at the risk of messing up document output. - \end{descr} + \end{description} Except for @{command "text_raw"} and @{command "txt_raw"}, the text passed to any of the above markup commands may refer to formal @@ -214,49 +214,48 @@ text @{verbatim "{"}@{verbatim "*"}~@{text "\"}~@{verbatim "*"}@{verbatim "}"}. - \begin{descr} + \begin{description} - \item [@{text "@{theory A}"}] prints the name @{text "A"}, which is + \item @{text "@{theory A}"} prints the name @{text "A"}, which is guaranteed to refer to a valid ancestor theory in the current context. - \item [@{text "@{thm a\<^sub>1 \ a\<^sub>n}"}] prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. + \item @{text "@{thm a\<^sub>1 \ a\<^sub>n}"} prints theorems @{text "a\<^sub>1 \ a\<^sub>n"}. Full fact expressions are allowed here, including attributes (\secref{sec:syn-att}). - \item [@{text "@{prop \}"}] prints a well-typed proposition @{text + \item @{text "@{prop \}"} prints a well-typed proposition @{text "\"}. - \item [@{text "@{lemma \ by m}"}] proves a well-typed proposition + \item @{text "@{lemma \ by m}"} proves a well-typed proposition @{text "\"} by method @{text m} and prints the original @{text "\"}. - \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}. + \item @{text "@{term t}"} prints a well-typed term @{text "t"}. - \item [@{text "@{const c}"}] prints a logical or syntactic constant + \item @{text "@{const c}"} prints a logical or syntactic constant @{text "c"}. - \item [@{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"}] prints a constant - abbreviation @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in - the current context. + \item @{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"} prints a constant abbreviation + @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in the current context. - \item [@{text "@{typeof t}"}] prints the type of a well-typed term + \item @{text "@{typeof t}"} prints the type of a well-typed term @{text "t"}. - \item [@{text "@{typ \}"}] prints a well-formed type @{text "\"}. + \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. - \item [@{text "@{thm_style s a}"}] prints theorem @{text a}, + \item @{text "@{thm_style s a}"} prints theorem @{text a}, previously applying a style @{text s} to it (see below). - \item [@{text "@{term_style s t}"}] prints a well-typed term @{text - t} after applying a style @{text s} to it (see below). + \item @{text "@{term_style s t}"} prints a well-typed term @{text t} + after applying a style @{text s} to it (see below). - \item [@{text "@{text s}"}] prints uninterpreted source text @{text + \item @{text "@{text s}"} prints uninterpreted source text @{text s}. This is particularly useful to print portions of text according to the Isabelle document style, without demanding well-formedness, e.g.\ small pieces of terms that should not be parsed or type-checked yet. - \item [@{text "@{goals}"}] prints the current \emph{dynamic} goal + \item @{text "@{goals}"} prints the current \emph{dynamic} goal state. This is mainly for support of tactic-emulation scripts within Isar. Presentation of goal states does not conform to the idea of human-readable proof documents! @@ -265,24 +264,24 @@ the reasoning via proper Isar proof commands, instead of peeking at the internal machine configuration. - \item [@{text "@{subgoals}"}] is similar to @{text "@{goals}"}, but + \item @{text "@{subgoals}"} is similar to @{text "@{goals}"}, but does not print the main goal. - \item [@{text "@{prf a\<^sub>1 \ a\<^sub>n}"}] prints the (compact) proof terms + \item @{text "@{prf a\<^sub>1 \ a\<^sub>n}"} prints the (compact) proof terms corresponding to the theorems @{text "a\<^sub>1 \ a\<^sub>n"}. Note that this requires proof terms to be switched on for the current logic session. - \item [@{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"}] is like @{text - "@{prf a\<^sub>1 \ a\<^sub>n}"}, but prints the full proof terms, i.e.\ also - displays information omitted in the compact proof term, which is - denoted by ``@{text _}'' placeholders there. + \item @{text "@{full_prf a\<^sub>1 \ a\<^sub>n}"} is like @{text "@{prf a\<^sub>1 \ + a\<^sub>n}"}, but prints the full proof terms, i.e.\ also displays + information omitted in the compact proof term, which is denoted by + ``@{text _}'' placeholders there. - \item [@{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text - "@{ML_struct s}"}] check text @{text s} as ML value, type, and + \item @{text "@{ML s}"}, @{text "@{ML_type s}"}, and @{text + "@{ML_struct s}"} check text @{text s} as ML value, type, and structure, respectively. The source is printed verbatim. - \end{descr} + \end{description} *} @@ -292,23 +291,23 @@ term_style} admit an extra \emph{style} specification to modify the printed result. The following standard styles are available: - \begin{descr} + \begin{description} - \item [@{text lhs}] extracts the first argument of any application + \item @{text lhs} extracts the first argument of any application form with at least two arguments --- typically meta-level or object-level equality, or any other binary relation. - \item [@{text rhs}] is like @{text lhs}, but extracts the second + \item @{text rhs} is like @{text lhs}, but extracts the second argument. - \item [@{text "concl"}] extracts the conclusion @{text C} from a rule + \item @{text "concl"} extracts the conclusion @{text C} from a rule in Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"}. - \item [@{text "prem1"}, \dots, @{text "prem9"}] extract premise - number @{text "1, \, 9"}, respectively, from from a rule in - Horn-clause normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} + \item @{text "prem1"}, \dots, @{text "prem9"} extract premise number + @{text "1, \, 9"}, respectively, from from a rule in Horn-clause + normal form @{text "A\<^sub>1 \ \ A\<^sub>n \ C"} - \end{descr} + \end{description} *} @@ -318,63 +317,63 @@ of antiquotations. Note that many of these coincide with global ML flags of the same names. - \begin{descr} + \begin{description} - \item[@{text "show_types = bool"} and @{text "show_sorts = bool"}] + \item @{text "show_types = bool"} and @{text "show_sorts = bool"} control printing of explicit type and sort constraints. - \item[@{text "show_structs = bool"}] controls printing of implicit + \item @{text "show_structs = bool"} controls printing of implicit structures. - \item[@{text "long_names = bool"}] forces names of types and + \item @{text "long_names = bool"} forces names of types and constants etc.\ to be printed in their fully qualified internal form. - \item[@{text "short_names = bool"}] forces names of types and + \item @{text "short_names = bool"} forces names of types and constants etc.\ to be printed unqualified. Note that internalizing the output again in the current context may well yield a different result. - \item[@{text "unique_names = bool"}] determines whether the printed + \item @{text "unique_names = bool"} determines whether the printed version of qualified names should be made sufficiently long to avoid overlap with names declared further back. Set to @{text false} for more concise output. - \item[@{text "eta_contract = bool"}] prints terms in @{text + \item @{text "eta_contract = bool"} prints terms in @{text \}-contracted form. - \item[@{text "display = bool"}] indicates if the text is to be - output as multi-line ``display material'', rather than a small piece - of text without line breaks (which is the default). + \item @{text "display = bool"} indicates if the text is to be output + as multi-line ``display material'', rather than a small piece of + text without line breaks (which is the default). In this mode the embedded entities are printed in the same style as the main theory text. - \item[@{text "break = bool"}] controls line breaks in non-display + \item @{text "break = bool"} controls line breaks in non-display material. - \item[@{text "quotes = bool"}] indicates if the output should be + \item @{text "quotes = bool"} indicates if the output should be enclosed in double quotes. - \item[@{text "mode = name"}] adds @{text name} to the print mode to + \item @{text "mode = name"} adds @{text name} to the print mode to be used for presentation (see also \cite{isabelle-ref}). Note that the standard setup for {\LaTeX} output is already present by default, including the modes @{text latex} and @{text xsymbols}. - \item[@{text "margin = nat"} and @{text "indent = nat"}] change the + \item @{text "margin = nat"} and @{text "indent = nat"} change the margin or indentation for pretty printing of display material. - \item[@{text "goals_limit = nat"}] determines the maximum number of + \item @{text "goals_limit = nat"} determines the maximum number of goals to be printed (for goal-based antiquotation). - \item[@{text "locale = name"}] specifies an alternative locale + \item @{text "locale = name"} specifies an alternative locale context used for evaluating and printing the subsequent argument. - \item[@{text "source = bool"}] prints the original source text of - the antiquotation arguments, rather than its internal - representation. Note that formal checking of @{antiquotation - "thm"}, @{antiquotation "term"}, etc. is still enabled; use the - @{antiquotation "text"} antiquotation for unchecked output. + \item @{text "source = bool"} prints the original source text of the + antiquotation arguments, rather than its internal representation. + Note that formal checking of @{antiquotation "thm"}, @{antiquotation + "term"}, etc. is still enabled; use the @{antiquotation "text"} + antiquotation for unchecked output. Regular @{text "term"} and @{text "typ"} antiquotations with @{text "source = false"} involve a full round-trip from the original source @@ -387,7 +386,7 @@ given source text, with the desirable well-formedness check in the background, but without modification of the printed text. - \end{descr} + \end{description} For boolean flags, ``@{text "name = true"}'' may be abbreviated as ``@{text name}''. All of the above flags are disabled by default, @@ -462,15 +461,15 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "display_drafts"}~@{text paths} and @{command - "print_drafts"}~@{text paths}] perform simple output of a given list + \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} + \end{description} *} end diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/Generic.thy Thu Nov 13 21:43:46 2008 +0100 @@ -32,18 +32,17 @@ name ('=' ('true' | 'false' | int | name))? \end{rail} - \begin{descr} + \begin{description} - \item [@{command "print_configs"}] prints the available - configuration options, with names, types, and current values. + \item @{command "print_configs"} prints the available configuration + options, with names, types, and current values. - \item [@{text "name = value"}] as an attribute expression modifies - the named option, with the syntax of the value depending on the - option's type. For @{ML_type bool} the default value is @{text - true}. Any attempt to change a global option in a local context is - ignored. + \item @{text "name = value"} as an attribute expression modifies the + named option, with the syntax of the value depending on the option's + type. For @{ML_type bool} the default value is @{text true}. Any + attempt to change a global option in a local context is ignored. - \end{descr} + \end{description} *} @@ -70,25 +69,24 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method unfold}~@{text "a\<^sub>1 \ a\<^sub>n"} and @{method - fold}~@{text "a\<^sub>1 \ a\<^sub>n"}] expand (or fold back) the - given definitions throughout all goals; any chained facts provided - are inserted into the goal and subject to rewriting as well. + \item @{method unfold}~@{text "a\<^sub>1 \ a\<^sub>n"} and @{method fold}~@{text + "a\<^sub>1 \ a\<^sub>n"} expand (or fold back) the given definitions throughout + all goals; any chained facts provided are inserted into the goal and + subject to rewriting as well. - \item [@{method insert}~@{text "a\<^sub>1 \ a\<^sub>n"}] inserts - theorems as facts into all goals of the proof state. Note that - current facts indicated for forward chaining are ignored. + \item @{method insert}~@{text "a\<^sub>1 \ a\<^sub>n"} inserts theorems as facts + into all goals of the proof state. Note that current facts + indicated for forward chaining are ignored. - \item [@{method erule}~@{text "a\<^sub>1 \ a\<^sub>n"}, @{method - drule}~@{text "a\<^sub>1 \ a\<^sub>n"}, and @{method frule}~@{text - "a\<^sub>1 \ a\<^sub>n"}] are similar to the basic @{method rule} - method (see \secref{sec:pure-meth-att}), but apply rules by - elim-resolution, destruct-resolution, and forward-resolution, - respectively \cite{isabelle-ref}. The optional natural number - argument (default 0) specifies additional assumption steps to be - performed here. + \item @{method erule}~@{text "a\<^sub>1 \ a\<^sub>n"}, @{method drule}~@{text "a\<^sub>1 + \ a\<^sub>n"}, and @{method frule}~@{text "a\<^sub>1 \ a\<^sub>n"} are similar to the + basic @{method rule} method (see \secref{sec:pure-meth-att}), but + apply rules by elim-resolution, destruct-resolution, and + forward-resolution, respectively \cite{isabelle-ref}. The optional + natural number argument (default 0) specifies additional assumption + steps to be performed here. Note that these methods are improper ones, mainly serving for experimentation and tactic script emulation. Different modes of @@ -98,15 +96,15 @@ the plain @{method rule} method, with forward chaining of current facts. - \item [@{method succeed}] yields a single (unchanged) result; it is + \item @{method succeed} yields a single (unchanged) result; it is the identity of the ``@{text ","}'' method combinator (cf.\ \secref{sec:proof-meth}). - \item [@{method fail}] yields an empty result sequence; it is the + \item @{method fail} yields an empty result sequence; it is the identity of the ``@{text "|"}'' method combinator (cf.\ \secref{sec:proof-meth}). - \end{descr} + \end{description} \begin{matharray}{rcl} @{attribute_def tagged} & : & \isaratt \\ @@ -133,45 +131,45 @@ 'rotated' ( int )? \end{rail} - \begin{descr} + \begin{description} - \item [@{attribute tagged}~@{text "name arg"} and @{attribute - untagged}~@{text name}] add and remove \emph{tags} of some theorem. + \item @{attribute tagged}~@{text "name arg"} and @{attribute + untagged}~@{text name} add and remove \emph{tags} of some theorem. Tags may be any list of string pairs that serve as formal comment. The first string is considered the tag name, the second its argument. Note that @{attribute untagged} removes any tags of the same name. - \item [@{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}] + \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a} compose rules by resolution. @{attribute THEN} resolves with the first premise of @{text a} (an alternative position may be also specified); the @{attribute COMP} version skips the automatic lifting process that is normally intended (cf.\ @{ML "op RS"} and @{ML "op COMP"} in \cite[\S5]{isabelle-ref}). - \item [@{attribute unfolded}~@{text "a\<^sub>1 \ a\<^sub>n"} and - @{attribute folded}~@{text "a\<^sub>1 \ a\<^sub>n"}] expand and fold - back again the given definitions throughout a rule. + \item @{attribute unfolded}~@{text "a\<^sub>1 \ a\<^sub>n"} and @{attribute + folded}~@{text "a\<^sub>1 \ a\<^sub>n"} expand and fold back again the given + definitions throughout a rule. - \item [@{attribute rotated}~@{text n}] rotate the premises of a + \item @{attribute rotated}~@{text n} rotate the premises of a theorem by @{text n} (default 1). - \item [@{attribute (Pure) elim_format}] turns a destruction rule - into elimination rule format, by resolving with the rule @{prop - "PROP A \ (PROP A \ PROP B) \ PROP B"}. + \item @{attribute (Pure) elim_format} turns a destruction rule into + elimination rule format, by resolving with the rule @{prop "PROP A \ + (PROP A \ PROP B) \ PROP B"}. Note that the Classical Reasoner (\secref{sec:classical}) provides its own version of this operation. - \item [@{attribute standard}] puts a theorem into the standard form - of object-rules at the outermost theory level. Note that this + \item @{attribute standard} puts a theorem into the standard form of + object-rules at the outermost theory level. Note that this operation violates the local proof context (including active locales). - \item [@{attribute no_vars}] replaces schematic variables by free + \item @{attribute no_vars} replaces schematic variables by free ones; this is mainly for tuning output of pretty printed theorems. - \end{descr} + \end{description} *} @@ -198,48 +196,48 @@ provide the canonical way for automated normalization (see \secref{sec:simplifier}). - \begin{descr} + \begin{description} - \item [@{method subst}~@{text eq}] performs a single substitution - step using rule @{text eq}, which may be either a meta or object + \item @{method subst}~@{text eq} performs a single substitution step + using rule @{text eq}, which may be either a meta or object equality. - \item [@{method subst}~@{text "(asm) eq"}] substitutes in an + \item @{method subst}~@{text "(asm) eq"} substitutes in an assumption. - \item [@{method subst}~@{text "(i \ j) eq"}] performs several + \item @{method subst}~@{text "(i \ j) eq"} performs several substitutions in the conclusion. The numbers @{text i} to @{text j} indicate the positions to substitute at. Positions are ordered from the top of the term tree moving down from left to right. For example, in @{text "(a + b) + (c + d)"} there are three positions - where commutativity of @{text "+"} is applicable: 1 refers to - @{text "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. + where commutativity of @{text "+"} is applicable: 1 refers to @{text + "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. If the positions in the list @{text "(i \ j)"} are non-overlapping (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may assume all substitutions are performed simultaneously. Otherwise the behaviour of @{text subst} is not specified. - \item [@{method subst}~@{text "(asm) (i \ j) eq"}] performs the + \item @{method subst}~@{text "(asm) (i \ j) eq"} performs the substitutions in the assumptions. The positions refer to the assumptions in order from left to right. For example, given in a goal of the form @{text "P (a + b) \ P (c + d) \ \"}, position 1 of commutativity of @{text "+"} is the subterm @{text "a + b"} and position 2 is the subterm @{text "c + d"}. - \item [@{method hypsubst}] performs substitution using some + \item @{method hypsubst} performs substitution using some assumption; this only works for equations of the form @{text "x = t"} where @{text x} is a free or bound variable. - \item [@{method split}~@{text "a\<^sub>1 \ a\<^sub>n"}] performs - single-step case splitting using the given rules. By default, - splitting is performed in the conclusion of a goal; the @{text - "(asm)"} option indicates to operate on assumptions instead. + \item @{method split}~@{text "a\<^sub>1 \ a\<^sub>n"} performs single-step case + splitting using the given rules. By default, splitting is performed + in the conclusion of a goal; the @{text "(asm)"} option indicates to + operate on assumptions instead. Note that the @{method simp} method already involves repeated application of split rules as declared in the current context. - \end{descr} + \end{description} *} @@ -304,9 +302,9 @@ ; \end{rail} -\begin{descr} +\begin{description} - \item [@{method rule_tac} etc.] do resolution of rules with explicit + \item @{method rule_tac} etc. do resolution of rules with explicit instantiation. This works the same way as the ML tactics @{ML res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}) @@ -314,46 +312,45 @@ @{method rule_tac} is the same as @{ML resolve_tac} in ML (see \cite[\S3]{isabelle-ref}). - \item [@{method cut_tac}] inserts facts into the proof state as + \item @{method cut_tac} inserts facts into the proof state as assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note that the scope of schematic variables is spread over the main goal statement. Instantiations - may be given as well, see also ML tactic @{ML cut_inst_tac} - in \cite[\S3]{isabelle-ref}. - - \item [@{method thin_tac}~@{text \}] deletes the specified - assumption from a subgoal; note that @{text \} may contain schematic - variables. See also @{ML thin_tac} in + may be given as well, see also ML tactic @{ML cut_inst_tac} in \cite[\S3]{isabelle-ref}. - \item [@{method subgoal_tac}~@{text \}] adds @{text \} as an + \item @{method thin_tac}~@{text \} deletes the specified assumption + from a subgoal; note that @{text \} may contain schematic variables. + See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}. + + \item @{method subgoal_tac}~@{text \} adds @{text \} as an assumption to a subgoal. See also @{ML subgoal_tac} and @{ML subgoals_tac} in \cite[\S3]{isabelle-ref}. - \item [@{method rename_tac}~@{text "x\<^sub>1 \ x\<^sub>n"}] renames - parameters of a goal according to the list @{text "x\<^sub>1, \, - x\<^sub>n"}, which refers to the \emph{suffix} of variables. + \item @{method rename_tac}~@{text "x\<^sub>1 \ x\<^sub>n"} renames parameters of a + goal according to the list @{text "x\<^sub>1, \, x\<^sub>n"}, which refers to the + \emph{suffix} of variables. - \item [@{method rotate_tac}~@{text n}] rotates the assumptions of a + \item @{method rotate_tac}~@{text n} rotates the assumptions of a goal by @{text n} positions: from right to left if @{text n} is positive, and from left to right if @{text n} is negative; the default value is 1. See also @{ML rotate_tac} in \cite[\S3]{isabelle-ref}. - \item [@{method tactic}~@{text "text"}] produces a proof method from + \item @{method tactic}~@{text "text"} produces a proof method from any ML text of type @{ML_type tactic}. Apart from the usual ML environment and the current proof context, the ML code may refer to the locally bound values @{ML_text facts}, which indicates any current facts used for forward-chaining. - \item [@{method raw_tactic}] is similar to @{method tactic}, but + \item @{method raw_tactic} is similar to @{method tactic}, but presents the goal state in its raw internal form, where simultaneous subgoals appear as conjunction of the logical framework instead of the usual split into several subgoals. While feature this is useful for debugging of complex method definitions, it should not never appear in production theories. - \end{descr} + \end{description} *} @@ -379,9 +376,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method simp}] invokes the Simplifier, after declaring + \item @{method simp} invokes the Simplifier, after declaring additional rules according to the arguments given. Note that the \railtterm{only} modifier first removes all other rewrite rules, congruences, and looper tactics (including splits), and then behaves @@ -397,10 +394,10 @@ include the Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). - \item [@{method simp_all}] is similar to @{method simp}, but acts on + \item @{method simp_all} is similar to @{method simp}, but acts on all goals (backwards from the last to the first one). - \end{descr} + \end{description} By default the Simplifier methods take local assumptions fully into account, using equational assumptions in the subsequent @@ -453,19 +450,19 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "print_simpset"}] prints the collection of rules + \item @{command "print_simpset"} prints the collection of rules declared to the Simplifier, which is also known as ``simpset'' internally \cite{isabelle-ref}. - \item [@{attribute simp}] declares simplification rules. + \item @{attribute simp} declares simplification rules. - \item [@{attribute cong}] declares congruence rules. + \item @{attribute cong} declares congruence rules. - \item [@{attribute split}] declares case split rules. + \item @{attribute split} declares case split rules. - \end{descr} + \end{description} *} @@ -485,9 +482,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "simproc_setup"}] defines a named simplification + \item @{command "simproc_setup"} defines a named simplification procedure that is invoked by the Simplifier whenever any of the given term patterns match the current redex. The implementation, which is provided as ML source text, needs to be of type @{ML_type @@ -506,12 +503,12 @@ Morphisms and identifiers are only relevant for simprocs that are defined within a local target context, e.g.\ in a locale. - \item [@{text "simproc add: name"} and @{text "simproc del: name"}] + \item @{text "simproc add: name"} and @{text "simproc del: name"} add or delete named simprocs to the current Simplifier context. The default is to add a simproc. Note that @{command "simproc_setup"} already adds the new simproc to the subsequent context. - \end{descr} + \end{description} *} @@ -530,15 +527,14 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{attribute simplified}~@{text "a\<^sub>1 \ a\<^sub>n"}] - causes a theorem to be simplified, either by exactly the specified - rules @{text "a\<^sub>1, \, a\<^sub>n"}, or the implicit Simplifier - context if no arguments are given. The result is fully simplified - by default, including assumptions and conclusion; the options @{text - no_asm} etc.\ tune the Simplifier in the same way as the for the - @{text simp} method. + \item @{attribute simplified}~@{text "a\<^sub>1 \ a\<^sub>n"} causes a theorem to + be simplified, either by exactly the specified rules @{text "a\<^sub>1, \, + a\<^sub>n"}, or the implicit Simplifier context if no arguments are given. + The result is fully simplified by default, including assumptions and + conclusion; the options @{text no_asm} etc.\ tune the Simplifier in + the same way as the for the @{text simp} method. Note that forward simplification restricts the simplifier to its most basic operation of term rewriting; solver and looper tactics @@ -546,7 +542,7 @@ simplified} attribute should be only rarely required under normal circumstances. - \end{descr} + \end{description} *} @@ -567,9 +563,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method rule}] as offered by the Classical Reasoner is a + \item @{method rule} as offered by the Classical Reasoner is a refinement over the primitive one (see \secref{sec:pure-meth-att}). Both versions essentially work the same, but the classical version observes the classical rule context in addition to that of @@ -580,18 +576,18 @@ ones), but only few declarations to the rule context of Isabelle/Pure (\secref{sec:pure-meth-att}). - \item [@{method contradiction}] solves some goal by contradiction, + \item @{method contradiction} solves some goal by contradiction, deriving any result from both @{text "\ A"} and @{text A}. Chained facts, which are guaranteed to participate, may appear in either order. - \item [@{method intro} and @{method elim}] repeatedly refine some - goal by intro- or elim-resolution, after having inserted any chained + \item @{method intro} and @{method elim} repeatedly refine some goal + by intro- or elim-resolution, after having inserted any chained facts. Exactly the rules given as arguments are taken into account; this allows fine-tuned decomposition of a proof problem, in contrast to common automated tools. - \end{descr} + \end{description} *} @@ -618,19 +614,19 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method blast}] refers to the classical tableau prover (see + \item @{method blast} refers to the classical tableau prover (see @{ML blast_tac} in \cite[\S11]{isabelle-ref}). The optional argument specifies a user-supplied search bound (default 20). - \item [@{method fast}, @{method slow}, @{method best}, @{method - safe}, and @{method clarify}] refer to the generic classical + \item @{method fast}, @{method slow}, @{method best}, @{method + safe}, and @{method clarify} refer to the generic classical reasoner. See @{ML fast_tac}, @{ML slow_tac}, @{ML best_tac}, @{ML safe_tac}, and @{ML clarify_tac} in \cite[\S11]{isabelle-ref} for more information. - \end{descr} + \end{description} Any of the above methods support additional modifiers of the context of classical rules. Their semantics is analogous to the attributes @@ -666,11 +662,11 @@ (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs \end{rail} - \begin{descr} + \begin{description} - \item [@{method auto}, @{method force}, @{method clarsimp}, @{method - fastsimp}, @{method slowsimp}, and @{method bestsimp}] provide - access to Isabelle's combined simplification and classical reasoning + \item @{method auto}, @{method force}, @{method clarsimp}, @{method + fastsimp}, @{method slowsimp}, and @{method bestsimp} provide access + to Isabelle's combined simplification and classical reasoning tactics. These correspond to @{ML auto_tac}, @{ML force_tac}, @{ML clarsimp_tac}, and Classical Reasoner tactics with the Simplifier added as wrapper, see \cite[\S11]{isabelle-ref} for more @@ -683,7 +679,7 @@ doing the search. The ``@{text "!"}'' argument causes the full context of assumptions to be included as well. - \end{descr} + \end{description} *} @@ -708,13 +704,13 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "print_claset"}] prints the collection of rules + \item @{command "print_claset"} prints the collection of rules declared to the Classical Reasoner, which is also known as ``claset'' internally \cite{isabelle-ref}. - \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}] + \item @{attribute intro}, @{attribute elim}, and @{attribute dest} declare introduction, elimination, and destruction rules, respectively. By default, rules are considered as \emph{unsafe} (i.e.\ not applied blindly without backtracking), while ``@{text @@ -725,10 +721,10 @@ specifies an explicit weight argument, which is ignored by automated tools, but determines the search order of single rule steps. - \item [@{attribute rule}~@{text del}] deletes introduction, + \item @{attribute rule}~@{text del} deletes introduction, elimination, or destruction rules from the context. - \item [@{attribute iff}] declares logical equivalences to the + \item @{attribute iff} declares logical equivalences to the Simplifier and the Classical reasoner at the same time. Non-conditional rules result in a ``safe'' introduction and elimination pair; conditional ones are considered ``unsafe''. Rules @@ -739,7 +735,7 @@ the Isabelle/Pure context only, and omits the Simplifier declaration. - \end{descr} + \end{description} *} @@ -750,13 +746,13 @@ @{attribute_def swapped} & : & \isaratt \\ \end{matharray} - \begin{descr} + \begin{description} - \item [@{attribute swapped}] turns an introduction rule into an + \item @{attribute swapped} turns an introduction rule into an elimination, by resolving with the classical swap principle @{text "(\ B \ A) \ (\ A \ B)"}. - \end{descr} + \end{description} *} @@ -800,18 +796,18 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "judgment"}~@{text "c :: \ (mx)"}] declares - constant @{text c} as the truth judgment of the current - object-logic. Its type @{text \} should specify a coercion of the - category of object-level propositions to @{text prop} of the Pure - meta-logic; the mixfix annotation @{text "(mx)"} would typically - just link the object language (internally of syntactic category - @{text logic}) with that of @{text prop}. Only one @{command - "judgment"} declaration may be given in any theory development. + \item @{command "judgment"}~@{text "c :: \ (mx)"} declares constant + @{text c} as the truth judgment of the current object-logic. Its + type @{text \} should specify a coercion of the category of + object-level propositions to @{text prop} of the Pure meta-logic; + the mixfix annotation @{text "(mx)"} would typically just link the + object language (internally of syntactic category @{text logic}) + with that of @{text prop}. Only one @{command "judgment"} + declaration may be given in any theory development. - \item [@{method atomize} (as a method)] rewrites any non-atomic + \item @{method atomize} (as a method) rewrites any non-atomic premises of a sub-goal, using the meta-level equations declared via @{attribute atomize} (as an attribute) beforehand. As a result, heavily nested goals become amenable to fundamental operations such @@ -826,18 +822,18 @@ Meta-level conjunction should be covered as well (this is particularly important for locales, see \secref{sec:locale}). - \item [@{attribute rule_format}] rewrites a theorem by the - equalities declared as @{attribute rulify} rules in the current - object-logic. By default, the result is fully normalized, including - assumptions and conclusions at any depth. The @{text "(no_asm)"} - option restricts the transformation to the conclusion of a rule. + \item @{attribute rule_format} rewrites a theorem by the equalities + declared as @{attribute rulify} rules in the current object-logic. + By default, the result is fully normalized, including assumptions + and conclusions at any depth. The @{text "(no_asm)"} option + restricts the transformation to the conclusion of a rule. In common object-logics (HOL, FOL, ZF), the effect of @{attribute rule_format} is to replace (bounded) universal quantification (@{text "\"}) and implication (@{text "\"}) by the corresponding rule statements over @{text "\"} and @{text "\"}. - \end{descr} + \end{description} *} end diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Nov 13 21:43:46 2008 +0100 @@ -28,19 +28,19 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) - t"}] is similar to the original @{command "typedecl"} of - Isabelle/Pure (see \secref{sec:types-pure}), but also declares type - arity @{text "t :: (type, \, type) type"}, making @{text t} an - actual HOL type constructor. %FIXME check, update + \item @{command (HOL) "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} is similar + to the original @{command "typedecl"} of Isabelle/Pure (see + \secref{sec:types-pure}), but also declares type arity @{text "t :: + (type, \, type) type"}, making @{text t} an actual HOL type + constructor. %FIXME check, update - \item [@{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) - t = A"}] sets up a goal stating non-emptiness of the set @{text A}. - After finishing the proof, the theory will be augmented by a - Gordon/HOL-style type definition, which establishes a bijection - between the representing set @{text A} and the new type @{text t}. + \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} sets up + a goal stating non-emptiness of the set @{text A}. After finishing + the proof, the theory will be augmented by a Gordon/HOL-style type + definition, which establishes a bijection between the representing + set @{text A} and the new type @{text t}. Technically, @{command (HOL) "typedef"} defines both a type @{text t} and a set (term constant) of the same name (an alternative base @@ -64,7 +64,7 @@ declaration suppresses a separate constant definition for the representing set. - \end{descr} + \end{description} Note that raw type declarations are rarely used in practice; the main application is with experimental (or even axiomatic!) theory @@ -87,21 +87,20 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m - \ \ \ q\<^sub>1 \ q\<^sub>n"}] puts expressions of - low-level tuple types into canonical form as specified by the - arguments given; the @{text i}-th collection of arguments refers to - occurrences in premise @{text i} of the rule. The ``@{text - "(complete)"}'' option causes \emph{all} arguments in function - applications to be represented canonically according to their tuple - type structure. + \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m \ \ + \ q\<^sub>1 \ q\<^sub>n"} puts expressions of low-level tuple types into + canonical form as specified by the arguments given; the @{text i}-th + collection of arguments refers to occurrences in premise @{text i} + of the rule. The ``@{text "(complete)"}'' option causes \emph{all} + arguments in function applications to be represented canonically + according to their tuple type structure. Note that these operations tend to invent funny names for new local parameters to be introduced. - \end{descr} + \end{description} *} @@ -194,11 +193,10 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "record"}~@{text "(\\<^sub>1, \, \\<^sub>m) t - = \ + c\<^sub>1 :: \\<^sub>1 \ c\<^sub>n :: \\<^sub>n"}] defines - extensible record type @{text "(\\<^sub>1, \, \\<^sub>m) t"}, + \item @{command (HOL) "record"}~@{text "(\\<^sub>1, \, \\<^sub>m) t = \ + c\<^sub>1 :: \\<^sub>1 + \ c\<^sub>n :: \\<^sub>n"} defines extensible record type @{text "(\\<^sub>1, \, \\<^sub>m) t"}, derived from the optional parent record @{text "\"} by adding new field components @{text "c\<^sub>i :: \\<^sub>i"} etc. @@ -224,7 +222,7 @@ @{text "\c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\"}. - \end{descr} + \end{description} *} @@ -376,16 +374,16 @@ cons: name (type *) mixfix? \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "datatype"}] defines inductive datatypes in + \item @{command (HOL) "datatype"} defines inductive datatypes in HOL. - \item [@{command (HOL) "rep_datatype"}] represents existing types as + \item @{command (HOL) "rep_datatype"} represents existing types as inductive ones, generating the standard infrastructure of derived concepts (primitive recursion etc.). - \end{descr} + \end{description} The induction and exhaustion theorems generated provide case names according to the constructors involved, while parameters are named @@ -425,12 +423,12 @@ 'termination' ( term )? \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "primrec"}] defines primitive recursive + \item @{command (HOL) "primrec"} defines primitive recursive functions over datatypes, see also \cite{isabelle-HOL}. - \item [@{command (HOL) "function"}] defines functions by general + \item @{command (HOL) "function"} defines functions by general wellfounded recursion. A detailed description with examples can be found in \cite{isabelle-function}. The function is specified by a set of (possibly conditional) recursive equations with arbitrary @@ -443,18 +441,18 @@ predicate @{text "f_dom"}. The @{command (HOL) "termination"} command can then be used to establish that the function is total. - \item [@{command (HOL) "fun"}] is a shorthand notation for - ``@{command (HOL) "function"}~@{text "(sequential)"}, followed by - automated proof attempts regarding pattern matching and termination. - See \cite{isabelle-function} for further details. + \item @{command (HOL) "fun"} is a shorthand notation for ``@{command + (HOL) "function"}~@{text "(sequential)"}, followed by automated + proof attempts regarding pattern matching and termination. See + \cite{isabelle-function} for further details. - \item [@{command (HOL) "termination"}~@{text f}] commences a + \item @{command (HOL) "termination"}~@{text f} commences a termination proof for the previously defined function @{text f}. If this is omitted, the command refers to the most recent function definition. After the proof is closed, the recursive equations and the induction principle is established. - \end{descr} + \end{description} %FIXME check @@ -479,31 +477,31 @@ The @{command (HOL) "function"} command accepts the following options. - \begin{descr} + \begin{description} - \item [@{text sequential}] enables a preprocessor which - disambiguates overlapping patterns by making them mutually disjoint. - Earlier equations take precedence over later ones. This allows to - give the specification in a format very similar to functional - programming. Note that the resulting simplification and induction - rules correspond to the transformed specification, not the one given + \item @{text sequential} enables a preprocessor which disambiguates + overlapping patterns by making them mutually disjoint. Earlier + equations take precedence over later ones. This allows to give the + specification in a format very similar to functional programming. + Note that the resulting simplification and induction rules + correspond to the transformed specification, not the one given originally. This usually means that each equation given by the user may result in several theroems. Also note that this automatic transformation only works for ML-style datatype patterns. - \item [@{text domintros}] enables the automated generation of + \item @{text domintros} enables the automated generation of introduction rules for the domain predicate. While mostly not needed, they can be helpful in some proofs about partial functions. - \item [@{text tailrec}] generates the unconstrained recursive + \item @{text tailrec} generates the unconstrained recursive equations even without a termination proof, provided that the function is tail-recursive. This currently only works - \item [@{text "default d"}] allows to specify a default value for a + \item @{text "default d"} allows to specify a default value for a (partial) function, which will ensure that @{text "f x = d x"} whenever @{text "x \ f_dom"}. - \end{descr} + \end{description} *} @@ -523,21 +521,21 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method (HOL) pat_completeness}] is a specialized method to + \item @{method (HOL) pat_completeness} is a specialized method to solve goals regarding the completeness of pattern matching, as required by the @{command (HOL) "function"} package (cf.\ \cite{isabelle-function}). - \item [@{method (HOL) relation}~@{text R}] introduces a termination + \item @{method (HOL) relation}~@{text R} introduces a termination proof using the relation @{text R}. The resulting proof state will contain goals expressing that @{text R} is wellfounded, and that the arguments of recursive calls decrease with respect to @{text R}. Usually, this method is used as the initial proof step of manual termination proofs. - \item [@{method (HOL) "lexicographic_order"}] attempts a fully + \item @{method (HOL) "lexicographic_order"} attempts a fully automated termination proof by searching for a lexicographic combination of size measures on the arguments of the function. The method accepts the same arguments as the @{method auto} method, @@ -548,7 +546,7 @@ In case of failure, extensive information is printed, which can help to analyse the situation (cf.\ \cite{isabelle-function}). - \end{descr} + \end{description} *} @@ -577,9 +575,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "recdef"}] defines general well-founded + \item @{command (HOL) "recdef"} defines general well-founded recursive functions (using the TFL package), see also \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells TFL to recover from failed proof attempts, returning unfinished @@ -590,7 +588,7 @@ context of the Simplifier (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\ \secref{sec:classical}). - \item [@{command (HOL) "recdef_tc"}~@{text "c (i)"}] recommences the + \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the proof for leftover termination condition number @{text i} (default 1) as generated by a @{command (HOL) "recdef"} definition of constant @{text c}. @@ -598,7 +596,7 @@ Note that in most cases, @{command (HOL) "recdef"} is able to finish its internal proofs without manual intervention. - \end{descr} + \end{description} \medskip Hints for @{command (HOL) "recdef"} may be also declared globally, using the following attributes. @@ -659,10 +657,10 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "inductive"} and @{command (HOL) - "coinductive"}] define (co)inductive predicates from the + \item @{command (HOL) "inductive"} and @{command (HOL) + "coinductive"} define (co)inductive predicates from the introduction rules given in the @{keyword "where"} part. The optional @{keyword "for"} part contains a list of parameters of the (co)inductive predicates that remain fixed throughout the @@ -672,15 +670,15 @@ \emph{must} be a theorem of the form @{text "A \ B \ M A \ M B"}, for each premise @{text "M R\<^sub>i t"} in an introduction rule! - \item [@{command (HOL) "inductive_set"} and @{command (HOL) - "coinductive_set"}] are wrappers for to the previous commands, + \item @{command (HOL) "inductive_set"} and @{command (HOL) + "coinductive_set"} are wrappers for to the previous commands, allowing the definition of (co)inductive sets. - \item [@{attribute (HOL) mono}] declares monotonicity rules. These + \item @{attribute (HOL) mono} declares monotonicity rules. These rule are involved in the automated monotonicity proof of @{command (HOL) "inductive"}. - \end{descr} + \end{description} *} @@ -692,14 +690,14 @@ \begin{description} - \item [@{text R.intros}] is the list of introduction rules as proven + \item @{text R.intros} is the list of introduction rules as proven theorems, for the recursive predicates (or sets). The rules are also available individually, using the names given them in the theory file; - \item [@{text R.cases}] is the case analysis (or elimination) rule; + \item @{text R.cases} is the case analysis (or elimination) rule; - \item [@{text R.induct} or @{text R.coinduct}] is the (co)induction + \item @{text R.induct} or @{text R.coinduct} is the (co)induction rule. \end{description} @@ -817,13 +815,12 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \ - prover\<^sub>n"}] invokes the specified automated theorem provers on - the first subgoal. Provers are run in parallel, the first - successful result is displayed, and the other attempts are - terminated. + \item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \ prover\<^sub>n"} + invokes the specified automated theorem provers on the first + subgoal. Provers are run in parallel, the first successful result + is displayed, and the other attempts are terminated. Provers are defined in the theory context, see also @{command (HOL) print_atps}. If no provers are given as arguments to @{command @@ -834,28 +831,28 @@ and the maximum number of independent prover processes (default: 5); excessive provers are automatically terminated. - \item [@{command (HOL) print_atps}] prints the list of automated + \item @{command (HOL) print_atps} prints the list of automated theorem provers available to the @{command (HOL) sledgehammer} command. - \item [@{command (HOL) atp_info}] prints information about presently + \item @{command (HOL) atp_info} prints information about presently running provers, including elapsed runtime, and the remaining time until timeout. - \item [@{command (HOL) atp_kill}] terminates all presently running + \item @{command (HOL) atp_kill} terminates all presently running provers. - \item [@{method (HOL) metis}~@{text "facts"}] invokes the Metis - prover with the given facts. Metis is an automated proof tool of - medium strength, but is fully integrated into Isabelle/HOL, with - explicit inferences going through the kernel. Thus its results are + \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover + with the given facts. Metis is an automated proof tool of medium + strength, but is fully integrated into Isabelle/HOL, with explicit + inferences going through the kernel. Thus its results are guaranteed to be ``correct by construction''. Note that all facts used with Metis need to be specified as explicit arguments. There are no rule declarations as for other Isabelle provers, like @{method blast} or @{method fast}. - \end{descr} + \end{description} *} @@ -887,13 +884,13 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}] - admit to reason about inductive types. Rules are selected according - to the declarations by the @{attribute cases} and @{attribute - induct} attributes, cf.\ \secref{sec:cases-induct}. The @{command - (HOL) datatype} package already takes care of this. + \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit + to reason about inductive types. Rules are selected according to + the declarations by the @{attribute cases} and @{attribute induct} + attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL) + datatype} package already takes care of this. These unstructured tactics feature both goal addressing and dynamic instantiation. Note that named rule cases are \emph{not} provided @@ -903,8 +900,8 @@ statements, only the compact object-logic conclusion of the subgoal being addressed. - \item [@{method (HOL) ind_cases} and @{command (HOL) - "inductive_cases"}] provide an interface to the internal @{ML_text + \item @{method (HOL) ind_cases} and @{command (HOL) + "inductive_cases"} provide an interface to the internal @{ML_text mk_cases} operation. Rules are simplified in an unrestricted forward manner. @@ -915,7 +912,7 @@ ind_cases} method allows to specify a list of variables that should be generalized before applying the resulting rule. - \end{descr} + \end{description} *} @@ -977,12 +974,12 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "value"}~@{text t}] evaluates and prints a - term using the code generator. + \item @{command (HOL) "value"}~@{text t} evaluates and prints a term + using the code generator. - \end{descr} + \end{description} \medskip The other framework generates code from functional programs (including overloading using type classes) to SML \cite{SML}, OCaml @@ -1079,14 +1076,14 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "export_code"}] is the canonical interface - for generating and serializing code: for a given list of constants, - code is generated for the specified target languages. Abstract code - is cached incrementally. If no constant is given, the currently - cached code is serialized. If no serialization instruction is - given, only abstract code is cached. + \item @{command (HOL) "export_code"} is the canonical interface for + generating and serializing code: for a given list of constants, code + is generated for the specified target languages. Abstract code is + cached incrementally. If no constant is given, the currently cached + code is serialized. If no serialization instruction is given, only + abstract code is cached. Constants may be specified by giving them literally, referring to all executable contants within a certain theory by giving @{text @@ -1111,71 +1108,70 @@ "deriving (Read, Show)"}'' clause to each appropriate datatype declaration. - \item [@{command (HOL) "code_thms"}] prints a list of theorems + \item @{command (HOL) "code_thms"} prints a list of theorems representing the corresponding program containing all given constants; if no constants are given, the currently cached code theorems are printed. - \item [@{command (HOL) "code_deps"}] visualizes dependencies of + \item @{command (HOL) "code_deps"} visualizes dependencies of theorems representing the corresponding program containing all given constants; if no constants are given, the currently cached code theorems are visualized. - \item [@{command (HOL) "code_datatype"}] specifies a constructor set + \item @{command (HOL) "code_datatype"} specifies a constructor set for a logical type. - \item [@{command (HOL) "code_const"}] associates a list of constants + \item @{command (HOL) "code_const"} associates a list of constants with target-specific serializations; omitting a serialization deletes an existing serialization. - \item [@{command (HOL) "code_type"}] associates a list of type + \item @{command (HOL) "code_type"} associates a list of type constructors with target-specific serializations; omitting a serialization deletes an existing serialization. - \item [@{command (HOL) "code_class"}] associates a list of classes - with target-specific class names; omitting a - serialization deletes an existing serialization. - This applies only to \emph{Haskell}. + \item @{command (HOL) "code_class"} associates a list of classes + with target-specific class names; omitting a serialization deletes + an existing serialization. This applies only to \emph{Haskell}. - \item [@{command (HOL) "code_instance"}] declares a list of type + \item @{command (HOL) "code_instance"} declares a list of type constructor / class instance relations as ``already present'' for a given target. Omitting a ``@{text "-"}'' deletes an existing ``already present'' declaration. This applies only to \emph{Haskell}. - \item [@{command (HOL) "code_monad"}] provides an auxiliary - mechanism to generate monadic code for Haskell. + \item @{command (HOL) "code_monad"} provides an auxiliary mechanism + to generate monadic code for Haskell. - \item [@{command (HOL) "code_reserved"}] declares a list of names as + \item @{command (HOL) "code_reserved"} declares a list of names as reserved for a given target, preventing it to be shadowed by any generated code. - \item [@{command (HOL) "code_include"}] adds arbitrary named content + \item @{command (HOL) "code_include"} adds arbitrary named content (``include'') to generated code. A ``@{text "-"}'' as last argument will remove an already added ``include''. - \item [@{command (HOL) "code_modulename"}] declares aliasings from - one module name onto another. + \item @{command (HOL) "code_modulename"} declares aliasings from one + module name onto another. - \item [@{command (HOL) "code_abort"}] declares constants which - are not required to have a definition by means of defining equations; - if needed these are implemented by program abort instead. + \item @{command (HOL) "code_abort"} declares constants which are not + required to have a definition by means of defining equations; if + needed these are implemented by program abort instead. - \item [@{attribute (HOL) code}] explicitly selects (or - with option ``@{text "del"}'' deselects) a defining equation for - code generation. Usually packages introducing defining equations - provide a reasonable default setup for selection. + \item @{attribute (HOL) code} explicitly selects (or with option + ``@{text "del"}'' deselects) a defining equation for code + generation. Usually packages introducing defining equations provide + a reasonable default setup for selection. - \item [@{attribute (HOL) code}@{text inline}] declares (or with + \item @{attribute (HOL) code}~@{text inline} declares (or with option ``@{text "del"}'' removes) inlining theorems which are applied as rewrite rules to any defining equation during preprocessing. - \item [@{command (HOL) "print_codesetup"}] gives an overview on + \item @{command (HOL) "print_codesetup"} gives an overview on selected defining equations, code generator datatypes and preprocessor setup. - \end{descr} + \end{description} *} @@ -1193,27 +1189,27 @@ decl: ((name ':')? term '(' 'overloaded' ')'?) \end{rail} - \begin{descr} + \begin{description} - \item [@{command (HOL) "specification"}~@{text "decls \"}] sets up a + \item @{command (HOL) "specification"}~@{text "decls \"} sets up a goal stating the existence of terms with the properties specified to hold for the constants given in @{text decls}. After finishing the proof, the theory will be augmented with definitions for the given constants, as well as with theorems stating the properties for these constants. - \item [@{command (HOL) "ax_specification"}~@{text "decls \"}] sets - up a goal stating the existence of terms with the properties - specified to hold for the constants given in @{text decls}. After - finishing the proof, the theory will be augmented with axioms - expressing the properties given in the first place. + \item @{command (HOL) "ax_specification"}~@{text "decls \"} sets up + a goal stating the existence of terms with the properties specified + to hold for the constants given in @{text decls}. After finishing + the proof, the theory will be augmented with axioms expressing the + properties given in the first place. - \item [@{text decl}] declares a constant to be defined by the + \item @{text decl} declares a constant to be defined by the specification given. The definition for the constant @{text c} is bound to the name @{text c_def} unless a theorem name is given in the declaration. Overloaded constants should be declared as such. - \end{descr} + \end{description} Whether to use @{command (HOL) "specification"} or @{command (HOL) "ax_specification"} is to some extent a matter of style. @{command diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/Misc.thy --- a/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/Misc.thy Thu Nov 13 21:43:46 2008 +0100 @@ -43,42 +43,42 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "pr"}~@{text "goals, prems"}] prints the current + \item @{command "pr"}~@{text "goals, prems"} prints the current proof state (if present), including the proof context, current facts and goals. The optional limit arguments affect the number of goals and premises to be displayed, which is initially 10 for both. Omitting limit values leaves the current setting unchanged. - \item [@{command "thm"}~@{text "a\<^sub>1 \ a\<^sub>n"}] retrieves + \item @{command "thm"}~@{text "a\<^sub>1 \ a\<^sub>n"} retrieves theorems from the current theory or proof context. Note that any attributes included in the theorem specifications are applied to a temporary context derived from the current theory or proof; the result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, \, a\<^sub>n"} do not have any permanent effect. - \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \}] + \item @{command "term"}~@{text t} and @{command "prop"}~@{text \} read, type-check and print terms or propositions according to the current theory or proof context; the inferred type of @{text t} is output as well. Note that these commands are also useful in inspecting the current environment of term abbreviations. - \item [@{command "typ"}~@{text \}] reads and prints types of the + \item @{command "typ"}~@{text \} reads and prints types of the meta-logic according to the current theory or proof context. - \item [@{command "prf"}] displays the (compact) proof term of the + \item @{command "prf"} displays the (compact) proof term of the current proof state (if present), or of the given theorems. Note that this requires proof terms to be switched on for the current object logic (see the ``Proof terms'' section of the Isabelle reference manual for information on how to do this). - \item [@{command "full_prf"}] is like @{command "prf"}, but displays + \item @{command "full_prf"} is like @{command "prf"}, but displays the full proof term, i.e.\ also displays information omitted in the compact proof term, which is denoted by ``@{text _}'' placeholders there. - \end{descr} + \end{description} All of the diagnostic commands above admit a list of @{text modes} to be specified, which is appended to the current print mode (see @@ -128,31 +128,31 @@ Note that there are some further ones available, such as for the set of rules declared for simplifications. - \begin{descr} + \begin{description} - \item [@{command "print_commands"}] prints Isabelle's outer theory + \item @{command "print_commands"} prints Isabelle's outer theory syntax, including keywords and command. - \item [@{command "print_theory"}] prints the main logical content of + \item @{command "print_theory"} prints the main logical content of the theory context; the ``@{text "!"}'' option indicates extra verbosity. - \item [@{command "print_syntax"}] prints the inner syntax of types + \item @{command "print_syntax"} prints the inner syntax of types and terms, depending on the current context. The output can be very verbose, including grammar tables and syntax translation rules. See \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's inner syntax. - \item [@{command "print_methods"}] prints all proof methods + \item @{command "print_methods"} prints all proof methods available in the current theory context. - \item [@{command "print_attributes"}] prints all attributes + \item @{command "print_attributes"} prints all attributes available in the current theory context. - \item [@{command "print_theorems"}] prints theorems resulting from + \item @{command "print_theorems"} prints theorems resulting from the last command. - \item [@{command "find_theorems"}~@{text criteria}] retrieves facts + \item @{command "find_theorems"}~@{text criteria} retrieves facts from the theory or proof context matching all of given search criteria. The criterion @{text "name: p"} selects all theorems whose fully qualified name matches pattern @{text p}, which may @@ -172,17 +172,17 @@ default, duplicates are removed from the search result. Use @{text with_dups} to display duplicates. - \item [@{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"}] + \item @{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"} visualizes dependencies of facts, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - \item [@{command "print_facts"}] prints all local facts of the + \item @{command "print_facts"} prints all local facts of the current context, both named and unnamed ones. - \item [@{command "print_binds"}] prints all term abbreviations + \item @{command "print_binds"} prints all term abbreviations present in the context. - \end{descr} + \end{description} *} @@ -229,18 +229,18 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "cd"}~@{text path}] changes the current directory + \item @{command "cd"}~@{text path} changes the current directory of the Isabelle process. - \item [@{command "pwd"}] prints the current working directory. + \item @{command "pwd"} prints the current working directory. - \item [@{command "use_thy"}~@{text A}] preload theory @{text A}. + \item @{command "use_thy"}~@{text A} preload theory @{text A}. These system commands are scarcely used when working interactively, since loading of theories is done automatically as required. - \end{descr} + \end{description} *} end diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/Proof.thy Thu Nov 13 21:43:46 2008 +0100 @@ -13,24 +13,24 @@ facts, and open goals. Isar/VM transitions are \emph{typed} according to the following three different modes of operation: - \begin{descr} + \begin{description} - \item [@{text "proof(prove)"}] means that a new goal has just been + \item @{text "proof(prove)"} means that a new goal has just been stated that is now to be \emph{proven}; the next command may refine it by some proof method, and enter a sub-proof to establish the actual result. - \item [@{text "proof(state)"}] is like a nested theory mode: the + \item @{text "proof(state)"} is like a nested theory mode: the context may be augmented by \emph{stating} additional assumptions, intermediate results etc. - \item [@{text "proof(chain)"}] is intermediate between @{text + \item @{text "proof(chain)"} is intermediate between @{text "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\ the contents of the special ``@{fact_ref this}'' register) have been just picked up in order to be used when refining the goal claimed next. - \end{descr} + \end{description} The proof mode indicator may be read as a verb telling the writer what kind of operation may be performed next. The corresponding @@ -67,12 +67,12 @@ parentheses as well. These typically achieve a stronger forward style of reasoning. - \begin{descr} + \begin{description} - \item [@{command "next"}] switches to a fresh block within a + \item @{command "next"} switches to a fresh block within a sub-proof, resetting the local context to the initial one. - \item [@{command "{"} and @{command "}"}] explicitly open and close + \item @{command "{"} and @{command "}"} explicitly open and close blocks. Any current facts pass through ``@{command "{"}'' unchanged, while ``@{command "}"}'' causes any result to be \emph{exported} into the enclosing context. Thus fixed variables @@ -82,7 +82,7 @@ forward reasoning --- in contrast to plain backward reasoning with the result exported at @{command "show"} time. - \end{descr} + \end{description} *} @@ -170,13 +170,13 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "fix"}~@{text x}] introduces a local variable - @{text x} that is \emph{arbitrary, but fixed.} + \item @{command "fix"}~@{text x} introduces a local variable @{text + x} that is \emph{arbitrary, but fixed.} - \item [@{command "assume"}~@{text "a: \"} and @{command - "presume"}~@{text "a: \"}] introduce a local fact @{text "\ \ \"} by + \item @{command "assume"}~@{text "a: \"} and @{command + "presume"}~@{text "a: \"} introduce a local fact @{text "\ \ \"} by assumption. Subsequent results applied to an enclosing goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command "assume"} expects to be able to unify with existing premises in the @@ -186,7 +186,7 @@ @{keyword_ref "and"}; the resulting list of current facts consists of all of these concatenated. - \item [@{command "def"}~@{text "x \ t"}] introduces a local + \item @{command "def"}~@{text "x \ t"} introduces a local (non-polymorphic) definition. In results exported from the context, @{text x} is replaced by @{text t}. Basically, ``@{command "def"}~@{text "x \ t"}'' abbreviates ``@{command "fix"}~@{text @@ -196,7 +196,7 @@ The default name for the definitional equation is @{text x_def}. Several simultaneous definitions may be given at the same time. - \end{descr} + \end{description} The special name @{fact_ref prems} refers to all assumptions of the current context as a list of theorems. This feature should be used @@ -246,20 +246,18 @@ The syntax of @{keyword "is"} patterns follows \railnonterm{termpat} or \railnonterm{proppat} (see \secref{sec:term-decls}). - \begin{descr} + \begin{description} - \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \ \ - p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text - "p\<^sub>1, \, p\<^sub>n"} by simultaneous higher-order matching - against terms @{text "t\<^sub>1, \, t\<^sub>n"}. + \item @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \ \ p\<^sub>n = t\<^sub>n"} binds any + text variables in patterns @{text "p\<^sub>1, \, p\<^sub>n"} by simultaneous + higher-order matching against terms @{text "t\<^sub>1, \, t\<^sub>n"}. - \item [@{text "(\ p\<^sub>1 \ p\<^sub>n)"}] resembles @{command - "let"}, but matches @{text "p\<^sub>1, \, p\<^sub>n"} against the - preceding statement. Also note that @{keyword "is"} is not a - separate command, but part of others (such as @{command "assume"}, - @{command "have"} etc.). + \item @{text "(\ p\<^sub>1 \ p\<^sub>n)"} resembles @{command "let"}, but + matches @{text "p\<^sub>1, \, p\<^sub>n"} against the preceding statement. Also + note that @{keyword "is"} is not a separate command, but part of + others (such as @{command "assume"}, @{command "have"} etc.). - \end{descr} + \end{description} Some \emph{implicit} term abbreviations\index{term abbreviations} for goals and facts are available as well. For any open goal, @@ -304,14 +302,14 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "note"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] - recalls existing facts @{text "b\<^sub>1, \, b\<^sub>n"}, binding - the result as @{text a}. Note that attributes may be involved as - well, both on the left and right hand sides. + \item @{command "note"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} recalls existing facts + @{text "b\<^sub>1, \, b\<^sub>n"}, binding the result as @{text a}. Note that + attributes may be involved as well, both on the left and right hand + sides. - \item [@{command "then"}] indicates forward chaining by the current + \item @{command "then"} indicates forward chaining by the current facts in order to establish the goal to be claimed next. The initial proof method invoked to refine that will be offered the facts to do ``anything appropriate'' (see also @@ -321,26 +319,23 @@ facts into the goal state before operation. This provides a simple scheme to control relevance of facts in automated proof search. - \item [@{command "from"}~@{text b}] abbreviates ``@{command + \item @{command "from"}~@{text b} abbreviates ``@{command "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is equivalent to ``@{command "from"}~@{text this}''. - \item [@{command "with"}~@{text "b\<^sub>1 \ b\<^sub>n"}] - abbreviates ``@{command "from"}~@{text "b\<^sub>1 \ b\<^sub>n \ - this"}''; thus the forward chaining is from earlier facts together - with the current ones. + \item @{command "with"}~@{text "b\<^sub>1 \ b\<^sub>n"} abbreviates ``@{command + "from"}~@{text "b\<^sub>1 \ b\<^sub>n \ this"}''; thus the forward chaining + is from earlier facts together with the current ones. - \item [@{command "using"}~@{text "b\<^sub>1 \ b\<^sub>n"}] augments - the facts being currently indicated for use by a subsequent - refinement step (such as @{command_ref "apply"} or @{command_ref - "proof"}). + \item @{command "using"}~@{text "b\<^sub>1 \ b\<^sub>n"} augments the facts being + currently indicated for use by a subsequent refinement step (such as + @{command_ref "apply"} or @{command_ref "proof"}). - \item [@{command "unfolding"}~@{text "b\<^sub>1 \ b\<^sub>n"}] is - structurally similar to @{command "using"}, but unfolds definitional - equations @{text "b\<^sub>1, \ b\<^sub>n"} throughout the goal state - and facts. + \item @{command "unfolding"}~@{text "b\<^sub>1 \ b\<^sub>n"} is structurally + similar to @{command "using"}, but unfolds definitional equations + @{text "b\<^sub>1, \ b\<^sub>n"} throughout the goal state and facts. - \end{descr} + \end{description} Forward chaining with an empty list of theorems is the same as not chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no @@ -426,9 +421,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "lemma"}~@{text "a: \"}] enters proof mode with + \item @{command "lemma"}~@{text "a: \"} enters proof mode with @{text \} as main goal, eventually resulting in some fact @{text "\ \"} to be put back into the target context. An additional \railnonterm{context} specification may build up an initial proof @@ -436,20 +431,20 @@ and syntax as well, see the definition of @{syntax contextelem} in \secref{sec:locale}. - \item [@{command "theorem"}~@{text "a: \"} and @{command - "corollary"}~@{text "a: \"}] are essentially the same as @{command + \item @{command "theorem"}~@{text "a: \"} and @{command + "corollary"}~@{text "a: \"} are essentially the same as @{command "lemma"}~@{text "a: \"}, but the facts are internally marked as being of a different kind. This discrimination acts like a formal comment. - \item [@{command "have"}~@{text "a: \"}] claims a local goal, + \item @{command "have"}~@{text "a: \"} claims a local goal, eventually resulting in a fact within the current logical context. This operation is completely independent of any pending sub-goals of an enclosing goal statements, so @{command "have"} may be freely used for experimental exploration of potential results within a proof body. - \item [@{command "show"}~@{text "a: \"}] is like @{command + \item @{command "show"}~@{text "a: \"} is like @{command "have"}~@{text "a: \"} plus a second stage to refine some pending sub-goal for each one of the finished result, after having been exported into the corresponding context (at the head of the @@ -466,20 +461,20 @@ Problem! Local statement will fail to solve any pending goal \end{ttbox} - \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command + \item @{command "hence"} abbreviates ``@{command "then"}~@{command "have"}'', i.e.\ claims a local goal to be proven by forward chaining the current facts. Note that @{command "hence"} is also equivalent to ``@{command "from"}~@{text this}~@{command "have"}''. - \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command + \item @{command "thus"} abbreviates ``@{command "then"}~@{command "show"}''. Note that @{command "thus"} is also equivalent to ``@{command "from"}~@{text this}~@{command "show"}''. - \item [@{command "print_statement"}~@{text a}] prints facts from the + \item @{command "print_statement"}~@{text a} prints facts from the current theory or proof context in long statement form, according to the syntax for @{command "lemma"} given above. - \end{descr} + \end{description} Any goal statement causes some term abbreviations (such as @{variable_ref "?thesis"}) to be bound automatically, see also @@ -621,45 +616,43 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by - proof method @{text "m\<^sub>1"}; facts for forward chaining are - passed if so indicated by @{text "proof(chain)"} mode. + \item @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof + method @{text "m\<^sub>1"}; facts for forward chaining are passed if so + indicated by @{text "proof(chain)"} mode. - \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining - goals by proof method @{text "m\<^sub>2"} and concludes the - sub-proof by assumption. If the goal had been @{text "show"} (or - @{text "thus"}), some pending sub-goal is solved as well by the rule - resulting from the result \emph{exported} into the enclosing goal - context. Thus @{text "qed"} may fail for two reasons: either @{text - "m\<^sub>2"} fails, or the resulting rule does not fit to any - pending goal\footnote{This includes any additional ``strong'' - assumptions as introduced by @{command "assume"}.} of the enclosing - context. Debugging such a situation might involve temporarily - changing @{command "show"} into @{command "have"}, or weakening the - local context by replacing occurrences of @{command "assume"} by - @{command "presume"}. + \item @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by + proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption. + If the goal had been @{text "show"} (or @{text "thus"}), some + pending sub-goal is solved as well by the rule resulting from the + result \emph{exported} into the enclosing goal context. Thus @{text + "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the + resulting rule does not fit to any pending goal\footnote{This + includes any additional ``strong'' assumptions as introduced by + @{command "assume"}.} of the enclosing context. Debugging such a + situation might involve temporarily changing @{command "show"} into + @{command "have"}, or weakening the local context by replacing + occurrences of @{command "assume"} by @{command "presume"}. - \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a - \emph{terminal proof}\index{proof!terminal}; it abbreviates - @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text - "m\<^sub>2"}, but with backtracking across both methods. Debugging - an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} - command can be done by expanding its definition; in many cases - @{command "proof"}~@{text "m\<^sub>1"} (or even @{text - "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the + \item @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \emph{terminal + proof}\index{proof!terminal}; it abbreviates @{command + "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text "m\<^sub>2"}, but with + backtracking across both methods. Debugging an unsuccessful + @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its + definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even + @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the problem. - \item [``@{command ".."}''] is a \emph{default + \item ``@{command ".."}'' is a \emph{default proof}\index{proof!default}; it abbreviates @{command "by"}~@{text "rule"}. - \item [``@{command "."}''] is a \emph{trivial + \item ``@{command "."}'' is a \emph{trivial proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text "this"}. - \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake} + \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake} pretending to solve the pending claim without further ado. This only works in interactive development, or if the @{ML quick_and_dirty} flag is enabled (in ML). Facts emerging from fake @@ -670,7 +663,7 @@ The most important application of @{command "sorry"} is to support experimentation and top-down proof development. - \end{descr} + \end{description} *} @@ -719,27 +712,27 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [``@{method "-"}'' (minus)] does nothing but insert the - forward chaining facts as premises into the goal. Note that command + \item ``@{method "-"}'' (minus) does nothing but insert the forward + chaining facts as premises into the goal. Note that command @{command_ref "proof"} without any method actually performs a single reduction step using the @{method_ref rule} method; thus a plain \emph{do-nothing} proof step would be ``@{command "proof"}~@{text "-"}'' rather than @{command "proof"} alone. - \item [@{method "fact"}~@{text "a\<^sub>1 \ a\<^sub>n"}] composes - some fact from @{text "a\<^sub>1, \, a\<^sub>n"} (or implicitly from - the current proof context) modulo unification of schematic type and - term variables. The rule structure is not taken into account, i.e.\ - meta-level implication is considered atomic. This is the same - principle underlying literal facts (cf.\ \secref{sec:syn-att}): - ``@{command "have"}~@{text "\"}~@{command "by"}~@{text fact}'' is - equivalent to ``@{command "note"}~@{verbatim "`"}@{text \}@{verbatim - "`"}'' provided that @{text "\ \"} is an instance of some known - @{text "\ \"} in the proof context. + \item @{method "fact"}~@{text "a\<^sub>1 \ a\<^sub>n"} composes some fact from + @{text "a\<^sub>1, \, a\<^sub>n"} (or implicitly from the current proof context) + modulo unification of schematic type and term variables. The rule + structure is not taken into account, i.e.\ meta-level implication is + considered atomic. This is the same principle underlying literal + facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~@{text + "\"}~@{command "by"}~@{text fact}'' is equivalent to ``@{command + "note"}~@{verbatim "`"}@{text \}@{verbatim "`"}'' provided that + @{text "\ \"} is an instance of some known @{text "\ \"} in the + proof context. - \item [@{method assumption}] solves some goal by a single assumption + \item @{method assumption} solves some goal by a single assumption step. All given facts are guaranteed to participate in the refinement; this means there may be only 0 or 1 in the first place. Recall that @{command "qed"} (\secref{sec:proof-steps}) already @@ -747,15 +740,14 @@ proofs usually need not quote the @{method assumption} method at all. - \item [@{method this}] applies all of the current facts directly as + \item @{method this} applies all of the current facts directly as rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~@{text this}''. - \item [@{method rule}~@{text "a\<^sub>1 \ a\<^sub>n"}] applies some - rule given as argument in backward manner; facts are used to reduce - the rule before applying it to the goal. Thus @{method rule} - without facts is plain introduction, while with facts it becomes - elimination. + \item @{method rule}~@{text "a\<^sub>1 \ a\<^sub>n"} applies some rule given as + argument in backward manner; facts are used to reduce the rule + before applying it to the goal. Thus @{method rule} without facts + is plain introduction, while with facts it becomes elimination. When no arguments are given, the @{method rule} method tries to pick appropriate rules automatically, as declared in the current context @@ -764,10 +756,10 @@ default behavior of @{command "proof"} and ``@{command ".."}'' (double-dot) steps (see \secref{sec:proof-steps}). - \item [@{method iprover}] performs intuitionistic proof search, + \item @{method iprover} performs intuitionistic proof search, depending on specifically declared rules from the context, or given as explicit arguments. Chained facts are inserted into the goal - before commencing proof search; ``@{method iprover}@{text "!"}'' + before commencing proof search; ``@{method iprover}@{text "!"}'' means to include the current @{fact prems} as well. Rules need to be classified as @{attribute (Pure) intro}, @@ -779,8 +771,8 @@ explicit weight annotation may be given as well; otherwise the number of rule premises will be taken into account here. - \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and - @{attribute (Pure) dest}] declare introduction, elimination, and + \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and + @{attribute (Pure) dest} declare introduction, elimination, and destruct rules, to be used with the @{method rule} and @{method iprover} methods. Note that the latter will ignore rules declared with ``@{text "?"}'', while ``@{text "!"}'' are used most @@ -791,33 +783,31 @@ present versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}. - \item [@{attribute rule}~@{text del}] undeclares introduction, + \item @{attribute rule}~@{text del} undeclares introduction, elimination, or destruct rules. - \item [@{attribute OF}~@{text "a\<^sub>1 \ a\<^sub>n"}] applies some - theorem to all of the given rules @{text "a\<^sub>1, \, a\<^sub>n"} - (in parallel). This corresponds to the @{ML [source=false] "op MRS"} operation in - ML, but note the reversed order. Positions may be effectively - skipped by including ``@{text _}'' (underscore) as argument. + \item @{attribute OF}~@{text "a\<^sub>1 \ a\<^sub>n"} applies some theorem to all + of the given rules @{text "a\<^sub>1, \, a\<^sub>n"} (in parallel). This + corresponds to the @{ML [source=false] "op MRS"} operation in ML, + but note the reversed order. Positions may be effectively skipped + by including ``@{text _}'' (underscore) as argument. - \item [@{attribute of}~@{text "t\<^sub>1 \ t\<^sub>n"}] performs - positional instantiation of term variables. The terms @{text - "t\<^sub>1, \, t\<^sub>n"} are substituted for any schematic - variables occurring in a theorem from left to right; ``@{text _}'' - (underscore) indicates to skip a position. Arguments following a - ``@{text "concl:"}'' specification refer to positions of the - conclusion of a rule. + \item @{attribute of}~@{text "t\<^sub>1 \ t\<^sub>n"} performs positional + instantiation of term variables. The terms @{text "t\<^sub>1, \, t\<^sub>n"} are + substituted for any schematic variables occurring in a theorem from + left to right; ``@{text _}'' (underscore) indicates to skip a + position. Arguments following a ``@{text "concl:"}'' specification + refer to positions of the conclusion of a rule. - \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \ \ - x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic - type and term variables occurring in a theorem. Schematic variables - have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}). - The question mark may be omitted if the variable name is a plain - identifier without index. As type instantiations are inferred from - term instantiations, explicit type instantiations are seldom - necessary. + \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \ \ x\<^sub>n = t\<^sub>n"} + performs named instantiation of schematic type and term variables + occurring in a theorem. Schematic variables have to be specified on + the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may + be omitted if the variable name is a plain identifier without index. + As type instantiations are inferred from term instantiations, + explicit type instantiations are seldom necessary. - \end{descr} + \end{description} *} @@ -851,20 +841,20 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "apply"}~@{text m}] applies proof method @{text m} - in initial position, but unlike @{command "proof"} it retains - ``@{text "proof(prove)"}'' mode. Thus consecutive method - applications may be given just as in tactic scripts. + \item @{command "apply"}~@{text m} applies proof method @{text m} in + initial position, but unlike @{command "proof"} it retains ``@{text + "proof(prove)"}'' mode. Thus consecutive method applications may be + given just as in tactic scripts. Facts are passed to @{text m} as indicated by the goal's forward-chain mode, and are \emph{consumed} afterwards. Thus any further @{command "apply"} command would always work in a purely backward manner. - \item [@{command "apply_end"}~@{text "m"}] applies proof method - @{text m} as if in terminal position. Basically, this simulates a + \item @{command "apply_end"}~@{text "m"} applies proof method @{text + m} as if in terminal position. Basically, this simulates a multi-step tactic script for @{command "qed"}, but may be given anywhere within the proof body. @@ -873,22 +863,22 @@ "qed"}). Thus the proof method may not refer to any assumptions introduced in the current body, for example. - \item [@{command "done"}] completes a proof script, provided that - the current goal state is solved completely. Note that actual + \item @{command "done"} completes a proof script, provided that the + current goal state is solved completely. Note that actual structured proof commands (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude proof scripts as well. - \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text - n}] shuffle the list of pending goals: @{command "defer"} puts off + \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n} + shuffle the list of pending goals: @{command "defer"} puts off sub-goal @{text n} to the end of the list (@{text "n = 1"} by default), while @{command "prefer"} brings sub-goal @{text n} to the front. - \item [@{command "back"}] does back-tracking over the result - sequence of the latest proof command. Basically, any proof command - may return multiple results. + \item @{command "back"} does back-tracking over the result sequence + of the latest proof command. Basically, any proof command may + return multiple results. - \end{descr} + \end{description} Any proper Isar proof method may be used with tactic script commands such as @{command "apply"}. A few additional emulations of actual @@ -909,9 +899,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "method_setup"}~@{text "name = text description"}] + \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 [source=false] "Args.src -> Proof.context -> Proof.method"}. Parsing concrete @@ -937,7 +927,7 @@ Drule.multi_resolves}), while automatic ones just insert the facts using @{ML Method.insert_tac} before applying the main tactic. - \end{descr} + \end{description} *} @@ -1082,44 +1072,44 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "also"}~@{text "(a\<^sub>1 \ a\<^sub>n)"}] - maintains the auxiliary @{fact calculation} register as follows. - The first occurrence of @{command "also"} in some calculational - thread initializes @{fact calculation} by @{fact this}. Any - subsequent @{command "also"} on the same level of block-structure - updates @{fact calculation} by some transitivity rule applied to - @{fact calculation} and @{fact this} (in that order). Transitivity - rules are picked from the current context, unless alternative rules - are given as explicit arguments. + \item @{command "also"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintains the auxiliary + @{fact calculation} register as follows. The first occurrence of + @{command "also"} in some calculational thread initializes @{fact + calculation} by @{fact this}. Any subsequent @{command "also"} on + the same level of block-structure updates @{fact calculation} by + some transitivity rule applied to @{fact calculation} and @{fact + this} (in that order). Transitivity rules are picked from the + current context, unless alternative rules are given as explicit + arguments. - \item [@{command "finally"}~@{text "(a\<^sub>1 \ a\<^sub>n)"}] - maintaining @{fact calculation} in the same way as @{command - "also"}, and concludes the current calculational thread. The final - result is exhibited as fact for forward chaining towards the next - goal. Basically, @{command "finally"} just abbreviates @{command - "also"}~@{command "from"}~@{fact calculation}. Typical idioms for - concluding calculational proofs are ``@{command "finally"}~@{command + \item @{command "finally"}~@{text "(a\<^sub>1 \ a\<^sub>n)"} maintaining @{fact + calculation} in the same way as @{command "also"}, and concludes the + current calculational thread. The final result is exhibited as fact + for forward chaining towards the next goal. Basically, @{command + "finally"} just abbreviates @{command "also"}~@{command + "from"}~@{fact calculation}. Typical idioms for concluding + calculational proofs are ``@{command "finally"}~@{command "show"}~@{text ?thesis}~@{command "."}'' and ``@{command "finally"}~@{command "have"}~@{text \}~@{command "."}''. - \item [@{command "moreover"} and @{command "ultimately"}] are + \item @{command "moreover"} and @{command "ultimately"} are analogous to @{command "also"} and @{command "finally"}, but collect results only, without applying rules. - \item [@{command "print_trans_rules"}] prints the list of - transitivity rules (for calculational commands @{command "also"} and - @{command "finally"}) and symmetry rules (for the @{attribute - symmetric} operation and single step elimination patters) of the - current context. + \item @{command "print_trans_rules"} prints the list of transitivity + rules (for calculational commands @{command "also"} and @{command + "finally"}) and symmetry rules (for the @{attribute symmetric} + operation and single step elimination patters) of the current + context. - \item [@{attribute trans}] declares theorems as transitivity rules. + \item @{attribute trans} declares theorems as transitivity rules. - \item [@{attribute sym}] declares symmetry rules, as well as + \item @{attribute sym} declares symmetry rules, as well as @{attribute "Pure.elim"}@{text "?"} rules. - \item [@{attribute symmetric}] resolves a theorem with some rule + \item @{attribute symmetric} resolves a theorem with some rule declared as @{attribute sym} in the current context. For example, ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a swapped fact derived from that assumption. @@ -1129,7 +1119,7 @@ "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text "y = x"}~@{command ".."}''. - \end{descr} + \end{description} *} @@ -1209,60 +1199,55 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "case"}~@{text "(c x\<^sub>1 \ x\<^sub>m)"}] - invokes a named local context @{text "c: x\<^sub>1, \, x\<^sub>m, - \\<^sub>1, \, \\<^sub>m"}, as provided by an appropriate - proof method (such as @{method_ref cases} and @{method_ref induct}). - The command ``@{command "case"}~@{text "(c x\<^sub>1 \ - x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ - x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ - \\<^sub>n"}''. + \item @{command "case"}~@{text "(c x\<^sub>1 \ x\<^sub>m)"} invokes a named local + context @{text "c: x\<^sub>1, \, x\<^sub>m, \\<^sub>1, \, \\<^sub>m"}, as provided by an + appropriate proof method (such as @{method_ref cases} and + @{method_ref induct}). The command ``@{command "case"}~@{text "(c + x\<^sub>1 \ x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \ + x\<^sub>m"}~@{command "assume"}~@{text "c: \\<^sub>1 \ \\<^sub>n"}''. - \item [@{command "print_cases"}] prints all local contexts of the + \item @{command "print_cases"} prints all local contexts of the current state, using Isar proof language notation. - \item [@{attribute case_names}~@{text "c\<^sub>1 \ c\<^sub>k"}] - declares names for the local contexts of premises of a theorem; - @{text "c\<^sub>1, \, c\<^sub>k"} refers to the \emph{suffix} of the - list of premises. + \item @{attribute case_names}~@{text "c\<^sub>1 \ c\<^sub>k"} declares names for + the local contexts of premises of a theorem; @{text "c\<^sub>1, \, c\<^sub>k"} + refers to the \emph{suffix} of the list of premises. - \item [@{attribute case_conclusion}~@{text "c d\<^sub>1 \ - d\<^sub>k"}] declares names for the conclusions of a named premise - @{text c}; here @{text "d\<^sub>1, \, d\<^sub>k"} refers to the - prefix of arguments of a logical formula built by nesting a binary - connective (e.g.\ @{text "\"}). + \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \ d\<^sub>k"} declares + names for the conclusions of a named premise @{text c}; here @{text + "d\<^sub>1, \, d\<^sub>k"} refers to the prefix of arguments of a logical formula + built by nesting a binary connective (e.g.\ @{text "\"}). Note that proof methods such as @{method induct} and @{method coinduct} already provide a default name for the conclusion as a whole. The need to name subformulas only arises with cases that split into several sub-cases, as in common co-induction rules. - \item [@{attribute params}~@{text "p\<^sub>1 \ p\<^sub>m \ \ - q\<^sub>1 \ q\<^sub>n"}] renames the innermost parameters of - premises @{text "1, \, n"} of some theorem. An empty list of names - may be given to skip positions, leaving the present parameters - unchanged. + \item @{attribute params}~@{text "p\<^sub>1 \ p\<^sub>m \ \ q\<^sub>1 \ q\<^sub>n"} renames + the innermost parameters of premises @{text "1, \, n"} of some + theorem. An empty list of names may be given to skip positions, + leaving the present parameters unchanged. Note that the default usage of case rules does \emph{not} directly expose parameters to the proof context. - \item [@{attribute consumes}~@{text n}] declares the number of - ``major premises'' of a rule, i.e.\ the number of facts to be - consumed when it is applied by an appropriate proof method. The - default value of @{attribute consumes} is @{text "n = 1"}, which is - appropriate for the usual kind of cases and induction rules for - inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any - @{attribute consumes} declaration given are treated as if - @{attribute consumes}~@{text 0} had been specified. + \item @{attribute consumes}~@{text n} declares the number of ``major + premises'' of a rule, i.e.\ the number of facts to be consumed when + it is applied by an appropriate proof method. The default value of + @{attribute consumes} is @{text "n = 1"}, which is appropriate for + the usual kind of cases and induction rules for inductive sets (cf.\ + \secref{sec:hol-inductive}). Rules without any @{attribute + consumes} declaration given are treated as if @{attribute + consumes}~@{text 0} had been specified. Note that explicit @{attribute consumes} declarations are only rarely needed; this is already taken care of automatically by the higher-level @{attribute cases}, @{attribute induct}, and @{attribute coinduct} declarations. - \end{descr} + \end{description} *} @@ -1310,9 +1295,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{method cases}~@{text "insts R"}] applies method @{method + \item @{method cases}~@{text "insts R"} applies method @{method rule} with an appropriate case distinction theorem, instantiated to the subjects @{text insts}. Symbolic case names are bound according to the rule's local contexts. @@ -1336,7 +1321,7 @@ term needs to be specified; this refers to the first variable of the last premise (it is usually the same for all cases). - \item [@{method induct}~@{text "insts R"}] is analogous to the + \item @{method induct}~@{text "insts R"} is analogous to the @{method cases} method, but refers to induction rules, which are determined as follows: @@ -1378,7 +1363,7 @@ pending variables in the rule. Such schematic induction rules rarely occur in practice, though. - \item [@{method coinduct}~@{text "inst R"}] is analogous to the + \item @{method coinduct}~@{text "inst R"} is analogous to the @{method induct} method, but refers to coinduction rules, which are determined as follows: @@ -1404,7 +1389,7 @@ specification may be required in order to specify the bisimulation to be used in the coinduction step. - \end{descr} + \end{description} Above methods produce named local contexts, as determined by the instantiated rule as given in the text. Beyond that, the @{method @@ -1473,13 +1458,13 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "print_induct_rules"}] prints cases and induct - rules for predicates (or sets) and types of the current context. + \item @{command "print_induct_rules"} prints cases and induct rules + for predicates (or sets) and types of the current context. - \item [@{attribute cases}, @{attribute induct}, and @{attribute - coinduct}] (as attributes) declare rules for reasoning about + \item @{attribute cases}, @{attribute induct}, and @{attribute + coinduct} (as attributes) declare rules for reasoning about (co)inductive predicates (or sets) and types, using the corresponding methods of the same name. Certain definitional packages of object-logics usually declare emerging cases and @@ -1498,7 +1483,7 @@ consumes}~@{text 0} is specified for ``type'' rules and @{attribute consumes}~@{text 1} for ``predicate'' / ``set'' rules. - \end{descr} + \end{description} *} end diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 21:43:46 2008 +0100 @@ -41,11 +41,11 @@ uses: 'uses' ((name | parname) +); \end{rail} - \begin{descr} + \begin{description} - \item [@{command "theory"}~@{text "A \ B\<^sub>1 \ - B\<^sub>n \"}] starts a new theory @{text A} based on the - merge of existing theories @{text "B\<^sub>1 \ B\<^sub>n"}. + \item @{command "theory"}~@{text "A \ B\<^sub>1 \ B\<^sub>n \"} + starts a new theory @{text A} based on the merge of existing + theories @{text "B\<^sub>1 \ B\<^sub>n"}. Due to the possibility to import more than one ancestor, the resulting theory structure of an Isabelle session forms a directed @@ -62,11 +62,11 @@ other file formats require specific load commands defined by the corresponding tools or packages. - \item [@{command (global) "end"}] concludes the current theory + \item @{command (global) "end"} concludes the current theory definition. Note that local theory targets involve a local @{command (local) "end"}, which is clear from the nesting. - \end{descr} + \end{description} *} @@ -95,20 +95,20 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "context"}~@{text "c \"}] recommences an + \item @{command "context"}~@{text "c \"} recommences an existing locale or class context @{text c}. Note that locale and class definitions allow to include the @{keyword "begin"} keyword as well, in order to continue the local theory immediately after the initial specification. - \item [@{command (local) "end"}] concludes the current local theory + \item @{command (local) "end"} concludes the current local theory and continues the enclosing global theory. Note that a global @{command (global) "end"} has a different meaning: it concludes the theory itself (\secref{sec:begin-thy}). - \item [@{text "(\ c)"}] given after any local theory command + \item @{text "(\ c)"} given after any local theory command specifies an immediate target, e.g.\ ``@{command "definition"}~@{text "(\ c) \"}'' or ``@{command "theorem"}~@{text "(\ c) \"}''. This works both in a local or @@ -117,7 +117,7 @@ always produce a global result independently of the current target context. - \end{descr} + \end{description} The exact meaning of results produced within a local theory context depends on the underlying target infrastructure (locale, type class @@ -176,20 +176,20 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m - \ \\<^sub>1 \ \\<^sub>n"}] introduces several constants - simultaneously and states axiomatic properties for these. The - constants are marked as being specified once and for all, which - prevents additional specifications being issued later on. + \item @{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m \ \\<^sub>1 \ \\<^sub>n"} + introduces several constants simultaneously and states axiomatic + properties for these. The constants are marked as being specified + once and for all, which prevents additional specifications being + issued later on. Note that axiomatic specifications are only appropriate when declaring a new logical system; axiomatic specifications are restricted to global theory contexts. Normal applications should only use definitional mechanisms! - \item [@{command "definition"}~@{text "c \ eq"}] produces an + \item @{command "definition"}~@{text "c \ eq"} produces an internal definition @{text "c \ t"} according to the specification given as @{text eq}, which is then turned into a proven fact. The given proposition may deviate from internal meta-level equality @@ -203,9 +203,9 @@ @{text "f \ \x y. t"} and @{text "y \ 0 \ g x y = u"} instead of an unrestricted @{text "g \ \x y. u"}. - \item [@{command "abbreviation"}~@{text "c \ eq"}] introduces - a syntactic constant which is associated with a certain term - according to the meta-level equality @{text eq}. + \item @{command "abbreviation"}~@{text "c \ eq"} introduces a + syntactic constant which is associated with a certain term according + to the meta-level equality @{text eq}. Abbreviations participate in the usual type-inference process, but are expanded before the logic ever sees them. Pretty printing of @@ -220,20 +220,20 @@ declared for abbreviations, cf.\ @{command "syntax"} in \secref{sec:syn-trans}. - \item [@{command "print_abbrevs"}] prints all constant abbreviations + \item @{command "print_abbrevs"} prints all constant abbreviations of the current context. - \item [@{command "notation"}~@{text "c (mx)"}] associates mixfix + \item @{command "notation"}~@{text "c (mx)"} associates mixfix syntax with an existing constant or fixed variable. This is a robust interface to the underlying @{command "syntax"} primitive (\secref{sec:syn-trans}). Type declaration and internal syntactic representation of the given entity is retrieved from the context. - \item [@{command "no_notation"}] is similar to @{command - "notation"}, but removes the specified syntax annotation from the - present context. + \item @{command "no_notation"} is similar to @{command "notation"}, + but removes the specified syntax annotation from the present + context. - \end{descr} + \end{description} All of these specifications support local theory targets (cf.\ \secref{sec:target}). @@ -264,21 +264,21 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "declaration"}~@{text d}] adds the declaration + \item @{command "declaration"}~@{text d} adds the declaration function @{text d} of ML type @{ML_type declaration}, to the current local theory under construction. In later application contexts, the function is transformed according to the morphisms being involved in the interpretation hierarchy. - \item [@{command "declare"}~@{text thms}] declares theorems to the + \item @{command "declare"}~@{text thms} declares theorems to the current local theory context. No theorem binding is involved here, unlike @{command "theorems"} or @{command "lemmas"} (cf.\ \secref{sec:axms-thms}), so @{command "declare"} only has the effect of applying attributes as included in the theorem specification. - \end{descr} + \end{description} *} @@ -332,9 +332,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "locale"}~@{text "loc = import + body"}] defines a + \item @{command "locale"}~@{text "loc = import + body"} defines a new locale @{text loc} as a context consisting of a certain view of existing locales (@{text import}) plus some additional elements (@{text body}). Both @{text import} and @{text body} are optional; @@ -361,39 +361,43 @@ The @{text body} consists of basic context elements, further context expressions may be included as well. - \begin{descr} + \begin{description} - \item [@{element "fixes"}~@{text "x :: \ (mx)"}] declares a local + \item @{element "fixes"}~@{text "x :: \ (mx)"} declares a local parameter of type @{text \} and mixfix annotation @{text mx} (both are optional). The special syntax declaration ``@{text "(\)"}'' means that @{text x} may be referenced implicitly in this context. - \item [@{element "constrains"}~@{text "x :: \"}] introduces a type + \item @{element "constrains"}~@{text "x :: \"} introduces a type constraint @{text \} on the local parameter @{text x}. - \item [@{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"}] + \item @{element "assumes"}~@{text "a: \\<^sub>1 \ \\<^sub>n"} introduces local premises, similar to @{command "assume"} within a proof (cf.\ \secref{sec:proof-context}). - \item [@{element "defines"}~@{text "a: x \ t"}] defines a previously + \item @{element "defines"}~@{text "a: x \ t"} defines a previously declared parameter. This is similar to @{command "def"} within a proof (cf.\ \secref{sec:proof-context}), but @{element "defines"} takes an equational proposition instead of variable-term pair. The left-hand side of the equation may have additional arguments, e.g.\ ``@{element "defines"}~@{text "f x\<^sub>1 \ x\<^sub>n \ t"}''. - \item [@{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] + \item @{element "notes"}~@{text "a = b\<^sub>1 \ b\<^sub>n"} reconsiders facts within a local context. Most notably, this may include arbitrary declarations in any attribute specifications included here, e.g.\ a local @{attribute simp} rule. - The initial @{text import} specification of a locale + \item @{element "includes"}~@{text c} copies the specified context + in a statically scoped manner. Only available in the long goal + format of \secref{sec:goals}. + + In contrast, the initial @{text import} specification of a locale expression maintains a dynamic relation to the locales being referenced (benefiting from any later fact declarations in the obvious manner). - \end{descr} + \end{description} Note that ``@{text "(\ p\<^sub>1 \ p\<^sub>n)"}'' patterns given in the syntax of @{element "assumes"} and @{element "defines"} above @@ -419,7 +423,7 @@ \secref{sec:object-logic}). Separate introduction rules @{text loc_axioms.intro} and @{text loc.intro} are provided as well. - \item [@{command "print_locale"}~@{text "import + body"}] prints the + \item @{command "print_locale"}~@{text "import + body"} prints the specified locale expression in a flattened form. The notable special case @{command "print_locale"}~@{text loc} just prints the contents of the named locale, but keep in mind that type-inference @@ -427,20 +431,21 @@ order. The command omits @{element "notes"} elements by default. Use @{command "print_locale"}@{text "!"} to get them included. - \item [@{command "print_locales"}] prints the names of all locales + \item @{command "print_locales"} prints the names of all locales of the current theory. - \item [@{method intro_locales} and @{method unfold_locales}] + \item @{method intro_locales} and @{method unfold_locales} repeatedly expand all introduction rules of locale predicates of the theory. While @{method intro_locales} only applies the @{text loc.intro} introduction rules and therefore does not decend to assumptions, @{method unfold_locales} is more aggressive and applies @{text loc_axioms.intro} as well. Both methods are aware of locale - specifications entailed by the context, both from target statements, - and from interpretations (see below). New goals that are entailed - by the current context are discharged automatically. + specifications entailed by the context, both from target and + @{element "includes"} statements, and from interpretations (see + below). New goals that are entailed by the current context are + discharged automatically. - \end{descr} + \end{description} *} @@ -476,9 +481,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "interpretation"}~@{text "expr insts \ eqns"}] + \item @{command "interpretation"}~@{text "expr insts \ eqns"} The first form of @{command "interpretation"} interprets @{text expr} in the theory. The instantiation is given as a list of terms @@ -518,7 +523,7 @@ interpretations dynamically participate in any facts added to locales. - \item [@{command "interpretation"}~@{text "name \ expr"}] + \item @{command "interpretation"}~@{text "name \ expr"} This form of the command interprets @{text expr} in the locale @{text name}. It requires a proof that the specification of @{text @@ -549,18 +554,18 @@ prefix and attributes, although only for fragments of @{text expr} that are not interpreted in the theory already. - \item [@{command "interpret"}~@{text "expr insts \ eqns"}] + \item @{command "interpret"}~@{text "expr insts \ eqns"} interprets @{text expr} in the proof context and is otherwise similar to interpretation in theories. - \item [@{command "print_interps"}~@{text loc}] prints the + \item @{command "print_interps"}~@{text loc} prints the interpretations of a particular locale @{text loc} that are active in the current context, either theory or proof context. The exclamation point argument triggers printing of \emph{witness} theorems justifying interpretations. These are normally omitted from the output. - \end{descr} + \end{description} \begin{warn} Since attributes are applied to interpreted theorems, @@ -621,9 +626,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "class"}~@{text "c = superclasses + body"}] defines + \item @{command "class"}~@{text "c = superclasses + body"} defines a new class @{text c}, inheriting from @{text superclasses}. This introduces a locale @{text c} with import of all locales @{text superclasses}. @@ -641,43 +646,42 @@ --- the @{method intro_classes} method takes care of the details of class membership proofs. - \item [@{command "instantiation"}~@{text "t :: (s\<^sub>1, \, - s\<^sub>n) s \"}] opens a theory target (cf.\ - \secref{sec:target}) which allows to specify class operations @{text - "f\<^sub>1, \, f\<^sub>n"} corresponding to sort @{text s} at the - particular type instance @{text "(\\<^sub>1 :: s\<^sub>1, \, - \\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command - in the target body poses a goal stating these type arities. The - target is concluded by an @{command_ref (local) "end"} command. + \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) s + \"} opens a theory target (cf.\ \secref{sec:target}) which + allows to specify class operations @{text "f\<^sub>1, \, f\<^sub>n"} corresponding + to sort @{text s} at the particular type instance @{text "(\\<^sub>1 :: s\<^sub>1, + \, \\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the + target body poses a goal stating these type arities. The target is + concluded by an @{command_ref (local) "end"} command. Note that a list of simultaneous type constructors may be given; this corresponds nicely to mutual recursive type definitions, e.g.\ in Isabelle/HOL. - \item [@{command "instance"}] in an instantiation target body sets + \item @{command "instance"} in an instantiation target body sets up a goal stating the type arities claimed at the opening @{command "instantiation"}. The proof would usually proceed by @{method intro_classes}, and then establish the characteristic theorems of the type classes involved. After finishing the proof, the background theory will be augmented by the proven type arities. - \item [@{command "subclass"}~@{text c}] in a class context for class + \item @{command "subclass"}~@{text c} in a class context for class @{text d} sets up a goal stating that class @{text c} is logically contained in class @{text d}. After finishing the proof, class @{text d} is proven to be subclass @{text c} and the locale @{text c} is interpreted into @{text d} simultaneously. - \item [@{command "print_classes"}] prints all classes in the current + \item @{command "print_classes"} prints all classes in the current theory. - \item [@{method intro_classes}] repeatedly expands all class + \item @{method intro_classes} repeatedly expands all class introduction rules of this theory. Note that this method usually needs not be named explicitly, as it is already included in the default proof step (e.g.\ of @{command "proof"}). In particular, instantiation of trivial (syntactic) classes may be performed by a single ``@{command ".."}'' proof step. - \end{descr} + \end{description} *} @@ -728,15 +732,15 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "axclass"}~@{text "c \ c\<^sub>1, \, c\<^sub>n - axms"}] defines an axiomatic type class as the intersection of - existing classes, with additional axioms holding. Class axioms may - not contain more than one type variable. The class axioms (with - implicit sort constraints added) are bound to the given names. - Furthermore a class introduction rule is generated (being bound as - @{text c_class.intro}); this rule is employed by method @{method + \item @{command "axclass"}~@{text "c \ c\<^sub>1, \, c\<^sub>n axms"} defines an + axiomatic type class as the intersection of existing classes, with + additional axioms holding. Class axioms may not contain more than + one type variable. The class axioms (with implicit sort constraints + added) are bound to the given names. Furthermore a class + introduction rule is generated (being bound as @{text + c_class.intro}); this rule is employed by method @{method intro_classes} to support instantiation proofs of this class. The ``class axioms'' are stored as theorems according to the given @@ -744,15 +748,15 @@ the same facts are also stored collectively as @{text c_class.axioms}. - \item [@{command "instance"}~@{text "c\<^sub>1 \ c\<^sub>2"} and - @{command "instance"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) s"}] - setup a goal stating a class relation or type arity. The proof - would usually proceed by @{method intro_classes}, and then establish - the characteristic theorems of the type classes involved. After - finishing the proof, the theory will be augmented by a type - signature declaration corresponding to the resulting theorem. + \item @{command "instance"}~@{text "c\<^sub>1 \ c\<^sub>2"} and @{command + "instance"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) s"} setup a goal stating a + class relation or type arity. The proof would usually proceed by + @{method intro_classes}, and then establish the characteristic + theorems of the type classes involved. After finishing the proof, + the theory will be augmented by a type signature declaration + corresponding to the resulting theorem. - \end{descr} + \end{description} *} @@ -776,25 +780,24 @@ ( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' \end{rail} - \begin{descr} + \begin{description} - \item [@{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: - \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"}] + \item @{command "overloading"}~@{text "x\<^sub>1 \ c\<^sub>1 :: \\<^sub>1 \ \ x\<^sub>n \ c\<^sub>n :: \\<^sub>n \"} opens a theory target (cf.\ \secref{sec:target}) which allows to specify constants with overloaded definitions. These are identified - by an explicitly given mapping from variable names @{text - "x\<^sub>i"} to constants @{text "c\<^sub>i"} at particular type - instances. The definitions themselves are established using common - specification tools, using the names @{text "x\<^sub>i"} as - reference to the corresponding constants. The target is concluded - by @{command (local) "end"}. + by an explicitly given mapping from variable names @{text "x\<^sub>i"} to + constants @{text "c\<^sub>i"} at particular type instances. The + definitions themselves are established using common specification + tools, using the names @{text "x\<^sub>i"} as reference to the + corresponding constants. The target is concluded by @{command + (local) "end"}. A @{text "(unchecked)"} option disables global dependency checks for the corresponding definition, which is occasionally useful for exotic overloading. It is at the discretion of the user to avoid malformed theory specifications! - \end{descr} + \end{description} *} @@ -808,9 +811,12 @@ @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\ @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\ @{command_def "setup"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{mldecls} @{index_ML bind_thms: "string * thm list -> unit"} \\ @{index_ML bind_thm: "string * thm -> unit"} \\ - \end{matharray} + \end{mldecls} \begin{rail} 'use' name @@ -819,9 +825,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "use"}~@{text "file"}] reads and executes ML + \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 [source=false] "Context.>>"} or derived ML commands. The file name is checked with @@ -831,25 +837,25 @@ Top-level ML bindings are stored within the (global or local) theory context. - \item [@{command "ML"}~@{text "text"}] is similar to @{command - "use"}, but executes ML commands directly from the given @{text - "text"}. Top-level ML bindings are stored within the (global or - local) theory context. + \item @{command "ML"}~@{text "text"} is similar to @{command "use"}, + but executes ML commands directly from the given @{text "text"}. + Top-level ML bindings are stored within the (global or local) theory + context. - \item [@{command "ML_prf"}] is analogous to @{command "ML"} but - works within a proof context. + \item @{command "ML_prf"} is analogous to @{command "ML"} but works + within a proof context. Top-level ML bindings are stored within the proof context in a purely sequential fashion, disregarding the nested proof structure. ML bindings introduced by @{command "ML_prf"} are discarded at the end of the proof. - \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 "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 + \item @{command "setup"}~@{text "text"} changes the current theory context by applying @{text "text"}, which refers to an ML expression of type @{ML_type [source=false] "theory -> theory"}. This enables to initialize any object-logic specific tools and packages written @@ -863,7 +869,7 @@ \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a singleton theorem. - \end{descr} + \end{description} *} @@ -888,27 +894,27 @@ ; \end{rail} - \begin{descr} + \begin{description} - \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 "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 "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 + \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, + \item @{command "class_deps"} visualizes the subclass relation, using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - \end{descr} + \end{description} *} @@ -933,31 +939,31 @@ ; \end{rail} - \begin{descr} + \begin{description} - \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 "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 "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 "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. + \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} + \end{description} *} @@ -1029,14 +1035,14 @@ ; \end{rail} - \begin{descr} + \begin{description} - \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 "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} + \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 @@ -1049,12 +1055,12 @@ 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 + \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! + 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 @@ -1068,7 +1074,7 @@ "\"} (printed as ``@{text "\"}''). The latter concept is particularly useful with locales (see also \S\ref{sec:locale}). - \end{descr} + \end{description} *} @@ -1088,9 +1094,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "axioms"}~@{text "a: \"}] introduces arbitrary + \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. @@ -1099,16 +1105,15 @@ 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 "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 + \item @{command "theorems"} is essentially the same as @{command "lemmas"}, but marks the result as a different kind of facts. - \end{descr} + \end{description} *} @@ -1138,16 +1143,16 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "oracle"}~@{text "name = text"}] turns the given ML + \item @{command "oracle"}~@{text "name = text"} turns the given ML expression @{text "text"} of type @{ML_text "'a -> cterm"} into an ML function of type @{ML_text "'a -> thm"}, which is bound to the global identifier @{ML_text name}. This acts like an infinitary specification of axioms! Invoking the oracle only works within the scope of the resulting theory. - \end{descr} + \end{description} See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of defining a new primitive rule as oracle, and turning it into a proof @@ -1175,19 +1180,19 @@ name spaces by hand, yet the following commands provide some way to do so. - \begin{descr} + \begin{description} - \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. + \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 + \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 @@ -1198,7 +1203,7 @@ longer accessible to the user are printed with the special qualifier ``@{text "??"}'' prefixed to the full internal name. - \end{descr} + \end{description} *} @@ -1224,9 +1229,9 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to + \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, @@ -1235,22 +1240,21 @@ "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 "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 + \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 + \item @{command "no_translations"}~@{text rules} removes syntactic translation rules, which are interpreted in the same manner as for @{command "translations"} above. - \end{descr} + \end{description} *} diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/Thy/ZF_Specific.thy --- a/doc-src/IsarRef/Thy/ZF_Specific.thy Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Thu Nov 13 21:43:46 2008 +0100 @@ -26,18 +26,18 @@ ; \end{rail} - \begin{descr} + \begin{description} - \item [@{command (ZF) "print_tcset"}] prints the collection of + \item @{command (ZF) "print_tcset"} prints the collection of typechecking rules of the current context. - \item [@{method (ZF) typecheck}] attempts to solve any pending + \item @{method (ZF) typecheck} attempts to solve any pending type-checking problems in subgoals. - \item [@{attribute (ZF) TC}] adds or deletes type-checking rules - from the context. + \item @{attribute (ZF) TC} adds or deletes type-checking rules from + the context. - \end{descr} + \end{description} *} diff -r 8358fabeea95 -r cbc435f7b16b doc-src/IsarRef/style.sty --- a/doc-src/IsarRef/style.sty Thu Nov 13 21:41:04 2008 +0100 +++ b/doc-src/IsarRef/style.sty Thu Nov 13 21:43:46 2008 +0100 @@ -16,12 +16,9 @@ \newcommand{\figref}[1]{figure~\ref{#1}} \newcommand{\Figref}[1]{Figure~\ref{#1}} -%% index -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}} -\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}} -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}} -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}} -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}} +%% ML +\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup} +\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}} %% math \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}