src/Doc/Isar_Ref/Outer_Syntax.thy
author wenzelm
Tue Oct 20 23:53:40 2015 +0200 (2015-10-20)
changeset 61493 0debd22f0c0e
parent 61477 e467ae7aa808
child 61494 63b18f758874
permissions -rw-r--r--
isabelle update_cartouches -t;
     1 theory Outer_Syntax
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>Outer syntax --- the theory language \label{ch:outer-syntax}\<close>
     6 
     7 text \<open>
     8   The rather generic framework of Isabelle/Isar syntax emerges from
     9   three main syntactic categories: \<^emph>\<open>commands\<close> of the top-level
    10   Isar engine (covering theory and proof elements), \<^emph>\<open>methods\<close> for
    11   general goal refinements (analogous to traditional ``tactics''), and
    12   \<^emph>\<open>attributes\<close> for operations on facts (within a certain
    13   context).  Subsequently we give a reference of basic syntactic
    14   entities underlying Isabelle/Isar syntax in a bottom-up manner.
    15   Concrete theory and proof language elements will be introduced later
    16   on.
    17 
    18   \<^medskip>
    19   In order to get started with writing well-formed
    20   Isabelle/Isar documents, the most important aspect to be noted is
    21   the difference of \<^emph>\<open>inner\<close> versus \<^emph>\<open>outer\<close> syntax.  Inner
    22   syntax is that of Isabelle types and terms of the logic, while outer
    23   syntax is that of Isabelle/Isar theory sources (specifications and
    24   proofs).  As a general rule, inner syntax entities may occur only as
    25   \<^emph>\<open>atomic entities\<close> within outer syntax.  For example, the string
    26   @{verbatim \<open>"x + y"\<close>} and identifier @{verbatim z} are legal term
    27   specifications within a theory, while @{verbatim "x + y"} without
    28   quotes is not.
    29 
    30   Printed theory documents usually omit quotes to gain readability
    31   (this is a matter of {\LaTeX} macro setup, say via @{verbatim
    32   "\\isabellestyle"}, see also @{cite "isabelle-system"}).  Experienced
    33   users of Isabelle/Isar may easily reconstruct the lost technical
    34   information, while mere readers need not care about quotes at all.
    35 \<close>
    36 
    37 
    38 section \<open>Commands\<close>
    39 
    40 text \<open>
    41   \begin{matharray}{rcl}
    42     @{command_def "print_commands"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
    43     @{command_def "help"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
    44   \end{matharray}
    45 
    46   @{rail \<open>
    47     @@{command help} (@{syntax name} * )
    48   \<close>}
    49 
    50   \<^descr> @{command "print_commands"} prints all outer syntax keywords
    51   and commands.
    52 
    53   \<^descr> @{command "help"}~\<open>pats\<close> retrieves outer syntax
    54   commands according to the specified name patterns.
    55 \<close>
    56 
    57 
    58 subsubsection \<open>Examples\<close>
    59 
    60 text \<open>Some common diagnostic commands are retrieved like this
    61   (according to usual naming conventions):\<close>
    62 
    63 help "print"
    64 help "find"
    65 
    66 
    67 section \<open>Lexical matters \label{sec:outer-lex}\<close>
    68 
    69 text \<open>The outer lexical syntax consists of three main categories of
    70   syntax tokens:
    71 
    72   \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available
    73   in the present logic session;
    74 
    75   \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required
    76   by the syntax of commands;
    77 
    78   \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
    79 
    80 
    81   Major keywords and minor keywords are guaranteed to be disjoint.
    82   This helps user-interfaces to determine the overall structure of a
    83   theory text, without knowing the full details of command syntax.
    84   Internally, there is some additional information about the kind of
    85   major keywords, which approximates the command type (theory command,
    86   proof command etc.).
    87 
    88   Keywords override named tokens.  For example, the presence of a
    89   command called @{verbatim term} inhibits the identifier @{verbatim
    90   term}, but the string @{verbatim \<open>"term"\<close>} can be used instead.
    91   By convention, the outer syntax always allows quoted strings in
    92   addition to identifiers, wherever a named entity is expected.
    93 
    94   When tokenizing a given input sequence, the lexer repeatedly takes
    95   the longest prefix of the input that forms a valid token.  Spaces,
    96   tabs, newlines and formfeeds between tokens serve as explicit
    97   separators.
    98 
    99   \<^medskip>
   100   The categories for named tokens are defined once and for all as follows.
   101 
   102   \begin{center}
   103   \begin{supertabular}{rcl}
   104     @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
   105     @{syntax_def longident} & = & \<open>ident(\<close>@{verbatim "."}\<open>ident)\<^sup>+\<close> \\
   106     @{syntax_def symident} & = & \<open>sym\<^sup>+  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>ident\<close>@{verbatim ">"} \\
   107     @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
   108     @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}\<open>  |  \<close>@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
   109     @{syntax_def var} & = & @{verbatim "?"}\<open>ident  |  \<close>@{verbatim "?"}\<open>ident\<close>@{verbatim "."}\<open>nat\<close> \\
   110     @{syntax_def typefree} & = & @{verbatim "'"}\<open>ident\<close> \\
   111     @{syntax_def typevar} & = & @{verbatim "?"}\<open>typefree  |  \<close>@{verbatim "?"}\<open>typefree\<close>@{verbatim "."}\<open>nat\<close> \\
   112     @{syntax_def string} & = & @{verbatim \<open>"\<close>} \<open>\<dots>\<close> @{verbatim \<open>"\<close>} \\
   113     @{syntax_def altstring} & = & @{verbatim "`"} \<open>\<dots>\<close> @{verbatim "`"} \\
   114     @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
   115     @{syntax_def verbatim} & = & @{verbatim "{*"} \<open>\<dots>\<close> @{verbatim "*}"} \\[1ex]
   116 
   117     \<open>letter\<close> & = & \<open>latin  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin\<close>@{verbatim ">"}\<open>  |  \<close>@{verbatim \<open>\\<close>}@{verbatim "<"}\<open>latin latin\<close>@{verbatim ">"}\<open>  |  greek  |\<close> \\
   118     \<open>subscript\<close> & = & @{verbatim "\<^sub>"} \\
   119     \<open>quasiletter\<close> & = & \<open>letter  |  digit  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "'"} \\
   120     \<open>latin\<close> & = & @{verbatim a}\<open>  | \<dots> |  \<close>@{verbatim z}\<open>  |  \<close>@{verbatim A}\<open>  |  \<dots> |  \<close>@{verbatim Z} \\
   121     \<open>digit\<close> & = & @{verbatim "0"}\<open>  |  \<dots> |  \<close>@{verbatim "9"} \\
   122     \<open>sym\<close> & = & @{verbatim "!"}\<open>  |  \<close>@{verbatim "#"}\<open>  |  \<close>@{verbatim "$"}\<open>  |  \<close>@{verbatim "%"}\<open>  |  \<close>@{verbatim "&"}\<open>  |  \<close>@{verbatim "*"}\<open>  |  \<close>@{verbatim "+"}\<open>  |  \<close>@{verbatim "-"}\<open>  |  \<close>@{verbatim "/"}\<open>  |\<close> \\
   123     & & @{verbatim "<"}\<open>  |  \<close>@{verbatim "="}\<open>  |  \<close>@{verbatim ">"}\<open>  |  \<close>@{verbatim "?"}\<open>  |  \<close>@{verbatim "@"}\<open>  |  \<close>@{verbatim "^"}\<open>  |  \<close>@{verbatim "_"}\<open>  |  \<close>@{verbatim "|"}\<open>  |  \<close>@{verbatim "~"} \\
   124     \<open>greek\<close> & = & @{verbatim "\<alpha>"}\<open>  |  \<close>@{verbatim "\<beta>"}\<open>  |  \<close>@{verbatim "\<gamma>"}\<open>  |  \<close>@{verbatim "\<delta>"}\<open>  |\<close> \\
   125           &   & @{verbatim "\<epsilon>"}\<open>  |  \<close>@{verbatim "\<zeta>"}\<open>  |  \<close>@{verbatim "\<eta>"}\<open>  |  \<close>@{verbatim "\<theta>"}\<open>  |\<close> \\
   126           &   & @{verbatim "\<iota>"}\<open>  |  \<close>@{verbatim "\<kappa>"}\<open>  |  \<close>@{verbatim "\<mu>"}\<open>  |  \<close>@{verbatim "\<nu>"}\<open>  |\<close> \\
   127           &   & @{verbatim "\<xi>"}\<open>  |  \<close>@{verbatim "\<pi>"}\<open>  |  \<close>@{verbatim "\<rho>"}\<open>  |  \<close>@{verbatim "\<sigma>"}\<open>  |  \<close>@{verbatim "\<tau>"}\<open>  |\<close> \\
   128           &   & @{verbatim "\<upsilon>"}\<open>  |  \<close>@{verbatim "\<phi>"}\<open>  |  \<close>@{verbatim "\<chi>"}\<open>  |  \<close>@{verbatim "\<psi>"}\<open>  |\<close> \\
   129           &   & @{verbatim "\<omega>"}\<open>  |  \<close>@{verbatim "\<Gamma>"}\<open>  |  \<close>@{verbatim "\<Delta>"}\<open>  |  \<close>@{verbatim "\<Theta>"}\<open>  |\<close> \\
   130           &   & @{verbatim "\<Lambda>"}\<open>  |  \<close>@{verbatim "\<Xi>"}\<open>  |  \<close>@{verbatim "\<Pi>"}\<open>  |  \<close>@{verbatim "\<Sigma>"}\<open>  |\<close> \\
   131           &   & @{verbatim "\<Upsilon>"}\<open>  |  \<close>@{verbatim "\<Phi>"}\<open>  |  \<close>@{verbatim "\<Psi>"}\<open>  |  \<close>@{verbatim "\<Omega>"} \\
   132   \end{supertabular}
   133   \end{center}
   134 
   135   A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
   136   which is internally a pair of base name and index (ML type @{ML_type
   137   indexname}).  These components are either separated by a dot as in
   138   \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>.  The latter form is possible if the base name does not end
   139   with digits.  If the index is 0, it may be dropped altogether:
   140   \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the
   141   same unknown, with basename \<open>x\<close> and index 0.
   142 
   143   The syntax of @{syntax_ref string} admits any characters, including
   144   newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}''
   145   (backslash) need to be escaped by a backslash; arbitrary
   146   character codes may be specified as ``@{verbatim \<open>\\<close>}\<open>ddd\<close>'',
   147   with three decimal digits.  Alternative strings according to
   148   @{syntax_ref altstring} are analogous, using single back-quotes
   149   instead.
   150 
   151   The body of @{syntax_ref verbatim} may consist of any text not containing
   152   ``@{verbatim "*}"}''; this allows to include quotes without further
   153   escapes, but there is no way to escape ``@{verbatim "*}"}''. Cartouches
   154   do not have this limitation.
   155 
   156   A @{syntax_ref cartouche} consists of arbitrary text, with properly
   157   balanced blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim
   158   "\<close>"}''.  Note that the rendering of cartouche delimiters is
   159   usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
   160 
   161   Source comments take the form @{verbatim "(*"}~\<open>\<dots>\<close>~@{verbatim "*)"} and may be nested, although the user-interface
   162   might prevent this.  Note that this form indicates source comments
   163   only, which are stripped after lexical analysis of the input.  The
   164   Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are
   165   considered as part of the text (see \secref{sec:comments}).
   166 
   167   Common mathematical symbols such as \<open>\<forall>\<close> are represented in
   168   Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
   169   symbols like this, although proper presentation is left to front-end
   170   tools such as {\LaTeX} or Isabelle/jEdit.  A list of
   171   predefined Isabelle symbols that work well with these tools is given
   172   in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"} does not belong
   173   to the \<open>letter\<close> category, since it is already used differently
   174   in the Pure term language.\<close>
   175 
   176 
   177 section \<open>Common syntax entities\<close>
   178 
   179 text \<open>
   180   We now introduce several basic syntactic entities, such as names,
   181   terms, and theorem specifications, which are factored out of the
   182   actual Isar language elements to be described later.
   183 \<close>
   184 
   185 
   186 subsection \<open>Names\<close>
   187 
   188 text \<open>Entity @{syntax name} usually refers to any name of types,
   189   constants, theorems etc.\ that are to be \<^emph>\<open>declared\<close> or
   190   \<^emph>\<open>defined\<close> (so qualified identifiers are excluded here).  Quoted
   191   strings provide an escape for non-identifier names or those ruled
   192   out by outer syntax keywords (e.g.\ quoted @{verbatim \<open>"let"\<close>}).
   193   Already existing objects are usually referenced by @{syntax
   194   nameref}.
   195 
   196   @{rail \<open>
   197     @{syntax_def name}: @{syntax ident} | @{syntax symident} |
   198       @{syntax string} | @{syntax nat}
   199     ;
   200     @{syntax_def par_name}: '(' @{syntax name} ')'
   201     ;
   202     @{syntax_def nameref}: @{syntax name} | @{syntax longident}
   203   \<close>}
   204 \<close>
   205 
   206 
   207 subsection \<open>Numbers\<close>
   208 
   209 text \<open>The outer lexical syntax (\secref{sec:outer-lex}) admits
   210   natural numbers and floating point numbers.  These are combined as
   211   @{syntax int} and @{syntax real} as follows.
   212 
   213   @{rail \<open>
   214     @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
   215     ;
   216     @{syntax_def real}: @{syntax float} | @{syntax int}
   217   \<close>}
   218 
   219   Note that there is an overlap with the category @{syntax name},
   220   which also includes @{syntax nat}.
   221 \<close>
   222 
   223 
   224 subsection \<open>Comments \label{sec:comments}\<close>
   225 
   226 text \<open>Large chunks of plain @{syntax text} are usually given @{syntax
   227   verbatim}, i.e.\ enclosed in @{verbatim "{*"}~\<open>\<dots>\<close>~@{verbatim "*}"},
   228   or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For convenience, any of the
   229   smaller text units conforming to @{syntax nameref} are admitted as well. A
   230   marginal @{syntax comment} is of the form @{verbatim "--"}~@{syntax text}.
   231   Any number of these may occur within Isabelle/Isar commands.
   232 
   233   @{rail \<open>
   234     @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
   235     ;
   236     @{syntax_def comment}: '--' @{syntax text}
   237   \<close>}
   238 \<close>
   239 
   240 
   241 subsection \<open>Type classes, sorts and arities\<close>
   242 
   243 text \<open>
   244   Classes are specified by plain names.  Sorts have a very simple
   245   inner syntax, which is either a single class name \<open>c\<close> or a
   246   list \<open>{c\<^sub>1, \<dots>, c\<^sub>n}\<close> referring to the
   247   intersection of these classes.  The syntax of type arities is given
   248   directly at the outer level.
   249 
   250   @{rail \<open>
   251     @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
   252     ;
   253     @{syntax_def sort}: @{syntax nameref}
   254     ;
   255     @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
   256   \<close>}
   257 \<close>
   258 
   259 
   260 subsection \<open>Types and terms \label{sec:types-terms}\<close>
   261 
   262 text \<open>
   263   The actual inner Isabelle syntax, that of types and terms of the
   264   logic, is far too sophisticated in order to be modelled explicitly
   265   at the outer theory level.  Basically, any such entity has to be
   266   quoted to turn it into a single token (the parsing and type-checking
   267   is performed internally later).  For convenience, a slightly more
   268   liberal convention is adopted: quotes may be omitted for any type or
   269   term that is already atomic at the outer level.  For example, one
   270   may just write @{verbatim x} instead of quoted @{verbatim \<open>"x"\<close>}.
   271   Note that symbolic identifiers (e.g.\ @{verbatim "++"} or \<open>\<forall>\<close> are available as well, provided these have not been superseded
   272   by commands or other keywords already (such as @{verbatim "="} or
   273   @{verbatim "+"}).
   274 
   275   @{rail \<open>
   276     @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
   277       @{syntax typevar}
   278     ;
   279     @{syntax_def term}: @{syntax nameref} | @{syntax var}
   280     ;
   281     @{syntax_def prop}: @{syntax term}
   282   \<close>}
   283 
   284   Positional instantiations are specified as a sequence of terms, or the
   285   placeholder ``\<open>_\<close>'' (underscore), which means to skip a position.
   286 
   287   @{rail \<open>
   288     @{syntax_def inst}: '_' | @{syntax term}
   289     ;
   290     @{syntax_def insts}: (@{syntax inst} *)
   291   \<close>}
   292 
   293   Named instantiations are specified as pairs of assignments \<open>v =
   294   t\<close>, which refer to schematic variables in some theorem that is
   295   instantiated. Both type and terms instantiations are admitted, and
   296   distinguished by the usual syntax of variable names.
   297 
   298   @{rail \<open>
   299     @{syntax_def named_inst}: variable '=' (type | term)
   300     ;
   301     @{syntax_def named_insts}: (named_inst @'and' +)
   302     ;
   303     variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}
   304   \<close>}
   305 
   306   Type declarations and definitions usually refer to @{syntax
   307   typespec} on the left-hand side.  This models basic type constructor
   308   application at the outer syntax level.  Note that only plain postfix
   309   notation is available here, but no infixes.
   310 
   311   @{rail \<open>
   312     @{syntax_def typespec}:
   313       (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
   314     ;
   315     @{syntax_def typespec_sorts}:
   316       (() | (@{syntax typefree} ('::' @{syntax sort})?) |
   317         '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
   318   \<close>}
   319 \<close>
   320 
   321 
   322 subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close>
   323 
   324 text \<open>Wherever explicit propositions (or term fragments) occur in a
   325   proof text, casual binding of schematic term variables may be given
   326   specified via patterns of the form ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''.
   327   This works both for @{syntax term} and @{syntax prop}.
   328 
   329   @{rail \<open>
   330     @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
   331     ;
   332     @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
   333   \<close>}
   334 
   335   \<^medskip>
   336   Declarations of local variables \<open>x :: \<tau>\<close> and
   337   logical propositions \<open>a : \<phi>\<close> represent different views on
   338   the same principle of introducing a local scope.  In practice, one
   339   may usually omit the typing of @{syntax vars} (due to
   340   type-inference), and the naming of propositions (due to implicit
   341   references of current facts).  In any case, Isar proof elements
   342   usually admit to introduce multiple such items simultaneously.
   343 
   344   @{rail \<open>
   345     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
   346     ;
   347     @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
   348   \<close>}
   349 
   350   The treatment of multiple declarations corresponds to the
   351   complementary focus of @{syntax vars} versus @{syntax props}.  In
   352   ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the typing refers to all variables, while
   353   in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to all propositions
   354   collectively.  Isar language elements that refer to @{syntax vars}
   355   or @{syntax props} typically admit separate typings or namings via
   356   another level of iteration, with explicit @{keyword_ref "and"}
   357   separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   358   \secref{sec:proof-context}.
   359 
   360   @{rail \<open>
   361     @{syntax_def "fixes"}:
   362       ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
   363     ;
   364     @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
   365   \<close>}
   366 
   367   The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
   368   admits specification of mixfix syntax for the entities that are introduced
   369   into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>''
   370   is admitted in many situations to indicate a so-called ``eigen-context''
   371   of a formal element: the result will be exported and thus generalized over
   372   the given variables.\<close>
   373 
   374 
   375 subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
   376 
   377 text \<open>Attributes have their own ``semi-inner'' syntax, in the sense
   378   that input conforming to @{syntax args} below is parsed by the
   379   attribute a second time.  The attribute argument specifications may
   380   be any sequence of atomic entities (identifiers, strings etc.), or
   381   properly bracketed argument lists.  Below @{syntax atom} refers to
   382   any atomic entity, including any @{syntax keyword} conforming to
   383   @{syntax symident}.
   384 
   385   @{rail \<open>
   386     @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
   387       @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
   388       @{syntax keyword} | @{syntax cartouche}
   389     ;
   390     arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
   391     ;
   392     @{syntax_def args}: arg *
   393     ;
   394     @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
   395   \<close>}
   396 
   397   Theorem specifications come in several flavors: @{syntax axmdecl}
   398   and @{syntax thmdecl} usually refer to axioms, assumptions or
   399   results of goal statements, while @{syntax thmdef} collects lists of
   400   existing theorems.  Existing theorems are given by @{syntax thmref}
   401   and @{syntax thmrefs}, the former requires an actual singleton
   402   result.
   403 
   404   There are three forms of theorem references:
   405 
   406   \<^enum> named facts \<open>a\<close>,
   407 
   408   \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>,
   409 
   410   \<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
   411   @{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"} or @{syntax_ref cartouche}
   412   \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}).
   413 
   414 
   415   Any kind of theorem specification may include lists of attributes
   416   both on the left and right hand sides; attributes are applied to any
   417   immediately preceding fact.  If names are omitted, the theorems are
   418   not stored within the theorem database of the theory or proof
   419   context, but any given attributes are applied nonetheless.
   420 
   421   An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'') abbreviates a theorem reference involving an
   422   internal dummy fact, which will be ignored later on.  So only the
   423   effect of the attribute on the background context will persist.
   424   This form of in-place declarations is particularly useful with
   425   commands like @{command "declare"} and @{command "using"}.
   426 
   427   @{rail \<open>
   428     @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
   429     ;
   430     @{syntax_def thmbind}:
   431       @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
   432     ;
   433     @{syntax_def thmdecl}: thmbind ':'
   434     ;
   435     @{syntax_def thmdef}: thmbind '='
   436     ;
   437     @{syntax_def thmref}:
   438       (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
   439         @{syntax attributes}? |
   440       '[' @{syntax attributes} ']'
   441     ;
   442     @{syntax_def thmrefs}: @{syntax thmref} +
   443     ;
   444     selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
   445   \<close>}
   446 \<close>
   447 
   448 
   449 section \<open>Diagnostic commands\<close>
   450 
   451 text \<open>
   452   \begin{matharray}{rcl}
   453     @{command_def "print_theory"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   454     @{command_def "print_definitions"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   455     @{command_def "print_methods"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   456     @{command_def "print_attributes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   457     @{command_def "print_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   458     @{command_def "find_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   459     @{command_def "find_consts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   460     @{command_def "thm_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   461     @{command_def "unused_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   462     @{command_def "print_facts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   463     @{command_def "print_term_bindings"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   464   \end{matharray}
   465 
   466   @{rail \<open>
   467     (@@{command print_theory} |
   468       @@{command print_definitions} |
   469       @@{command print_methods} |
   470       @@{command print_attributes} |
   471       @@{command print_theorems} |
   472       @@{command print_facts}) ('!'?)
   473     ;
   474     @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
   475     ;
   476     thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
   477       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
   478     ;
   479     @@{command find_consts} (const_criterion*)
   480     ;
   481     const_criterion: ('-'?)
   482       ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
   483     ;
   484     @@{command thm_deps} @{syntax thmrefs}
   485     ;
   486     @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
   487   \<close>}
   488 
   489   These commands print certain parts of the theory and proof context.
   490   Note that there are some further ones available, such as for the set
   491   of rules declared for simplifications.
   492 
   493   \<^descr> @{command "print_theory"} prints the main logical content of the
   494   background theory; the ``\<open>!\<close>'' option indicates extra verbosity.
   495 
   496   \<^descr> @{command "print_definitions"} prints dependencies of definitional
   497   specifications within the background theory, which may be constants
   498   \secref{sec:consts} or types (\secref{sec:types-pure},
   499   \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra
   500   verbosity.
   501 
   502   \<^descr> @{command "print_methods"} prints all proof methods available in the
   503   current theory context; the ``\<open>!\<close>'' option indicates extra
   504   verbosity.
   505 
   506   \<^descr> @{command "print_attributes"} prints all attributes available in the
   507   current theory context; the ``\<open>!\<close>'' option indicates extra
   508   verbosity.
   509 
   510   \<^descr> @{command "print_theorems"} prints theorems of the background theory
   511   resulting from the last command; the ``\<open>!\<close>'' option indicates
   512   extra verbosity.
   513 
   514   \<^descr> @{command "print_facts"} prints all local facts of the current
   515   context, both named and unnamed ones; the ``\<open>!\<close>'' option indicates
   516   extra verbosity.
   517 
   518   \<^descr> @{command "print_term_bindings"} prints all term bindings that
   519   are present in the context.
   520 
   521   \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts
   522   from the theory or proof context matching all of given search
   523   criteria.  The criterion \<open>name: p\<close> selects all theorems
   524   whose fully qualified name matches pattern \<open>p\<close>, which may
   525   contain ``\<open>*\<close>'' wildcards.  The criteria \<open>intro\<close>,
   526   \<open>elim\<close>, and \<open>dest\<close> select theorems that match the
   527   current goal as introduction, elimination or destruction rules,
   528   respectively.  The criterion \<open>solves\<close> returns all rules
   529   that would directly solve the current goal.  The criterion
   530   \<open>simp: t\<close> selects all rewrite rules whose left-hand side
   531   matches the given term.  The criterion term \<open>t\<close> selects all
   532   theorems that contain the pattern \<open>t\<close> -- as usual, patterns
   533   may contain occurrences of the dummy ``\<open>_\<close>'', schematic
   534   variables, and type constraints.
   535 
   536   Criteria can be preceded by ``\<open>-\<close>'' to select theorems that
   537   do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria
   538   yields \<^emph>\<open>all\<close> currently known facts.  An optional limit for the
   539   number of printed facts may be given; the default is 40.  By
   540   default, duplicates are removed from the search result. Use
   541   \<open>with_dups\<close> to display duplicates.
   542 
   543   \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants
   544   whose type meets all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type that matches the type pattern
   545   \<open>ty\<close>.  Patterns may contain both the dummy type ``\<open>_\<close>''
   546   and sort constraints. The criterion \<open>ty\<close> is similar, but it
   547   also matches against subtypes. The criterion \<open>name: p\<close> and
   548   the prefix ``\<open>-\<close>'' function as described for @{command
   549   "find_theorems"}.
   550 
   551   \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
   552   visualizes dependencies of facts, using Isabelle's graph browser
   553   tool (see also @{cite "isabelle-system"}).
   554 
   555   \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close>
   556   displays all theorems that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>
   557   or their parents but not in \<open>A\<^sub>1 \<dots> A\<^sub>m\<close> or their parents and
   558   that are never used.
   559   If \<open>n\<close> is \<open>0\<close>, the end of the range of theories
   560   defaults to the current theory. If no range is specified,
   561   only the unused theorems in the current theory are displayed.
   562 \<close>
   563 
   564 end