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