--- 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).