src/Doc/Isar_Ref/Proof_Script.thy
author wenzelm
Mon Jun 15 14:10:41 2015 +0200 (2015-06-15)
changeset 60484 98ee86354354
child 60631 441fdbfbb2d3
permissions -rw-r--r--
moved sections;
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@60484
    91
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
wenzelm@60484
    92
wenzelm@60484
    93
text \<open>
wenzelm@60484
    94
  The following improper proof methods emulate traditional tactics.
wenzelm@60484
    95
  These admit direct access to the goal state, which is normally
wenzelm@60484
    96
  considered harmful!  In particular, this may involve both numbered
wenzelm@60484
    97
  goal addressing (default 1), and dynamic instantiation within the
wenzelm@60484
    98
  scope of some subgoal.
wenzelm@60484
    99
wenzelm@60484
   100
  \begin{warn}
wenzelm@60484
   101
    Dynamic instantiations refer to universally quantified parameters
wenzelm@60484
   102
    of a subgoal (the dynamic context) rather than fixed variables and
wenzelm@60484
   103
    term abbreviations of a (static) Isar context.
wenzelm@60484
   104
  \end{warn}
wenzelm@60484
   105
wenzelm@60484
   106
  Tactic emulation methods, unlike their ML counterparts, admit
wenzelm@60484
   107
  simultaneous instantiation from both dynamic and static contexts.
wenzelm@60484
   108
  If names occur in both contexts goal parameters hide locally fixed
wenzelm@60484
   109
  variables.  Likewise, schematic variables refer to term
wenzelm@60484
   110
  abbreviations, if present in the static context.  Otherwise the
wenzelm@60484
   111
  schematic variable is interpreted as a schematic variable and left
wenzelm@60484
   112
  to be solved by unification with certain parts of the subgoal.
wenzelm@60484
   113
wenzelm@60484
   114
  Note that the tactic emulation proof methods in Isabelle/Isar are
wenzelm@60484
   115
  consistently named @{text foo_tac}.  Note also that variable names
wenzelm@60484
   116
  occurring on left hand sides of instantiations must be preceded by a
wenzelm@60484
   117
  question mark if they coincide with a keyword or contain dots.  This
wenzelm@60484
   118
  is consistent with the attribute @{attribute "where"} (see
wenzelm@60484
   119
  \secref{sec:pure-meth-att}).
wenzelm@60484
   120
wenzelm@60484
   121
  \begin{matharray}{rcl}
wenzelm@60484
   122
    @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   123
    @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   124
    @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   125
    @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   126
    @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   127
    @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   128
    @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   129
    @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   130
    @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   131
    @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   132
    @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
wenzelm@60484
   133
  \end{matharray}
wenzelm@60484
   134
wenzelm@60484
   135
  @{rail \<open>
wenzelm@60484
   136
    (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
wenzelm@60484
   137
      @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
wenzelm@60484
   138
    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
wenzelm@60484
   139
    ;
wenzelm@60484
   140
    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
wenzelm@60484
   141
    ;
wenzelm@60484
   142
    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
wenzelm@60484
   143
    ;
wenzelm@60484
   144
    @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
wenzelm@60484
   145
    ;
wenzelm@60484
   146
    @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
wenzelm@60484
   147
    ;
wenzelm@60484
   148
    (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
wenzelm@60484
   149
  \<close>}
wenzelm@60484
   150
wenzelm@60484
   151
\begin{description}
wenzelm@60484
   152
wenzelm@60484
   153
  \item @{method rule_tac} etc. do resolution of rules with explicit
wenzelm@60484
   154
  instantiation.  This works the same way as the ML tactics @{ML
wenzelm@60484
   155
  Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
wenzelm@60484
   156
wenzelm@60484
   157
  Multiple rules may be only given if there is no instantiation; then
wenzelm@60484
   158
  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
wenzelm@60484
   159
  @{cite "isabelle-implementation"}).
wenzelm@60484
   160
wenzelm@60484
   161
  \item @{method cut_tac} inserts facts into the proof state as
wenzelm@60484
   162
  assumption of a subgoal; instantiations may be given as well.  Note
wenzelm@60484
   163
  that the scope of schematic variables is spread over the main goal
wenzelm@60484
   164
  statement and rule premises are turned into new subgoals.  This is
wenzelm@60484
   165
  in contrast to the regular method @{method insert} which inserts
wenzelm@60484
   166
  closed rule statements.
wenzelm@60484
   167
wenzelm@60484
   168
  \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
wenzelm@60484
   169
  from a subgoal.  Note that @{text \<phi>} may contain schematic
wenzelm@60484
   170
  variables, to abbreviate the intended proposition; the first
wenzelm@60484
   171
  matching subgoal premise will be deleted.  Removing useless premises
wenzelm@60484
   172
  from a subgoal increases its readability and can make search tactics
wenzelm@60484
   173
  run faster.
wenzelm@60484
   174
wenzelm@60484
   175
  \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
wenzelm@60484
   176
  @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
wenzelm@60484
   177
  as new subgoals (in the original context).
wenzelm@60484
   178
wenzelm@60484
   179
  \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
wenzelm@60484
   180
  goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
wenzelm@60484
   181
  \emph{suffix} of variables.
wenzelm@60484
   182
wenzelm@60484
   183
  \item @{method rotate_tac}~@{text n} rotates the premises of a
wenzelm@60484
   184
  subgoal by @{text n} positions: from right to left if @{text n} is
wenzelm@60484
   185
  positive, and from left to right if @{text n} is negative; the
wenzelm@60484
   186
  default value is 1.
wenzelm@60484
   187
wenzelm@60484
   188
  \item @{method tactic}~@{text "text"} produces a proof method from
wenzelm@60484
   189
  any ML text of type @{ML_type tactic}.  Apart from the usual ML
wenzelm@60484
   190
  environment and the current proof context, the ML code may refer to
wenzelm@60484
   191
  the locally bound values @{ML_text facts}, which indicates any
wenzelm@60484
   192
  current facts used for forward-chaining.
wenzelm@60484
   193
wenzelm@60484
   194
  \item @{method raw_tactic} is similar to @{method tactic}, but
wenzelm@60484
   195
  presents the goal state in its raw internal form, where simultaneous
wenzelm@60484
   196
  subgoals appear as conjunction of the logical framework instead of
wenzelm@60484
   197
  the usual split into several subgoals.  While feature this is useful
wenzelm@60484
   198
  for debugging of complex method definitions, it should not never
wenzelm@60484
   199
  appear in production theories.
wenzelm@60484
   200
wenzelm@60484
   201
  \end{description}
wenzelm@60484
   202
\<close>
wenzelm@60484
   203
wenzelm@60484
   204
end