doc-src/IsarRef/Thy/pure.thy

renamed theory "intro" to "Introduction";

(* $Id$ *)

theory pure
imports Pure
begin

chapter {* Basic language elements \label{ch:pure-syntax} *}

text {*
  Subsequently, we introduce the main part of Pure theory and proof
  commands, together with fundamental proof methods and attributes.
  \Chref{ch:gen-tools} describes further Isar elements provided by
  generic tools and packages (such as the Simplifier) that are either
  part of Pure Isabelle or pre-installed in most object logics.
  Specific language elements introduced by the major object-logics are
  described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
  (Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF).  Nevertheless,
  examples given in the generic parts will usually refer to
  Isabelle/HOL as well.

  \medskip Isar commands may be either \emph{proper} document
  constructors, or \emph{improper commands}.  Some proof methods and
  attributes introduced later are classified as improper as well.
  Improper Isar language elements, which are subsequently marked by
  ``@{text "\<^sup>*"}'', are often helpful when developing proof
  documents, while their use is discouraged for the final
  human-readable outcome.  Typical examples are diagnostic commands
  that print terms or theorems according to the current context; other
  commands emulate old-style tactical theorem proving.
*}


section {* Theory commands *}

subsection {* Markup commands \label{sec:markup-thy} *}

text {*
  \begin{matharray}{rcl}
    @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
    @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
    @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
    @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
    @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
    @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\
  \end{matharray}

  Apart from formal comments (see \secref{sec:comments}), markup
  commands provide a structured way to insert text into the document
  generated from a theory (see \cite{isabelle-sys} for more
  information on Isabelle's document preparation tools).

  \begin{rail}
    ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
    ;
    'text\_raw' text
    ;
  \end{rail}

  \begin{descr}

  \item [@{command "chapter"}, @{command "section"}, @{command
  "subsection"}, and @{command "subsubsection"}] mark chapter and
  section headings.

  \item [@{command "text"}] specifies paragraphs of plain text.

  \item [@{command "text_raw"}] inserts {\LaTeX} source into the
  output, without additional markup.  Thus the full range of document
  manipulations becomes available.

  \end{descr}

  The @{text "text"} argument of these markup commands (except for
  @{command "text_raw"}) may contain references to formal entities
  (``antiquotations'', see also \secref{sec:antiq}).  These are
  interpreted in the present theory context, or the named @{text
  "target"}.

  Any of these markup elements corresponds to a {\LaTeX} command with
  the name prefixed by @{verbatim "\\isamarkup"}.  For the sectioning
  commands this is a plain macro with a single argument, e.g.\
  @{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
  @{command "chapter"}.  The @{command "text"} markup results in a
  {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text
  "\<dots>"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
  causes the text to be inserted directly into the {\LaTeX} source.

  \medskip Additional markup commands are available for proofs (see
  \secref{sec:markup-prf}).  Also note that the @{command_ref
  "header"} declaration (see \secref{sec:begin-thy}) admits to insert
  section markup just preceding the actual theory definition.
*}


subsection {* Type classes and sorts \label{sec:classes} *}

text {*
  \begin{matharray}{rcll}
    @{command_def "classes"} & : & \isartrans{theory}{theory} \\
    @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
    @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
    @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\
  \end{matharray}

  \begin{rail}
    'classes' (classdecl +)
    ;
    'classrel' (nameref ('<' | subseteq) nameref + 'and')
    ;
    'defaultsort' sort
    ;
  \end{rail}

  \begin{descr}

  \item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
  declares class @{text c} to be a subclass of existing classes @{text
  "c\<^sub>1, \<dots>, c\<^sub>n"}.  Cyclic class structures are not permitted.

  \item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> 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
  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,
  using Isabelle's graph browser tool (see also \cite{isabelle-sys}).

  \end{descr}
*}


subsection {* Primitive types and type abbreviations \label{sec:types-pure} *}

text {*
  \begin{matharray}{rcll}
    @{command_def "types"} & : & \isartrans{theory}{theory} \\
    @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
    @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
    @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
  \end{matharray}

  \begin{rail}
    'types' (typespec '=' type infix? +)
    ;
    'typedecl' typespec infix?
    ;
    'nonterminals' (name +)
    ;
    'arities' (nameref '::' arity +)
    ;
  \end{rail}

  \begin{descr}

  \item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
  introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
  for existing type @{text "\<tau>"}.  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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^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 "arities"}~@{text "t :: (s\<^sub>1, \<dots>, 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}
*}


subsection {* Primitive constants and definitions \label{sec:consts} *}

text {*
  Definitions essentially express abbreviations within the logic.  The
  simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
  c} is a newly declared constant.  Isabelle also allows derived forms
  where the arguments of @{text c} appear on the left, abbreviating a
  prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
  written more conveniently as @{text "c x y \<equiv> t"}.  Moreover,
  definitions may be weakened by adding arbitrary pre-conditions:
  @{text "A \<Longrightarrow> c x y \<equiv> t"}.

  \medskip The built-in well-formedness conditions for definitional
  specifications are:

  \begin{itemize}

  \item Arguments (on the left-hand side) must be distinct variables.

  \item All variables on the right-hand side must also appear on the
  left-hand side.

  \item All type variables on the right-hand side must also appear on
  the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
  \<alpha> list)"} for example.

  \item The definition must not be recursive.  Most object-logics
  provide definitional principles that can be used to express
  recursion safely.

  \end{itemize}

  Overloading means that a constant being declared as @{text "c :: \<alpha>
  decl"} may be defined separately on type instances @{text "c ::
  (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
  t}.  The right-hand side may mention overloaded constants
  recursively at type instances corresponding to the immediate
  argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}.  Incomplete
  specification patterns impose global constraints on all occurrences,
  e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
  corresponding occurrences on some right-hand side need to be an
  instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.

  \begin{matharray}{rcl}
    @{command_def "consts"} & : & \isartrans{theory}{theory} \\
    @{command_def "defs"} & : & \isartrans{theory}{theory} \\
    @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
  \end{matharray}

  \begin{rail}
    'consts' ((name '::' type mixfix?) +)
    ;
    'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
    ;
  \end{rail}

  \begin{rail}
    'constdefs' structs? (constdecl? constdef +)
    ;

    structs: '(' 'structure' (vars + 'and') ')'
    ;
    constdecl:  ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
    ;
    constdef: thmdecl? prop
    ;
  \end{rail}

  \begin{descr}

  \item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
  @{text c} to have any instance of type scheme @{text \<sigma>}.  The
  optional mixfix annotations may attach concrete syntax to the
  constants declared.
  
  \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
  for this definition, which is occasionally useful for exotic
  overloading.  It is at the discretion of the user to avoid malformed
  theory specifications!
  
  The @{text "(overloaded)"} option declares definitions to be
  potentially overloaded.  Unless this option is given, a warning
  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
  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!
  
  The constant name may be omitted altogether, if neither type nor
  syntax declarations are given.  The canonical name of the
  definitional axiom for constant @{text c} will be @{text c_def},
  unless specified otherwise.  Also note that the given list of
  specifications is processed in a strictly sequential manner, with
  type-checking being performed independently.
  
  An optional initial context of @{text "(structure)"} declarations
  admits use of indexed syntax, using the special symbol @{verbatim
  "\<index>"} (printed as ``@{text "\<index>"}'').  The latter concept is
  particularly useful with locales (see also \S\ref{sec:locale}).

  \end{descr}
*}


subsection {* Syntax and translations \label{sec:syn-trans} *}

text {*
  \begin{matharray}{rcl}
    @{command_def "syntax"} & : & \isartrans{theory}{theory} \\
    @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
    @{command_def "translations"} & : & \isartrans{theory}{theory} \\
    @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
  \end{matharray}

  \begin{rail}
    ('syntax' | 'no\_syntax') mode? (constdecl +)
    ;
    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
    ;

    mode: ('(' ( name | 'output' | name 'output' ) ')')
    ;
    transpat: ('(' nameref ')')? string
    ;
  \end{rail}

  \begin{descr}
  
  \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,
  independently of the logic.  The @{text mode} argument refers to the
  print mode that the grammar rules belong; unless the @{keyword_ref
  "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 "translations"}~@{text rules}] specifies syntactic
  translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
  parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
  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
  translation rules, which are interpreted in the same manner as for
  @{command "translations"} above.

  \end{descr}
*}


subsection {* Axioms and theorems \label{sec:axms-thms} *}

text {*
  \begin{matharray}{rcll}
    @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
    @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
    @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\
  \end{matharray}

  \begin{rail}
    'axioms' (axmdecl prop +)
    ;
    ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
    ;
  \end{rail}

  \begin{descr}
  
  \item [@{command "axioms"}~@{text "a: \<phi>"}] 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.
  
  Axioms are usually only introduced when declaring new logical
  systems.  Everyday work is typically done the hard way, with proper
  definitions and proven theorems.
  
  \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> 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
  "lemmas"}, but marks the result as a different kind of facts.

  \end{descr}
*}


subsection {* Name spaces *}

text {*
  \begin{matharray}{rcl}
    @{command_def "global"} & : & \isartrans{theory}{theory} \\
    @{command_def "local"} & : & \isartrans{theory}{theory} \\
    @{command_def "hide"} & : & \isartrans{theory}{theory} \\
  \end{matharray}

  \begin{rail}
    'hide' ('(open)')? name (nameref + )
    ;
  \end{rail}

  Isabelle organizes any kind of name declarations (of types,
  constants, theorems etc.) by separate hierarchically structured name
  spaces.  Normally the user does not have to control the behavior of
  name spaces by hand, yet the following commands provide some way to
  do so.

  \begin{descr}

  \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
  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
  (unqualified) names may never be hidden.
  
  Note that hiding name space accesses has no impact on logical
  declarations -- they remain valid internally.  Entities that are no
  longer accessible to the user are printed with the special qualifier
  ``@{text "??"}'' prefixed to the full internal name.

  \end{descr}
*}


subsection {* Incorporating ML code \label{sec:ML} *}

text {*
  \begin{matharray}{rcl}
    @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
    @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
    @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
    @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
    @{command_def "setup"} & : & \isartrans{theory}{theory} \\
    @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
  \end{matharray}

  \begin{rail}
    'use' name
    ;
    ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
    ;
    'method\_setup' name '=' text text
    ;
  \end{rail}

  \begin{descr}

  \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
  "Context.>>"} or derived ML commands.  The file name is checked with
  the @{keyword_ref "uses"} dependency declaration given in the theory
  header (see also \secref{sec:begin-thy}).
  
  \item [@{command "ML"}~@{text "text"}] is similar to @{command
  "use"}, but executes ML commands directly from the given @{text
  "text"}.

  \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
  context by applying @{text "text"}, which refers to an ML expression
  of type @{ML_type "theory -> theory"}.  This enables to initialize
  any object-logic specific tools and packages written in ML, for
  example.
  
  \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 "Args.src ->
  Proof.context -> Proof.method"}.  Parsing concrete method syntax
  from @{ML_type Args.src} input can be quite tedious in general.  The
  following simple examples are for methods without any explicit
  arguments, or a list of theorems, respectively.

%FIXME proper antiquotations
{\footnotesize
\begin{verbatim}
 Method.no_args (Method.METHOD (fn facts => foobar_tac))
 Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
 Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
 Method.thms_ctxt_args (fn thms => fn ctxt =>
    Method.METHOD (fn facts => foobar_tac))
\end{verbatim}
}

  Note that mere tactic emulations may ignore the @{text facts}
  parameter above.  Proper proof methods would do something
  appropriate with the list of current facts, though.  Single-rule
  methods usually do strict forward-chaining (e.g.\ by using @{ML
  Drule.multi_resolves}), while automatic ones just insert the facts
  using @{ML Method.insert_tac} before applying the main tactic.

  \end{descr}
*}


