tuned;
authorwenzelm
Thu Nov 13 21:34:23 2008 +0100 (2008-11-13)
changeset 28752754f10154d73
parent 28751 aad88e7344f0
child 28753 b5926a48c943
tuned;
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/Outer_Syntax.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Nov 13 21:33:56 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu Nov 13 21:34:23 2008 +0100
     1.3 @@ -859,7 +859,7 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *}
     1.8 +section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
     1.9  
    1.10  text {*
    1.11    The following tools of Isabelle/HOL support cases analysis and
     2.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:33:56 2008 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:34:23 2008 +0100
     2.3 @@ -262,6 +262,51 @@
     2.4  *}
     2.5  
     2.6  
     2.7 +subsection {* Term patterns and declarations \label{sec:term-decls} *}
     2.8 +
     2.9 +text {*
    2.10 +  Wherever explicit propositions (or term fragments) occur in a proof
    2.11 +  text, casual binding of schematic term variables may be given
    2.12 +  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
    2.13 +  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
    2.14 +
    2.15 +  \indexouternonterm{termpat}\indexouternonterm{proppat}
    2.16 +  \begin{rail}
    2.17 +    termpat: '(' ('is' term +) ')'
    2.18 +    ;
    2.19 +    proppat: '(' ('is' prop +) ')'
    2.20 +    ;
    2.21 +  \end{rail}
    2.22 +
    2.23 +  \medskip Declarations of local variables @{text "x :: \<tau>"} and
    2.24 +  logical propositions @{text "a : \<phi>"} represent different views on
    2.25 +  the same principle of introducing a local scope.  In practice, one
    2.26 +  may usually omit the typing of \railnonterm{vars} (due to
    2.27 +  type-inference), and the naming of propositions (due to implicit
    2.28 +  references of current facts).  In any case, Isar proof elements
    2.29 +  usually admit to introduce multiple such items simultaneously.
    2.30 +
    2.31 +  \indexouternonterm{vars}\indexouternonterm{props}
    2.32 +  \begin{rail}
    2.33 +    vars: (name+) ('::' type)?
    2.34 +    ;
    2.35 +    props: thmdecl? (prop proppat? +)
    2.36 +    ;
    2.37 +  \end{rail}
    2.38 +
    2.39 +  The treatment of multiple declarations corresponds to the
    2.40 +  complementary focus of \railnonterm{vars} versus
    2.41 +  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
    2.42 +  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
    2.43 +  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
    2.44 +  Isar language elements that refer to \railnonterm{vars} or
    2.45 +  \railnonterm{props} typically admit separate typings or namings via
    2.46 +  another level of iteration, with explicit @{keyword_ref "and"}
    2.47 +  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
    2.48 +  \secref{sec:proof-context}.
    2.49 +*}
    2.50 +
    2.51 +
    2.52  subsection {* Mixfix annotations *}
    2.53  
    2.54  text {*
    2.55 @@ -274,7 +319,7 @@
    2.56  
    2.57    \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
    2.58    \begin{rail}
    2.59 -    infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
    2.60 +    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
    2.61      ;
    2.62      mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
    2.63      ;
    2.64 @@ -286,16 +331,90 @@
    2.65    \end{rail}
    2.66  
    2.67    Here the \railtok{string} specifications refer to the actual mixfix
    2.68 -  template (see also \cite{isabelle-ref}), which may include literal
    2.69 -  text, spacing, blocks, and arguments (denoted by ``@{text _}''); the
    2.70 -  special symbol ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'')
    2.71 -  represents an index argument that specifies an implicit structure
    2.72 -  reference (see also \secref{sec:locale}).  Infix and binder
    2.73 -  declarations provide common abbreviations for particular mixfix
    2.74 -  declarations.  So in practice, mixfix templates mostly degenerate to
    2.75 -  literal text for concrete syntax, such as ``@{verbatim "++"}'' for
    2.76 -  an infix symbol, or ``@{verbatim "++"}@{text "\<index>"}'' for an infix of
    2.77 -  an implicit structure.
    2.78 +  template, which may include literal text, spacing, blocks, and
    2.79 +  arguments (denoted by ``@{text _}''); the special symbol
    2.80 +  ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
    2.81 +  argument that specifies an implicit structure reference (see also
    2.82 +  \secref{sec:locale}).  Infix and binder declarations provide common
    2.83 +  abbreviations for particular mixfix declarations.  So in practice,
    2.84 +  mixfix templates mostly degenerate to literal text for concrete
    2.85 +  syntax, such as ``@{verbatim "++"}'' for an infix symbol.
    2.86 +
    2.87 +  \medskip In full generality, mixfix declarations work as follows.
    2.88 +  Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
    2.89 +  annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
    2.90 +  "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
    2.91 +  delimiters that surround argument positions as indicated by
    2.92 +  underscores.
    2.93 +
    2.94 +  Altogether this determines a production for a context-free priority
    2.95 +  grammar, where for each argument @{text "i"} the syntactic category
    2.96 +  is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
    2.97 +  the result category is determined from @{text "\<tau>"} (with
    2.98 +  priority @{text "p"}).  Priority specifications are optional, with
    2.99 +  default 0 for arguments and 1000 for the result.
   2.100 +
   2.101 +  Since @{text "\<tau>"} may be again a function type, the constant
   2.102 +  type scheme may have more argument positions than the mixfix
   2.103 +  pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
   2.104 +  @{text "m > n"} works by attaching concrete notation only to the
   2.105 +  innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
   2.106 +  instead.  If a term has fewer arguments than specified in the mixfix
   2.107 +  template, the concrete syntax is ignored.
   2.108 +
   2.109 +  \medskip A mixfix template may also contain additional directives
   2.110 +  for pretty printing, notably spaces, blocks, and breaks.  The
   2.111 +  general template format is a sequence over any of the following
   2.112 +  entities.
   2.113 +
   2.114 +  \begin{itemize}
   2.115 +
   2.116 +  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
   2.117 +  sequence of characters other than the special characters @{text "'"}
   2.118 +  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
   2.119 +  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
   2.120 +  (parentheses).
   2.121 +
   2.122 +  A single quote escapes the special meaning of these meta-characters,
   2.123 +  producing a literal version of the following character, unless that
   2.124 +  is a blank.  A single quote followed by a blank separates
   2.125 +  delimiters, without affecting printing, but input tokens may have
   2.126 +  additional white space here.
   2.127 +
   2.128 +  \item @{text "_"} is an argument position, which stands for a
   2.129 +  certain syntactic category in the underlying grammar.
   2.130 +
   2.131 +  \item @{text "\<index>"} is an indexed argument position; this is
   2.132 +  the place where implicit structure arguments can be attached.
   2.133 +
   2.134 +  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
   2.135 +  printing.  This and the following specifications do not affect
   2.136 +  parsing at all.
   2.137 +
   2.138 +  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
   2.139 +  optional number specifies how much indentation to add when a line
   2.140 +  break occurs within the block.  If the parenthesis is not followed
   2.141 +  by digits, the indentation defaults to 0.  A block specified via
   2.142 +  @{text "(00"} is unbreakable.
   2.143 +
   2.144 +  \item @{text ")"} closes a pretty printing block.
   2.145 +
   2.146 +  \item @{text "//"} forces a line break.
   2.147 +
   2.148 +  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
   2.149 +  "\<^bold>s"} stands for the string of spaces (zero or more) right
   2.150 +  after the slash.  These spaces are printed if the break is
   2.151 +  \emph{not} taken.
   2.152 +
   2.153 +  \end{itemize}
   2.154 +
   2.155 +  For example, the template @{text "(_ +/ _)"} specifies an infix
   2.156 +  operator.  There are two argument positions; the delimiter @{text
   2.157 +  "+"} is preceded by a space and followed by a space or line break;
   2.158 +  the entire phrase is a pretty printing block.
   2.159 +
   2.160 +  The general idea of pretty printing with blocks and breaks is also
   2.161 +  described in \cite{paulson-ml2}.
   2.162  *}
   2.163  
   2.164  
   2.165 @@ -424,49 +543,4 @@
   2.166    \end{rail}
   2.167  *}
   2.168  
   2.169 -
   2.170 -subsection {* Term patterns and declarations \label{sec:term-decls} *}
   2.171 -
   2.172 -text {*
   2.173 -  Wherever explicit propositions (or term fragments) occur in a proof
   2.174 -  text, casual binding of schematic term variables may be given
   2.175 -  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
   2.176 -  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
   2.177 -
   2.178 -  \indexouternonterm{termpat}\indexouternonterm{proppat}
   2.179 -  \begin{rail}
   2.180 -    termpat: '(' ('is' term +) ')'
   2.181 -    ;
   2.182 -    proppat: '(' ('is' prop +) ')'
   2.183 -    ;
   2.184 -  \end{rail}
   2.185 -
   2.186 -  \medskip Declarations of local variables @{text "x :: \<tau>"} and
   2.187 -  logical propositions @{text "a : \<phi>"} represent different views on
   2.188 -  the same principle of introducing a local scope.  In practice, one
   2.189 -  may usually omit the typing of \railnonterm{vars} (due to
   2.190 -  type-inference), and the naming of propositions (due to implicit
   2.191 -  references of current facts).  In any case, Isar proof elements
   2.192 -  usually admit to introduce multiple such items simultaneously.
   2.193 -
   2.194 -  \indexouternonterm{vars}\indexouternonterm{props}
   2.195 -  \begin{rail}
   2.196 -    vars: (name+) ('::' type)?
   2.197 -    ;
   2.198 -    props: thmdecl? (prop proppat? +)
   2.199 -    ;
   2.200 -  \end{rail}
   2.201 -
   2.202 -  The treatment of multiple declarations corresponds to the
   2.203 -  complementary focus of \railnonterm{vars} versus
   2.204 -  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
   2.205 -  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
   2.206 -  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
   2.207 -  Isar language elements that refer to \railnonterm{vars} or
   2.208 -  \railnonterm{props} typically admit separate typings or namings via
   2.209 -  another level of iteration, with explicit @{keyword_ref "and"}
   2.210 -  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   2.211 -  \secref{sec:proof-context}.
   2.212 -*}
   2.213 -
   2.214  end