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