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