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