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