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;
     1 theory Proof_Script
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>Proof scripts\<close>
     6 
     7 text \<open>
     8   Interactive theorem proving is traditionally associated with ``proof
     9   scripts'', but Isabelle/Isar is centered around structured \emph{proof
    10   documents} instead (see also \chref{ch:proofs}).
    11 
    12   Nonetheless, it is possible to emulate proof scripts by sequential
    13   refinements of a proof state in backwards mode, notably with the @{command
    14   apply} command (see \secref{sec:tactic-commands}). There are also various
    15   proof methods that allow to refer to implicit goal state information that
    16   is normally not accessible to structured Isar proofs (see
    17   \secref{sec:tactics}).
    18 \<close>
    19 
    20 
    21 section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
    22 
    23 text \<open>
    24   \begin{matharray}{rcl}
    25     @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    26     @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    27     @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
    28     @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
    29     @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    30     @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    31     @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    32   \end{matharray}
    33 
    34   @{rail \<open>
    35     @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    36     ;
    37     ( @@{command apply} | @@{command apply_end} ) @{syntax method}
    38     ;
    39     @@{command defer} @{syntax nat}?
    40     ;
    41     @@{command prefer} @{syntax nat}
    42   \<close>}
    43 
    44   \begin{description}
    45 
    46   \item @{command "supply"} supports fact definitions during goal
    47   refinement: it is similar to @{command "note"}, but it operates in
    48   backwards mode and does not have any impact on chained facts.
    49 
    50   \item @{command "apply"}~@{text m} applies proof method @{text m} in
    51   initial position, but unlike @{command "proof"} it retains ``@{text
    52   "proof(prove)"}'' mode.  Thus consecutive method applications may be
    53   given just as in tactic scripts.
    54 
    55   Facts are passed to @{text m} as indicated by the goal's
    56   forward-chain mode, and are \emph{consumed} afterwards.  Thus any
    57   further @{command "apply"} command would always work in a purely
    58   backward manner.
    59 
    60   \item @{command "apply_end"}~@{text "m"} applies proof method @{text
    61   m} as if in terminal position.  Basically, this simulates a
    62   multi-step tactic script for @{command "qed"}, but may be given
    63   anywhere within the proof body.
    64 
    65   No facts are passed to @{text m} here.  Furthermore, the static
    66   context is that of the enclosing goal (as for actual @{command
    67   "qed"}).  Thus the proof method may not refer to any assumptions
    68   introduced in the current body, for example.
    69 
    70   \item @{command "done"} completes a proof script, provided that the
    71   current goal state is solved completely.  Note that actual
    72   structured proof commands (e.g.\ ``@{command "."}'' or @{command
    73   "sorry"}) may be used to conclude proof scripts as well.
    74 
    75   \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
    76   shuffle the list of pending goals: @{command "defer"} puts off
    77   sub-goal @{text n} to the end of the list (@{text "n = 1"} by
    78   default), while @{command "prefer"} brings sub-goal @{text n} to the
    79   front.
    80 
    81   \item @{command "back"} does back-tracking over the result sequence
    82   of the latest proof command.  Any proof command may return multiple
    83   results, and this command explores the possibilities step-by-step.
    84   It is mainly useful for experimentation and interactive exploration,
    85   and should be avoided in finished proofs.
    86 
    87   \end{description}
    88 \<close>
    89 
    90 
    91 section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
    92 
    93 text \<open>
    94   The following improper proof methods emulate traditional tactics.
    95   These admit direct access to the goal state, which is normally
    96   considered harmful!  In particular, this may involve both numbered
    97   goal addressing (default 1), and dynamic instantiation within the
    98   scope of some subgoal.
    99 
   100   \begin{warn}
   101     Dynamic instantiations refer to universally quantified parameters
   102     of a subgoal (the dynamic context) rather than fixed variables and
   103     term abbreviations of a (static) Isar context.
   104   \end{warn}
   105 
   106   Tactic emulation methods, unlike their ML counterparts, admit
   107   simultaneous instantiation from both dynamic and static contexts.
   108   If names occur in both contexts goal parameters hide locally fixed
   109   variables.  Likewise, schematic variables refer to term
   110   abbreviations, if present in the static context.  Otherwise the
   111   schematic variable is interpreted as a schematic variable and left
   112   to be solved by unification with certain parts of the subgoal.
   113 
   114   Note that the tactic emulation proof methods in Isabelle/Isar are
   115   consistently named @{text foo_tac}.  Note also that variable names
   116   occurring on left hand sides of instantiations must be preceded by a
   117   question mark if they coincide with a keyword or contain dots.  This
   118   is consistent with the attribute @{attribute "where"} (see
   119   \secref{sec:pure-meth-att}).
   120 
   121   \begin{matharray}{rcl}
   122     @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   123     @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   124     @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   125     @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   126     @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
   127     @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
   128     @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
   129     @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
   130     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
   131     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
   132     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   133   \end{matharray}
   134 
   135   @{rail \<open>
   136     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   137       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
   138     (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
   139     ;
   140     @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
   141     ;
   142     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
   143     ;
   144     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
   145     ;
   146     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
   147     ;
   148     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   149   \<close>}
   150 
   151 \begin{description}
   152 
   153   \item @{method rule_tac} etc. do resolution of rules with explicit
   154   instantiation.  This works the same way as the ML tactics @{ML
   155   Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
   156 
   157   Multiple rules may be only given if there is no instantiation; then
   158   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   159   @{cite "isabelle-implementation"}).
   160 
   161   \item @{method cut_tac} inserts facts into the proof state as
   162   assumption of a subgoal; instantiations may be given as well.  Note
   163   that the scope of schematic variables is spread over the main goal
   164   statement and rule premises are turned into new subgoals.  This is
   165   in contrast to the regular method @{method insert} which inserts
   166   closed rule statements.
   167 
   168   \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
   169   from a subgoal.  Note that @{text \<phi>} may contain schematic
   170   variables, to abbreviate the intended proposition; the first
   171   matching subgoal premise will be deleted.  Removing useless premises
   172   from a subgoal increases its readability and can make search tactics
   173   run faster.
   174 
   175   \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
   176   @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
   177   as new subgoals (in the original context).
   178 
   179   \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   180   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   181   \emph{suffix} of variables.
   182 
   183   \item @{method rotate_tac}~@{text n} rotates the premises of a
   184   subgoal by @{text n} positions: from right to left if @{text n} is
   185   positive, and from left to right if @{text n} is negative; the
   186   default value is 1.
   187 
   188   \item @{method tactic}~@{text "text"} produces a proof method from
   189   any ML text of type @{ML_type tactic}.  Apart from the usual ML
   190   environment and the current proof context, the ML code may refer to
   191   the locally bound values @{ML_text facts}, which indicates any
   192   current facts used for forward-chaining.
   193 
   194   \item @{method raw_tactic} is similar to @{method tactic}, but
   195   presents the goal state in its raw internal form, where simultaneous
   196   subgoals appear as conjunction of the logical framework instead of
   197   the usual split into several subgoals.  While feature this is useful
   198   for debugging of complex method definitions, it should not never
   199   appear in production theories.
   200 
   201   \end{description}
   202 \<close>
   203 
   204 end