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.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.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