src/Doc/Isar_Ref/Proof_Script.thy
author nipkow
Wed Jan 10 15:25:09 2018 +0100 (21 months ago)
changeset 67399 eab6ce8368fa
parent 63531 847eefdca90d
child 69597 ff784d5a5bfb
permissions -rw-r--r--
ran isabelle update_op on all sources
wenzelm@61656
     1
(*:maxLineLen=78:*)
wenzelm@61656
     2
wenzelm@60484
     3
theory Proof_Script
wenzelm@63531
     4
  imports Main Base
wenzelm@60484
     5
begin
wenzelm@60484
     6
wenzelm@60484
     7
chapter \<open>Proof scripts\<close>
wenzelm@60484
     8
wenzelm@60484
     9
text \<open>
wenzelm@60484
    10
  Interactive theorem proving is traditionally associated with ``proof
wenzelm@61477
    11
  scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof
wenzelm@61477
    12
  documents\<close> instead (see also \chref{ch:proofs}).
wenzelm@60484
    13
wenzelm@60484
    14
  Nonetheless, it is possible to emulate proof scripts by sequential
wenzelm@60484
    15
  refinements of a proof state in backwards mode, notably with the @{command
wenzelm@62269
    16
  apply} command (see \secref{sec:tactic-commands}).
wenzelm@62269
    17
wenzelm@62269
    18
  There are also various proof methods that allow to refer to implicit goal
wenzelm@62269
    19
  state information that is not accessible to structured Isar proofs (see
wenzelm@62269
    20
  \secref{sec:tactics}). Note that the @{command subgoal}
wenzelm@62269
    21
  (\secref{sec:subgoal}) command usually eliminates the need for implicit goal
wenzelm@62269
    22
  state references.
wenzelm@60484
    23
\<close>
wenzelm@60484
    24
wenzelm@60484
    25
wenzelm@60484
    26
section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
wenzelm@60484
    27
wenzelm@60484
    28
text \<open>
wenzelm@60484
    29
  \begin{matharray}{rcl}
