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