src/Doc/Isar_Ref/Proof_Script.thy
changeset 60484 98ee86354354
child 60631 441fdbfbb2d3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Mon Jun 15 14:10:41 2015 +0200
     1.3 @@ -0,0 +1,204 @@
     1.4 +theory Proof_Script
     1.5 +imports Base Main
     1.6 +begin
     1.7 +
     1.8 +chapter \<open>Proof scripts\<close>
     1.9 +
    1.10 +text \<open>
    1.11 +  Interactive theorem proving is traditionally associated with ``proof
    1.12 +  scripts'', but Isabelle/Isar is centered around structured \emph{proof
    1.13 +  documents} instead (see also \chref{ch:proofs}).
    1.14 +
    1.15 +  Nonetheless, it is possible to emulate proof scripts by sequential
    1.16 +  refinements of a proof state in backwards mode, notably with the @{command
    1.17 +  apply} command (see \secref{sec:tactic-commands}). There are also various
    1.18 +  proof methods that allow to refer to implicit goal state information that
    1.19 +  is normally not accessible to structured Isar proofs (see
    1.20 +  \secref{sec:tactics}).
    1.21 +\<close>
    1.22 +
    1.23 +
    1.24 +section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
    1.25 +
    1.26 +text \<open>
    1.27 +  \begin{matharray}{rcl}
    1.28 +    @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    1.29 +    @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    1.30 +    @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
    1.31 +    @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
    1.32 +    @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    1.33 +    @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    1.34 +    @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    1.35 +  \end{matharray}
    1.36 +
    1.37 +  @{rail \<open>
    1.38 +    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    1.39 +    ;
    1.40 +    ( @@{command apply} | @@{command apply_end} ) @{syntax method}
    1.41 +    ;
    1.42 +    @@{command defer} @{syntax nat}?
    1.43 +    ;
    1.44 +    @@{command prefer} @{syntax nat}
    1.45 +  \<close>}
    1.46 +
    1.47 +  \begin{description}
    1.48 +
    1.49 +  \item @{command "supply"} supports fact definitions during goal
    1.50 +  refinement: it is similar to @{command "note"}, but it operates in
    1.51 +  backwards mode and does not have any impact on chained facts.
    1.52 +
    1.53 +  \item @{command "apply"}~@{text m} applies proof method @{text m} in
    1.54 +  initial position, but unlike @{command "proof"} it retains ``@{text
    1.55 +  "proof(prove)"}'' mode.  Thus consecutive method applications may be
    1.56 +  given just as in tactic scripts.
    1.57 +
    1.58 +  Facts are passed to @{text m} as indicated by the goal's
    1.59 +  forward-chain mode, and are \emph{consumed} afterwards.  Thus any
    1.60 +  further @{command "apply"} command would always work in a purely
    1.61 +  backward manner.
    1.62 +
    1.63 +  \item @{command "apply_end"}~@{text "m"} applies proof method @{text
    1.64 +  m} as if in terminal position.  Basically, this simulates a
    1.65 +  multi-step tactic script for @{command "qed"}, but may be given
    1.66 +  anywhere within the proof body.
    1.67 +
    1.68 +  No facts are passed to @{text m} here.  Furthermore, the static
    1.69 +  context is that of the enclosing goal (as for actual @{command
    1.70 +  "qed"}).  Thus the proof method may not refer to any assumptions
    1.71 +  introduced in the current body, for example.
    1.72 +
    1.73 +  \item @{command "done"} completes a proof script, provided that the
    1.74 +  current goal state is solved completely.  Note that actual
    1.75 +  structured proof commands (e.g.\ ``@{command "."}'' or @{command
    1.76 +  "sorry"}) may be used to conclude proof scripts as well.
    1.77 +
    1.78 +  \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
    1.79 +  shuffle the list of pending goals: @{command "defer"} puts off
    1.80 +  sub-goal @{text n} to the end of the list (@{text "n = 1"} by
    1.81 +  default), while @{command "prefer"} brings sub-goal @{text n} to the
    1.82 +  front.
    1.83 +
    1.84 +  \item @{command "back"} does back-tracking over the result sequence
    1.85 +  of the latest proof command.  Any proof command may return multiple
    1.86 +  results, and this command explores the possibilities step-by-step.
    1.87 +  It is mainly useful for experimentation and interactive exploration,
    1.88 +  and should be avoided in finished proofs.
    1.89 +
    1.90 +  \end{description}
    1.91 +\<close>
    1.92 +
    1.93 +
    1.94 +section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
    1.95 +
    1.96 +text \<open>
    1.97 +  The following improper proof methods emulate traditional tactics.
    1.98 +  These admit direct access to the goal state, which is normally
    1.99 +  considered harmful!  In particular, this may involve both numbered
   1.100 +  goal addressing (default 1), and dynamic instantiation within the
   1.101 +  scope of some subgoal.
   1.102 +
   1.103 +  \begin{warn}
   1.104 +    Dynamic instantiations refer to universally quantified parameters
   1.105 +    of a subgoal (the dynamic context) rather than fixed variables and
   1.106 +    term abbreviations of a (static) Isar context.
   1.107 +  \end{warn}
   1.108 +
   1.109 +  Tactic emulation methods, unlike their ML counterparts, admit
   1.110 +  simultaneous instantiation from both dynamic and static contexts.
   1.111 +  If names occur in both contexts goal parameters hide locally fixed
   1.112 +  variables.  Likewise, schematic variables refer to term
   1.113 +  abbreviations, if present in the static context.  Otherwise the
   1.114 +  schematic variable is interpreted as a schematic variable and left
   1.115 +  to be solved by unification with certain parts of the subgoal.
   1.116 +
   1.117 +  Note that the tactic emulation proof methods in Isabelle/Isar are
   1.118 +  consistently named @{text foo_tac}.  Note also that variable names
   1.119 +  occurring on left hand sides of instantiations must be preceded by a
   1.120 +  question mark if they coincide with a keyword or contain dots.  This
   1.121 +  is consistent with the attribute @{attribute "where"} (see
   1.122 +  \secref{sec:pure-meth-att}).
   1.123 +
   1.124 +  \begin{matharray}{rcl}
   1.125 +    @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.126 +    @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.127 +    @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.128 +    @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.129 +    @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.130 +    @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.131 +    @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.132 +    @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.133 +    @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
   1.134 +    @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
   1.135 +    @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   1.136 +  \end{matharray}
   1.137 +
   1.138 +  @{rail \<open>
   1.139 +    (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   1.140 +      @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
   1.141 +    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
   1.142 +    ;
   1.143 +    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
   1.144 +    ;
   1.145 +    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
   1.146 +    ;
   1.147 +    @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
   1.148 +    ;
   1.149 +    @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
   1.150 +    ;
   1.151 +    (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   1.152 +  \<close>}
   1.153 +
   1.154 +\begin{description}
   1.155 +
   1.156 +  \item @{method rule_tac} etc. do resolution of rules with explicit
   1.157 +  instantiation.  This works the same way as the ML tactics @{ML
   1.158 +  Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
   1.159 +
   1.160 +  Multiple rules may be only given if there is no instantiation; then
   1.161 +  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   1.162 +  @{cite "isabelle-implementation"}).
   1.163 +
   1.164 +  \item @{method cut_tac} inserts facts into the proof state as
   1.165 +  assumption of a subgoal; instantiations may be given as well.  Note
   1.166 +  that the scope of schematic variables is spread over the main goal
   1.167 +  statement and rule premises are turned into new subgoals.  This is
   1.168 +  in contrast to the regular method @{method insert} which inserts
   1.169 +  closed rule statements.
   1.170 +
   1.171 +  \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
   1.172 +  from a subgoal.  Note that @{text \<phi>} may contain schematic
   1.173 +  variables, to abbreviate the intended proposition; the first
   1.174 +  matching subgoal premise will be deleted.  Removing useless premises
   1.175 +  from a subgoal increases its readability and can make search tactics
   1.176 +  run faster.
   1.177 +
   1.178 +  \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
   1.179 +  @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
   1.180 +  as new subgoals (in the original context).
   1.181 +
   1.182 +  \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   1.183 +  goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   1.184 +  \emph{suffix} of variables.
   1.185 +
   1.186 +  \item @{method rotate_tac}~@{text n} rotates the premises of a
   1.187 +  subgoal by @{text n} positions: from right to left if @{text n} is
   1.188 +  positive, and from left to right if @{text n} is negative; the
   1.189 +  default value is 1.
   1.190 +
   1.191 +  \item @{method tactic}~@{text "text"} produces a proof method from
   1.192 +  any ML text of type @{ML_type tactic}.  Apart from the usual ML
   1.193 +  environment and the current proof context, the ML code may refer to
   1.194 +  the locally bound values @{ML_text facts}, which indicates any
   1.195 +  current facts used for forward-chaining.
   1.196 +
   1.197 +  \item @{method raw_tactic} is similar to @{method tactic}, but
   1.198 +  presents the goal state in its raw internal form, where simultaneous
   1.199 +  subgoals appear as conjunction of the logical framework instead of
   1.200 +  the usual split into several subgoals.  While feature this is useful
   1.201 +  for debugging of complex method definitions, it should not never
   1.202 +  appear in production theories.
   1.203 +
   1.204 +  \end{description}
   1.205 +\<close>
   1.206 +
   1.207 +end
   1.208 \ No newline at end of file