# HG changeset patch # User wenzelm # Date 1212444306 -7200 # Node ID 4bf8710b3242de74614f79570960130dc3eb131e # Parent 4a99797aa9f2f0c055313980cdac507060ccf6cd moved stuff from pure.thy to Misc.thy; diff -r 4a99797aa9f2 -r 4bf8710b3242 doc-src/IsarRef/Thy/Misc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/Misc.thy Tue Jun 03 00:05:06 2008 +0200 @@ -0,0 +1,245 @@ +(* $Id$ *) + +theory Misc +imports Main +begin + +chapter {* Other commands \label{ch:pure-syntax} *} + +section {* Diagnostics *} + +text {* + \begin{matharray}{rcl} + @{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + @{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + These diagnostic commands assist interactive development. Note that + @{command undo} does not apply here, the theory or proof + configuration is not changed. + + \begin{rail} + 'pr' modes? nat? (',' nat)? + ; + 'thm' modes? thmrefs + ; + 'term' modes? term + ; + 'prop' modes? prop + ; + 'typ' modes? type + ; + 'prf' modes? thmrefs? + ; + 'full\_prf' modes? thmrefs? + ; + + modes: '(' (name + ) ')' + ; + \end{rail} + + \begin{descr} + + \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 + 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 \}] + 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 + meta-logic according to the current theory or proof context. + + \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 + the full proof term, i.e.\ also displays information omitted in the + compact proof term, which is denoted by ``@{text _}'' placeholders + there. + + \end{descr} + + All of the diagnostic commands above admit a list of @{text modes} + to be specified, which is appended to the current print mode (see + also \cite{isabelle-ref}). Thus the output behavior may be modified + according particular print mode features. For example, @{command + "pr"}~@{text "(latex xsymbols symbols)"} would print the current + proof state with mathematical symbols and special characters + represented in {\LaTeX} source, according to the Isabelle style + \cite{isabelle-sys}. + + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more + systematic way to include formal items into the printed text + document. +*} + + +section {* Inspecting the context *} + +text {* + \begin{matharray}{rcl} + @{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + @{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ + @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ + \end{matharray} + + \begin{rail} + 'print\_theory' ( '!'?) + ; + + 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) + ; + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | + 'simp' ':' term | term) + ; + 'thm\_deps' thmrefs + ; + \end{rail} + + These commands print certain parts of the theory and proof context. + Note that there are some further ones available, such as for the set + of rules declared for simplifications. + + \begin{descr} + + \item [@{command "print_commands"}] prints Isabelle's outer theory + syntax, including keywords and command. + + \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 + 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 + available in the current theory context. + + \item [@{command "print_attributes"}] prints all attributes + available in the current theory context. + + \item [@{command "print_theorems"}] prints theorems resulting from + the last command. + + \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 + contain ``@{text "*"}'' wildcards. The criteria @{text intro}, + @{text elim}, and @{text dest} select theorems that match the + current goal as introduction, elimination or destruction rules, + respectively. The criterion @{text "simp: t"} selects all rewrite + rules whose left-hand side matches the given term. The criterion + term @{text t} selects all theorems that contain the pattern @{text + t} -- as usual, patterns may contain occurrences of the dummy + ``@{text _}'', schematic variables, and type constraints. + + Criteria can be preceded by ``@{text "-"}'' to select theorems that + do \emph{not} match. Note that giving the empty list of criteria + yields \emph{all} currently known facts. An optional limit for the + number of printed facts may be given; the default is 40. By + 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"}] + 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 + current context, both named and unnamed ones. + + \item [@{command "print_binds"}] prints all term abbreviations + present in the context. + + \end{descr} +*} + + +section {* History commands \label{sec:history} *} + +text {* + \begin{matharray}{rcl} + @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \end{matharray} + + The Isabelle/Isar top-level maintains a two-stage history, for + theory and proof state transformation. Basically, any command can + be undone using @{command "undo"}, excluding mere diagnostic + elements. Its effect may be revoked via @{command "redo"}, unless + the corresponding @{command "undo"} step has crossed the beginning + of a proof or theory. The @{command "kill"} command aborts the + current history node altogether, discontinuing a proof or even the + whole theory. This operation is \emph{not} undo-able. + + \begin{warn} + History commands should never be used with user interfaces such as + Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes + care of stepping forth and back itself. Interfering by manual + @{command "undo"}, @{command "redo"}, or even @{command "kill"} + commands would quickly result in utter confusion. + \end{warn} +*} + + +section {* System commands *} + +text {* + \begin{matharray}{rcl} + @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ + \end{matharray} + + \begin{rail} + ('cd' | 'use\_thy' | 'update\_thy') name + ; + \end{rail} + + \begin{descr} + + \item [@{command "cd"}~@{text path}] changes the current directory + of the Isabelle process. + + \item [@{command "pwd"}] prints the current working directory. + + \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 diff -r 4a99797aa9f2 -r 4bf8710b3242 doc-src/IsarRef/Thy/pure.thy --- a/doc-src/IsarRef/Thy/pure.thy Tue Jun 03 00:04:35 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,247 +0,0 @@ -(* $Id$ *) - -theory pure -imports Pure -begin - -chapter {* Basic language elements \label{ch:pure-syntax} *} - -section {* Other commands *} - -subsection {* Diagnostics *} - -text {* - \begin{matharray}{rcl} - @{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - \end{matharray} - - These diagnostic commands assist interactive development. Note that - @{command undo} does not apply here, the theory or proof - configuration is not changed. - - \begin{rail} - 'pr' modes? nat? (',' nat)? - ; - 'thm' modes? thmrefs - ; - 'term' modes? term - ; - 'prop' modes? prop - ; - 'typ' modes? type - ; - 'prf' modes? thmrefs? - ; - 'full\_prf' modes? thmrefs? - ; - - modes: '(' (name + ) ')' - ; - \end{rail} - - \begin{descr} - - \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 - 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 \}] - 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 - meta-logic according to the current theory or proof context. - - \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 - the full proof term, i.e.\ also displays information omitted in the - compact proof term, which is denoted by ``@{text _}'' placeholders - there. - - \end{descr} - - All of the diagnostic commands above admit a list of @{text modes} - to be specified, which is appended to the current print mode (see - also \cite{isabelle-ref}). Thus the output behavior may be modified - according particular print mode features. For example, @{command - "pr"}~@{text "(latex xsymbols symbols)"} would print the current - proof state with mathematical symbols and special characters - represented in {\LaTeX} source, according to the Isabelle style - \cite{isabelle-sys}. - - Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more - systematic way to include formal items into the printed text - document. -*} - - -subsection {* Inspecting the context *} - -text {* - \begin{matharray}{rcl} - @{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ - @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ - @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\ - \end{matharray} - - \begin{rail} - 'print\_theory' ( '!'?) - ; - - 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) - ; - criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | - 'simp' ':' term | term) - ; - 'thm\_deps' thmrefs - ; - \end{rail} - - These commands print certain parts of the theory and proof context. - Note that there are some further ones available, such as for the set - of rules declared for simplifications. - - \begin{descr} - - \item [@{command "print_commands"}] prints Isabelle's outer theory - syntax, including keywords and command. - - \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 - 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 - available in the current theory context. - - \item [@{command "print_attributes"}] prints all attributes - available in the current theory context. - - \item [@{command "print_theorems"}] prints theorems resulting from - the last command. - - \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 - contain ``@{text "*"}'' wildcards. The criteria @{text intro}, - @{text elim}, and @{text dest} select theorems that match the - current goal as introduction, elimination or destruction rules, - respectively. The criterion @{text "simp: t"} selects all rewrite - rules whose left-hand side matches the given term. The criterion - term @{text t} selects all theorems that contain the pattern @{text - t} -- as usual, patterns may contain occurrences of the dummy - ``@{text _}'', schematic variables, and type constraints. - - Criteria can be preceded by ``@{text "-"}'' to select theorems that - do \emph{not} match. Note that giving the empty list of criteria - yields \emph{all} currently known facts. An optional limit for the - number of printed facts may be given; the default is 40. By - 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"}] - 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 - current context, both named and unnamed ones. - - \item [@{command "print_binds"}] prints all term abbreviations - present in the context. - - \end{descr} -*} - - -subsection {* History commands \label{sec:history} *} - -text {* - \begin{matharray}{rcl} - @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ - @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ - @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ - \end{matharray} - - The Isabelle/Isar top-level maintains a two-stage history, for - theory and proof state transformation. Basically, any command can - be undone using @{command "undo"}, excluding mere diagnostic - elements. Its effect may be revoked via @{command "redo"}, unless - the corresponding @{command "undo"} step has crossed the beginning - of a proof or theory. The @{command "kill"} command aborts the - current history node altogether, discontinuing a proof or even the - whole theory. This operation is \emph{not} undo-able. - - \begin{warn} - History commands should never be used with user interfaces such as - Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes - care of stepping forth and back itself. Interfering by manual - @{command "undo"}, @{command "redo"}, or even @{command "kill"} - commands would quickly result in utter confusion. - \end{warn} -*} - - -subsection {* System operations *} - -text {* - \begin{matharray}{rcl} - @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\ - \end{matharray} - - \begin{rail} - ('cd' | 'use\_thy' | 'update\_thy') name - ; - \end{rail} - - \begin{descr} - - \item [@{command "cd"}~@{text path}] changes the current directory - of the Isabelle process. - - \item [@{command "pwd"}] prints the current working directory. - - \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