src/Doc/Isar_Ref/Proof_Script.thy
author wenzelm
Sun Oct 18 22:57:09 2015 +0200 (2015-10-18)
changeset 61477 e467ae7aa808
parent 61458 987533262fc2
child 61493 0debd22f0c0e
permissions -rw-r--r--
more control symbols;
     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>\<open>proof
    10   documents\<close> 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   \<^descr> @{command "supply"} supports fact definitions during goal
    45   refinement: it is similar to @{command "note"}, but it operates in
    46   backwards mode and does not have any impact on chained facts.
    47 
    48   \<^descr> @{command "apply"}~@{text m} applies proof method @{text m} in
    49   initial position, but unlike @{command "proof"} it retains ``@{text
    50   "proof(prove)"}'' mode.  Thus consecutive method applications may be
    51   given just as in tactic scripts.
    52 
    53   Facts are passed to @{text m} as indicated by the goal's
    54   forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards.  Thus any
    55   further @{command "apply"} command would always work in a purely
    56   backward manner.
    57 
    58   \<^descr> @{command "apply_end"}~@{text "m"} applies proof method @{text
    59   m} as if in terminal position.  Basically, this simulates a
    60   multi-step tactic script for @{command "qed"}, but may be given
    61   anywhere within the proof body.
    62 
    63   No facts are passed to @{text m} here.  Furthermore, the static
    64   context is that of the enclosing goal (as for actual @{command
    65   "qed"}).  Thus the proof method may not refer to any assumptions
    66   introduced in the current body, for example.
    67 
    68   \<^descr> @{command "done"} completes a proof script, provided that the
    69   current goal state is solved completely.  Note that actual
    70   structured proof commands (e.g.\ ``@{command "."}'' or @{command
    71   "sorry"}) may be used to conclude proof scripts as well.
    72 
    73   \<^descr> @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
    74   shuffle the list of pending goals: @{command "defer"} puts off
    75   sub-goal @{text n} to the end of the list (@{text "n = 1"} by
    76   default), while @{command "prefer"} brings sub-goal @{text n} to the
    77   front.
    78 
    79   \<^descr> @{command "back"} does back-tracking over the result sequence
    80   of the latest proof command.  Any proof command may return multiple
    81   results, and this command explores the possibilities step-by-step.
    82   It is mainly useful for experimentation and interactive exploration,
    83   and should be avoided in finished proofs.
    84 \<close>
    85 
    86 
    87 section \<open>Explicit subgoal structure\<close>
    88 
    89 text \<open>
    90   \begin{matharray}{rcl}
    91     @{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    92   \end{matharray}
    93 
    94   @{rail \<open>
    95     @@{command subgoal} @{syntax thmbind}? prems? params?
    96     ;
    97     prems: @'premises' @{syntax thmbind}?
    98     ;
    99     params: @'for' '\<dots>'? (('_' | @{syntax name})+)
   100   \<close>}
   101 
   102   \<^descr> @{command "subgoal"} allows to impose some structure on backward
   103   refinements, to avoid proof scripts degenerating into long of @{command
   104   apply} sequences.
   105 
   106   The current goal state, which is essentially a hidden part of the Isar/VM
   107   configurtation, is turned into a proof context and remaining conclusion.
   108   This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
   109   structured proofs, but the text of the parameters, premises and conclusion
   110   is not given explicitly.
   111 
   112   Goal parameters may be specified separately, in order to allow referring
   113   to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
   114   y z"}'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
   115   "for"}~@{text "\<dots> x y z"}'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
   116   latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
   117   positions may be skipped via dummies (underscore). Unspecified names
   118   remain internal, and thus inaccessible in the proof text.
   119 
   120   ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that
   121   goal premises should be turned into assumptions of the context (otherwise
   122   the remaining conclusion is a Pure implication). The fact name and
   123   attributes are optional; the particular name ``@{text prems}'' is a common
   124   convention for the premises of an arbitrary goal context in proof scripts.
   125 
   126   ``@{command subgoal}~@{text result}'' indicates a fact name for the result
   127   of a proven subgoal. Thus it may be re-used in further reasoning, similar
   128   to the 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 sorry
   137   subgoal sorry
   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 sorry
   143   subgoal for u v sorry
   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     sorry
   151   subgoal premises for u v
   152     using \<open>X u\<close>
   153     sorry
   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 sorry
   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 sorry
   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" sorry
   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.
   185   These admit direct access to the goal state, which is normally
   186   considered harmful!  In particular, this may involve both numbered
   187   goal addressing (default 1), and dynamic instantiation within the
   188   scope of some subgoal.
   189 
   190   \begin{warn}
   191     Dynamic instantiations refer to universally quantified parameters
   192     of a subgoal (the dynamic context) rather than fixed variables and
   193     term abbreviations of a (static) Isar context.
   194   \end{warn}
   195 
   196   Tactic emulation methods, unlike their ML counterparts, admit
   197   simultaneous instantiation from both dynamic and static contexts.
   198   If names occur in both contexts goal parameters hide locally fixed
   199   variables.  Likewise, schematic variables refer to term
   200   abbreviations, if present in the static context.  Otherwise the
   201   schematic variable is interpreted as a schematic variable and left
   202   to be solved by unification with certain parts of the subgoal.
   203 
   204   Note that the tactic emulation proof methods in Isabelle/Isar are
   205   consistently named @{text foo_tac}.  Note also that variable names
   206   occurring on left hand sides of instantiations must be preceded by a
   207   question mark if they coincide with a keyword or contain dots.  This
   208   is consistent with the attribute @{attribute "where"} (see
   209   \secref{sec:pure-meth-att}).
   210 
   211   \begin{matharray}{rcl}
   212     @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   213     @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   214     @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   215     @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
   216     @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
   217     @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
   218     @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
   219     @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
   220     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
   221     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
   222     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   223   \end{matharray}
   224 
   225   @{rail \<open>
   226     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
   227       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
   228     (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
   229     ;
   230     @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
   231     ;
   232     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
   233     ;
   234     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
   235     ;
   236     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
   237     ;
   238     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
   239   \<close>}
   240 
   241   \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
   242   instantiation.  This works the same way as the ML tactics @{ML
   243   Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
   244 
   245   Multiple rules may be only given if there is no instantiation; then
   246   @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
   247   @{cite "isabelle-implementation"}).
   248 
   249   \<^descr> @{method cut_tac} inserts facts into the proof state as
   250   assumption of a subgoal; instantiations may be given as well.  Note
   251   that the scope of schematic variables is spread over the main goal
   252   statement and rule premises are turned into new subgoals.  This is
   253   in contrast to the regular method @{method insert} which inserts
   254   closed rule statements.
   255 
   256   \<^descr> @{method thin_tac}~@{text \<phi>} deletes the specified premise
   257   from a subgoal.  Note that @{text \<phi>} may contain schematic
   258   variables, to abbreviate the intended proposition; the first
   259   matching subgoal premise will be deleted.  Removing useless premises
   260   from a subgoal increases its readability and can make search tactics
   261   run faster.
   262 
   263   \<^descr> @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
   264   @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
   265   as new subgoals (in the original context).
   266 
   267   \<^descr> @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
   268   goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
   269   \<^emph>\<open>suffix\<close> of variables.
   270 
   271   \<^descr> @{method rotate_tac}~@{text n} rotates the premises of a
   272   subgoal by @{text n} positions: from right to left if @{text n} is
   273   positive, and from left to right if @{text n} is negative; the
   274   default value is 1.
   275 
   276   \<^descr> @{method tactic}~@{text "text"} produces a proof method from
   277   any ML text of type @{ML_type tactic}.  Apart from the usual ML
   278   environment and the current proof context, the ML code may refer to
   279   the locally bound values @{ML_text facts}, which indicates any
   280   current facts used for forward-chaining.
   281 
   282   \<^descr> @{method raw_tactic} is similar to @{method tactic}, but
   283   presents the goal state in its raw internal form, where simultaneous
   284   subgoals appear as conjunction of the logical framework instead of
   285   the usual split into several subgoals.  While feature this is useful
   286   for debugging of complex method definitions, it should not never
   287   appear in production theories.
   288 \<close>
   289 
   290 end