subsection {* Syntax translation functions *}

text {*
  \begin{matharray}{rcl}
    @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
    @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
    @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
    @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
    @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
    @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
  \end{matharray}

  \begin{rail}
  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
  ;

  'token\_translation' text
  ;
  \end{rail}

  Syntax translation functions written in ML admit almost arbitrary
  manipulations of Isabelle's inner syntax.  Any of the above commands
  have a single \railqtok{text} argument that refers to an ML
  expression of appropriate type, which are as follows by default:

%FIXME proper antiquotations
\begin{ttbox}
val parse_ast_translation   : (string * (ast list -> ast)) list
val parse_translation       : (string * (term list -> term)) list
val print_translation       : (string * (term list -> term)) list
val typed_print_translation :
  (string * (bool -> typ -> term list -> term)) list
val print_ast_translation   : (string * (ast list -> ast)) list
val token_translation       :
  (string * string * (string -> string * real)) list
\end{ttbox}

  If the @{text "(advanced)"} option is given, the corresponding
  translation functions may depend on the current theory or proof
  context.  This allows to implement advanced syntax mechanisms, as
  translations functions may refer to specific theory declarations or
  auxiliary proof data.

  See also \cite[\S8]{isabelle-ref} for more information on the
  general concept of syntax transformations in Isabelle.

%FIXME proper antiquotations
\begin{ttbox}
val parse_ast_translation:
  (string * (Context.generic -> ast list -> ast)) list
val parse_translation:
  (string * (Context.generic -> term list -> term)) list
val print_translation:
  (string * (Context.generic -> term list -> term)) list
val typed_print_translation:
  (string * (Context.generic -> bool -> typ -> term list -> term)) list
val print_ast_translation:
  (string * (Context.generic -> ast list -> ast)) list
\end{ttbox}
*}