wenzelm@61493
    30
    @{command_def "supply"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
    31
    @{command_def "apply"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
wenzelm@61493
    32
    @{command_def "apply_end"}\<open>\<^sup>*\<close> & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
wenzelm@61493
    33
    @{command_def "done"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
wenzelm@61493
    34
    @{command_def "defer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
wenzelm@61493
    35
    @{command_def "prefer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
wenzelm@61493
    36
    @{command_def "back"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
wenzelm@60484
    37
  \end{matharray}
wenzelm@60484
    38
wenzelm@60484
    39
  @{rail \<open>
wenzelm@62969
    40
    @@{command supply} (@{syntax thmdef}? @{syntax thms} + @'and')
wenzelm@60484
    41
    ;
wenzelm@60484
    42
    ( @@{command apply} | @@{command apply_end} ) @{syntax method}
wenzelm@60484
    43
    ;
wenzelm@60484
    44
    @@{command defer} @{syntax nat}?
wenzelm@60484
    45
    ;
wenzelm@60484
    46
    @@{command prefer} @{syntax nat}
wenzelm@60484
    47
  \<close>}
wenzelm@60484
    48
wenzelm@61657
    49
  \<^descr> @{command "supply"} supports fact definitions during goal refinement: it
wenzelm@61657
    50
  is similar to @{command "note"}, but it operates in backwards mode and does
wenzelm@61657
    51
  not have any impact on chained facts.
wenzelm@60484
    52
wenzelm@61657
    53
  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in initial position, but
wenzelm@61657
    54
  unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus
wenzelm@61657
    55
  consecutive method applications may be given just as in tactic scripts.
wenzelm@60484
    56
wenzelm@61657
    57
  Facts are passed to \<open>m\<close> as indicated by the goal's forward-chain mode, and
wenzelm@61657
    58
  are \<^emph>\<open>consumed\<close> afterwards. Thus any further @{command "apply"} command
wenzelm@61657
    59
  would always work in a purely backward manner.
wenzelm@60484
    60
wenzelm@61657
    61
  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal
wenzelm@61657
    62
  position. Basically, this simulates a multi-step tactic script for @{command
wenzelm@61657
    63
  "qed"}, but may be given anywhere within the proof body.
wenzelm@60484
    64
wenzelm@61657
    65
  No facts are passed to \<open>m\<close> here. Furthermore, the static context is that of
wenzelm@61657
    66
  the enclosing goal (as for actual @{command "qed"}). Thus the proof method
wenzelm@61657
    67
  may not refer to any assumptions introduced in the current body, for
wenzelm@61657
    68
  example.
wenzelm@60484
    69
wenzelm@61657
    70
  \<^descr> @{command "done"} completes a proof script, provided that the current goal
wenzelm@61657
    71
  state is solved completely. Note that actual structured proof commands
wenzelm@61657
    72
  (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude
wenzelm@61657
    73
  proof scripts as well.
wenzelm@60484
    74
wenzelm@61657
    75
  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> shuffle the list of
wenzelm@61657
    76
  pending goals: @{command "defer"} puts off sub-goal \<open>n\<close> to the end of the
wenzelm@61657
    77
  list (\<open>n = 1\<close> by default), while @{command "prefer"} brings sub-goal \<open>n\<close> to
wenzelm@61657
    78
  the front.
wenzelm@60484
    79
wenzelm@61657
    80
  \<^descr> @{command "back"} does back-tracking over the result sequence of the
wenzelm@61657
    81
  latest proof command. Any proof command may return multiple results, and
wenzelm@61657
    82
  this command explores the possibilities step-by-step. It is mainly useful
wenzelm@61657
    83
  for experimentation and interactive exploration, and should be avoided in
wenzelm@61657
    84
  finished proofs.
wenzelm@60484
    85
\<close>
wenzelm@60484
    86
wenzelm@60484
    87
wenzelm@62269
    88
section \<open>Explicit subgoal structure \label{sec:subgoal}\<close>
wenzelm@60631
    89
wenzelm@60631
    90
text \<open>
wenzelm@60631
    91
  \begin{matharray}{rcl}
wenzelm@61493
    92
    @{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
wenzelm@60631
    93
  \end{matharray}
wenzelm@60631
    94
wenzelm@60631
    95
  @{rail \<open>
wenzelm@60631
    96
    @@{command subgoal} @{syntax thmbind}? prems? params?
wenzelm@60631
    97
    ;
wenzelm@60631
    98
    prems: @'premises' @{syntax thmbind}?
wenzelm@60631
    99
    ;
wenzelm@60631
   100
    params: @'for' '\<dots>'? (('_' | @{syntax name})+)
wenzelm@60631
   101
  \<close>}
wenzelm@60631
   102
wenzelm@61439
   103
  \<^descr> @{command "subgoal"} allows to impose some structure on backward
wenzelm@60631
   104
  refinements, to avoid proof scripts degenerating into long of @{command
wenzelm@60631
   105
  apply} sequences.
wenzelm@60631
   106
wenzelm@60631
   107
  The current goal state, which is essentially a hidden part of the Isar/VM
wenzelm@61866
   108
  configuration, is turned into a proof context and remaining conclusion.
wenzelm@61866
   109
  This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in
wenzelm@60631
   110
  structured proofs, but the text of the parameters, premises and conclusion
wenzelm@60631
   111
  is not given explicitly.
wenzelm@60631
   112
wenzelm@61657
   113
  Goal parameters may be specified separately, in order to allow referring to
wenzelm@61657
   114
  them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x y z\<close>''
wenzelm@61657
   115
  names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword "for"}~\<open>\<dots> x y z\<close>''
wenzelm@61657
   116
  names a \<^emph>\<open>suffix\<close> of goal parameters. The latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol
wenzelm@61657
   117
  as notation. Parameter positions may be skipped via dummies (underscore).
wenzelm@61657
   118
  Unspecified names remain internal, and thus inaccessible in the proof text.
wenzelm@60631
   119
wenzelm@61657
   120
  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that goal
wenzelm@61657
   121
  premises should be turned into assumptions of the context (otherwise the
wenzelm@61657
   122
  remaining conclusion is a Pure implication). The fact name and attributes
wenzelm@61657
   123
  are optional; the particular name ``\<open>prems\<close>'' is a common convention for the
wenzelm@61657
   124
  premises of an arbitrary goal context in proof scripts.
wenzelm@60631
   125
wenzelm@61657
   126
  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result of a
wenzelm@61657
   127
  proven subgoal. Thus it may be re-used in further reasoning, similar to the
wenzelm@61657
   128
  result of @{command show} in structured Isar proofs.
wenzelm@60631
   129
wenzelm@60631
   130
wenzelm@60631
   131
  Here are some abstract examples:
wenzelm@60631
   132
\<close>
wenzelm@60631
   133
wenzelm@60631
   134
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
wenzelm@60631
   135
  and "\<And>u v. X u \<Longrightarrow> Y v"
wenzelm@62271
   136
  subgoal \<proof>
wenzelm@62271
   137
  subgoal \<proof>
wenzelm@60631
   138
  done
wenzelm@60631
   139
wenzelm@60631
   140
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
wenzelm@60631
   141
  and "\<And>u v. X u \<Longrightarrow> Y v"
wenzelm@62271
   142
  subgoal for x y z \<proof>
wenzelm@62271
   143
  subgoal for u v \<proof>
wenzelm@60631
   144
  done
wenzelm@60631
   145
wenzelm@60631
   146
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
wenzelm@60631
   147
  and "\<And>u v. X u \<Longrightarrow> Y v"
wenzelm@60631
   148
  subgoal premises for x y z
wenzelm@60631
   149
    using \<open>A x\<close> \<open>B y\<close>
wenzelm@62271
   150
    \<proof>
wenzelm@60631
   151
  subgoal premises for u v
wenzelm@60631
   152
    using \<open>X u\<close>
wenzelm@62271
   153
    \<proof>
wenzelm@60631
   154
  done
wenzelm@60631
   155
wenzelm@60631
   156
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
wenzelm@60631
   157
  and "\<And>u v. X u \<Longrightarrow> Y v"
wenzelm@60631
   158
  subgoal r premises prems for x y z
wenzelm@60631
   159
  proof -
wenzelm@60631
   160
    have "A x" by (fact prems)
wenzelm@60631
   161
    moreover have "B y" by (fact prems)
wenzelm@62271
   162
    ultimately show ?thesis \<proof>
wenzelm@60631
   163
  qed
wenzelm@60631
   164
  subgoal premises prems for u v
wenzelm@60631
   165
  proof -
wenzelm@60631
   166
    have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
wenzelm@60631
   167
    moreover
wenzelm@60631
   168
    have "X u" by (fact prems)
wenzelm@62271
   169
    ultimately show ?thesis \<proof>
wenzelm@60631
   170
  qed
wenzelm@60631
   171
  done
wenzelm@60631
   172
wenzelm@60631
   173
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
wenzelm@60631
   174
  subgoal premises prems for \<dots> z
wenzelm@60631
   175
  proof -
wenzelm@62271
   176
    from prems show "C z" \<proof>
wenzelm@60631
   177
  qed
wenzelm@60631
   178
  done
wenzelm@60631
   179
wenzelm@60631
   180
wenzelm@60484
   181
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
wenzelm@60484
   182
wenzelm@60484
   183
text \<open>
wenzelm@61657
   184
  The following improper proof methods emulate traditional tactics. These
wenzelm@61657
   185
  admit direct access to the goal state, which is normally considered harmful!
wenzelm@61657
   186
  In particular, this may involve both numbered goal addressing (default 1),
wenzelm@61657
   187
  and dynamic instantiation within the scope of some subgoal.
wenzelm@60484
   188
wenzelm@60484
   189
  \begin{warn}
wenzelm@61657
   190
    Dynamic instantiations refer to universally quantified parameters of a
wenzelm@61657
   191
    subgoal (the dynamic context) rather than fixed variables and term
wenzelm@61657
   192
    abbreviations of a (static) Isar context.
wenzelm@60484
   193
  \end{warn}
wenzelm@60484
   194
wenzelm@61657
   195
  Tactic emulation methods, unlike their ML counterparts, admit simultaneous
wenzelm@61657
   196
  instantiation from both dynamic and static contexts. If names occur in both
wenzelm@61657
   197
  contexts goal parameters hide locally fixed variables. Likewise, schematic
wenzelm@61657
   198
  variables refer to term abbreviations, if present in the static context.
wenzelm@61657
   199
  Otherwise the schematic variable is interpreted as a schematic variable and
wenzelm@61657
   200
  left to be solved by unification with certain parts of the subgoal.
wenzelm@60484
   201
wenzelm@60484
   202
  Note that the tactic emulation proof methods in Isabelle/Isar are
wenzelm@61657
   203
  consistently named \<open>foo_tac\<close>. Note also that variable names occurring on
wenzelm@61657
   204
  left hand sides of instantiations must be preceded by a question mark if
wenzelm@61657
   205
  they coincide with a keyword or contain dots. This is consistent with the
wenzelm@61657
   206
  attribute @{attribute "where"} (see \secref{sec:pure-meth-att}).
wenzelm@60484
   207
wenzelm@60484
   208
  \begin{matharray}{rcl}
wenzelm@61493
   209
    @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   210
    @{method_def erule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   211
    @{method_def drule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   212
    @{method_def frule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   213
    @{method_def cut_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   214
    @{method_def thin_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   215
    @{method_def subgoal_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   216
    @{method_def rename_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   217
    @{method_def rotate_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   218
    @{method_def tactic}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@61493
   219
    @{method_def raw_tactic}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
wenzelm@60484
   220
  \end{matharray}
wenzelm@60484
   221
wenzelm@60484
   222
  @{rail \<open>
wenzelm@60484
   223
    (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
wenzelm@60484
   224
      @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
wenzelm@62969
   225
    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thm} | @{syntax thms} )
wenzelm@60484
   226
    ;
wenzelm@60484
   227
    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
wenzelm@60484
   228
    ;
wenzelm@60484
   229
    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
wenzelm@60484
   230
    ;
wenzelm@60484
   231
    @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
wenzelm@60484
   232
    ;
wenzelm@60484
   233
    @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
wenzelm@60484
   234
    ;
wenzelm@60484
   235
    (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
wenzelm@60484
   236
  \<close>}
wenzelm@60484
   237
wenzelm@61439
   238
  \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
wenzelm@61657
   239
  instantiation. This works the same way as the ML tactics @{ML
wenzelm@60484
   240
  Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
wenzelm@60484
   241
wenzelm@61657
   242
  Multiple rules may be only given if there is no instantiation; then @{method
wenzelm@61657
   243
  rule_tac} is the same as @{ML resolve_tac} in ML (see @{cite
wenzelm@61657
   244
  "isabelle-implementation"}).
wenzelm@60484
   245
wenzelm@61657
   246
  \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a
wenzelm@61657
   247
  subgoal; instantiations may be given as well. Note that the scope of
wenzelm@61657
   248
  schematic variables is spread over the main goal statement and rule premises
wenzelm@61657
   249
  are turned into new subgoals. This is in contrast to the regular method
wenzelm@61657
   250
  @{method insert} which inserts closed rule statements.
wenzelm@60484
   251
wenzelm@61657
   252
  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise from a subgoal. Note
wenzelm@61657
   253
  that \<open>\<phi>\<close> may contain schematic variables, to abbreviate the intended
wenzelm@61657
   254
  proposition; the first matching subgoal premise will be deleted. Removing
wenzelm@61657
   255
  useless premises from a subgoal increases its readability and can make
wenzelm@61657
   256
  search tactics run faster.
wenzelm@60484
   257
wenzelm@61657
   258
  \<^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
wenzelm@61657
   259
  local premises to a subgoal, and poses the same as new subgoals (in the
wenzelm@61657
   260
  original context).
wenzelm@60484
   261
wenzelm@61657
   262
  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a goal according to
wenzelm@61657
   263
  the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the \<^emph>\<open>suffix\<close> of variables.
wenzelm@61657
   264
wenzelm@61657
   265
  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a subgoal by \<open>n\<close>
wenzelm@61657
   266
  positions: from right to left if \<open>n\<close> is positive, and from left to right if
wenzelm@61657
   267
  \<open>n\<close> is negative; the default value is 1.
wenzelm@60484
   268
wenzelm@61657
   269
  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from any ML text of type
wenzelm@61657
   270
  @{ML_type tactic}. Apart from the usual ML environment and the current proof
wenzelm@61657
   271
  context, the ML code may refer to the locally bound values @{ML_text facts},
wenzelm@61657
   272
  which indicates any current facts used for forward-chaining.
wenzelm@60484
   273
wenzelm@61657
   274
  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but presents the goal
wenzelm@61657
   275
  state in its raw internal form, where simultaneous subgoals appear as
wenzelm@61657
   276
  conjunction of the logical framework instead of the usual split into several
wenzelm@61657
   277
  subgoals. While feature this is useful for debugging of complex method
wenzelm@61657
   278
  definitions, it should not never appear in production theories.
wenzelm@60484
   279
\<close>
wenzelm@60484
   280
nipkow@67399
   281
end