tuned whitespace;
authorwenzelm
Fri Nov 13 15:06:58 2015 +0100 (2015-11-13)
changeset 616575b878bc6ae98
parent 61656 cfabbc083977
child 61658 5dce70aecbfc
tuned whitespace;
src/Doc/Isar_Ref/Proof.thy
src/Doc/Isar_Ref/Proof_Script.thy
     1.1 --- a/src/Doc/Isar_Ref/Proof.thy	Fri Nov 13 14:49:30 2015 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Fri Nov 13 15:06:58 2015 +0100
     1.3 @@ -7,38 +7,33 @@
     1.4  chapter \<open>Proofs \label{ch:proofs}\<close>
     1.5  
     1.6  text \<open>
     1.7 -
     1.8 -  Proof commands perform transitions of Isar/VM machine
     1.9 -  configurations, which are block-structured, consisting of a stack of
    1.10 -  nodes with three main components: logical proof context, current
    1.11 -  facts, and open goals.  Isar/VM transitions are typed according to
    1.12 -  the following three different modes of operation:
    1.13 -
    1.14 -  \<^descr> \<open>proof(prove)\<close> means that a new goal has just been
    1.15 -  stated that is now to be \<^emph>\<open>proven\<close>; the next command may refine
    1.16 -  it by some proof method, and enter a sub-proof to establish the
    1.17 -  actual result.
    1.18 -
    1.19 -  \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the
    1.20 -  context may be augmented by \<^emph>\<open>stating\<close> additional assumptions,
    1.21 -  intermediate results etc.
    1.22 +  Proof commands perform transitions of Isar/VM machine configurations, which
    1.23 +  are block-structured, consisting of a stack of nodes with three main
    1.24 +  components: logical proof context, current facts, and open goals. Isar/VM
    1.25 +  transitions are typed according to the following three different modes of
    1.26 +  operation:
    1.27  
    1.28 -  \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and \<open>proof(prove)\<close>: existing facts (i.e.\ the
    1.29 -  contents of the special @{fact_ref this} register) have been just picked
    1.30 -  up in order to be used when refining the goal claimed next.
    1.31 -
    1.32 +    \<^descr> \<open>proof(prove)\<close> means that a new goal has just been stated that is now to
    1.33 +    be \<^emph>\<open>proven\<close>; the next command may refine it by some proof method, and
    1.34 +    enter a sub-proof to establish the actual result.
    1.35 +  
    1.36 +    \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the context may be
    1.37 +    augmented by \<^emph>\<open>stating\<close> additional assumptions, intermediate results etc.
    1.38 +  
    1.39 +    \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and
    1.40 +    \<open>proof(prove)\<close>: existing facts (i.e.\ the contents of the special
    1.41 +    @{fact_ref this} register) have been just picked up in order to be used
    1.42 +    when refining the goal claimed next.
    1.43  
    1.44 -  The proof mode indicator may be understood as an instruction to the
    1.45 -  writer, telling what kind of operation may be performed next.  The
    1.46 -  corresponding typings of proof commands restricts the shape of
    1.47 -  well-formed proof texts to particular command sequences.  So dynamic
    1.48 -  arrangements of commands eventually turn out as static texts of a
    1.49 -  certain structure.
    1.50 +  The proof mode indicator may be understood as an instruction to the writer,
    1.51 +  telling what kind of operation may be performed next. The corresponding
    1.52 +  typings of proof commands restricts the shape of well-formed proof texts to
    1.53 +  particular command sequences. So dynamic arrangements of commands eventually
    1.54 +  turn out as static texts of a certain structure.
    1.55  
    1.56 -  \Appref{ap:refcard} gives a simplified grammar of the (extensible)
    1.57 -  language emerging that way from the different types of proof
    1.58 -  commands.  The main ideas of the overall Isar framework are
    1.59 -  explained in \chref{ch:isar-framework}.
    1.60 +  \Appref{ap:refcard} gives a simplified grammar of the (extensible) language
    1.61 +  emerging that way from the different types of proof commands. The main ideas
    1.62 +  of the overall Isar framework are explained in \chref{ch:isar-framework}.
    1.63  \<close>
    1.64  
    1.65  
    1.66 @@ -57,9 +52,9 @@
    1.67      @@{command end}
    1.68    \<close>}
    1.69  
    1.70 -  \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without
    1.71 -  any goal statement. This allows to experiment with Isar, without producing
    1.72 -  any persistent result. The notepad is closed by @{command "end"}.
    1.73 +  \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without any
    1.74 +  goal statement. This allows to experiment with Isar, without producing any
    1.75 +  persistent result. The notepad is closed by @{command "end"}.
    1.76  \<close>
    1.77  
    1.78  
    1.79 @@ -72,32 +67,30 @@
    1.80      @{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
    1.81    \end{matharray}
    1.82  
    1.83 -  While Isar is inherently block-structured, opening and closing
    1.84 -  blocks is mostly handled rather casually, with little explicit
    1.85 -  user-intervention.  Any local goal statement automatically opens
    1.86 -  \<^emph>\<open>two\<close> internal blocks, which are closed again when concluding
    1.87 -  the sub-proof (by @{command "qed"} etc.).  Sections of different
    1.88 -  context within a sub-proof may be switched via @{command "next"},
    1.89 -  which is just a single block-close followed by block-open again.
    1.90 -  The effect of @{command "next"} is to reset the local proof context;
    1.91 +  While Isar is inherently block-structured, opening and closing blocks is
    1.92 +  mostly handled rather casually, with little explicit user-intervention. Any
    1.93 +  local goal statement automatically opens \<^emph>\<open>two\<close> internal blocks, which are
    1.94 +  closed again when concluding the sub-proof (by @{command "qed"} etc.).
    1.95 +  Sections of different context within a sub-proof may be switched via
    1.96 +  @{command "next"}, which is just a single block-close followed by block-open
    1.97 +  again. The effect of @{command "next"} is to reset the local proof context;
    1.98    there is no goal focus involved here!
    1.99  
   1.100    For slightly more advanced applications, there are explicit block
   1.101 -  parentheses as well.  These typically achieve a stronger forward
   1.102 -  style of reasoning.
   1.103 +  parentheses as well. These typically achieve a stronger forward style of
   1.104 +  reasoning.
   1.105  
   1.106 -  \<^descr> @{command "next"} switches to a fresh block within a
   1.107 -  sub-proof, resetting the local context to the initial one.
   1.108 +  \<^descr> @{command "next"} switches to a fresh block within a sub-proof, resetting
   1.109 +  the local context to the initial one.
   1.110  
   1.111 -  \<^descr> @{command "{"} and @{command "}"} explicitly open and close
   1.112 -  blocks.  Any current facts pass through ``@{command "{"}''
   1.113 -  unchanged, while ``@{command "}"}'' causes any result to be
   1.114 -  \<^emph>\<open>exported\<close> into the enclosing context.  Thus fixed variables
   1.115 -  are generalized, assumptions discharged, and local definitions
   1.116 -  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
   1.117 -  of @{command "assume"} and @{command "presume"} in this mode of
   1.118 -  forward reasoning --- in contrast to plain backward reasoning with
   1.119 -  the result exported at @{command "show"} time.
   1.120 +  \<^descr> @{command "{"} and @{command "}"} explicitly open and close blocks. Any
   1.121 +  current facts pass through ``@{command "{"}'' unchanged, while ``@{command
   1.122 +  "}"}'' causes any result to be \<^emph>\<open>exported\<close> into the enclosing context. Thus
   1.123 +  fixed variables are generalized, assumptions discharged, and local
   1.124 +  definitions unfolded (cf.\ \secref{sec:proof-context}). There is no
   1.125 +  difference of @{command "assume"} and @{command "presume"} in this mode of
   1.126 +  forward reasoning --- in contrast to plain backward reasoning with the
   1.127 +  result exported at @{command "show"} time.
   1.128  \<close>
   1.129  
   1.130  
   1.131 @@ -108,23 +101,20 @@
   1.132      @{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\
   1.133    \end{matharray}
   1.134  
   1.135 -  The @{command "oops"} command discontinues the current proof
   1.136 -  attempt, while considering the partial proof text as properly
   1.137 -  processed.  This is conceptually quite different from ``faking''
   1.138 -  actual proofs via @{command_ref "sorry"} (see
   1.139 -  \secref{sec:proof-steps}): @{command "oops"} does not observe the
   1.140 -  proof structure at all, but goes back right to the theory level.
   1.141 -  Furthermore, @{command "oops"} does not produce any result theorem
   1.142 -  --- there is no intended claim to be able to complete the proof
   1.143 -  in any way.
   1.144 +  The @{command "oops"} command discontinues the current proof attempt, while
   1.145 +  considering the partial proof text as properly processed. This is
   1.146 +  conceptually quite different from ``faking'' actual proofs via @{command_ref
   1.147 +  "sorry"} (see \secref{sec:proof-steps}): @{command "oops"} does not observe
   1.148 +  the proof structure at all, but goes back right to the theory level.
   1.149 +  Furthermore, @{command "oops"} does not produce any result theorem --- there
   1.150 +  is no intended claim to be able to complete the proof in any way.
   1.151  
   1.152    A typical application of @{command "oops"} is to explain Isar proofs
   1.153 -  \<^emph>\<open>within\<close> the system itself, in conjunction with the document
   1.154 -  preparation tools of Isabelle described in \chref{ch:document-prep}.
   1.155 -  Thus partial or even wrong proof attempts can be discussed in a
   1.156 -  logically sound manner.  Note that the Isabelle {\LaTeX} macros can
   1.157 -  be easily adapted to print something like ``\<open>\<dots>\<close>'' instead of
   1.158 -  the keyword ``@{command "oops"}''.
   1.159 +  \<^emph>\<open>within\<close> the system itself, in conjunction with the document preparation
   1.160 +  tools of Isabelle described in \chref{ch:document-prep}. Thus partial or
   1.161 +  even wrong proof attempts can be discussed in a logically sound manner. Note
   1.162 +  that the Isabelle {\LaTeX} macros can be easily adapted to print something
   1.163 +  like ``\<open>\<dots>\<close>'' instead of the keyword ``@{command "oops"}''.
   1.164  \<close>
   1.165  
   1.166  
   1.167 @@ -140,34 +130,31 @@
   1.168      @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   1.169    \end{matharray}
   1.170  
   1.171 -  The logical proof context consists of fixed variables and
   1.172 -  assumptions.  The former closely correspond to Skolem constants, or
   1.173 -  meta-level universal quantification as provided by the Isabelle/Pure
   1.174 -  logical framework.  Introducing some \<^emph>\<open>arbitrary, but fixed\<close>
   1.175 -  variable via ``@{command "fix"}~\<open>x\<close>'' results in a local value
   1.176 -  that may be used in the subsequent proof as any other variable or
   1.177 -  constant.  Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close> exported from
   1.178 -  the context will be universally closed wrt.\ \<open>x\<close> at the
   1.179 -  outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal
   1.180 -  form using Isabelle's meta-variables).
   1.181 +  The logical proof context consists of fixed variables and assumptions. The
   1.182 +  former closely correspond to Skolem constants, or meta-level universal
   1.183 +  quantification as provided by the Isabelle/Pure logical framework.
   1.184 +  Introducing some \<^emph>\<open>arbitrary, but fixed\<close> variable via ``@{command
   1.185 +  "fix"}~\<open>x\<close>'' results in a local value that may be used in the subsequent
   1.186 +  proof as any other variable or constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close>
   1.187 +  exported from the context will be universally closed wrt.\ \<open>x\<close> at the
   1.188 +  outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal form using
   1.189 +  Isabelle's meta-variables).
   1.190  
   1.191 -  Similarly, introducing some assumption \<open>\<chi>\<close> has two effects.
   1.192 -  On the one hand, a local theorem is created that may be used as a
   1.193 -  fact in subsequent proof steps.  On the other hand, any result
   1.194 -  \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context becomes conditional wrt.\
   1.195 -  the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>.  Thus, solving an enclosing goal
   1.196 -  using such a result would basically introduce a new subgoal stemming
   1.197 -  from the assumption.  How this situation is handled depends on the
   1.198 -  version of assumption command used: while @{command "assume"}
   1.199 -  insists on solving the subgoal by unification with some premise of
   1.200 -  the goal, @{command "presume"} leaves the subgoal unchanged in order
   1.201 -  to be proved later by the user.
   1.202 +  Similarly, introducing some assumption \<open>\<chi>\<close> has two effects. On the one hand,
   1.203 +  a local theorem is created that may be used as a fact in subsequent proof
   1.204 +  steps. On the other hand, any result \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context
   1.205 +  becomes conditional wrt.\ the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an
   1.206 +  enclosing goal using such a result would basically introduce a new subgoal
   1.207 +  stemming from the assumption. How this situation is handled depends on the
   1.208 +  version of assumption command used: while @{command "assume"} insists on
   1.209 +  solving the subgoal by unification with some premise of the goal, @{command
   1.210 +  "presume"} leaves the subgoal unchanged in order to be proved later by the
   1.211 +  user.
   1.212  
   1.213 -  Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv>
   1.214 -  t\<close>'', are achieved by combining ``@{command "fix"}~\<open>x\<close>'' with
   1.215 -  another version of assumption that causes any hypothetical equation
   1.216 -  \<open>x \<equiv> t\<close> to be eliminated by the reflexivity rule.  Thus,
   1.217 -  exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
   1.218 +  Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv> t\<close>'', are achieved
   1.219 +  by combining ``@{command "fix"}~\<open>x\<close>'' with another version of assumption
   1.220 +  that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the
   1.221 +  reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
   1.222    \<phi>[t]\<close>.
   1.223  
   1.224    @{rail \<open>
   1.225 @@ -181,27 +168,27 @@
   1.226        @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
   1.227    \<close>}
   1.228  
   1.229 -  \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary, but fixed\<close>.
   1.230 +  \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,
   1.231 +  but fixed\<close>.
   1.232  
   1.233 -  \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command
   1.234 -  "presume"}~\<open>a: \<phi>\<close> introduce a local fact \<open>\<phi> \<turnstile> \<phi>\<close> by
   1.235 -  assumption.  Subsequent results applied to an enclosing goal (e.g.\
   1.236 -  by @{command_ref "show"}) are handled as follows: @{command
   1.237 -  "assume"} expects to be able to unify with existing premises in the
   1.238 -  goal, while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.
   1.239 +  \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command "presume"}~\<open>a: \<phi>\<close> introduce a
   1.240 +  local fact \<open>\<phi> \<turnstile> \<phi>\<close> by assumption. Subsequent results applied to an enclosing
   1.241 +  goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command
   1.242 +  "assume"} expects to be able to unify with existing premises in the goal,
   1.243 +  while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.
   1.244  
   1.245 -  Several lists of assumptions may be given (separated by
   1.246 -  @{keyword_ref "and"}; the resulting list of current facts consists
   1.247 -  of all of these concatenated.
   1.248 +  Several lists of assumptions may be given (separated by @{keyword_ref
   1.249 +  "and"}; the resulting list of current facts consists of all of these
   1.250 +  concatenated.
   1.251  
   1.252 -  \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local
   1.253 -  (non-polymorphic) definition.  In results exported from the context,
   1.254 -  \<open>x\<close> is replaced by \<open>t\<close>.  Basically, ``@{command
   1.255 -  "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>x \<equiv> t\<close>'', with the resulting
   1.256 -  hypothetical equation solved by reflexivity.
   1.257 +  \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local (non-polymorphic) definition.
   1.258 +  In results exported from the context, \<open>x\<close> is replaced by \<open>t\<close>. Basically,
   1.259 +  ``@{command "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command
   1.260 +  "assume"}~\<open>x \<equiv> t\<close>'', with the resulting hypothetical equation solved by
   1.261 +  reflexivity.
   1.262  
   1.263 -  The default name for the definitional equation is \<open>x_def\<close>.
   1.264 -  Several simultaneous definitions may be given at the same time.
   1.265 +  The default name for the definitional equation is \<open>x_def\<close>. Several
   1.266 +  simultaneous definitions may be given at the same time.
   1.267  \<close>
   1.268  
   1.269  
   1.270 @@ -213,31 +200,28 @@
   1.271      @{keyword_def "is"} & : & syntax \\
   1.272    \end{matharray}
   1.273  
   1.274 -  Abbreviations may be either bound by explicit @{command
   1.275 -  "let"}~\<open>p \<equiv> t\<close> statements, or by annotating assumptions or
   1.276 -  goal statements with a list of patterns ``\<open>(\<IS> p\<^sub>1 \<dots>
   1.277 -  p\<^sub>n)\<close>''.  In both cases, higher-order matching is invoked to
   1.278 -  bind extra-logical term variables, which may be either named
   1.279 -  schematic variables of the form \<open>?x\<close>, or nameless dummies
   1.280 -  ``@{variable _}'' (underscore). Note that in the @{command "let"}
   1.281 -  form the patterns occur on the left-hand side, while the @{keyword
   1.282 -  "is"} patterns are in postfix position.
   1.283 +  Abbreviations may be either bound by explicit @{command "let"}~\<open>p \<equiv> t\<close>
   1.284 +  statements, or by annotating assumptions or goal statements with a list of
   1.285 +  patterns ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is
   1.286 +  invoked to bind extra-logical term variables, which may be either named
   1.287 +  schematic variables of the form \<open>?x\<close>, or nameless dummies ``@{variable _}''
   1.288 +  (underscore). Note that in the @{command "let"} form the patterns occur on
   1.289 +  the left-hand side, while the @{keyword "is"} patterns are in postfix
   1.290 +  position.
   1.291  
   1.292 -  Polymorphism of term bindings is handled in Hindley-Milner style,
   1.293 -  similar to ML.  Type variables referring to local assumptions or
   1.294 -  open goal statements are \<^emph>\<open>fixed\<close>, while those of finished
   1.295 -  results or bound by @{command "let"} may occur in \<^emph>\<open>arbitrary\<close>
   1.296 -  instances later.  Even though actual polymorphism should be rarely
   1.297 -  used in practice, this mechanism is essential to achieve proper
   1.298 -  incremental type-inference, as the user proceeds to build up the
   1.299 -  Isar proof text from left to right.
   1.300 +  Polymorphism of term bindings is handled in Hindley-Milner style, similar to
   1.301 +  ML. Type variables referring to local assumptions or open goal statements
   1.302 +  are \<^emph>\<open>fixed\<close>, while those of finished results or bound by @{command "let"}
   1.303 +  may occur in \<^emph>\<open>arbitrary\<close> instances later. Even though actual polymorphism
   1.304 +  should be rarely used in practice, this mechanism is essential to achieve
   1.305 +  proper incremental type-inference, as the user proceeds to build up the Isar
   1.306 +  proof text from left to right.
   1.307  
   1.308    \<^medskip>
   1.309 -  Term abbreviations are quite different from local
   1.310 -  definitions as introduced via @{command "def"} (see
   1.311 -  \secref{sec:proof-context}).  The latter are visible within the
   1.312 -  logic as actual equations, while abbreviations disappear during the
   1.313 -  input process just after type checking.  Also note that @{command
   1.314 +  Term abbreviations are quite different from local definitions as introduced
   1.315 +  via @{command "def"} (see \secref{sec:proof-context}). The latter are
   1.316 +  visible within the logic as actual equations, while abbreviations disappear
   1.317 +  during the input process just after type checking. Also note that @{command
   1.318    "def"} does not support polymorphism.
   1.319  
   1.320    @{rail \<open>
   1.321 @@ -247,26 +231,24 @@
   1.322    The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
   1.323    @{syntax prop_pat} (see \secref{sec:term-decls}).
   1.324  
   1.325 -  \<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any
   1.326 -  text variables in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous
   1.327 -  higher-order matching against terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>.
   1.328 +    \<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables
   1.329 +    in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against
   1.330 +    terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>.
   1.331  
   1.332 -  \<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but
   1.333 -  matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> against the preceding statement.  Also
   1.334 -  note that @{keyword "is"} is not a separate command, but part of
   1.335 -  others (such as @{command "assume"}, @{command "have"} etc.).
   1.336 -
   1.337 +    \<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>,
   1.338 +    p\<^sub>n\<close> against the preceding statement. Also note that @{keyword "is"} is
   1.339 +    not a separate command, but part of others (such as @{command "assume"},
   1.340 +    @{command "have"} etc.).
   1.341  
   1.342 -  Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations}
   1.343 -  for goals and facts are available as well.  For any open goal,
   1.344 -  @{variable_ref thesis} refers to its object-level statement,
   1.345 -  abstracted over any meta-level parameters (if present).  Likewise,
   1.346 -  @{variable_ref this} is bound for fact statements resulting from
   1.347 -  assumptions or finished goals.  In case @{variable this} refers to
   1.348 -  an object-logic statement that is an application \<open>f t\<close>, then
   1.349 -  \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}''
   1.350 -  (three dots).  The canonical application of this convenience are
   1.351 -  calculational proofs (see \secref{sec:calculation}).
   1.352 +  Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} for goals and
   1.353 +  facts are available as well. For any open goal, @{variable_ref thesis}
   1.354 +  refers to its object-level statement, abstracted over any meta-level
   1.355 +  parameters (if present). Likewise, @{variable_ref this} is bound for fact
   1.356 +  statements resulting from assumptions or finished goals. In case @{variable
   1.357 +  this} refers to an object-logic statement that is an application \<open>f t\<close>, then
   1.358 +  \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}'' (three dots).
   1.359 +  The canonical application of this convenience are calculational proofs (see
   1.360 +  \secref{sec:calculation}).
   1.361  \<close>
   1.362  
   1.363  
   1.364 @@ -282,16 +264,15 @@
   1.365      @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
   1.366    \end{matharray}
   1.367  
   1.368 -  New facts are established either by assumption or proof of local
   1.369 -  statements.  Any fact will usually be involved in further proofs,
   1.370 -  either as explicit arguments of proof methods, or when forward
   1.371 -  chaining towards the next goal via @{command "then"} (and variants);
   1.372 -  @{command "from"} and @{command "with"} are composite forms
   1.373 -  involving @{command "note"}.  The @{command "using"} elements
   1.374 -  augments the collection of used facts \<^emph>\<open>after\<close> a goal has been
   1.375 -  stated.  Note that the special theorem name @{fact_ref this} refers
   1.376 -  to the most recently established facts, but only \<^emph>\<open>before\<close>
   1.377 -  issuing a follow-up claim.
   1.378 +  New facts are established either by assumption or proof of local statements.
   1.379 +  Any fact will usually be involved in further proofs, either as explicit
   1.380 +  arguments of proof methods, or when forward chaining towards the next goal
   1.381 +  via @{command "then"} (and variants); @{command "from"} and @{command
   1.382 +  "with"} are composite forms involving @{command "note"}. The @{command
   1.383 +  "using"} elements augments the collection of used facts \<^emph>\<open>after\<close> a goal has
   1.384 +  been stated. Note that the special theorem name @{fact_ref this} refers to
   1.385 +  the most recently established facts, but only \<^emph>\<open>before\<close> issuing a follow-up
   1.386 +  claim.
   1.387  
   1.388    @{rail \<open>
   1.389      @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   1.390 @@ -300,55 +281,51 @@
   1.391        (@{syntax thmrefs} + @'and')
   1.392    \<close>}
   1.393  
   1.394 -  \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts
   1.395 -  \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>, binding the result as \<open>a\<close>.  Note that
   1.396 -  attributes may be involved as well, both on the left and right hand
   1.397 -  sides.
   1.398 +  \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
   1.399 +  binding the result as \<open>a\<close>. Note that attributes may be involved as well,
   1.400 +  both on the left and right hand sides.
   1.401  
   1.402 -  \<^descr> @{command "then"} indicates forward chaining by the current
   1.403 -  facts in order to establish the goal to be claimed next.  The
   1.404 -  initial proof method invoked to refine that will be offered the
   1.405 -  facts to do ``anything appropriate'' (see also
   1.406 -  \secref{sec:proof-steps}).  For example, method @{method (Pure) rule}
   1.407 -  (see \secref{sec:pure-meth-att}) would typically do an elimination
   1.408 -  rather than an introduction.  Automatic methods usually insert the
   1.409 -  facts into the goal state before operation.  This provides a simple
   1.410 -  scheme to control relevance of facts in automated proof search.
   1.411 +  \<^descr> @{command "then"} indicates forward chaining by the current facts in order
   1.412 +  to establish the goal to be claimed next. The initial proof method invoked
   1.413 +  to refine that will be offered the facts to do ``anything appropriate'' (see
   1.414 +  also \secref{sec:proof-steps}). For example, method @{method (Pure) rule}
   1.415 +  (see \secref{sec:pure-meth-att}) would typically do an elimination rather
   1.416 +  than an introduction. Automatic methods usually insert the facts into the
   1.417 +  goal state before operation. This provides a simple scheme to control
   1.418 +  relevance of facts in automated proof search.
   1.419  
   1.420 -  \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command
   1.421 -  "note"}~\<open>b\<close>~@{command "then"}''; thus @{command "then"} is
   1.422 -  equivalent to ``@{command "from"}~\<open>this\<close>''.
   1.423 +  \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command "note"}~\<open>b\<close>~@{command
   1.424 +  "then"}''; thus @{command "then"} is equivalent to ``@{command
   1.425 +  "from"}~\<open>this\<close>''.
   1.426  
   1.427 -  \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command
   1.428 -  "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n \<AND> this\<close>''; thus the forward chaining
   1.429 -  is from earlier facts together with the current ones.
   1.430 +  \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n
   1.431 +  \<AND> this\<close>''; thus the forward chaining is from earlier facts together
   1.432 +  with the current ones.
   1.433  
   1.434 -  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being
   1.435 -  currently indicated for use by a subsequent refinement step (such as
   1.436 -  @{command_ref "apply"} or @{command_ref "proof"}).
   1.437 +  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being currently
   1.438 +  indicated for use by a subsequent refinement step (such as @{command_ref
   1.439 +  "apply"} or @{command_ref "proof"}).
   1.440  
   1.441 -  \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally
   1.442 -  similar to @{command "using"}, but unfolds definitional equations
   1.443 -  \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the goal state and facts.
   1.444 +  \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
   1.445 +  "using"}, but unfolds definitional equations \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the
   1.446 +  goal state and facts.
   1.447  
   1.448  
   1.449 -  Forward chaining with an empty list of theorems is the same as not
   1.450 -  chaining at all.  Thus ``@{command "from"}~\<open>nothing\<close>'' has no
   1.451 -  effect apart from entering \<open>prove(chain)\<close> mode, since
   1.452 -  @{fact_ref nothing} is bound to the empty list of theorems.
   1.453 +  Forward chaining with an empty list of theorems is the same as not chaining
   1.454 +  at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no effect apart from
   1.455 +  entering \<open>prove(chain)\<close> mode, since @{fact_ref nothing} is bound to the
   1.456 +  empty list of theorems.
   1.457  
   1.458    Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
   1.459 -  facts to be given in their proper order, corresponding to a prefix
   1.460 -  of the premises of the rule involved.  Note that positions may be
   1.461 -  easily skipped using something like @{command "from"}~\<open>_
   1.462 -  \<AND> a \<AND> b\<close>, for example.  This involves the trivial rule
   1.463 -  \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in Isabelle/Pure as
   1.464 -  ``@{fact_ref "_"}'' (underscore).
   1.465 +  facts to be given in their proper order, corresponding to a prefix of the
   1.466 +  premises of the rule involved. Note that positions may be easily skipped
   1.467 +  using something like @{command "from"}~\<open>_ \<AND> a \<AND> b\<close>, for example.
   1.468 +  This involves the trivial rule \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in
   1.469 +  Isabelle/Pure as ``@{fact_ref "_"}'' (underscore).
   1.470  
   1.471 -  Automated methods (such as @{method simp} or @{method auto}) just
   1.472 -  insert any given facts before their usual operation.  Depending on
   1.473 -  the kind of procedure involved, the order of facts is less
   1.474 -  significant here.
   1.475 +  Automated methods (such as @{method simp} or @{method auto}) just insert any
   1.476 +  given facts before their usual operation. Depending on the kind of procedure
   1.477 +  involved, the order of facts is less significant here.
   1.478  \<close>
   1.479  
   1.480  
   1.481 @@ -368,34 +345,31 @@
   1.482      @{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   1.483    \end{matharray}
   1.484  
   1.485 -  From a theory context, proof mode is entered by an initial goal command
   1.486 -  such as @{command "lemma"}. Within a proof context, new claims may be
   1.487 -  introduced locally; there are variants to interact with the overall proof
   1.488 -  structure specifically, such as @{command have} or @{command show}.
   1.489 +  From a theory context, proof mode is entered by an initial goal command such
   1.490 +  as @{command "lemma"}. Within a proof context, new claims may be introduced
   1.491 +  locally; there are variants to interact with the overall proof structure
   1.492 +  specifically, such as @{command have} or @{command show}.
   1.493  
   1.494 -  Goals may consist of multiple statements, resulting in a list of
   1.495 -  facts eventually.  A pending multi-goal is internally represented as
   1.496 -  a meta-level conjunction (\<open>&&&\<close>), which is usually
   1.497 -  split into the corresponding number of sub-goals prior to an initial
   1.498 -  method application, via @{command_ref "proof"}
   1.499 +  Goals may consist of multiple statements, resulting in a list of facts
   1.500 +  eventually. A pending multi-goal is internally represented as a meta-level
   1.501 +  conjunction (\<open>&&&\<close>), which is usually split into the corresponding number of
   1.502 +  sub-goals prior to an initial method application, via @{command_ref "proof"}
   1.503    (\secref{sec:proof-steps}) or @{command_ref "apply"}
   1.504 -  (\secref{sec:tactic-commands}).  The @{method_ref induct} method
   1.505 -  covered in \secref{sec:cases-induct} acts on multiple claims
   1.506 -  simultaneously.
   1.507 +  (\secref{sec:tactic-commands}). The @{method_ref induct} method covered in
   1.508 +  \secref{sec:cases-induct} acts on multiple claims simultaneously.
   1.509  
   1.510 -  Claims at the theory level may be either in short or long form.  A
   1.511 -  short goal merely consists of several simultaneous propositions
   1.512 -  (often just one).  A long goal includes an explicit context
   1.513 -  specification for the subsequent conclusion, involving local
   1.514 -  parameters and assumptions.  Here the role of each part of the
   1.515 -  statement is explicitly marked by separate keywords (see also
   1.516 -  \secref{sec:locale}); the local assumptions being introduced here
   1.517 -  are available as @{fact_ref assms} in the proof.  Moreover, there
   1.518 -  are two kinds of conclusions: @{element_def "shows"} states several
   1.519 -  simultaneous propositions (essentially a big conjunction), while
   1.520 -  @{element_def "obtains"} claims several simultaneous simultaneous
   1.521 -  contexts of (essentially a big disjunction of eliminated parameters
   1.522 -  and assumptions, cf.\ \secref{sec:obtain}).
   1.523 +  Claims at the theory level may be either in short or long form. A short goal
   1.524 +  merely consists of several simultaneous propositions (often just one). A
   1.525 +  long goal includes an explicit context specification for the subsequent
   1.526 +  conclusion, involving local parameters and assumptions. Here the role of
   1.527 +  each part of the statement is explicitly marked by separate keywords (see
   1.528 +  also \secref{sec:locale}); the local assumptions being introduced here are
   1.529 +  available as @{fact_ref assms} in the proof. Moreover, there are two kinds
   1.530 +  of conclusions: @{element_def "shows"} states several simultaneous
   1.531 +  propositions (essentially a big conjunction), while @{element_def "obtains"}
   1.532 +  claims several simultaneous simultaneous contexts of (essentially a big
   1.533 +  disjunction of eliminated parameters and assumptions, cf.\
   1.534 +  \secref{sec:obtain}).
   1.535  
   1.536    @{rail \<open>
   1.537      (@@{command lemma} | @@{command theorem} | @@{command corollary} |
   1.538 @@ -422,70 +396,64 @@
   1.539        (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   1.540    \<close>}
   1.541  
   1.542 -  \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with
   1.543 -  \<open>\<phi>\<close> as main goal, eventually resulting in some fact \<open>\<turnstile>
   1.544 -  \<phi>\<close> to be put back into the target context.  An additional @{syntax
   1.545 -  context} specification may build up an initial proof context for the
   1.546 -  subsequent claim; this includes local definitions and syntax as
   1.547 -  well, see also @{syntax "includes"} in \secref{sec:bundle} and
   1.548 -  @{syntax context_elem} in \secref{sec:locale}.
   1.549 +  \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,
   1.550 +  eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target
   1.551 +  context. An additional @{syntax context} specification may build up an
   1.552 +  initial proof context for the subsequent claim; this includes local
   1.553 +  definitions and syntax as well, see also @{syntax "includes"} in
   1.554 +  \secref{sec:bundle} and @{syntax context_elem} in \secref{sec:locale}.
   1.555  
   1.556 -  \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command
   1.557 -  "proposition"} are the same as @{command "lemma"}. The different command
   1.558 -  names merely serve as a formal comment in the theory source.
   1.559 +  \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}
   1.560 +  are the same as @{command "lemma"}. The different command names merely serve
   1.561 +  as a formal comment in the theory source.
   1.562  
   1.563 -  \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"},
   1.564 -  but allows the statement to contain unbound schematic variables.
   1.565 +  \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"}, but allows
   1.566 +  the statement to contain unbound schematic variables.
   1.567  
   1.568 -  Under normal circumstances, an Isar proof text needs to specify
   1.569 -  claims explicitly.  Schematic goals are more like goals in Prolog,
   1.570 -  where certain results are synthesized in the course of reasoning.
   1.571 -  With schematic statements, the inherent compositionality of Isar
   1.572 -  proofs is lost, which also impacts performance, because proof
   1.573 -  checking is forced into sequential mode.
   1.574 +  Under normal circumstances, an Isar proof text needs to specify claims
   1.575 +  explicitly. Schematic goals are more like goals in Prolog, where certain
   1.576 +  results are synthesized in the course of reasoning. With schematic
   1.577 +  statements, the inherent compositionality of Isar proofs is lost, which also
   1.578 +  impacts performance, because proof checking is forced into sequential mode.
   1.579  
   1.580 -  \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal,
   1.581 -  eventually resulting in a fact within the current logical context.
   1.582 -  This operation is completely independent of any pending sub-goals of
   1.583 -  an enclosing goal statements, so @{command "have"} may be freely
   1.584 -  used for experimental exploration of potential results within a
   1.585 -  proof body.
   1.586 +  \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal, eventually resulting in a
   1.587 +  fact within the current logical context. This operation is completely
   1.588 +  independent of any pending sub-goals of an enclosing goal statements, so
   1.589 +  @{command "have"} may be freely used for experimental exploration of
   1.590 +  potential results within a proof body.
   1.591  
   1.592 -  \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command
   1.593 -  "have"}~\<open>a: \<phi>\<close> plus a second stage to refine some pending
   1.594 -  sub-goal for each one of the finished result, after having been
   1.595 -  exported into the corresponding context (at the head of the
   1.596 -  sub-proof of this @{command "show"} command).
   1.597 +  \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command "have"}~\<open>a: \<phi>\<close> plus a second
   1.598 +  stage to refine some pending sub-goal for each one of the finished result,
   1.599 +  after having been exported into the corresponding context (at the head of
   1.600 +  the sub-proof of this @{command "show"} command).
   1.601  
   1.602 -  To accommodate interactive debugging, resulting rules are printed
   1.603 -  before being applied internally.  Even more, interactive execution
   1.604 -  of @{command "show"} predicts potential failure and displays the
   1.605 -  resulting error as a warning beforehand.  Watch out for the
   1.606 -  following message:
   1.607 +  To accommodate interactive debugging, resulting rules are printed before
   1.608 +  being applied internally. Even more, interactive execution of @{command
   1.609 +  "show"} predicts potential failure and displays the resulting error as a
   1.610 +  warning beforehand. Watch out for the following message:
   1.611    @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
   1.612  
   1.613 -  \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command
   1.614 -  "have"}'', i.e.\ claims a local goal to be proven by forward
   1.615 -  chaining the current facts.  Note that @{command "hence"} is also
   1.616 -  equivalent to ``@{command "from"}~\<open>this\<close>~@{command "have"}''.
   1.617 +  \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command "have"}'',
   1.618 +  i.e.\ claims a local goal to be proven by forward chaining the current
   1.619 +  facts. Note that @{command "hence"} is also equivalent to ``@{command
   1.620 +  "from"}~\<open>this\<close>~@{command "have"}''.
   1.621  
   1.622 -  \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command
   1.623 -  "show"}''.  Note that @{command "thus"} is also equivalent to
   1.624 -  ``@{command "from"}~\<open>this\<close>~@{command "show"}''.
   1.625 +  \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command "show"}''.
   1.626 +  Note that @{command "thus"} is also equivalent to ``@{command
   1.627 +  "from"}~\<open>this\<close>~@{command "show"}''.
   1.628  
   1.629 -  \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the
   1.630 -  current theory or proof context in long statement form, according to
   1.631 -  the syntax for @{command "lemma"} given above.
   1.632 +  \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the current theory or
   1.633 +  proof context in long statement form, according to the syntax for @{command
   1.634 +  "lemma"} given above.
   1.635  
   1.636  
   1.637 -  Any goal statement causes some term abbreviations (such as
   1.638 -  @{variable_ref "?thesis"}) to be bound automatically, see also
   1.639 -  \secref{sec:term-abbrev}.
   1.640 +  Any goal statement causes some term abbreviations (such as @{variable_ref
   1.641 +  "?thesis"}) to be bound automatically, see also \secref{sec:term-abbrev}.
   1.642  
   1.643    Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
   1.644    "when"} define the special fact @{fact_ref that} to refer to these
   1.645 -  assumptions in the proof body. The user may provide separate names
   1.646 -  according to the syntax of the statement.
   1.647 +  assumptions in the proof body. The user may provide separate names according
   1.648 +  to the syntax of the statement.
   1.649  \<close>
   1.650  
   1.651  
   1.652 @@ -503,38 +471,34 @@
   1.653      @{attribute symmetric} & : & \<open>attribute\<close> \\
   1.654    \end{matharray}
   1.655  
   1.656 -  Calculational proof is forward reasoning with implicit application
   1.657 -  of transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>,
   1.658 -  \<open><\<close>).  Isabelle/Isar maintains an auxiliary fact register
   1.659 -  @{fact_ref calculation} for accumulating results obtained by
   1.660 -  transitivity composed with the current result.  Command @{command
   1.661 -  "also"} updates @{fact calculation} involving @{fact this}, while
   1.662 -  @{command "finally"} exhibits the final @{fact calculation} by
   1.663 -  forward chaining towards the next goal statement.  Both commands
   1.664 -  require valid current facts, i.e.\ may occur only after commands
   1.665 -  that produce theorems such as @{command "assume"}, @{command
   1.666 -  "note"}, or some finished proof of @{command "have"}, @{command
   1.667 -  "show"} etc.  The @{command "moreover"} and @{command "ultimately"}
   1.668 -  commands are similar to @{command "also"} and @{command "finally"},
   1.669 -  but only collect further results in @{fact calculation} without
   1.670 -  applying any rules yet.
   1.671 +  Calculational proof is forward reasoning with implicit application of
   1.672 +  transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>, \<open><\<close>). Isabelle/Isar maintains an
   1.673 +  auxiliary fact register @{fact_ref calculation} for accumulating results
   1.674 +  obtained by transitivity composed with the current result. Command @{command
   1.675 +  "also"} updates @{fact calculation} involving @{fact this}, while @{command
   1.676 +  "finally"} exhibits the final @{fact calculation} by forward chaining
   1.677 +  towards the next goal statement. Both commands require valid current facts,
   1.678 +  i.e.\ may occur only after commands that produce theorems such as @{command
   1.679 +  "assume"}, @{command "note"}, or some finished proof of @{command "have"},
   1.680 +  @{command "show"} etc. The @{command "moreover"} and @{command "ultimately"}
   1.681 +  commands are similar to @{command "also"} and @{command "finally"}, but only
   1.682 +  collect further results in @{fact calculation} without applying any rules
   1.683 +  yet.
   1.684  
   1.685 -  Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has
   1.686 -  its canonical application with calculational proofs.  It refers to
   1.687 -  the argument of the preceding statement. (The argument of a curried
   1.688 -  infix expression happens to be its right-hand side.)
   1.689 +  Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has its canonical
   1.690 +  application with calculational proofs. It refers to the argument of the
   1.691 +  preceding statement. (The argument of a curried infix expression happens to
   1.692 +  be its right-hand side.)
   1.693  
   1.694 -  Isabelle/Isar calculations are implicitly subject to block structure
   1.695 -  in the sense that new threads of calculational reasoning are
   1.696 -  commenced for any new block (as opened by a local goal, for
   1.697 -  example).  This means that, apart from being able to nest
   1.698 -  calculations, there is no separate \<^emph>\<open>begin-calculation\<close> command
   1.699 -  required.
   1.700 +  Isabelle/Isar calculations are implicitly subject to block structure in the
   1.701 +  sense that new threads of calculational reasoning are commenced for any new
   1.702 +  block (as opened by a local goal, for example). This means that, apart from
   1.703 +  being able to nest calculations, there is no separate \<^emph>\<open>begin-calculation\<close>
   1.704 +  command required.
   1.705  
   1.706    \<^medskip>
   1.707 -  The Isar calculation proof commands may be defined as
   1.708 -  follows:\<^footnote>\<open>We suppress internal bookkeeping such as proper
   1.709 -  handling of block-structure.\<close>
   1.710 +  The Isar calculation proof commands may be defined as follows:\<^footnote>\<open>We suppress
   1.711 +  internal bookkeeping such as proper handling of block-structure.\<close>
   1.712  
   1.713    \begin{matharray}{rcl}
   1.714      @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
   1.715 @@ -550,49 +514,46 @@
   1.716      @@{attribute trans} (() | 'add' | 'del')
   1.717    \<close>}
   1.718  
   1.719 -  \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary
   1.720 -  @{fact calculation} register as follows.  The first occurrence of
   1.721 -  @{command "also"} in some calculational thread initializes @{fact
   1.722 -  calculation} by @{fact this}. Any subsequent @{command "also"} on
   1.723 -  the same level of block-structure updates @{fact calculation} by
   1.724 -  some transitivity rule applied to @{fact calculation} and @{fact
   1.725 -  this} (in that order).  Transitivity rules are picked from the
   1.726 -  current context, unless alternative rules are given as explicit
   1.727 +  \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary @{fact
   1.728 +  calculation} register as follows. The first occurrence of @{command "also"}
   1.729 +  in some calculational thread initializes @{fact calculation} by @{fact
   1.730 +  this}. Any subsequent @{command "also"} on the same level of block-structure
   1.731 +  updates @{fact calculation} by some transitivity rule applied to @{fact
   1.732 +  calculation} and @{fact this} (in that order). Transitivity rules are picked
   1.733 +  from the current context, unless alternative rules are given as explicit
   1.734    arguments.
   1.735  
   1.736 -  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact
   1.737 -  calculation} in the same way as @{command "also"}, and concludes the
   1.738 -  current calculational thread.  The final result is exhibited as fact
   1.739 -  for forward chaining towards the next goal. Basically, @{command
   1.740 -  "finally"} just abbreviates @{command "also"}~@{command
   1.741 -  "from"}~@{fact calculation}.  Typical idioms for concluding
   1.742 +  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact calculation} in the
   1.743 +  same way as @{command "also"}, and concludes the current calculational
   1.744 +  thread. The final result is exhibited as fact for forward chaining towards
   1.745 +  the next goal. Basically, @{command "finally"} just abbreviates @{command
   1.746 +  "also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding
   1.747    calculational proofs are ``@{command "finally"}~@{command
   1.748 -  "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command
   1.749 -  "finally"}~@{command "have"}~\<open>\<phi>\<close>~@{command "."}''.
   1.750 +  "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command "finally"}~@{command
   1.751 +  "have"}~\<open>\<phi>\<close>~@{command "."}''.
   1.752  
   1.753 -  \<^descr> @{command "moreover"} and @{command "ultimately"} are
   1.754 -  analogous to @{command "also"} and @{command "finally"}, but collect
   1.755 -  results only, without applying rules.
   1.756 +  \<^descr> @{command "moreover"} and @{command "ultimately"} are analogous to
   1.757 +  @{command "also"} and @{command "finally"}, but collect results only,
   1.758 +  without applying rules.
   1.759  
   1.760 -  \<^descr> @{command "print_trans_rules"} prints the list of transitivity
   1.761 -  rules (for calculational commands @{command "also"} and @{command
   1.762 -  "finally"}) and symmetry rules (for the @{attribute symmetric}
   1.763 -  operation and single step elimination patters) of the current
   1.764 -  context.
   1.765 +  \<^descr> @{command "print_trans_rules"} prints the list of transitivity rules (for
   1.766 +  calculational commands @{command "also"} and @{command "finally"}) and
   1.767 +  symmetry rules (for the @{attribute symmetric} operation and single step
   1.768 +  elimination patters) of the current context.
   1.769  
   1.770    \<^descr> @{attribute trans} declares theorems as transitivity rules.
   1.771  
   1.772 -  \<^descr> @{attribute sym} declares symmetry rules, as well as
   1.773 -  @{attribute "Pure.elim"}\<open>?\<close> rules.
   1.774 +  \<^descr> @{attribute sym} declares symmetry rules, as well as @{attribute
   1.775 +  "Pure.elim"}\<open>?\<close> rules.
   1.776  
   1.777 -  \<^descr> @{attribute symmetric} resolves a theorem with some rule
   1.778 -  declared as @{attribute sym} in the current context.  For example,
   1.779 -  ``@{command "assume"}~\<open>[symmetric]: x = y\<close>'' produces a
   1.780 -  swapped fact derived from that assumption.
   1.781 +  \<^descr> @{attribute symmetric} resolves a theorem with some rule declared as
   1.782 +  @{attribute sym} in the current context. For example, ``@{command
   1.783 +  "assume"}~\<open>[symmetric]: x = y\<close>'' produces a swapped fact derived from that
   1.784 +  assumption.
   1.785  
   1.786 -  In structured proof texts it is often more appropriate to use an
   1.787 -  explicit single-step elimination proof, such as ``@{command
   1.788 -  "assume"}~\<open>x = y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.
   1.789 +  In structured proof texts it is often more appropriate to use an explicit
   1.790 +  single-step elimination proof, such as ``@{command "assume"}~\<open>x =
   1.791 +  y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.
   1.792  \<close>
   1.793  
   1.794  
   1.795 @@ -600,16 +561,16 @@
   1.796  
   1.797  subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>
   1.798  
   1.799 -text \<open>Proof methods are either basic ones, or expressions composed of
   1.800 -  methods via ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural
   1.801 -  composition), ``\<^verbatim>\<open>|\<close>'' (alternative
   1.802 -  choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
   1.803 -  once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first
   1.804 -  \<open>n\<close> subgoals). In practice, proof methods are usually just a comma
   1.805 -  separated list of @{syntax nameref}~@{syntax args} specifications. Note
   1.806 -  that parentheses may be dropped for single method specifications (with no
   1.807 -  arguments). The syntactic precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close>
   1.808 -  \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low to high).
   1.809 +text \<open>
   1.810 +  Proof methods are either basic ones, or expressions composed of methods via
   1.811 +  ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural composition),
   1.812 +  ``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
   1.813 +  once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,
   1.814 +  proof methods are usually just a comma separated list of @{syntax
   1.815 +  nameref}~@{syntax args} specifications. Note that parentheses may be dropped
   1.816 +  for single method specifications (with no arguments). The syntactic
   1.817 +  precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low
   1.818 +  to high).
   1.819  
   1.820    @{rail \<open>
   1.821      @{syntax_def method}:
   1.822 @@ -618,35 +579,34 @@
   1.823      methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
   1.824    \<close>}
   1.825  
   1.826 -  Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but
   1.827 -  refer to the first subgoal or to all subgoals uniformly. Nonetheless,
   1.828 -  the subsequent mechanisms allow to imitate the effect of subgoal
   1.829 -  addressing that is known from ML tactics.
   1.830 +  Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer
   1.831 +  to the first subgoal or to all subgoals uniformly. Nonetheless, the
   1.832 +  subsequent mechanisms allow to imitate the effect of subgoal addressing that
   1.833 +  is known from ML tactics.
   1.834  
   1.835    \<^medskip>
   1.836 -  Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a
   1.837 -  way that certain subgoals are exposed, and other subgoals are ``parked''
   1.838 -  elsewhere. Thus a proof method has no other chance than to operate on the
   1.839 -  subgoals that are presently exposed.
   1.840 +  Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a way that
   1.841 +  certain subgoals are exposed, and other subgoals are ``parked'' elsewhere.
   1.842 +  Thus a proof method has no other chance than to operate on the subgoals that
   1.843 +  are presently exposed.
   1.844  
   1.845 -  Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means
   1.846 -  that method \<open>m\<^sub>1\<close> is applied with restriction to the first subgoal,
   1.847 -  then \<open>m\<^sub>2\<close> is applied consecutively with restriction to each subgoal
   1.848 -  that has newly emerged due to \<open>m\<^sub>1\<close>. This is analogous to the tactic
   1.849 -  combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite
   1.850 -  "isabelle-implementation"}. For example, \<open>(rule r; blast)\<close> applies
   1.851 -  rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
   1.852 +  Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is
   1.853 +  applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
   1.854 +  consecutively with restriction to each subgoal that has newly emerged due to
   1.855 +  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator @{ML_op THEN_ALL_NEW} in
   1.856 +  Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
   1.857 +  r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
   1.858  
   1.859 -  Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes
   1.860 -  only the first \<open>n\<close> subgoals (which need to exist), with default
   1.861 -  \<open>n = 1\<close>. For example, the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals, while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from
   1.862 +  Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the
   1.863 +  first \<open>n\<close> subgoals (which need to exist), with default \<open>n = 1\<close>. For example,
   1.864 +  the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals,
   1.865 +  while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from
   1.866    applying rule \<open>r\<close> to the originally first one.
   1.867  
   1.868    \<^medskip>
   1.869 -  Improper methods, notably tactic emulations, offer low-level goal
   1.870 -  addressing as explicit argument to the individual tactic being involved.
   1.871 -  Here ``\<open>[!]\<close>'' refers to all goals, and ``\<open>[n-]\<close>'' to all
   1.872 -  goals starting from \<open>n\<close>.
   1.873 +  Improper methods, notably tactic emulations, offer low-level goal addressing
   1.874 +  as explicit argument to the individual tactic being involved. Here ``\<open>[!]\<close>''
   1.875 +  refers to all goals, and ``\<open>[n-]\<close>'' to all goals starting from \<open>n\<close>.
   1.876  
   1.877    @{rail \<open>
   1.878      @{syntax_def goal_spec}:
   1.879 @@ -668,39 +628,37 @@
   1.880      @{method_def standard} & : & \<open>method\<close> \\
   1.881    \end{matharray}
   1.882  
   1.883 -  Arbitrary goal refinement via tactics is considered harmful.
   1.884 -  Structured proof composition in Isar admits proof methods to be
   1.885 -  invoked in two places only.
   1.886 -
   1.887 -  \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref
   1.888 -  "proof"}~\<open>m\<^sub>1\<close> reduces a newly stated goal to a number
   1.889 -  of sub-goals that are to be solved later.  Facts are passed to
   1.890 -  \<open>m\<^sub>1\<close> for forward chaining, if so indicated by \<open>proof(chain)\<close> mode.
   1.891 +  Arbitrary goal refinement via tactics is considered harmful. Structured
   1.892 +  proof composition in Isar admits proof methods to be invoked in two places
   1.893 +  only.
   1.894  
   1.895 -  \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to solve remaining goals.  No facts are
   1.896 -  passed to \<open>m\<^sub>2\<close>.
   1.897 -
   1.898 +    \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref "proof"}~\<open>m\<^sub>1\<close> reduces a
   1.899 +    newly stated goal to a number of sub-goals that are to be solved later.
   1.900 +    Facts are passed to \<open>m\<^sub>1\<close> for forward chaining, if so indicated by
   1.901 +    \<open>proof(chain)\<close> mode.
   1.902 +  
   1.903 +    \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to
   1.904 +    solve remaining goals. No facts are passed to \<open>m\<^sub>2\<close>.
   1.905  
   1.906 -  The only other (proper) way to affect pending goals in a proof body
   1.907 -  is by @{command_ref "show"}, which involves an explicit statement of
   1.908 -  what is to be solved eventually.  Thus we avoid the fundamental
   1.909 -  problem of unstructured tactic scripts that consist of numerous
   1.910 -  consecutive goal transformations, with invisible effects.
   1.911 +  The only other (proper) way to affect pending goals in a proof body is by
   1.912 +  @{command_ref "show"}, which involves an explicit statement of what is to be
   1.913 +  solved eventually. Thus we avoid the fundamental problem of unstructured
   1.914 +  tactic scripts that consist of numerous consecutive goal transformations,
   1.915 +  with invisible effects.
   1.916  
   1.917    \<^medskip>
   1.918 -  As a general rule of thumb for good proof style, initial
   1.919 -  proof methods should either solve the goal completely, or constitute
   1.920 -  some well-understood reduction to new sub-goals.  Arbitrary
   1.921 -  automatic proof tools that are prone leave a large number of badly
   1.922 -  structured sub-goals are no help in continuing the proof document in
   1.923 -  an intelligible manner.
   1.924 +  As a general rule of thumb for good proof style, initial proof methods
   1.925 +  should either solve the goal completely, or constitute some well-understood
   1.926 +  reduction to new sub-goals. Arbitrary automatic proof tools that are prone
   1.927 +  leave a large number of badly structured sub-goals are no help in continuing
   1.928 +  the proof document in an intelligible manner.
   1.929  
   1.930 -  Unless given explicitly by the user, the default initial method is
   1.931 -  @{method standard}, which subsumes at least @{method_ref (Pure) rule} or
   1.932 -  its classical variant @{method_ref (HOL) rule}. These methods apply a
   1.933 -  single standard elimination or introduction rule according to the topmost
   1.934 -  logical connective involved. There is no separate default terminal method.
   1.935 -  Any remaining goals are always solved by assumption in the very last step.
   1.936 +  Unless given explicitly by the user, the default initial method is @{method
   1.937 +  standard}, which subsumes at least @{method_ref (Pure) rule} or its
   1.938 +  classical variant @{method_ref (HOL) rule}. These methods apply a single
   1.939 +  standard elimination or introduction rule according to the topmost logical
   1.940 +  connective involved. There is no separate default terminal method. Any
   1.941 +  remaining goals are always solved by assumption in the very last step.
   1.942  
   1.943    @{rail \<open>
   1.944      @@{command proof} method?
   1.945 @@ -712,70 +670,64 @@
   1.946      (@@{command "."} | @@{command ".."} | @@{command sorry})
   1.947    \<close>}
   1.948  
   1.949 -  \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof
   1.950 -  method \<open>m\<^sub>1\<close>; facts for forward chaining are passed if so
   1.951 -  indicated by \<open>proof(chain)\<close> mode.
   1.952 +  \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof method \<open>m\<^sub>1\<close>; facts for
   1.953 +  forward chaining are passed if so indicated by \<open>proof(chain)\<close> mode.
   1.954  
   1.955 -  \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by
   1.956 -  proof method \<open>m\<^sub>2\<close> and concludes the sub-proof by assumption.
   1.957 -  If the goal had been \<open>show\<close> (or \<open>thus\<close>), some
   1.958 -  pending sub-goal is solved as well by the rule resulting from the
   1.959 -  result \<^emph>\<open>exported\<close> into the enclosing goal context.  Thus \<open>qed\<close> may fail for two reasons: either \<open>m\<^sub>2\<close> fails, or the
   1.960 -  resulting rule does not fit to any pending goal\<^footnote>\<open>This
   1.961 -  includes any additional ``strong'' assumptions as introduced by
   1.962 -  @{command "assume"}.\<close> of the enclosing context.  Debugging such a
   1.963 -  situation might involve temporarily changing @{command "show"} into
   1.964 -  @{command "have"}, or weakening the local context by replacing
   1.965 -  occurrences of @{command "assume"} by @{command "presume"}.
   1.966 +  \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by proof method \<open>m\<^sub>2\<close>
   1.967 +  and concludes the sub-proof by assumption. If the goal had been \<open>show\<close> (or
   1.968 +  \<open>thus\<close>), some pending sub-goal is solved as well by the rule resulting from
   1.969 +  the result \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail
   1.970 +  for two reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to
   1.971 +  any pending goal\<^footnote>\<open>This includes any additional ``strong'' assumptions as
   1.972 +  introduced by @{command "assume"}.\<close> of the enclosing context. Debugging such
   1.973 +  a situation might involve temporarily changing @{command "show"} into
   1.974 +  @{command "have"}, or weakening the local context by replacing occurrences
   1.975 +  of @{command "assume"} by @{command "presume"}.
   1.976  
   1.977 -  \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal
   1.978 -  proof\<close>\index{proof!terminal}; it abbreviates @{command
   1.979 -  "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with
   1.980 -  backtracking across both methods.  Debugging an unsuccessful
   1.981 -  @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its
   1.982 -  definition; in many cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even
   1.983 -  \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient to see the
   1.984 -  problem.
   1.985 +  \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal proof\<close>\index{proof!terminal}; it
   1.986 +  abbreviates @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with
   1.987 +  backtracking across both methods. Debugging an unsuccessful @{command
   1.988 +  "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its definition; in many
   1.989 +  cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient
   1.990 +  to see the problem.
   1.991  
   1.992 -  \<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard
   1.993 -  proof\<close>\index{proof!standard}; it abbreviates @{command "by"}~\<open>standard\<close>.
   1.994 +  \<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard proof\<close>\index{proof!standard}; it
   1.995 +  abbreviates @{command "by"}~\<open>standard\<close>.
   1.996  
   1.997 -  \<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial
   1.998 -  proof\<close>\index{proof!trivial}; it abbreviates @{command "by"}~\<open>this\<close>.
   1.999 +  \<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial proof\<close>\index{proof!trivial}; it
  1.1000 +  abbreviates @{command "by"}~\<open>this\<close>.
  1.1001  
  1.1002 -  \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake}
  1.1003 -  pretending to solve the pending claim without further ado.  This
  1.1004 -  only works in interactive development, or if the @{attribute
  1.1005 -  quick_and_dirty} is enabled.  Facts emerging from fake
  1.1006 -  proofs are not the real thing.  Internally, the derivation object is
  1.1007 -  tainted by an oracle invocation, which may be inspected via the
  1.1008 +  \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to
  1.1009 +  solve the pending claim without further ado. This only works in interactive
  1.1010 +  development, or if the @{attribute quick_and_dirty} is enabled. Facts
  1.1011 +  emerging from fake proofs are not the real thing. Internally, the derivation
  1.1012 +  object is tainted by an oracle invocation, which may be inspected via the
  1.1013    theorem status @{cite "isabelle-implementation"}.
  1.1014  
  1.1015    The most important application of @{command "sorry"} is to support
  1.1016    experimentation and top-down proof development.
  1.1017  
  1.1018 -  \<^descr> @{method standard} refers to the default refinement step of some
  1.1019 -  Isar language elements (notably @{command proof} and ``@{command ".."}'').
  1.1020 -  It is \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the
  1.1021 -  application environment.
  1.1022 +  \<^descr> @{method standard} refers to the default refinement step of some Isar
  1.1023 +  language elements (notably @{command proof} and ``@{command ".."}''). It is
  1.1024 +  \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the application
  1.1025 +  environment.
  1.1026  
  1.1027    In Isabelle/Pure, @{method standard} performs elementary introduction~/
  1.1028 -  elimination steps (@{method_ref (Pure) rule}), introduction of type
  1.1029 -  classes (@{method_ref intro_classes}) and locales (@{method_ref
  1.1030 -  intro_locales}).
  1.1031 +  elimination steps (@{method_ref (Pure) rule}), introduction of type classes
  1.1032 +  (@{method_ref intro_classes}) and locales (@{method_ref intro_locales}).
  1.1033  
  1.1034 -  In Isabelle/HOL, @{method standard} also takes classical rules into
  1.1035 -  account (cf.\ \secref{sec:classical}).
  1.1036 +  In Isabelle/HOL, @{method standard} also takes classical rules into account
  1.1037 +  (cf.\ \secref{sec:classical}).
  1.1038  \<close>
  1.1039  
  1.1040  
  1.1041  subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close>
  1.1042  
  1.1043  text \<open>
  1.1044 -  The following proof methods and attributes refer to basic logical
  1.1045 -  operations of Isar.  Further methods and attributes are provided by
  1.1046 -  several generic and object-logic specific tools and packages (see
  1.1047 -  \chref{ch:gen-tools} and \partref{part:hol}).
  1.1048 +  The following proof methods and attributes refer to basic logical operations
  1.1049 +  of Isar. Further methods and attributes are provided by several generic and
  1.1050 +  object-logic specific tools and packages (see \chref{ch:gen-tools} and
  1.1051 +  \partref{part:hol}).
  1.1052  
  1.1053    \begin{matharray}{rcl}
  1.1054      @{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]
  1.1055 @@ -816,113 +768,103 @@
  1.1056      @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}
  1.1057    \<close>}
  1.1058  
  1.1059 -  \<^descr> @{command "print_rules"} prints rules declared via attributes
  1.1060 -  @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
  1.1061 -  (Pure) dest} of Isabelle/Pure.
  1.1062 +  \<^descr> @{command "print_rules"} prints rules declared via attributes @{attribute
  1.1063 +  (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of
  1.1064 +  Isabelle/Pure.
  1.1065  
  1.1066 -  See also the analogous @{command "print_claset"} command for similar
  1.1067 -  rule declarations of the classical reasoner
  1.1068 -  (\secref{sec:classical}).
  1.1069 +  See also the analogous @{command "print_claset"} command for similar rule
  1.1070 +  declarations of the classical reasoner (\secref{sec:classical}).
  1.1071  
  1.1072 -  \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as
  1.1073 -  premises into the goal, and nothing else.
  1.1074 +  \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as premises
  1.1075 +  into the goal, and nothing else.
  1.1076  
  1.1077    Note that command @{command_ref "proof"} without any method actually
  1.1078 -  performs a single reduction step using the @{method_ref (Pure) rule}
  1.1079 -  method; thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command
  1.1080 -  "proof"}~\<open>-\<close>'' rather than @{command "proof"} alone.
  1.1081 +  performs a single reduction step using the @{method_ref (Pure) rule} method;
  1.1082 +  thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command "proof"}~\<open>-\<close>''
  1.1083 +  rather than @{command "proof"} alone.
  1.1084  
  1.1085 -  \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals
  1.1086 -  into cases within the context (see also \secref{sec:cases-induct}). The
  1.1087 -  specified case names are used if present; otherwise cases are numbered
  1.1088 -  starting from 1.
  1.1089 +  \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals into cases
  1.1090 +  within the context (see also \secref{sec:cases-induct}). The specified case
  1.1091 +  names are used if present; otherwise cases are numbered starting from 1.
  1.1092  
  1.1093    Invoking cases in the subsequent proof body via the @{command_ref case}
  1.1094    command will @{command fix} goal parameters, @{command assume} goal
  1.1095    premises, and @{command let} variable @{variable_ref ?case} refer to the
  1.1096    conclusion.
  1.1097  
  1.1098 -  \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from
  1.1099 -  \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or implicitly from the current proof context)
  1.1100 -  modulo unification of schematic type and term variables.  The rule
  1.1101 -  structure is not taken into account, i.e.\ meta-level implication is
  1.1102 -  considered atomic.  This is the same principle underlying literal
  1.1103 -  facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
  1.1104 -  "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that
  1.1105 -  \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close> in the
  1.1106 -  proof context.
  1.1107 +  \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or
  1.1108 +  implicitly from the current proof context) modulo unification of schematic
  1.1109 +  type and term variables. The rule structure is not taken into account, i.e.\
  1.1110 +  meta-level implication is considered atomic. This is the same principle
  1.1111 +  underlying literal facts (cf.\ \secref{sec:syn-att}): ``@{command
  1.1112 +  "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
  1.1113 +  "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close>
  1.1114 +  in the proof context.
  1.1115  
  1.1116 -  \<^descr> @{method assumption} solves some goal by a single assumption
  1.1117 -  step.  All given facts are guaranteed to participate in the
  1.1118 -  refinement; this means there may be only 0 or 1 in the first place.
  1.1119 -  Recall that @{command "qed"} (\secref{sec:proof-steps}) already
  1.1120 -  concludes any remaining sub-goals by assumption, so structured
  1.1121 -  proofs usually need not quote the @{method assumption} method at
  1.1122 -  all.
  1.1123 +  \<^descr> @{method assumption} solves some goal by a single assumption step. All
  1.1124 +  given facts are guaranteed to participate in the refinement; this means
  1.1125 +  there may be only 0 or 1 in the first place. Recall that @{command "qed"}
  1.1126 +  (\secref{sec:proof-steps}) already concludes any remaining sub-goals by
  1.1127 +  assumption, so structured proofs usually need not quote the @{method
  1.1128 +  assumption} method at all.
  1.1129  
  1.1130 -  \<^descr> @{method this} applies all of the current facts directly as
  1.1131 -  rules.  Recall that ``@{command "."}'' (dot) abbreviates ``@{command
  1.1132 -  "by"}~\<open>this\<close>''.
  1.1133 +  \<^descr> @{method this} applies all of the current facts directly as rules. Recall
  1.1134 +  that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~\<open>this\<close>''.
  1.1135  
  1.1136 -  \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as
  1.1137 -  argument in backward manner; facts are used to reduce the rule
  1.1138 -  before applying it to the goal.  Thus @{method (Pure) rule} without facts
  1.1139 -  is plain introduction, while with facts it becomes elimination.
  1.1140 +  \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as argument in
  1.1141 +  backward manner; facts are used to reduce the rule before applying it to the
  1.1142 +  goal. Thus @{method (Pure) rule} without facts is plain introduction, while
  1.1143 +  with facts it becomes elimination.
  1.1144  
  1.1145 -  When no arguments are given, the @{method (Pure) rule} method tries to
  1.1146 -  pick appropriate rules automatically, as declared in the current context
  1.1147 -  using the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
  1.1148 -  (Pure) dest} attributes (see below). This is included in the standard
  1.1149 -  behaviour of @{command "proof"} and ``@{command ".."}'' (double-dot) steps
  1.1150 -  (see \secref{sec:proof-steps}).
  1.1151 +  When no arguments are given, the @{method (Pure) rule} method tries to pick
  1.1152 +  appropriate rules automatically, as declared in the current context using
  1.1153 +  the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
  1.1154 +  dest} attributes (see below). This is included in the standard behaviour of
  1.1155 +  @{command "proof"} and ``@{command ".."}'' (double-dot) steps (see
  1.1156 +  \secref{sec:proof-steps}).
  1.1157  
  1.1158 -  \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
  1.1159 -  @{attribute (Pure) dest} declare introduction, elimination, and
  1.1160 -  destruct rules, to be used with method @{method (Pure) rule}, and similar
  1.1161 -  tools.  Note that the latter will ignore rules declared with
  1.1162 -  ``\<open>?\<close>'', while ``\<open>!\<close>''  are used most aggressively.
  1.1163 +  \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute
  1.1164 +  (Pure) dest} declare introduction, elimination, and destruct rules, to be
  1.1165 +  used with method @{method (Pure) rule}, and similar tools. Note that the
  1.1166 +  latter will ignore rules declared with ``\<open>?\<close>'', while ``\<open>!\<close>'' are used most
  1.1167 +  aggressively.
  1.1168  
  1.1169 -  The classical reasoner (see \secref{sec:classical}) introduces its
  1.1170 -  own variants of these attributes; use qualified names to access the
  1.1171 -  present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
  1.1172 -  "Pure.intro"}.
  1.1173 +  The classical reasoner (see \secref{sec:classical}) introduces its own
  1.1174 +  variants of these attributes; use qualified names to access the present
  1.1175 +  versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}.
  1.1176  
  1.1177 -  \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction,
  1.1178 -  elimination, or destruct rules.
  1.1179 +  \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction, elimination, or
  1.1180 +  destruct rules.
  1.1181  
  1.1182 -  \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all
  1.1183 -  of the given rules \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left
  1.1184 -  order, which means that premises stemming from the \<open>a\<^sub>i\<close>
  1.1185 -  emerge in parallel in the result, without interfering with each
  1.1186 -  other.  In many practical situations, the \<open>a\<^sub>i\<close> do not have
  1.1187 -  premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually
  1.1188 -  read as functional application (modulo unification).
  1.1189 +  \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all of the given rules
  1.1190 +  \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left order, which means that premises
  1.1191 +  stemming from the \<open>a\<^sub>i\<close> emerge in parallel in the result, without
  1.1192 +  interfering with each other. In many practical situations, the \<open>a\<^sub>i\<close> do not
  1.1193 +  have premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually read as
  1.1194 +  functional application (modulo unification).
  1.1195  
  1.1196 -  Argument positions may be effectively skipped by using ``\<open>_\<close>''
  1.1197 -  (underscore), which refers to the propositional identity rule in the
  1.1198 -  Pure theory.
  1.1199 +  Argument positions may be effectively skipped by using ``\<open>_\<close>'' (underscore),
  1.1200 +  which refers to the propositional identity rule in the Pure theory.
  1.1201  
  1.1202 -  \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional
  1.1203 -  instantiation of term variables.  The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are
  1.1204 -  substituted for any schematic variables occurring in a theorem from
  1.1205 -  left to right; ``\<open>_\<close>'' (underscore) indicates to skip a
  1.1206 -  position.  Arguments following a ``\<open>concl:\<close>'' specification
  1.1207 -  refer to positions of the conclusion of a rule.
  1.1208 +  \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional instantiation of term
  1.1209 +  variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are substituted for any schematic
  1.1210 +  variables occurring in a theorem from left to right; ``\<open>_\<close>'' (underscore)
  1.1211 +  indicates to skip a position. Arguments following a ``\<open>concl:\<close>''
  1.1212 +  specification refer to positions of the conclusion of a rule.
  1.1213  
  1.1214 -  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may
  1.1215 -  be specified: the instantiated theorem is exported, and these
  1.1216 -  variables become schematic (usually with some shifting of indices).
  1.1217 +  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified:
  1.1218 +  the instantiated theorem is exported, and these variables become schematic
  1.1219 +  (usually with some shifting of indices).
  1.1220  
  1.1221 -  \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close>
  1.1222 -  performs named instantiation of schematic type and term variables
  1.1223 -  occurring in a theorem.  Schematic variables have to be specified on
  1.1224 -  the left-hand side (e.g.\ \<open>?x1.3\<close>).  The question mark may
  1.1225 -  be omitted if the variable name is a plain identifier without index.
  1.1226 -  As type instantiations are inferred from term instantiations,
  1.1227 -  explicit type instantiations are seldom necessary.
  1.1228 +  \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close> performs named
  1.1229 +  instantiation of schematic type and term variables occurring in a theorem.
  1.1230 +  Schematic variables have to be specified on the left-hand side (e.g.\
  1.1231 +  \<open>?x1.3\<close>). The question mark may be omitted if the variable name is a plain
  1.1232 +  identifier without index. As type instantiations are inferred from term
  1.1233 +  instantiations, explicit type instantiations are seldom necessary.
  1.1234  
  1.1235 -  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may
  1.1236 -  be specified as for @{attribute "of"} above.
  1.1237 +  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified
  1.1238 +  as for @{attribute "of"} above.
  1.1239  \<close>
  1.1240  
  1.1241  
  1.1242 @@ -937,14 +879,13 @@
  1.1243      @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
  1.1244    \<close>}
  1.1245  
  1.1246 -  \<^descr> @{command "method_setup"}~\<open>name = text description\<close>
  1.1247 -  defines a proof method in the current context.  The given \<open>text\<close> has to be an ML expression of type
  1.1248 -  @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
  1.1249 -  basic parsers defined in structure @{ML_structure Args} and @{ML_structure
  1.1250 -  Attrib}.  There are also combinators like @{ML METHOD} and @{ML
  1.1251 -  SIMPLE_METHOD} to turn certain tactic forms into official proof
  1.1252 -  methods; the primed versions refer to tactics with explicit goal
  1.1253 -  addressing.
  1.1254 +  \<^descr> @{command "method_setup"}~\<open>name = text description\<close> defines a proof method
  1.1255 +  in the current context. The given \<open>text\<close> has to be an ML expression of type
  1.1256 +  @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\ basic
  1.1257 +  parsers defined in structure @{ML_structure Args} and @{ML_structure
  1.1258 +  Attrib}. There are also combinators like @{ML METHOD} and @{ML
  1.1259 +  SIMPLE_METHOD} to turn certain tactic forms into official proof methods; the
  1.1260 +  primed versions refer to tactics with explicit goal addressing.
  1.1261  
  1.1262    Here are some example method definitions:
  1.1263  \<close>
  1.1264 @@ -980,52 +921,47 @@
  1.1265      @{attribute_def consumes} & : & \<open>attribute\<close> \\
  1.1266    \end{matharray}
  1.1267  
  1.1268 -  The puristic way to build up Isar proof contexts is by explicit
  1.1269 -  language elements like @{command "fix"}, @{command "assume"},
  1.1270 -  @{command "let"} (see \secref{sec:proof-context}).  This is adequate
  1.1271 -  for plain natural deduction, but easily becomes unwieldy in concrete
  1.1272 -  verification tasks, which typically involve big induction rules with
  1.1273 -  several cases.
  1.1274 +  The puristic way to build up Isar proof contexts is by explicit language
  1.1275 +  elements like @{command "fix"}, @{command "assume"}, @{command "let"} (see
  1.1276 +  \secref{sec:proof-context}). This is adequate for plain natural deduction,
  1.1277 +  but easily becomes unwieldy in concrete verification tasks, which typically
  1.1278 +  involve big induction rules with several cases.
  1.1279  
  1.1280 -  The @{command "case"} command provides a shorthand to refer to a
  1.1281 -  local context symbolically: certain proof methods provide an
  1.1282 -  environment of named ``cases'' of the form \<open>c: x\<^sub>1, \<dots>,
  1.1283 -  x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of ``@{command
  1.1284 -  "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots>
  1.1285 -  \<phi>\<^sub>n\<close>''.  Term bindings may be covered as well, notably
  1.1286 -  @{variable ?case} for the main conclusion.
  1.1287 +  The @{command "case"} command provides a shorthand to refer to a local
  1.1288 +  context symbolically: certain proof methods provide an environment of named
  1.1289 +  ``cases'' of the form \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of
  1.1290 +  ``@{command "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots>
  1.1291 +  x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Term bindings may be covered as
  1.1292 +  well, notably @{variable ?case} for the main conclusion.
  1.1293  
  1.1294 -  By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of
  1.1295 -  a case value is marked as hidden, i.e.\ there is no way to refer to
  1.1296 -  such parameters in the subsequent proof text.  After all, original
  1.1297 -  rule parameters stem from somewhere outside of the current proof
  1.1298 -  text.  By using the explicit form ``@{command "case"}~\<open>(c
  1.1299 -  y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to
  1.1300 -  chose local names that fit nicely into the current context.
  1.1301 +  By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of a case value is marked as
  1.1302 +  hidden, i.e.\ there is no way to refer to such parameters in the subsequent
  1.1303 +  proof text. After all, original rule parameters stem from somewhere outside
  1.1304 +  of the current proof text. By using the explicit form ``@{command
  1.1305 +  "case"}~\<open>(c y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to chose local
  1.1306 +  names that fit nicely into the current context.
  1.1307  
  1.1308    \<^medskip>
  1.1309 -  It is important to note that proper use of @{command
  1.1310 -  "case"} does not provide means to peek at the current goal state,
  1.1311 -  which is not directly observable in Isar!  Nonetheless, goal
  1.1312 -  refinement commands do provide named cases \<open>goal\<^sub>i\<close>
  1.1313 -  for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.
  1.1314 -  Using this extra feature requires great care, because some bits of
  1.1315 -  the internal tactical machinery intrude the proof text.  In
  1.1316 -  particular, parameter names stemming from the left-over of automated
  1.1317 -  reasoning tools are usually quite unpredictable.
  1.1318 +  It is important to note that proper use of @{command "case"} does not
  1.1319 +  provide means to peek at the current goal state, which is not directly
  1.1320 +  observable in Isar! Nonetheless, goal refinement commands do provide named
  1.1321 +  cases \<open>goal\<^sub>i\<close> for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.
  1.1322 +  Using this extra feature requires great care, because some bits of the
  1.1323 +  internal tactical machinery intrude the proof text. In particular, parameter
  1.1324 +  names stemming from the left-over of automated reasoning tools are usually
  1.1325 +  quite unpredictable.
  1.1326  
  1.1327    Under normal circumstances, the text of cases emerge from standard
  1.1328 -  elimination or induction rules, which in turn are derived from
  1.1329 -  previous theory specifications in a canonical way (say from
  1.1330 -  @{command "inductive"} definitions).
  1.1331 +  elimination or induction rules, which in turn are derived from previous
  1.1332 +  theory specifications in a canonical way (say from @{command "inductive"}
  1.1333 +  definitions).
  1.1334  
  1.1335    \<^medskip>
  1.1336 -  Proper cases are only available if both the proof method
  1.1337 -  and the rules involved support this.  By using appropriate
  1.1338 -  attributes, case names, conclusions, and parameters may be also
  1.1339 -  declared by hand.  Thus variant versions of rules that have been
  1.1340 -  derived manually become ready to use in advanced case analysis
  1.1341 -  later.
  1.1342 +  Proper cases are only available if both the proof method and the rules
  1.1343 +  involved support this. By using appropriate attributes, case names,
  1.1344 +  conclusions, and parameters may be also declared by hand. Thus variant
  1.1345 +  versions of rules that have been derived manually become ready to use in
  1.1346 +  advanced case analysis later.
  1.1347  
  1.1348    @{rail \<open>
  1.1349      @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
  1.1350 @@ -1039,67 +975,62 @@
  1.1351      @@{attribute consumes} @{syntax int}?
  1.1352    \<close>}
  1.1353  
  1.1354 -  \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local
  1.1355 -  context \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an
  1.1356 -  appropriate proof method (such as @{method_ref cases} and @{method_ref
  1.1357 -  induct}). The command ``@{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>''
  1.1358 -  abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command
  1.1359 -  "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by the
  1.1360 -  prefix \<open>a\<close>, and all such facts are collectively bound to the name
  1.1361 -  \<open>a\<close>.
  1.1362 +  \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local context \<open>c:
  1.1363 +  x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an appropriate proof method (such
  1.1364 +  as @{method_ref cases} and @{method_ref induct}). The command ``@{command
  1.1365 +  "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>'' abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots>
  1.1366 +  x\<^sub>m\<close>~@{command "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by
  1.1367 +  the prefix \<open>a\<close>, and all such facts are collectively bound to the name \<open>a\<close>.
  1.1368  
  1.1369 -  The fact name is specification \<open>a\<close> is optional, the default is to
  1.1370 -  re-use \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same
  1.1371 -  as @{command "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.
  1.1372 -
  1.1373 -  \<^descr> @{command "print_cases"} prints all local contexts of the
  1.1374 -  current state, using Isar proof language notation.
  1.1375 +  The fact name is specification \<open>a\<close> is optional, the default is to re-use
  1.1376 +  \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same as @{command
  1.1377 +  "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.
  1.1378  
  1.1379 -  \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for
  1.1380 -  the local contexts of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close>
  1.1381 -  refers to the \<^emph>\<open>prefix\<close> of the list of premises. Each of the
  1.1382 -  cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where
  1.1383 -  the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close>
  1.1384 -  from left to right.
  1.1385 +  \<^descr> @{command "print_cases"} prints all local contexts of the current state,
  1.1386 +  using Isar proof language notation.
  1.1387 +
  1.1388 +  \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for the local contexts
  1.1389 +  of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close> refers to the \<^emph>\<open>prefix\<close> of the list
  1.1390 +  of premises. Each of the cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where
  1.1391 +  the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close> from left to
  1.1392 +  right.
  1.1393  
  1.1394 -  \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares
  1.1395 -  names for the conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix of arguments of a logical formula
  1.1396 -  built by nesting a binary connective (e.g.\ \<open>\<or>\<close>).
  1.1397 +  \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares names for the
  1.1398 +  conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix
  1.1399 +  of arguments of a logical formula built by nesting a binary connective
  1.1400 +  (e.g.\ \<open>\<or>\<close>).
  1.1401  
  1.1402 -  Note that proof methods such as @{method induct} and @{method
  1.1403 -  coinduct} already provide a default name for the conclusion as a
  1.1404 -  whole.  The need to name subformulas only arises with cases that
  1.1405 -  split into several sub-cases, as in common co-induction rules.
  1.1406 +  Note that proof methods such as @{method induct} and @{method coinduct}
  1.1407 +  already provide a default name for the conclusion as a whole. The need to
  1.1408 +  name subformulas only arises with cases that split into several sub-cases,
  1.1409 +  as in common co-induction rules.
  1.1410  
  1.1411 -  \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames
  1.1412 -  the innermost parameters of premises \<open>1, \<dots>, n\<close> of some
  1.1413 -  theorem.  An empty list of names may be given to skip positions,
  1.1414 -  leaving the present parameters unchanged.
  1.1415 +  \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames the innermost
  1.1416 +  parameters of premises \<open>1, \<dots>, n\<close> of some theorem. An empty list of names may
  1.1417 +  be given to skip positions, leaving the present parameters unchanged.
  1.1418  
  1.1419 -  Note that the default usage of case rules does \<^emph>\<open>not\<close> directly
  1.1420 -  expose parameters to the proof context.
  1.1421 +  Note that the default usage of case rules does \<^emph>\<open>not\<close> directly expose
  1.1422 +  parameters to the proof context.
  1.1423  
  1.1424 -  \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major
  1.1425 -  premises'' of a rule, i.e.\ the number of facts to be consumed when
  1.1426 -  it is applied by an appropriate proof method.  The default value of
  1.1427 -  @{attribute consumes} is \<open>n = 1\<close>, which is appropriate for
  1.1428 -  the usual kind of cases and induction rules for inductive sets (cf.\
  1.1429 -  \secref{sec:hol-inductive}).  Rules without any @{attribute
  1.1430 -  consumes} declaration given are treated as if @{attribute
  1.1431 +  \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major premises'' of a
  1.1432 +  rule, i.e.\ the number of facts to be consumed when it is applied by an
  1.1433 +  appropriate proof method. The default value of @{attribute consumes} is \<open>n =
  1.1434 +  1\<close>, which is appropriate for the usual kind of cases and induction rules for
  1.1435 +  inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
  1.1436 +  @{attribute consumes} declaration given are treated as if @{attribute
  1.1437    consumes}~\<open>0\<close> had been specified.
  1.1438  
  1.1439 -  A negative \<open>n\<close> is interpreted relatively to the total number
  1.1440 -  of premises of the rule in the target context.  Thus its absolute
  1.1441 -  value specifies the remaining number of premises, after subtracting
  1.1442 -  the prefix of major premises as indicated above. This form of
  1.1443 -  declaration has the technical advantage of being stable under more
  1.1444 -  morphisms, notably those that export the result from a nested
  1.1445 -  @{command_ref context} with additional assumptions.
  1.1446 +  A negative \<open>n\<close> is interpreted relatively to the total number of premises of
  1.1447 +  the rule in the target context. Thus its absolute value specifies the
  1.1448 +  remaining number of premises, after subtracting the prefix of major premises
  1.1449 +  as indicated above. This form of declaration has the technical advantage of
  1.1450 +  being stable under more morphisms, notably those that export the result from
  1.1451 +  a nested @{command_ref context} with additional assumptions.
  1.1452  
  1.1453 -  Note that explicit @{attribute consumes} declarations are only
  1.1454 -  rarely needed; this is already taken care of automatically by the
  1.1455 -  higher-level @{attribute cases}, @{attribute induct}, and
  1.1456 -  @{attribute coinduct} declarations.
  1.1457 +  Note that explicit @{attribute consumes} declarations are only rarely
  1.1458 +  needed; this is already taken care of automatically by the higher-level
  1.1459 +  @{attribute cases}, @{attribute induct}, and @{attribute coinduct}
  1.1460 +  declarations.
  1.1461  \<close>
  1.1462  
  1.1463  
  1.1464 @@ -1113,25 +1044,23 @@
  1.1465      @{method_def coinduct} & : & \<open>method\<close> \\
  1.1466    \end{matharray}
  1.1467  
  1.1468 -  The @{method cases}, @{method induct}, @{method induction},
  1.1469 -  and @{method coinduct}
  1.1470 -  methods provide a uniform interface to common proof techniques over
  1.1471 -  datatypes, inductive predicates (or sets), recursive functions etc.
  1.1472 -  The corresponding rules may be specified and instantiated in a
  1.1473 -  casual manner.  Furthermore, these methods provide named local
  1.1474 -  contexts that may be invoked via the @{command "case"} proof command
  1.1475 -  within the subsequent proof text.  This accommodates compact proof
  1.1476 -  texts even when reasoning about large specifications.
  1.1477 +  The @{method cases}, @{method induct}, @{method induction}, and @{method
  1.1478 +  coinduct} methods provide a uniform interface to common proof techniques
  1.1479 +  over datatypes, inductive predicates (or sets), recursive functions etc. The
  1.1480 +  corresponding rules may be specified and instantiated in a casual manner.
  1.1481 +  Furthermore, these methods provide named local contexts that may be invoked
  1.1482 +  via the @{command "case"} proof command within the subsequent proof text.
  1.1483 +  This accommodates compact proof texts even when reasoning about large
  1.1484 +  specifications.
  1.1485  
  1.1486 -  The @{method induct} method also provides some additional
  1.1487 -  infrastructure in order to be applicable to structure statements
  1.1488 -  (either using explicit meta-level connectives, or including facts
  1.1489 -  and parameters separately).  This avoids cumbersome encoding of
  1.1490 -  ``strengthened'' inductive statements within the object-logic.
  1.1491 +  The @{method induct} method also provides some additional infrastructure in
  1.1492 +  order to be applicable to structure statements (either using explicit
  1.1493 +  meta-level connectives, or including facts and parameters separately). This
  1.1494 +  avoids cumbersome encoding of ``strengthened'' inductive statements within
  1.1495 +  the object-logic.
  1.1496  
  1.1497 -  Method @{method induction} differs from @{method induct} only in
  1.1498 -  the names of the facts in the local context invoked by the @{command "case"}
  1.1499 -  command.
  1.1500 +  Method @{method induction} differs from @{method induct} only in the names
  1.1501 +  of the facts in the local context invoked by the @{command "case"} command.
  1.1502  
  1.1503    @{rail \<open>
  1.1504      @@{method cases} ('(' 'no_simp' ')')? \<newline>
  1.1505 @@ -1154,13 +1083,12 @@
  1.1506      taking: 'taking' ':' @{syntax insts}
  1.1507    \<close>}
  1.1508  
  1.1509 -  \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method
  1.1510 -  rule} with an appropriate case distinction theorem, instantiated to
  1.1511 -  the subjects \<open>insts\<close>.  Symbolic case names are bound according
  1.1512 -  to the rule's local contexts.
  1.1513 +  \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method rule} with an
  1.1514 +  appropriate case distinction theorem, instantiated to the subjects \<open>insts\<close>.
  1.1515 +  Symbolic case names are bound according to the rule's local contexts.
  1.1516  
  1.1517 -  The rule is determined as follows, according to the facts and
  1.1518 -  arguments passed to the @{method cases} method:
  1.1519 +  The rule is determined as follows, according to the facts and arguments
  1.1520 +  passed to the @{method cases} method:
  1.1521  
  1.1522    \<^medskip>
  1.1523    \begin{tabular}{llll}
  1.1524 @@ -1173,16 +1101,16 @@
  1.1525    \end{tabular}
  1.1526    \<^medskip>
  1.1527  
  1.1528 -  Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close>
  1.1529 -  of premises of the case rule; within each premise, the \<^emph>\<open>prefix\<close>
  1.1530 -  of variables is instantiated.  In most situations, only a single
  1.1531 -  term needs to be specified; this refers to the first variable of the
  1.1532 -  last premise (it is usually the same for all cases).  The \<open>(no_simp)\<close> option can be used to disable pre-simplification of
  1.1533 -  cases (see the description of @{method induct} below for details).
  1.1534 +  Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close> of premises
  1.1535 +  of the case rule; within each premise, the \<^emph>\<open>prefix\<close> of variables is
  1.1536 +  instantiated. In most situations, only a single term needs to be specified;
  1.1537 +  this refers to the first variable of the last premise (it is usually the
  1.1538 +  same for all cases). The \<open>(no_simp)\<close> option can be used to disable
  1.1539 +  pre-simplification of cases (see the description of @{method induct} below
  1.1540 +  for details).
  1.1541  
  1.1542 -  \<^descr> @{method induct}~\<open>insts R\<close> and
  1.1543 -  @{method induction}~\<open>insts R\<close> are analogous to the
  1.1544 -  @{method cases} method, but refer to induction rules, which are
  1.1545 +  \<^descr> @{method induct}~\<open>insts R\<close> and @{method induction}~\<open>insts R\<close> are analogous
  1.1546 +  to the @{method cases} method, but refer to induction rules, which are
  1.1547    determined as follows:
  1.1548  
  1.1549    \<^medskip>
  1.1550 @@ -1194,51 +1122,44 @@
  1.1551    \end{tabular}
  1.1552    \<^medskip>
  1.1553  
  1.1554 -  Several instantiations may be given, each referring to some part of
  1.1555 -  a mutual inductive definition or datatype --- only related partial
  1.1556 -  induction rules may be used together, though.  Any of the lists of
  1.1557 -  terms \<open>P, x, \<dots>\<close> refers to the \<^emph>\<open>suffix\<close> of variables
  1.1558 -  present in the induction rule.  This enables the writer to specify
  1.1559 -  only induction variables, or both predicates and variables, for
  1.1560 -  example.
  1.1561 +  Several instantiations may be given, each referring to some part of a mutual
  1.1562 +  inductive definition or datatype --- only related partial induction rules
  1.1563 +  may be used together, though. Any of the lists of terms \<open>P, x, \<dots>\<close> refers to
  1.1564 +  the \<^emph>\<open>suffix\<close> of variables present in the induction rule. This enables the
  1.1565 +  writer to specify only induction variables, or both predicates and
  1.1566 +  variables, for example.
  1.1567  
  1.1568 -  Instantiations may be definitional: equations \<open>x \<equiv> t\<close>
  1.1569 -  introduce local definitions, which are inserted into the claim and
  1.1570 -  discharged after applying the induction rule.  Equalities reappear
  1.1571 -  in the inductive cases, but have been transformed according to the
  1.1572 -  induction principle being involved here.  In order to achieve
  1.1573 -  practically useful induction hypotheses, some variables occurring in
  1.1574 -  \<open>t\<close> need to be fixed (see below).  Instantiations of the form
  1.1575 -  \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a
  1.1576 -  shorthand for \mbox{\<open>x \<equiv> t\<close>}, where \<open>x\<close> is a fresh
  1.1577 -  variable. If this is not intended, \<open>t\<close> has to be enclosed in
  1.1578 -  parentheses.  By default, the equalities generated by definitional
  1.1579 -  instantiations are pre-simplified using a specific set of rules,
  1.1580 -  usually consisting of distinctness and injectivity theorems for
  1.1581 -  datatypes. This pre-simplification may cause some of the parameters
  1.1582 -  of an inductive case to disappear, or may even completely delete
  1.1583 -  some of the inductive cases, if one of the equalities occurring in
  1.1584 -  their premises can be simplified to \<open>False\<close>.  The \<open>(no_simp)\<close> option can be used to disable pre-simplification.
  1.1585 -  Additional rules to be used in pre-simplification can be declared
  1.1586 -  using the @{attribute_def induct_simp} attribute.
  1.1587 +  Instantiations may be definitional: equations \<open>x \<equiv> t\<close> introduce local
  1.1588 +  definitions, which are inserted into the claim and discharged after applying
  1.1589 +  the induction rule. Equalities reappear in the inductive cases, but have
  1.1590 +  been transformed according to the induction principle being involved here.
  1.1591 +  In order to achieve practically useful induction hypotheses, some variables
  1.1592 +  occurring in \<open>t\<close> need to be fixed (see below). Instantiations of the form
  1.1593 +  \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv> t\<close>,
  1.1594 +  where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be
  1.1595 +  enclosed in parentheses. By default, the equalities generated by
  1.1596 +  definitional instantiations are pre-simplified using a specific set of
  1.1597 +  rules, usually consisting of distinctness and injectivity theorems for
  1.1598 +  datatypes. This pre-simplification may cause some of the parameters of an
  1.1599 +  inductive case to disappear, or may even completely delete some of the
  1.1600 +  inductive cases, if one of the equalities occurring in their premises can be
  1.1601 +  simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable
  1.1602 +  pre-simplification. Additional rules to be used in pre-simplification can be
  1.1603 +  declared using the @{attribute_def induct_simp} attribute.
  1.1604  
  1.1605 -  The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>''
  1.1606 -  specification generalizes variables \<open>x\<^sub>1, \<dots>,
  1.1607 -  x\<^sub>m\<close> of the original goal before applying induction.  One can
  1.1608 -  separate variables by ``\<open>and\<close>'' to generalize them in other
  1.1609 -  goals then the first. Thus induction hypotheses may become
  1.1610 -  sufficiently general to get the proof through.  Together with
  1.1611 -  definitional instantiations, one may effectively perform induction
  1.1612 -  over expressions of a certain structure.
  1.1613 +  The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables
  1.1614 +  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can
  1.1615 +  separate variables by ``\<open>and\<close>'' to generalize them in other goals then the
  1.1616 +  first. Thus induction hypotheses may become sufficiently general to get the
  1.1617 +  proof through. Together with definitional instantiations, one may
  1.1618 +  effectively perform induction over expressions of a certain structure.
  1.1619  
  1.1620 -  The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>''
  1.1621 -  specification provides additional instantiations of a prefix of
  1.1622 -  pending variables in the rule.  Such schematic induction rules
  1.1623 -  rarely occur in practice, though.
  1.1624 +  The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional
  1.1625 +  instantiations of a prefix of pending variables in the rule. Such schematic
  1.1626 +  induction rules rarely occur in practice, though.
  1.1627  
  1.1628 -  \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the
  1.1629 -  @{method induct} method, but refers to coinduction rules, which are
  1.1630 -  determined as follows:
  1.1631 +  \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the @{method induct} method,
  1.1632 +  but refers to coinduction rules, which are determined as follows:
  1.1633  
  1.1634    \<^medskip>
  1.1635    \begin{tabular}{llll}
  1.1636 @@ -1249,69 +1170,63 @@
  1.1637    \end{tabular}
  1.1638    \<^medskip>
  1.1639  
  1.1640 -  Coinduction is the dual of induction.  Induction essentially
  1.1641 -  eliminates \<open>A x\<close> towards a generic result \<open>P x\<close>,
  1.1642 -  while coinduction introduces \<open>A x\<close> starting with \<open>B
  1.1643 -  x\<close>, for a suitable ``bisimulation'' \<open>B\<close>.  The cases of a
  1.1644 -  coinduct rule are typically named after the predicates or sets being
  1.1645 -  covered, while the conclusions consist of several alternatives being
  1.1646 -  named after the individual destructor patterns.
  1.1647 +  Coinduction is the dual of induction. Induction essentially eliminates \<open>A x\<close>
  1.1648 +  towards a generic result \<open>P x\<close>, while coinduction introduces \<open>A x\<close> starting
  1.1649 +  with \<open>B x\<close>, for a suitable ``bisimulation'' \<open>B\<close>. The cases of a coinduct
  1.1650 +  rule are typically named after the predicates or sets being covered, while
  1.1651 +  the conclusions consist of several alternatives being named after the
  1.1652 +  individual destructor patterns.
  1.1653  
  1.1654 -  The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables
  1.1655 -  occurring in the rule's major premise, or conclusion if unavailable.
  1.1656 -  An additional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>''
  1.1657 -  specification may be required in order to specify the bisimulation
  1.1658 -  to be used in the coinduction step.
  1.1659 +  The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables occurring in
  1.1660 +  the rule's major premise, or conclusion if unavailable. An additional
  1.1661 +  ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification may be required in order to specify
  1.1662 +  the bisimulation to be used in the coinduction step.
  1.1663  
  1.1664  
  1.1665    Above methods produce named local contexts, as determined by the
  1.1666 -  instantiated rule as given in the text.  Beyond that, the @{method
  1.1667 -  induct} and @{method coinduct} methods guess further instantiations
  1.1668 -  from the goal specification itself.  Any persisting unresolved
  1.1669 -  schematic variables of the resulting rule will render the the
  1.1670 -  corresponding case invalid.  The term binding @{variable ?case} for
  1.1671 -  the conclusion will be provided with each case, provided that term
  1.1672 -  is fully specified.
  1.1673 +  instantiated rule as given in the text. Beyond that, the @{method induct}
  1.1674 +  and @{method coinduct} methods guess further instantiations from the goal
  1.1675 +  specification itself. Any persisting unresolved schematic variables of the
  1.1676 +  resulting rule will render the the corresponding case invalid. The term
  1.1677 +  binding @{variable ?case} for the conclusion will be provided with each
  1.1678 +  case, provided that term is fully specified.
  1.1679  
  1.1680 -  The @{command "print_cases"} command prints all named cases present
  1.1681 -  in the current proof state.
  1.1682 +  The @{command "print_cases"} command prints all named cases present in the
  1.1683 +  current proof state.
  1.1684  
  1.1685    \<^medskip>
  1.1686 -  Despite the additional infrastructure, both @{method cases}
  1.1687 -  and @{method coinduct} merely apply a certain rule, after
  1.1688 -  instantiation, while conforming due to the usual way of monotonic
  1.1689 -  natural deduction: the context of a structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close>
  1.1690 -  reappears unchanged after the case split.
  1.1691 +  Despite the additional infrastructure, both @{method cases} and @{method
  1.1692 +  coinduct} merely apply a certain rule, after instantiation, while conforming
  1.1693 +  due to the usual way of monotonic natural deduction: the context of a
  1.1694 +  structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close> reappears unchanged after
  1.1695 +  the case split.
  1.1696  
  1.1697 -  The @{method induct} method is fundamentally different in this
  1.1698 -  respect: the meta-level structure is passed through the
  1.1699 -  ``recursive'' course involved in the induction.  Thus the original
  1.1700 -  statement is basically replaced by separate copies, corresponding to
  1.1701 -  the induction hypotheses and conclusion; the original goal context
  1.1702 -  is no longer available.  Thus local assumptions, fixed parameters
  1.1703 -  and definitions effectively participate in the inductive rephrasing
  1.1704 -  of the original statement.
  1.1705 +  The @{method induct} method is fundamentally different in this respect: the
  1.1706 +  meta-level structure is passed through the ``recursive'' course involved in
  1.1707 +  the induction. Thus the original statement is basically replaced by separate
  1.1708 +  copies, corresponding to the induction hypotheses and conclusion; the
  1.1709 +  original goal context is no longer available. Thus local assumptions, fixed
  1.1710 +  parameters and definitions effectively participate in the inductive
  1.1711 +  rephrasing of the original statement.
  1.1712  
  1.1713    In @{method induct} proofs, local assumptions introduced by cases are split
  1.1714 -  into two different kinds: \<open>hyps\<close> stemming from the rule and
  1.1715 -  \<open>prems\<close> from the goal statement.  This is reflected in the
  1.1716 -  extracted cases accordingly, so invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and \<open>c.prems\<close>,
  1.1717 -  as well as fact \<open>c\<close> to hold the all-inclusive list.
  1.1718 +  into two different kinds: \<open>hyps\<close> stemming from the rule and \<open>prems\<close> from the
  1.1719 +  goal statement. This is reflected in the extracted cases accordingly, so
  1.1720 +  invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and
  1.1721 +  \<open>c.prems\<close>, as well as fact \<open>c\<close> to hold the all-inclusive list.
  1.1722  
  1.1723    In @{method induction} proofs, local assumptions introduced by cases are
  1.1724 -  split into three different kinds: \<open>IH\<close>, the induction hypotheses,
  1.1725 -  \<open>hyps\<close>, the remaining hypotheses stemming from the rule, and
  1.1726 -  \<open>prems\<close>, the assumptions from the goal statement. The names are
  1.1727 -  \<open>c.IH\<close>, \<open>c.hyps\<close> and \<open>c.prems\<close>, as above.
  1.1728 -
  1.1729 +  split into three different kinds: \<open>IH\<close>, the induction hypotheses, \<open>hyps\<close>,
  1.1730 +  the remaining hypotheses stemming from the rule, and \<open>prems\<close>, the
  1.1731 +  assumptions from the goal statement. The names are \<open>c.IH\<close>, \<open>c.hyps\<close> and
  1.1732 +  \<open>c.prems\<close>, as above.
  1.1733  
  1.1734    \<^medskip>
  1.1735 -  Facts presented to either method are consumed according to
  1.1736 -  the number of ``major premises'' of the rule involved, which is
  1.1737 -  usually 0 for plain cases and induction rules of datatypes etc.\ and
  1.1738 -  1 for rules of inductive predicates or sets and the like.  The
  1.1739 -  remaining facts are inserted into the goal verbatim before the
  1.1740 -  actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is
  1.1741 +  Facts presented to either method are consumed according to the number of
  1.1742 +  ``major premises'' of the rule involved, which is usually 0 for plain cases
  1.1743 +  and induction rules of datatypes etc.\ and 1 for rules of inductive
  1.1744 +  predicates or sets and the like. The remaining facts are inserted into the
  1.1745 +  goal verbatim before the actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is
  1.1746    applied.
  1.1747  \<close>
  1.1748  
  1.1749 @@ -1337,27 +1252,24 @@
  1.1750      spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
  1.1751    \<close>}
  1.1752  
  1.1753 -  \<^descr> @{command "print_induct_rules"} prints cases and induct rules
  1.1754 -  for predicates (or sets) and types of the current context.
  1.1755 +  \<^descr> @{command "print_induct_rules"} prints cases and induct rules for
  1.1756 +  predicates (or sets) and types of the current context.
  1.1757  
  1.1758 -  \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute
  1.1759 -  coinduct} (as attributes) declare rules for reasoning about
  1.1760 -  (co)inductive predicates (or sets) and types, using the
  1.1761 -  corresponding methods of the same name.  Certain definitional
  1.1762 -  packages of object-logics usually declare emerging cases and
  1.1763 +  \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute coinduct} (as
  1.1764 +  attributes) declare rules for reasoning about (co)inductive predicates (or
  1.1765 +  sets) and types, using the corresponding methods of the same name. Certain
  1.1766 +  definitional packages of object-logics usually declare emerging cases and
  1.1767    induction rules as expected, so users rarely need to intervene.
  1.1768  
  1.1769 -  Rules may be deleted via the \<open>del\<close> specification, which
  1.1770 -  covers all of the \<open>type\<close>/\<open>pred\<close>/\<open>set\<close>
  1.1771 -  sub-categories simultaneously.  For example, @{attribute
  1.1772 -  cases}~\<open>del\<close> removes any @{attribute cases} rules declared for
  1.1773 -  some type, predicate, or set.
  1.1774 +  Rules may be deleted via the \<open>del\<close> specification, which covers all of the
  1.1775 +  \<open>type\<close>/\<open>pred\<close>/\<open>set\<close> sub-categories simultaneously. For example, @{attribute
  1.1776 +  cases}~\<open>del\<close> removes any @{attribute cases} rules declared for some type,
  1.1777 +  predicate, or set.
  1.1778  
  1.1779 -  Manual rule declarations usually refer to the @{attribute
  1.1780 -  case_names} and @{attribute params} attributes to adjust names of
  1.1781 -  cases and parameters of a rule; the @{attribute consumes}
  1.1782 -  declaration is taken care of automatically: @{attribute
  1.1783 -  consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute
  1.1784 +  Manual rule declarations usually refer to the @{attribute case_names} and
  1.1785 +  @{attribute params} attributes to adjust names of cases and parameters of a
  1.1786 +  rule; the @{attribute consumes} declaration is taken care of automatically:
  1.1787 +  @{attribute consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute
  1.1788    consumes}~\<open>1\<close> for ``predicate'' / ``set'' rules.
  1.1789  \<close>
  1.1790  
  1.1791 @@ -1371,11 +1283,11 @@
  1.1792      @{command_def "guess"}\<open>\<^sup>*\<close> & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
  1.1793    \end{matharray}
  1.1794  
  1.1795 -  Generalized elimination means that hypothetical parameters and premises
  1.1796 -  may be introduced in the current context, potentially with a split into
  1.1797 -  cases. This works by virtue of a locally proven rule that establishes the
  1.1798 -  soundness of this temporary context extension. As representative examples,
  1.1799 -  one may think of standard rules from Isabelle/HOL like this:
  1.1800 +  Generalized elimination means that hypothetical parameters and premises may
  1.1801 +  be introduced in the current context, potentially with a split into cases.
  1.1802 +  This works by virtue of a locally proven rule that establishes the soundness
  1.1803 +  of this temporary context extension. As representative examples, one may
  1.1804 +  think of standard rules from Isabelle/HOL like this:
  1.1805  
  1.1806    \<^medskip>
  1.1807    \begin{tabular}{ll}
  1.1808 @@ -1386,9 +1298,9 @@
  1.1809    \<^medskip>
  1.1810  
  1.1811    In general, these particular rules and connectives need to get involved at
  1.1812 -  all: this concept works directly in Isabelle/Pure via Isar commands
  1.1813 -  defined below. In particular, the logic of elimination and case splitting
  1.1814 -  is delegated to an Isar proof, which often involves automated tools.
  1.1815 +  all: this concept works directly in Isabelle/Pure via Isar commands defined
  1.1816 +  below. In particular, the logic of elimination and case splitting is
  1.1817 +  delegated to an Isar proof, which often involves automated tools.
  1.1818  
  1.1819    @{rail \<open>
  1.1820      @@{command consider} @{syntax obtain_clauses}
  1.1821 @@ -1399,21 +1311,21 @@
  1.1822      @@{command guess} (@{syntax "fixes"} + @'and')
  1.1823    \<close>}
  1.1824  
  1.1825 -  \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
  1.1826 -  | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case
  1.1827 -  splitting into separate subgoals, such that each case involves new
  1.1828 -  parameters and premises. After the proof is finished, the resulting rule
  1.1829 -  may be used directly with the @{method cases} proof method
  1.1830 -  (\secref{sec:cases-induct}), in order to perform actual case-splitting of
  1.1831 -  the proof text via @{command case} and @{command next} as usual.
  1.1832 +  \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)
  1.1833 +  \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting
  1.1834 +  into separate subgoals, such that each case involves new parameters and
  1.1835 +  premises. After the proof is finished, the resulting rule may be used
  1.1836 +  directly with the @{method cases} proof method (\secref{sec:cases-induct}),
  1.1837 +  in order to perform actual case-splitting of the proof text via @{command
  1.1838 +  case} and @{command next} as usual.
  1.1839  
  1.1840 -  Optional names in round parentheses refer to case names: in the proof of
  1.1841 -  the rule this is a fact name, in the resulting rule it is used as
  1.1842 -  annotation with the @{attribute_ref case_names} attribute.
  1.1843 +  Optional names in round parentheses refer to case names: in the proof of the
  1.1844 +  rule this is a fact name, in the resulting rule it is used as annotation
  1.1845 +  with the @{attribute_ref case_names} attribute.
  1.1846  
  1.1847    \<^medskip>
  1.1848 -  Formally, the command @{command consider} is defined as derived
  1.1849 -  Isar language element as follows:
  1.1850 +  Formally, the command @{command consider} is defined as derived Isar
  1.1851 +  language element as follows:
  1.1852  
  1.1853    \begin{matharray}{l}
  1.1854      @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]
  1.1855 @@ -1426,25 +1338,24 @@
  1.1856    \end{matharray}
  1.1857  
  1.1858    See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
  1.1859 -  statements, as well as @{command print_statement} to print existing rules
  1.1860 -  in a similar format.
  1.1861 +  statements, as well as @{command print_statement} to print existing rules in
  1.1862 +  a similar format.
  1.1863  
  1.1864 -  \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close>
  1.1865 -  states a generalized elimination rule with exactly one case. After the
  1.1866 -  proof is finished, it is activated for the subsequent proof text: the
  1.1867 -  context is augmented via @{command fix}~\<open>\<^vec>x\<close> @{command
  1.1868 -  assume}~\<open>\<^vec>A \<^vec>x\<close>, with special provisions to export
  1.1869 -  later results by discharging these assumptions again.
  1.1870 +  \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> states a
  1.1871 +  generalized elimination rule with exactly one case. After the proof is
  1.1872 +  finished, it is activated for the subsequent proof text: the context is
  1.1873 +  augmented via @{command fix}~\<open>\<^vec>x\<close> @{command assume}~\<open>\<^vec>A
  1.1874 +  \<^vec>x\<close>, with special provisions to export later results by discharging
  1.1875 +  these assumptions again.
  1.1876  
  1.1877    Note that according to the parameter scopes within the elimination rule,
  1.1878 -  results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the
  1.1879 -  export will fail! This restriction conforms to the usual manner of
  1.1880 -  existential reasoning in Natural Deduction.
  1.1881 +  results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the export
  1.1882 +  will fail! This restriction conforms to the usual manner of existential
  1.1883 +  reasoning in Natural Deduction.
  1.1884  
  1.1885    \<^medskip>
  1.1886 -  Formally, the command @{command obtain} is defined as derived
  1.1887 -  Isar language element as follows, using an instrumented variant of
  1.1888 -  @{command assume}:
  1.1889 +  Formally, the command @{command obtain} is defined as derived Isar language
  1.1890 +  element as follows, using an instrumented variant of @{command assume}:
  1.1891  
  1.1892    \begin{matharray}{l}
  1.1893      @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]
  1.1894 @@ -1462,23 +1373,23 @@
  1.1895    \<^emph>\<open>improper\<close>.
  1.1896  
  1.1897    A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The
  1.1898 -  subsequent refinement steps may turn this to anything of the form \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
  1.1899 -  subgoals. The final goal state is then used as reduction rule for the
  1.1900 -  obtain pattern described above. Obtained parameters \<open>\<^vec>x\<close> are
  1.1901 -  marked as internal by default, and thus inaccessible in the proof text.
  1.1902 -  The variable names and type constraints given as arguments for @{command
  1.1903 -  "guess"} specify a prefix of accessible parameters.
  1.1904 +  subsequent refinement steps may turn this to anything of the form
  1.1905 +  \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
  1.1906 +  subgoals. The final goal state is then used as reduction rule for the obtain
  1.1907 +  pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as
  1.1908 +  internal by default, and thus inaccessible in the proof text. The variable
  1.1909 +  names and type constraints given as arguments for @{command "guess"} specify
  1.1910 +  a prefix of accessible parameters.
  1.1911  
  1.1912  
  1.1913 -  In the proof of @{command consider} and @{command obtain} the local
  1.1914 -  premises are always bound to the fact name @{fact_ref that}, according to
  1.1915 -  structured Isar statements involving @{keyword_ref "if"}
  1.1916 -  (\secref{sec:goals}).
  1.1917 +  In the proof of @{command consider} and @{command obtain} the local premises
  1.1918 +  are always bound to the fact name @{fact_ref that}, according to structured
  1.1919 +  Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).
  1.1920  
  1.1921 -  Facts that are established by @{command "obtain"} and @{command "guess"}
  1.1922 -  may not be polymorphic: any type-variables occurring here are fixed in the
  1.1923 -  present context. This is a natural consequence of the role of @{command
  1.1924 -  fix} and @{command assume} in these constructs.
  1.1925 +  Facts that are established by @{command "obtain"} and @{command "guess"} may
  1.1926 +  not be polymorphic: any type-variables occurring here are fixed in the
  1.1927 +  present context. This is a natural consequence of the role of @{command fix}
  1.1928 +  and @{command assume} in these constructs.
  1.1929  \<close>
  1.1930  
  1.1931  end
     2.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Fri Nov 13 14:49:30 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Fri Nov 13 15:06:58 2015 +0100
     2.3 @@ -14,8 +14,8 @@
     2.4    Nonetheless, it is possible to emulate proof scripts by sequential
     2.5    refinements of a proof state in backwards mode, notably with the @{command
     2.6    apply} command (see \secref{sec:tactic-commands}). There are also various
     2.7 -  proof methods that allow to refer to implicit goal state information that
     2.8 -  is normally not accessible to structured Isar proofs (see
     2.9 +  proof methods that allow to refer to implicit goal state information that is
    2.10 +  normally not accessible to structured Isar proofs (see
    2.11    \secref{sec:tactics}).
    2.12  \<close>
    2.13  
    2.14 @@ -43,44 +43,42 @@
    2.15      @@{command prefer} @{syntax nat}
    2.16    \<close>}
    2.17  
    2.18 -  \<^descr> @{command "supply"} supports fact definitions during goal
    2.19 -  refinement: it is similar to @{command "note"}, but it operates in
    2.20 -  backwards mode and does not have any impact on chained facts.
    2.21 +  \<^descr> @{command "supply"} supports fact definitions during goal refinement: it
    2.22 +  is similar to @{command "note"}, but it operates in backwards mode and does
    2.23 +  not have any impact on chained facts.
    2.24  
    2.25 -  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in
    2.26 -  initial position, but unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode.  Thus consecutive method applications may be
    2.27 -  given just as in tactic scripts.
    2.28 +  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in initial position, but
    2.29 +  unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus
    2.30 +  consecutive method applications may be given just as in tactic scripts.
    2.31  
    2.32 -  Facts are passed to \<open>m\<close> as indicated by the goal's
    2.33 -  forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards.  Thus any
    2.34 -  further @{command "apply"} command would always work in a purely
    2.35 -  backward manner.
    2.36 +  Facts are passed to \<open>m\<close> as indicated by the goal's forward-chain mode, and
    2.37 +  are \<^emph>\<open>consumed\<close> afterwards. Thus any further @{command "apply"} command
    2.38 +  would always work in a purely backward manner.
    2.39  
    2.40 -  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal position.  Basically, this simulates a
    2.41 -  multi-step tactic script for @{command "qed"}, but may be given
    2.42 -  anywhere within the proof body.
    2.43 +  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal
    2.44 +  position. Basically, this simulates a multi-step tactic script for @{command
    2.45 +  "qed"}, but may be given anywhere within the proof body.
    2.46  
    2.47 -  No facts are passed to \<open>m\<close> here.  Furthermore, the static
    2.48 -  context is that of the enclosing goal (as for actual @{command
    2.49 -  "qed"}).  Thus the proof method may not refer to any assumptions
    2.50 -  introduced in the current body, for example.
    2.51 +  No facts are passed to \<open>m\<close> here. Furthermore, the static context is that of
    2.52 +  the enclosing goal (as for actual @{command "qed"}). Thus the proof method
    2.53 +  may not refer to any assumptions introduced in the current body, for
    2.54 +  example.
    2.55  
    2.56 -  \<^descr> @{command "done"} completes a proof script, provided that the
    2.57 -  current goal state is solved completely.  Note that actual
    2.58 -  structured proof commands (e.g.\ ``@{command "."}'' or @{command
    2.59 -  "sorry"}) may be used to conclude proof scripts as well.
    2.60 +  \<^descr> @{command "done"} completes a proof script, provided that the current goal
    2.61 +  state is solved completely. Note that actual structured proof commands
    2.62 +  (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude
    2.63 +  proof scripts as well.
    2.64  
    2.65 -  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close>
    2.66 -  shuffle the list of pending goals: @{command "defer"} puts off
    2.67 -  sub-goal \<open>n\<close> to the end of the list (\<open>n = 1\<close> by
    2.68 -  default), while @{command "prefer"} brings sub-goal \<open>n\<close> to the
    2.69 -  front.
    2.70 +  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> shuffle the list of
    2.71 +  pending goals: @{command "defer"} puts off sub-goal \<open>n\<close> to the end of the
    2.72 +  list (\<open>n = 1\<close> by default), while @{command "prefer"} brings sub-goal \<open>n\<close> to
    2.73 +  the front.
    2.74  
    2.75 -  \<^descr> @{command "back"} does back-tracking over the result sequence
    2.76 -  of the latest proof command.  Any proof command may return multiple
    2.77 -  results, and this command explores the possibilities step-by-step.
    2.78 -  It is mainly useful for experimentation and interactive exploration,
    2.79 -  and should be avoided in finished proofs.
    2.80 +  \<^descr> @{command "back"} does back-tracking over the result sequence of the
    2.81 +  latest proof command. Any proof command may return multiple results, and
    2.82 +  this command explores the possibilities step-by-step. It is mainly useful
    2.83 +  for experimentation and interactive exploration, and should be avoided in
    2.84 +  finished proofs.
    2.85  \<close>
    2.86  
    2.87  
    2.88 @@ -109,23 +107,22 @@
    2.89    structured proofs, but the text of the parameters, premises and conclusion
    2.90    is not given explicitly.
    2.91  
    2.92 -  Goal parameters may be specified separately, in order to allow referring
    2.93 -  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
    2.94 -  y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
    2.95 -  "for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
    2.96 -  latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
    2.97 -  positions may be skipped via dummies (underscore). Unspecified names
    2.98 -  remain internal, and thus inaccessible in the proof text.
    2.99 +  Goal parameters may be specified separately, in order to allow referring to
   2.100 +  them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x y z\<close>''
   2.101 +  names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword "for"}~\<open>\<dots> x y z\<close>''
   2.102 +  names a \<^emph>\<open>suffix\<close> of goal parameters. The latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol
   2.103 +  as notation. Parameter positions may be skipped via dummies (underscore).
   2.104 +  Unspecified names remain internal, and thus inaccessible in the proof text.
   2.105  
   2.106 -  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that
   2.107 -  goal premises should be turned into assumptions of the context (otherwise
   2.108 -  the remaining conclusion is a Pure implication). The fact name and
   2.109 -  attributes are optional; the particular name ``\<open>prems\<close>'' is a common
   2.110 -  convention for the premises of an arbitrary goal context in proof scripts.
   2.111 +  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that goal
   2.112 +  premises should be turned into assumptions of the context (otherwise the
   2.113 +  remaining conclusion is a Pure implication). The fact name and attributes
   2.114 +  are optional; the particular name ``\<open>prems\<close>'' is a common convention for the
   2.115 +  premises of an arbitrary goal context in proof scripts.
   2.116  
   2.117 -  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result
   2.118 -  of a proven subgoal. Thus it may be re-used in further reasoning, similar
   2.119 -  to the result of @{command show} in structured Isar proofs.
   2.120 +  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result of a
   2.121 +  proven subgoal. Thus it may be re-used in further reasoning, similar to the
   2.122 +  result of @{command show} in structured Isar proofs.
   2.123  
   2.124  
   2.125    Here are some abstract examples:
   2.126 @@ -181,32 +178,29 @@
   2.127  section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
   2.128  
   2.129  text \<open>
   2.130 -  The following improper proof methods emulate traditional tactics.
   2.131 -  These admit direct access to the goal state, which is normally
   2.132 -  considered harmful!  In particular, this may involve both numbered
   2.133 -  goal addressing (default 1), and dynamic instantiation within the
   2.134 -  scope of some subgoal.
   2.135 +  The following improper proof methods emulate traditional tactics. These
   2.136 +  admit direct access to the goal state, which is normally considered harmful!
   2.137 +  In particular, this may involve both numbered goal addressing (default 1),
   2.138 +  and dynamic instantiation within the scope of some subgoal.
   2.139  
   2.140    \begin{warn}
   2.141 -    Dynamic instantiations refer to universally quantified parameters
   2.142 -    of a subgoal (the dynamic context) rather than fixed variables and
   2.143 -    term abbreviations of a (static) Isar context.
   2.144 +    Dynamic instantiations refer to universally quantified parameters of a
   2.145 +    subgoal (the dynamic context) rather than fixed variables and term
   2.146 +    abbreviations of a (static) Isar context.
   2.147    \end{warn}
   2.148  
   2.149 -  Tactic emulation methods, unlike their ML counterparts, admit
   2.150 -  simultaneous instantiation from both dynamic and static contexts.
   2.151 -  If names occur in both contexts goal parameters hide locally fixed
   2.152 -  variables.  Likewise, schematic variables refer to term
   2.153 -  abbreviations, if present in the static context.  Otherwise the
   2.154 -  schematic variable is interpreted as a schematic variable and left
   2.155 -  to be solved by unification with certain parts of the subgoal.
   2.156 +  Tactic emulation methods, unlike their ML counterparts, admit simultaneous
   2.157 +  instantiation from both dynamic and static contexts. If names occur in both
   2.158 +  contexts goal parameters hide locally fixed variables. Likewise, schematic
   2.159 +  variables refer to term abbreviations, if present in the static context.
   2.160 +  Otherwise the schematic variable is interpreted as a schematic variable and
   2.161 +  left to be solved by unification with certain parts of the subgoal.
   2.162  
   2.163    Note that the tactic emulation proof methods in Isabelle/Isar are
   2.164 -  consistently named \<open>foo_tac\<close>.  Note also that variable names
   2.165 -  occurring on left hand sides of instantiations must be preceded by a
   2.166 -  question mark if they coincide with a keyword or contain dots.  This
   2.167 -  is consistent with the attribute @{attribute "where"} (see
   2.168 -  \secref{sec:pure-meth-att}).
   2.169 +  consistently named \<open>foo_tac\<close>. Note also that variable names occurring on
   2.170 +  left hand sides of instantiations must be preceded by a question mark if
   2.171 +  they coincide with a keyword or contain dots. This is consistent with the
   2.172 +  attribute @{attribute "where"} (see \secref{sec:pure-meth-att}).
   2.173  
   2.174    \begin{matharray}{rcl}
   2.175      @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
   2.176 @@ -239,52 +233,46 @@
   2.177    \<close>}
   2.178  
   2.179    \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
   2.180 -  instantiation.  This works the same way as the ML tactics @{ML
   2.181 +  instantiation. This works the same way as the ML tactics @{ML
   2.182    Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
   2.183  
   2.184 -  Multiple rules may be only given if there is no instantiation; then
   2.185 -  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   2.186 -  @{cite "isabelle-implementation"}).
   2.187 -
   2.188 -  \<^descr> @{method cut_tac} inserts facts into the proof state as
   2.189 -  assumption of a subgoal; instantiations may be given as well.  Note
   2.190 -  that the scope of schematic variables is spread over the main goal
   2.191 -  statement and rule premises are turned into new subgoals.  This is
   2.192 -  in contrast to the regular method @{method insert} which inserts
   2.193 -  closed rule statements.
   2.194 +  Multiple rules may be only given if there is no instantiation; then @{method
   2.195 +  rule_tac} is the same as @{ML resolve_tac} in ML (see @{cite
   2.196 +  "isabelle-implementation"}).
   2.197  
   2.198 -  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise
   2.199 -  from a subgoal.  Note that \<open>\<phi>\<close> may contain schematic
   2.200 -  variables, to abbreviate the intended proposition; the first
   2.201 -  matching subgoal premise will be deleted.  Removing useless premises
   2.202 -  from a subgoal increases its readability and can make search tactics
   2.203 -  run faster.
   2.204 +  \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a
   2.205 +  subgoal; instantiations may be given as well. Note that the scope of
   2.206 +  schematic variables is spread over the main goal statement and rule premises
   2.207 +  are turned into new subgoals. This is in contrast to the regular method
   2.208 +  @{method insert} which inserts closed rule statements.
   2.209  
   2.210 -  \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions
   2.211 -  \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as local premises to a subgoal, and poses the same
   2.212 -  as new subgoals (in the original context).
   2.213 +  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise from a subgoal. Note
   2.214 +  that \<open>\<phi>\<close> may contain schematic variables, to abbreviate the intended
   2.215 +  proposition; the first matching subgoal premise will be deleted. Removing
   2.216 +  useless premises from a subgoal increases its readability and can make
   2.217 +  search tactics run faster.
   2.218  
   2.219 -  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a
   2.220 -  goal according to the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the
   2.221 -  \<^emph>\<open>suffix\<close> of variables.
   2.222 +  \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as
   2.223 +  local premises to a subgoal, and poses the same as new subgoals (in the
   2.224 +  original context).
   2.225  
   2.226 -  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a
   2.227 -  subgoal by \<open>n\<close> positions: from right to left if \<open>n\<close> is
   2.228 -  positive, and from left to right if \<open>n\<close> is negative; the
   2.229 -  default value is 1.
   2.230 +  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a goal according to
   2.231 +  the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the \<^emph>\<open>suffix\<close> of variables.
   2.232 +
   2.233 +  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a subgoal by \<open>n\<close>
   2.234 +  positions: from right to left if \<open>n\<close> is positive, and from left to right if
   2.235 +  \<open>n\<close> is negative; the default value is 1.
   2.236  
   2.237 -  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from
   2.238 -  any ML text of type @{ML_type tactic}.  Apart from the usual ML
   2.239 -  environment and the current proof context, the ML code may refer to
   2.240 -  the locally bound values @{ML_text facts}, which indicates any
   2.241 -  current facts used for forward-chaining.
   2.242 +  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from any ML text of type
   2.243 +  @{ML_type tactic}. Apart from the usual ML environment and the current proof
   2.244 +  context, the ML code may refer to the locally bound values @{ML_text facts},
   2.245 +  which indicates any current facts used for forward-chaining.
   2.246  
   2.247 -  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but
   2.248 -  presents the goal state in its raw internal form, where simultaneous
   2.249 -  subgoals appear as conjunction of the logical framework instead of
   2.250 -  the usual split into several subgoals.  While feature this is useful
   2.251 -  for debugging of complex method definitions, it should not never
   2.252 -  appear in production theories.
   2.253 +  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but presents the goal
   2.254 +  state in its raw internal form, where simultaneous subgoals appear as
   2.255 +  conjunction of the logical framework instead of the usual split into several
   2.256 +  subgoals. While feature this is useful for debugging of complex method
   2.257 +  definitions, it should not never appear in production theories.
   2.258  \<close>
   2.259  
   2.260  end
   2.261 \ No newline at end of file