doc-src/IsarRef/Thy/Outer_Syntax.thy

     ;
   \end{rail}
 *}
 
 
-subsection {* Mixfix annotations *}
-
-text {*
-  Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
-  types and terms.  Some commands such as @{command "types"} (see
-  \secref{sec:types-pure}) admit infixes only, while @{command
-  "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
-  \secref{sec:syn-trans}) support the full range of general mixfixes
-  and binders.
-
-  \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
-  \begin{rail}
-    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
-    ;
-    mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
-    ;
-    structmixfix: mixfix | '(' 'structure' ')'
-    ;
-
-    prios: '[' (nat + ',') ']'
-    ;
-  \end{rail}
-
-  Here the \railtok{string} specifications refer to the actual mixfix
-  template, which may include literal text, spacing, blocks, and
-  arguments (denoted by ``@{text _}''); the special symbol
-  ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
-  argument that specifies an implicit structure reference (see also
-  \secref{sec:locale}).  Infix and binder declarations provide common
-  abbreviations for particular mixfix declarations.  So in practice,
-  mixfix templates mostly degenerate to literal text for concrete
-  syntax, such as ``@{verbatim "++"}'' for an infix symbol.
-
-  \medskip In full generality, mixfix declarations work as follows.
-  Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
-  annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
-  "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
-  delimiters that surround argument positions as indicated by
-  underscores.
-
-  Altogether this determines a production for a context-free priority
-  grammar, where for each argument @{text "i"} the syntactic category
-  is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
-  the result category is determined from @{text "\<tau>"} (with
-  priority @{text "p"}).  Priority specifications are optional, with
-  default 0 for arguments and 1000 for the result.
-
-  Since @{text "\<tau>"} may be again a function type, the constant
-  type scheme may have more argument positions than the mixfix
-  pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
-  @{text "m > n"} works by attaching concrete notation only to the
-  innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
-  instead.  If a term has fewer argument than specified in the mixfix
-  template, the concrete syntax is ignored.
-
-  \medskip A mixfix template may also contain additional directives
-  for pretty printing, notably spaces, blocks, and breaks.  The
-  general template format is a sequence over any of the following
-  entities.
-
-  \begin{itemize}
-
-  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
-  sequence of characters other than the special characters @{text "'"}
-  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
-  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
-  (parentheses).
-
-  A single quote escapes the special meaning of these meta-characters,
-  producing a literal version of the following character, unless that
-  is a blank.  A single quote followed by a blank separates
-  delimiters, without affecting printing, but input tokens may have
-  additional white space here.
-
-  \item @{text "_"} is an argument position, which stands for a
-  certain syntactic category in the underlying grammar.
-
-  \item @{text "\<index>"} is an indexed argument position; this is
-  the place where implicit structure arguments can be attached.
-
-  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
-  printing.  This and the following specifications do not affect
-  parsing at all.
-
-  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
-  optional number specifies how much indentation to add when a line
-  break occurs within the block.  If the parenthesis is not followed
-  by digits, the indentation defaults to 0.  A block specified via
-  @{text "(00"} is unbreakable.
-
-  \item @{text ")"} closes a pretty printing block.
-
-  \item @{text "//"} forces a line break.
-
-  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
-  "\<^bold>s"} stands for the string of spaces (zero or more) right
-  after the slash.  These spaces are printed if the break is
-  \emph{not} taken.
-
-  \end{itemize}
-
-  For example, the template @{text "(_ +/ _)"} specifies an infix
-  operator.  There are two argument positions; the delimiter @{text
-  "+"} is preceded by a space and followed by a space or line break;
-  the entire phrase is a pretty printing block.  
-
-  The general idea of pretty printing with blocks and breaks is also
-  described in \cite{paulson-ml2}.
-*}
-
-
-subsection {* Proof methods \label{sec:syn-meth} *}
-
-text {*
-  Proof methods are either basic ones, or expressions composed of
-  methods via ``@{verbatim ","}'' (sequential composition),
-  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
-  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
-  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
-  sub-goals, with default @{text "n = 1"}).  In practice, proof
-  methods are usually just a comma separated list of
-  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
-  parentheses may be dropped for single method specifications (with no
-  arguments).
-
-  \indexouternonterm{method}
-  \begin{rail}
-    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
-    ;
-    methods: (nameref args | method) + (',' | '|')
-    ;
-  \end{rail}
-
-  Proper Isar proof methods do \emph{not} admit arbitrary goal
-  addressing, but refer either to the first sub-goal or all sub-goals
-  uniformly.  The goal restriction operator ``@{text "[n]"}''
-  evaluates a method expression within a sandbox consisting of the
-  first @{text n} sub-goals (which need to exist).  For example, the
-  method ``@{text "simp_all[3]"}'' simplifies the first three
-  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
-  new goals that emerge from applying rule @{text "foo"} to the
-  originally first one.
-
-  Improper methods, notably tactic emulations, offer a separate
-  low-level goal addressing scheme as explicit argument to the
-  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
-  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
-  "n"}.
-
-  \indexouternonterm{goalspec}
-  \begin{rail}
-    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
-    ;
-  \end{rail}
-*}
-
-
-subsection {* Attributes and theorems \label{sec:syn-att} *}
-
-text {*
-  Attributes (and proof methods, see \secref{sec:syn-meth}) have their
-  own ``semi-inner'' syntax, in the sense that input conforming to
-  \railnonterm{args} below is parsed by the attribute a second time.
-  The attribute argument specifications may be any sequence of atomic
-  entities (identifiers, strings etc.), or properly bracketed argument
-  lists.  Below \railqtok{atom} refers to any atomic entity, including
-  any \railtok{keyword} conforming to \railtok{symident}.
-
-  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
-  \begin{rail}
-    atom: nameref | typefree | typevar | var | nat | keyword
-    ;
-    arg: atom | '(' args ')' | '[' args ']'
-    ;
-    args: arg *
-    ;
-    attributes: '[' (nameref args * ',') ']'
-    ;
-  \end{rail}
-
-  Theorem specifications come in several flavors:
-  \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
-  axioms, assumptions or results of goal statements, while
-  \railnonterm{thmdef} collects lists of existing theorems.  Existing
-  theorems are given by \railnonterm{thmref} and
-  \railnonterm{thmrefs}, the former requires an actual singleton
-  result.
-
-  There are three forms of theorem references:
-  \begin{enumerate}
-  
-  \item named facts @{text "a"},
-
-  \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
-
-  \item literal fact propositions using @{syntax_ref altstring} syntax
-  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
-  @{method_ref fact} in \secref{sec:pure-meth-att}).
-
-  \end{enumerate}
-
-  Any kind of theorem specification may include lists of attributes
-  both on the left and right hand sides; attributes are applied to any
-  immediately preceding fact.  If names are omitted, the theorems are
-  not stored within the theorem database of the theory or proof
-  context, but any given attributes are applied nonetheless.
-
-  An extra pair of brackets around attributes (like ``@{text
-  "[[simproc a]]"}'') abbreviates a theorem reference involving an
-  internal dummy fact, which will be ignored later on.  So only the
-  effect of the attribute on the background context will persist.
-  This form of in-place declarations is particularly useful with
-  commands like @{command "declare"} and @{command "using"}.
-
-  \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
-  \indexouternonterm{thmdef}\indexouternonterm{thmref}
-  \indexouternonterm{thmrefs}\indexouternonterm{selection}
-  \begin{rail}
-    axmdecl: name attributes? ':'
-    ;
-    thmdecl: thmbind ':'
-    ;
-    thmdef: thmbind '='
-    ;
-    thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
-    ;
-    thmrefs: thmref +
-    ;
-
-    thmbind: name attributes | name | attributes
-    ;
-    selection: '(' ((nat | nat '-' nat?) + ',') ')'
-    ;
-  \end{rail}
-*}
-
-
 subsection {* Term patterns and declarations \label{sec:term-decls} *}
 
 text {*
   Wherever explicit propositions (or term fragments) occur in a proof
   text, casual binding of schematic term variables may be given

   another level of iteration, with explicit @{keyword_ref "and"}
   separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   \secref{sec:proof-context}.
 *}
 