subsection {* Oracles *}

text {*
  \begin{matharray}{rcl}
    @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
  \end{matharray}

  The oracle interface promotes a given ML function @{ML_text
  "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
  type @{ML_text T} given by the user.  This acts like an infinitary
  specification of axioms -- there is no internal check of the
  correctness of the results!  The inference kernel records oracle
  invocations within the internal derivation object of theorems, and
  the pretty printer attaches ``@{text "[!]"}'' to indicate results
  that are not fully checked by Isabelle inferences.

  \begin{rail}
    'oracle' name '(' type ')' '=' text
    ;
  \end{rail}

  \begin{descr}

  \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
  given ML expression @{text "text"} of type
  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
  ML function of type
  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
  bound to the global identifier @{ML_text name}.

  \end{descr}
*}


section {* Proof commands *}

subsection {* Markup commands \label{sec:markup-prf} *}

text {*
  \begin{matharray}{rcl}
    @{command_def "sect"} & : & \isartrans{proof}{proof} \\
    @{command_def "subsect"} & : & \isartrans{proof}{proof} \\
    @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
    @{command_def "txt"} & : & \isartrans{proof}{proof} \\
    @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
  \end{matharray}

  These markup commands for proof mode closely correspond to the ones
  of theory mode (see \S\ref{sec:markup-thy}).

  \begin{rail}
    ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
    ;
  \end{rail}
*}


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 \<dots> 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,
  \<dots>, a\<^sub>n"} do not have any permanent effect.

  \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}]
  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 \<tau>}] 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 \<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{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} \\
    @{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
    @{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
  \end{matharray}

  \begin{rail}
    ('cd' | 'use\_thy' | 'update\_thy') name
    ;
    ('display\_drafts' | 'print\_drafts') (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.

  \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