src/Doc/Isar_Ref/Proof_Script.thy
 author wenzelm Sun Feb 07 19:32:35 2016 +0100 (2016-02-07) changeset 62269 c56cff1c0e73 parent 61866 6fa60a4f7e48 child 62271 4cfe65cfd369 permissions -rw-r--r--
tuned;
     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}).

    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 thmrefs} + @'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 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. 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 thmref} | @{syntax thmrefs} )

   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