+
+subsection {* Mixfix annotations *}
+
+text {*
+  Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
+  types and terms.  Some commands such as @{command "types"} (see
+  \secref{sec:types-pure}) admit infixes only, while @{command
+  "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
+  \secref{sec:syn-trans}) support the full range of general mixfixes
+  and binders.
+
+  \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
+  \begin{rail}
+    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
+    ;
+    mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
+    ;
+    structmixfix: mixfix | '(' 'structure' ')'
+    ;
+
+    prios: '[' (nat + ',') ']'
+    ;
+  \end{rail}
+
+  Here the \railtok{string} specifications refer to the actual mixfix
+  template, which may include literal text, spacing, blocks, and
+  arguments (denoted by ``@{text _}''); the special symbol
+  ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
+  argument that specifies an implicit structure reference (see also
+  \secref{sec:locale}).  Infix and binder declarations provide common
+  abbreviations for particular mixfix declarations.  So in practice,
+  mixfix templates mostly degenerate to literal text for concrete
+  syntax, such as ``@{verbatim "++"}'' for an infix symbol.
+
+  \medskip In full generality, mixfix declarations work as follows.
+  Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
+  annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
+  "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
+  delimiters that surround argument positions as indicated by
+  underscores.
+
+  Altogether this determines a production for a context-free priority
+  grammar, where for each argument @{text "i"} the syntactic category
+  is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
+  the result category is determined from @{text "\<tau>"} (with
+  priority @{text "p"}).  Priority specifications are optional, with
+  default 0 for arguments and 1000 for the result.
+
+  Since @{text "\<tau>"} may be again a function type, the constant
+  type scheme may have more argument positions than the mixfix
+  pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
+  @{text "m > n"} works by attaching concrete notation only to the
+  innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
+  instead.  If a term has fewer arguments than specified in the mixfix
+  template, the concrete syntax is ignored.
+
+  \medskip A mixfix template may also contain additional directives
+  for pretty printing, notably spaces, blocks, and breaks.  The
+  general template format is a sequence over any of the following
+  entities.
+
+  \begin{itemize}
+
+  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
+  sequence of characters other than the special characters @{text "'"}
+  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
+  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
+  (parentheses).
+
+  A single quote escapes the special meaning of these meta-characters,
+  producing a literal version of the following character, unless that
+  is a blank.  A single quote followed by a blank separates
+  delimiters, without affecting printing, but input tokens may have
+  additional white space here.
+
+  \item @{text "_"} is an argument position, which stands for a
+  certain syntactic category in the underlying grammar.
+
+  \item @{text "\<index>"} is an indexed argument position; this is
+  the place where implicit structure arguments can be attached.
+
+  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
+  printing.  This and the following specifications do not affect
+  parsing at all.
+
+  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
+  optional number specifies how much indentation to add when a line
+  break occurs within the block.  If the parenthesis is not followed
+  by digits, the indentation defaults to 0.  A block specified via
+  @{text "(00"} is unbreakable.
+
+  \item @{text ")"} closes a pretty printing block.
+
+  \item @{text "//"} forces a line break.
+
+  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
+  "\<^bold>s"} stands for the string of spaces (zero or more) right
+  after the slash.  These spaces are printed if the break is
+  \emph{not} taken.
+
+  \end{itemize}
+
+  For example, the template @{text "(_ +/ _)"} specifies an infix
+  operator.  There are two argument positions; the delimiter @{text
+  "+"} is preceded by a space and followed by a space or line break;
+  the entire phrase is a pretty printing block.
+
+  The general idea of pretty printing with blocks and breaks is also
+  described in \cite{paulson-ml2}.
+*}
+
+
+subsection {* Attributes and theorems \label{sec:syn-att} *}
+
+text {* Attributes have their own ``semi-inner'' syntax, in the sense
+  that input conforming to \railnonterm{args} below is parsed by the
+  attribute a second time.  The attribute argument specifications may
+  be any sequence of atomic entities (identifiers, strings etc.), or
+  properly bracketed argument lists.  Below \railqtok{atom} refers to
+  any atomic entity, including any \railtok{keyword} conforming to
+  \railtok{symident}.
+
+  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
+  \begin{rail}
+    atom: nameref | typefree | typevar | var | nat | keyword
+    ;
+    arg: atom | '(' args ')' | '[' args ']'
+    ;
+    args: arg *
+    ;
+    attributes: '[' (nameref args * ',') ']'
+    ;
+  \end{rail}
+
+  Theorem specifications come in several flavors:
+  \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
+  axioms, assumptions or results of goal statements, while
+  \railnonterm{thmdef} collects lists of existing theorems.  Existing
+  theorems are given by \railnonterm{thmref} and
+  \railnonterm{thmrefs}, the former requires an actual singleton
+  result.
+
+  There are three forms of theorem references:
+  \begin{enumerate}
+  
+  \item named facts @{text "a"},
+
+  \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
+
+  \item literal fact propositions using @{syntax_ref altstring} syntax
+  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
+  @{method_ref fact}).
+
+  \end{enumerate}
+
+  Any kind of theorem specification may include lists of attributes
+  both on the left and right hand sides; attributes are applied to any
+  immediately preceding fact.  If names are omitted, the theorems are
+  not stored within the theorem database of the theory or proof
+  context, but any given attributes are applied nonetheless.
+
+  An extra pair of brackets around attributes (like ``@{text
+  "[[simproc a]]"}'') abbreviates a theorem reference involving an
+  internal dummy fact, which will be ignored later on.  So only the
+  effect of the attribute on the background context will persist.
+  This form of in-place declarations is particularly useful with
+  commands like @{command "declare"} and @{command "using"}.
+
+  \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
+  \indexouternonterm{thmdef}\indexouternonterm{thmref}
+  \indexouternonterm{thmrefs}\indexouternonterm{selection}
+  \begin{rail}
+    axmdecl: name attributes? ':'
+    ;
+    thmdecl: thmbind ':'
+    ;
+    thmdef: thmbind '='
+    ;
+    thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
+    ;
+    thmrefs: thmref +
+    ;
+
+    thmbind: name attributes | name | attributes
+    ;
+    selection: '(' ((nat | nat '-' nat?) + ',') ')'
+    ;
+  \end{rail}
+*}
+
 end