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