diff -r b1a051891ec4 -r eb95e2f3b218 doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 15:37:17 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Tue May 03 16:00:29 2011 +0200 @@ -169,76 +169,71 @@ \isamarkuptrue% % \begin{isamarkuptext}% -\begin{mldecls} - \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\ - \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\ - \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\ - \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\ - \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Config.T| & default \verb|false| \\ - \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\ - \end{mldecls} +\begin{tabular}{rcll} + \indexdef{}{attribute}{show\_types}\hypertarget{attribute.show-types}{\hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{show\_sorts}\hypertarget{attribute.show-sorts}{\hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\ + \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\ + \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\ + \indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\ + \indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{show\_hyps}\hypertarget{attribute.show-hyps}{\hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{show\_tags}\hypertarget{attribute.show-tags}{\hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}}} & : & \isa{attribute} & default \isa{false} \\ + \indexdef{}{attribute}{show\_question\_marks}\hypertarget{attribute.show-question-marks}{\hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}}} & : & \isa{attribute} & default \isa{true} \\ + \end{tabular} + \medskip - These global ML variables control the detail of information that is - displayed for types, terms, theorems, goals etc. - - In interactive sessions, the user interface usually manages these - global parameters of the Isabelle process, even with some concept of - persistence. Nonetheless it is occasionally useful to manipulate ML - variables directly, e.g.\ using \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}}. - - Batch-mode logic sessions may be configured by putting appropriate - ML text directly into the \verb|ROOT.ML| file. + These configuration options control the detail of information that + is displayed for types, terms, theorems, goals etc. See also + \secref{sec:config}. \begin{description} - \item \verb|show_types| and \verb|show_sorts| control printing of type - constraints for term variables, and sort constraints for type - variables. By default, neither of these are shown in output. If - \verb|show_sorts| is set to \verb|true|, types are always shown as - well. + \item \hyperlink{attribute.show-types}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}types}}} and \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} control + printing of type constraints for term variables, and sort + constraints for type variables. By default, neither of these are + shown in output. If \hyperlink{attribute.show-sorts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}sorts}}} is enabled, types are + always shown as well. Note that displaying types and sorts may explain why a polymorphic inference rule fails to resolve with some goal, or why a rewrite rule does not apply as expected. - \item \verb|show_consts| controls printing of types of constants when - displaying a goal state. + \item \hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}} controls printing of types of + constants when displaying a goal state. Note that the output can be enormous, because polymorphic constants often occur at several different type instances. - \item \verb|show_abbrevs| controls folding of constant abbreviations. + \item \hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}} controls folding of constant + abbreviations. - \item \verb|show_brackets| controls bracketing in pretty printed - output. If set to \verb|true|, all sub-expressions of the pretty + \item \hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}} controls bracketing in pretty + printed output. If enabled, all sub-expressions of the pretty printing tree will be parenthesized, even if this produces malformed term syntax! This crude way of showing the internal structure of pretty printed entities may occasionally help to diagnose problems with operator priorities, for example. - \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and - \verb|Name_Space.unique_names| control the way of printing fully + \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and + \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully qualified internal names in external form. See also \secref{sec:antiq} for the document antiquotation options of the same names. - \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of - terms. + \item \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted + printing of terms. The \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contraction law asserts \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ f{\isaliteral{22}{\isachardoublequote}}}, provided \isa{x} is not free in \isa{f}. It asserts \emph{extensionality} of functions: \isa{{\isaliteral{22}{\isachardoublequote}}f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g{\isaliteral{22}{\isachardoublequote}}} if \isa{{\isaliteral{22}{\isachardoublequote}}f\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g\ x{\isaliteral{22}{\isachardoublequote}}} for all \isa{x}. Higher-order unification frequently puts terms into a fully \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded form. For example, if \isa{F} has type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} then its expanded form is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. - Setting \verb|eta_contract| makes Isabelle perform \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contractions before printing, so that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} + Enabling \hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}} makes Isabelle perform \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-contractions before printing, so that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}h{\isaliteral{2E}{\isachardot}}\ F\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} appears simply as \isa{F}. Note that the distinction between a term and its \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-expanded @@ -246,33 +241,34 @@ rewriting operate modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-conversion, some other tools might look at terms more discretely. - \item \verb|Goal_Display.goals_limit| controls the maximum number of + \item \hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}} controls the maximum number of subgoals to be shown in goal output. - \item \verb|Goal_Display.show_main_goal| controls whether the main - result to be proven should be displayed. This information might be + \item \hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}} controls whether the main result + to be proven should be displayed. This information might be relevant for schematic goals, to inspect the current claim that has been synthesized so far. - \item \verb|show_hyps| controls printing of implicit hypotheses of - local facts. Normally, only those hypotheses are displayed that are - \emph{not} covered by the assumptions of the current context: this - situation indicates a fault in some tool being used. + \item \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}} controls printing of implicit + hypotheses of local facts. Normally, only those hypotheses are + displayed that are \emph{not} covered by the assumptions of the + current context: this situation indicates a fault in some tool being + used. - By setting \verb|show_hyps| to \verb|true|, output of \emph{all} - hypotheses can be enforced, which is occasionally useful for - diagnostic purposes. + By enabling \hyperlink{attribute.show-hyps}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}hyps}}}, output of \emph{all} hypotheses + can be enforced, which is occasionally useful for diagnostic + purposes. - \item \verb|show_tags| controls printing of extra annotations within - theorems, such as internal position information, or the case names - being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}. + \item \hyperlink{attribute.show-tags}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}tags}}} controls printing of extra annotations + within theorems, such as internal position information, or the case + names being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}. Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} attributes provide low-level access to the collection of tags associated with a theorem. - \item \verb|show_question_marks| controls printing of question marks - for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}. Only the leading + \item \hyperlink{attribute.show-question-marks}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}question{\isaliteral{5F}{\isacharunderscore}}marks}}} controls printing of question + marks for schematic variables, such as \isa{{\isaliteral{3F}{\isacharquery}}x}. Only the leading question mark is affected, the remaining text is unchanged (including proper markup for schematic variables that might be relevant for user interfaces).