src/Doc/Isar_Ref/Proof_Script.thy
changeset 61657 5b878bc6ae98
parent 61656 cfabbc083977
child 61866 6fa60a4f7e48
     1.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Fri Nov 13 14:49:30 2015 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Fri Nov 13 15:06:58 2015 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4    Nonetheless, it is possible to emulate proof scripts by sequential
     1.5    refinements of a proof state in backwards mode, notably with the @{command
     1.6    apply} command (see \secref{sec:tactic-commands}). There are also various
     1.7 -  proof methods that allow to refer to implicit goal state information that
     1.8 -  is normally not accessible to structured Isar proofs (see
     1.9 +  proof methods that allow to refer to implicit goal state information that is
    1.10 +  normally not accessible to structured Isar proofs (see
    1.11    \secref{sec:tactics}).
    1.12  \<close>
    1.13  
    1.14 @@ -43,44 +43,42 @@
    1.15      @@{command prefer} @{syntax nat}
    1.16    \<close>}
    1.17  
    1.18 -  \<^descr> @{command "supply"} supports fact definitions during goal
    1.19 -  refinement: it is similar to @{command "note"}, but it operates in
    1.20 -  backwards mode and does not have any impact on chained facts.
    1.21 +  \<^descr> @{command "supply"} supports fact definitions during goal refinement: it
    1.22 +  is similar to @{command "note"}, but it operates in backwards mode and does
    1.23 +  not have any impact on chained facts.
    1.24  
    1.25 -  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in
    1.26 -  initial position, but unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode.  Thus consecutive method applications may be
    1.27 -  given just as in tactic scripts.
    1.28 +  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in initial position, but
    1.29 +  unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus
    1.30 +  consecutive method applications may be given just as in tactic scripts.
    1.31  
    1.32 -  Facts are passed to \<open>m\<close> as indicated by the goal's
    1.33 -  forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards.  Thus any
    1.34 -  further @{command "apply"} command would always work in a purely
    1.35 -  backward manner.
    1.36 +  Facts are passed to \<open>m\<close> as indicated by the goal's forward-chain mode, and
    1.37 +  are \<^emph>\<open>consumed\<close> afterwards. Thus any further @{command "apply"} command
    1.38 +  would always work in a purely backward manner.
    1.39  
    1.40 -  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal position.  Basically, this simulates a
    1.41 -  multi-step tactic script for @{command "qed"}, but may be given
    1.42 -  anywhere within the proof body.
    1.43 +  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal
    1.44 +  position. Basically, this simulates a multi-step tactic script for @{command
    1.45 +  "qed"}, but may be given anywhere within the proof body.
    1.46  
    1.47 -  No facts are passed to \<open>m\<close> here.  Furthermore, the static
    1.48 -  context is that of the enclosing goal (as for actual @{command
    1.49 -  "qed"}).  Thus the proof method may not refer to any assumptions
    1.50 -  introduced in the current body, for example.
    1.51 +  No facts are passed to \<open>m\<close> here. Furthermore, the static context is that of
    1.52 +  the enclosing goal (as for actual @{command "qed"}). Thus the proof method
    1.53 +  may not refer to any assumptions introduced in the current body, for
    1.54 +  example.
    1.55  
    1.56 -  \<^descr> @{command "done"} completes a proof script, provided that the
    1.57 -  current goal state is solved completely.  Note that actual
    1.58 -  structured proof commands (e.g.\ ``@{command "."}'' or @{command
    1.59 -  "sorry"}) may be used to conclude proof scripts as well.
    1.60 +  \<^descr> @{command "done"} completes a proof script, provided that the current goal
    1.61 +  state is solved completely. Note that actual structured proof commands
    1.62 +  (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude
    1.63 +  proof scripts as well.
    1.64  
    1.65 -  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close>
    1.66 -  shuffle the list of pending goals: @{command "defer"} puts off
    1.67 -  sub-goal \<open>n\<close> to the end of the list (\<open>n = 1\<close> by
    1.68 -  default), while @{command "prefer"} brings sub-goal \<open>n\<close> to the
    1.69 -  front.
    1.70 +  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> shuffle the list of
    1.71 +  pending goals: @{command "defer"} puts off sub-goal \<open>n\<close> to the end of the
    1.72 +  list (\<open>n = 1\<close> by default), while @{command "prefer"} brings sub-goal \<open>n\<close> to
    1.73 +  the front.
    1.74  
    1.75 -  \<^descr> @{command "back"} does back-tracking over the result sequence
    1.76 -  of the latest proof command.  Any proof command may return multiple
    1.77 -  results, and this command explores the possibilities step-by-step.
    1.78 -  It is mainly useful for experimentation and interactive exploration,
    1.79 -  and should be avoided in finished proofs.
    1.80 +  \<^descr> @{command "back"} does back-tracking over the result sequence of the
    1.81 +  latest proof command. Any proof command may return multiple results, and
    1.82 +  this command explores the possibilities step-by-step. It is mainly useful
    1.83 +  for experimentation and interactive exploration, and should be avoided in
    1.84 +  finished proofs.
    1.85  \<close>
    1.86  
    1.87  
    1.88 @@ -109,23 +107,22 @@
    1.89    structured proofs, but the text of the parameters, premises and conclusion
    1.90    is not given explicitly.
    1.91  
    1.92 -  Goal parameters may be specified separately, in order to allow referring
    1.93 -  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
    1.94 -  y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
    1.95 -  "for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
    1.96 -  latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
    1.97 -  positions may be skipped via dummies (underscore). Unspecified names
    1.98 -  remain internal, and thus inaccessible in the proof text.
    1.99 +  Goal parameters may be specified separately, in order to allow referring to
   1.100 +  them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x y z\<close>''
   1.101 +  names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword "for"}~\<open>\<dots> x y z\<close>''
   1.102 +  names a \<^emph>\<open>suffix\<close> of goal parameters. The latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol
   1.103 +  as notation. Parameter positions may be skipped via dummies (underscore).
   1.104 +  Unspecified names remain internal, and thus inaccessible in the proof text.
   1.105  
   1.106 -  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that
   1.107 -  goal premises should be turned into assumptions of the context (otherwise
   1.108 -  the remaining conclusion is a Pure implication). The fact name and
   1.109 -  attributes are optional; the particular name ``\<open>prems\<close>'' is a common
   1.110 -  convention for the premises of an arbitrary goal context in proof scripts.
   1.111 +  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that goal
   1.112 +  premises should be turned into assumptions of the context (otherwise the
   1.113 +  remaining conclusion is a Pure implication). The fact name and attributes
   1.114 +  are optional; the particular name ``\<open>prems\<close>'' is a common convention for the
   1.115 +  premises of an arbitrary goal context in proof scripts.
   1.116  
   1.117 -  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result
   1.118 -  of a proven subgoal. Thus it may be re-used in further reasoning, similar
   1.119 -  to the result of @{command show} in structured Isar proofs.
   1.120 +  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result of a
   1.121 +  proven subgoal. Thus it may be re-used in further reasoning, similar to the
   1.122 +  result of @{command show} in structured Isar proofs.
   1.123  
   1.124  
   1.125    Here are some abstract examples:
   1.126 @@ -181,32 +178,29 @@
   1.127  section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
   1.128  
   1.129  text \<open>
   1.130 -  The following improper proof methods emulate traditional tactics.
   1.131 -  These admit direct access to the goal state, which is normally
   1.132 -  considered harmful!  In particular, this may involve both numbered
   1.133 -  goal addressing (default 1), and dynamic instantiation within the
   1.134 -  scope of some subgoal.
   1.135 +  The following improper proof methods emulate traditional tactics. These
   1.136 +  admit direct access to the goal state, which is normally considered harmful!
   1.137 +  In particular, this may involve both numbered goal addressing (default 1),
   1.138 +  and dynamic instantiation within the scope of some subgoal.
   1.139  
   1.140    \begin{warn}
   1.141 -    Dynamic instantiations refer to universally quantified parameters
   1.142 -    of a subgoal (the dynamic context) rather than fixed variables and
   1.143 -    term abbreviations of a (static) Isar context.
   1.144 +    Dynamic instantiations refer to universally quantified parameters of a
   1.145 +    subgoal (the dynamic context) rather than fixed variables and term
   1.146 +    abbreviations of a (static) Isar context.
   1.147    \end{warn}
   1.148  
   1.149 -  Tactic emulation methods, unlike their ML counterparts, admit
   1.150 -  simultaneous instantiation from both dynamic and static contexts.
   1.151 -  If names occur in both contexts goal parameters hide locally fixed
   1.152 -  variables.  Likewise, schematic variables refer to term
   1.153 -  abbreviations, if present in the static context.  Otherwise the
   1.154 -  schematic variable is interpreted as a schematic variable and left
   1.155 -  to be solved by unification with certain parts of the subgoal.
   1.156 +  Tactic emulation methods, unlike their ML counterparts, admit simultaneous
   1.157 +  instantiation from both dynamic and static contexts. If names occur in both
   1.158 +  contexts goal parameters hide locally fixed variables. Likewise, schematic
   1.159 +  variables refer to term abbreviations, if present in the static context.
   1.160 +  Otherwise the schematic variable is interpreted as a schematic variable and
   1.161 +  left to be solved by unification with certain parts of the subgoal.
   1.162  
   1.163    Note that the tactic emulation proof methods in Isabelle/Isar are
   1.164 -  consistently named \<open>foo_tac\<close>.  Note also that variable names
   1.165 -  occurring on left hand sides of instantiations must be preceded by a
   1.166 -  question mark if they coincide with a keyword or contain dots.  This
   1.167 -  is consistent with the attribute @{attribute "where"} (see
   1.168 -  \secref{sec:pure-meth-att}).
   1.169 +  consistently named \<open>foo_tac\<close>. Note also that variable names occurring on
   1.170 +  left hand sides of instantiations must be preceded by a question mark if
   1.171 +  they coincide with a keyword or contain dots. This is consistent with the
   1.172 +  attribute @{attribute "where"} (see \secref{sec:pure-meth-att}).
   1.173  
   1.174    \begin{matharray}{rcl}
   1.175      @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
   1.176 @@ -239,52 +233,46 @@
   1.177    \<close>}
   1.178  
   1.179    \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
   1.180 -  instantiation.  This works the same way as the ML tactics @{ML
   1.181 +  instantiation. This works the same way as the ML tactics @{ML
   1.182    Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
   1.183  
   1.184 -  Multiple rules may be only given if there is no instantiation; then
   1.185 -  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   1.186 -  @{cite "isabelle-implementation"}).
   1.187 -
   1.188 -  \<^descr> @{method cut_tac} inserts facts into the proof state as
   1.189 -  assumption of a subgoal; instantiations may be given as well.  Note
   1.190 -  that the scope of schematic variables is spread over the main goal
   1.191 -  statement and rule premises are turned into new subgoals.  This is
   1.192 -  in contrast to the regular method @{method insert} which inserts
   1.193 -  closed rule statements.
   1.194 +  Multiple rules may be only given if there is no instantiation; then @{method
   1.195 +  rule_tac} is the same as @{ML resolve_tac} in ML (see @{cite
   1.196 +  "isabelle-implementation"}).
   1.197  
   1.198 -  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise
   1.199 -  from a subgoal.  Note that \<open>\<phi>\<close> may contain schematic
   1.200 -  variables, to abbreviate the intended proposition; the first
   1.201 -  matching subgoal premise will be deleted.  Removing useless premises
   1.202 -  from a subgoal increases its readability and can make search tactics
   1.203 -  run faster.
   1.204 +  \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a
   1.205 +  subgoal; instantiations may be given as well. Note that the scope of
   1.206 +  schematic variables is spread over the main goal statement and rule premises
   1.207 +  are turned into new subgoals. This is in contrast to the regular method
   1.208 +  @{method insert} which inserts closed rule statements.
   1.209  
   1.210 -  \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions
   1.211 -  \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as local premises to a subgoal, and poses the same
   1.212 -  as new subgoals (in the original context).
   1.213 +  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise from a subgoal. Note
   1.214 +  that \<open>\<phi>\<close> may contain schematic variables, to abbreviate the intended
   1.215 +  proposition; the first matching subgoal premise will be deleted. Removing
   1.216 +  useless premises from a subgoal increases its readability and can make
   1.217 +  search tactics run faster.
   1.218  
   1.219 -  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a
   1.220 -  goal according to the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the
   1.221 -  \<^emph>\<open>suffix\<close> of variables.
   1.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
   1.223 +  local premises to a subgoal, and poses the same as new subgoals (in the
   1.224 +  original context).
   1.225  
   1.226 -  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a
   1.227 -  subgoal by \<open>n\<close> positions: from right to left if \<open>n\<close> is
   1.228 -  positive, and from left to right if \<open>n\<close> is negative; the
   1.229 -  default value is 1.
   1.230 +  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a goal according to
   1.231 +  the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the \<^emph>\<open>suffix\<close> of variables.
   1.232 +
   1.233 +  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a subgoal by \<open>n\<close>
   1.234 +  positions: from right to left if \<open>n\<close> is positive, and from left to right if
   1.235 +  \<open>n\<close> is negative; the default value is 1.
   1.236  
   1.237 -  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from
   1.238 -  any ML text of type @{ML_type tactic}.  Apart from the usual ML
   1.239 -  environment and the current proof context, the ML code may refer to
   1.240 -  the locally bound values @{ML_text facts}, which indicates any
   1.241 -  current facts used for forward-chaining.
   1.242 +  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from any ML text of type
   1.243 +  @{ML_type tactic}. Apart from the usual ML environment and the current proof
   1.244 +  context, the ML code may refer to the locally bound values @{ML_text facts},
   1.245 +  which indicates any current facts used for forward-chaining.
   1.246  
   1.247 -  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but
   1.248 -  presents the goal state in its raw internal form, where simultaneous
   1.249 -  subgoals appear as conjunction of the logical framework instead of
   1.250 -  the usual split into several subgoals.  While feature this is useful
   1.251 -  for debugging of complex method definitions, it should not never
   1.252 -  appear in production theories.
   1.253 +  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but presents the goal
   1.254 +  state in its raw internal form, where simultaneous subgoals appear as
   1.255 +  conjunction of the logical framework instead of the usual split into several
   1.256 +  subgoals. While feature this is useful for debugging of complex method
   1.257 +  definitions, it should not never appear in production theories.
   1.258  \<close>
   1.259  
   1.260  end
   1.261 \ No newline at end of file