doc-src/IsarRef/Thy/Misc.thy

updated and elaborated Pure grammer;

(* $Id$ *)

theory Misc
imports Main
begin

chapter {* Other commands \label{ch:pure-syntax} *}

section {* Inspecting the context *}

text {*
  \begin{matharray}{rcl}
    @{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    @{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  \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{description}
  
  \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 \<dots> 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{description}
*}


section {* History commands \label{sec:history} *}

text {*
  \begin{matharray}{rcl}
    @{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
    @{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
    @{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\
  \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.  Note that a theorem statement with a \emph{finished}
  proof is treated as a single unit by @{command "undo"}.  In
  contrast, the variant @{command "linear_undo"} admits to step back
  into the middle of a proof.  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 "linear_undo"}, 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>*"} & : & @{text "any \<rightarrow>"} \\
    @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
    @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
  \end{matharray}

  \begin{rail}
    ('cd' | 'use\_thy' | 'update\_thy') name
    ;
  \end{rail}

  \begin{description}

  \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{description}
*}

end