(*:maxLineLen=78:*)
theory Proof_Script
imports Main Base
begin
chapter ‹Proof scripts
›
text ‹
Interactive
theorem proving
is traditionally associated
with ``
proof
scripts
'', but Isabelle/Isar
is centered around structured
🚫‹proof
documents
› instead (see
also \chref{ch:proofs}).
Nonetheless, it
is possible
to emulate
proof scripts
by sequential
refinements of a
proof state
in backwards mode, notably
with the @{command
apply} command (see
\secref{sec:tactic-commands}).
There are
also various
proof methods that allow
to refer
to implicit goal
state information that
is not accessible
to structured Isar proofs (see
\secref{sec:tactics}).
Note that the @{command subgoal}
(
\secref{sec:subgoal}) command usually eliminates the need
for implicit goal
state references.
›
section ‹Commands
for step-wise refinement
\label{sec:tactic-commands}
›
text ‹
\begin{matharray}{rcl}
@{command_def
"supply"}
‹🚫*
› & : &
‹proof(prove)
→ proof(prove)
› \\
@{command_def
"apply"}
‹🚫*
› & : &
‹proof(prove)
→ proof(prove)
› \\
@{command_def
"apply_end"}
‹🚫*
› & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"done"}
‹🚫*
› & : &
‹proof(prove)
→ proof(state) | local_theory |
theory› \\
@{command_def
"defer"}
‹🚫*
› & : &
‹proof → proof› \\
@{command_def
"prefer"}
‹🚫*
› & : &
‹proof → proof› \\
@{command_def
"back"}
‹🚫*
› & : &
‹proof → proof› \\
\end{matharray}
🚫‹
@@{command supply} (@{
syntax thmdef}? @{
syntax thms} + @
'and')
;
( @@{command
apply} | @@{command
apply_end} ) @{
syntax method}
;
@@{command
defer} @{
syntax nat}?
;
@@{command
prefer} @{
syntax nat}
›
🚫 @{command
"supply"} supports fact definitions during goal refinement: it
is similar
to @{command
"note"}, but it operates
in backwards mode
and does
not
have any impact on chained facts.
🚫 @{command
"apply"}~
‹m
› applies
proof method
‹m
› in initial position, but
unlike @{command
"proof"} it retains ``
‹proof(prove)
›'' mode.
Thus
consecutive method applications may be given just as
in tactic scripts.
Facts are passed
to ‹m
› as indicated
by the goal
's forward-chain mode, and
are
🚫‹consumed
› afterwards.
Thus any further @{command
"apply"} command
would always work
in a purely backward manner.
🚫 @{command
"apply_end"}~
‹m
› applies
proof method
‹m
› as
if in terminal
position. Basically, this simulates a multi-step tactic script
for @{command
"qed"}, but may be given anywhere within the
proof body.
No facts are passed
to ‹m
› here. Furthermore, the static
context is that of
the enclosing goal (as
for actual @{command
"qed"}).
Thus the
proof method
may not refer
to any assumptions introduced
in the current body,
for
example.
🚫 @{command
"done"} completes a
proof script, provided that the current goal
state
is solved completely.
Note that actual structured
proof commands
(e.g.
\ ``@{command
"."}
'' or @{command
"sorry"}) may be used
to conclude
proof scripts as well.
🚫 @{command
"defer"}~
‹n
› and @{command
"prefer"}~
‹n
› shuffle the list of
pending goals: @{command
"defer"} puts off sub-goal
‹n
› to the
end of the
list (
‹n = 1
› by default), while @{command
"prefer"} brings sub-goal
‹n
› to
the front.
🚫 @{command
"back"} does back-tracking over the result sequence of the
latest
proof command. Any
proof command may return multiple results,
and
this command explores the possibilities step-by-step. It
is mainly useful
for experimentation
and interactive exploration,
and should be avoided
in
finished proofs.
›
section ‹Explicit subgoal
structure \label{sec:subgoal}
›
text ‹
\begin{matharray}{rcl}
@{command_def
"subgoal"}
‹🚫*
› & : &
‹proof → proof› \\
\end{matharray}
🚫‹
@@{command subgoal} @{
syntax thmbind}? prems? params?
;
prems: @
'premises' @{
syntax thmbind}?
;
params: @
'for' '\'? ((
'_' | @{
syntax name})+)
›
🚫 @{command
"subgoal"} allows
to impose some
structure on backward
refinements,
to avoid
proof scripts degenerating into long of @{command
apply} sequences.
The current goal state, which
is essentially a hidden part of the Isar/VM
configuration,
is turned into a
proof context and remaining conclusion.
This corresponds
to @{command
fix}~/ @{command
assume}~/ @{command
show}
in
structured proofs, but the
text of the parameters, premises
and conclusion
is not given explicitly.
Goal parameters may be specified separately,
in order
to allow referring
to
them
in the
proof body: ``@{command subgoal}~@{keyword
"for"}~
‹x y z
›''
names a
🚫‹prefix
›,
and ``@{command subgoal}~@{keyword
"for"}~
‹… x y z
›''
names a
🚫‹suffix
› of goal parameters. The latter
uses a literal
🍋‹…› symbol
as
notation. Parameter positions may be skipped via dummies (underscore).
Unspecified names remain internal,
and thus inaccessible
in the
proof text.
``@{command subgoal}~@{keyword
"premises"}~
‹prems
›'' indicates that goal
premises should be turned into assumptions of the
context (
otherwise the
remaining conclusion
is a Pure implication). The fact name
and attributes
are optional; the particular name ``
‹prems
›'' is a common convention
for the
premises of an arbitrary goal
context in proof scripts.
``@{command subgoal}~
‹result
›'' indicates a fact name
for the result of a
proven subgoal.
Thus it may be re-used
in further reasoning, similar
to the
result of @{command
show}
in structured Isar proofs.
Here are some abstract examples:
›
lemma "\x y z. A x \ B y \ C z"
and "\u v. X u \ Y v"
subgoal
🍋
subgoal
🍋
done
lemma "\x y z. A x \ B y \ C z"
and "\u v. X u \ Y v"
subgoal
for x y z
🍋
subgoal
for u v
🍋
done
lemma "\x y z. A x \ B y \ C z"
and "\u v. X u \ Y v"
subgoal premises
for x y z
using ‹A x
› ‹B y
›
🍋
subgoal premises
for u v
using ‹X u
›
🍋
done
lemma "\x y z. A x \ B y \ C z"
and "\u v. X u \ Y v"
subgoal r premises prems
for x y z
proof -
have "A x" by (fact prems)
moreover have "B y" by (fact prems)
ultimately show ?thesis
🍋
qed
subgoal premises prems
for u v
proof -
have "\x y z. A x \ B y \ C z" by (fact r)
moreover
have "X u" by (fact prems)
ultimately show ?thesis
🍋
qed
done
lemma "\x y z. A x \ B y \ C z"
subgoal premises prems
for … z
proof -
from prems
show "C z" 🍋
qed
done
section ‹Tactics: improper
proof methods
\label{sec:tactics}
›
text ‹
The following improper
proof methods emulate traditional tactics. These
admit direct access
to the goal state, which
is normally considered harmful!
In particular, this may involve both numbered goal addressing (default 1),
and dynamic
instantiation within the scope of some subgoal.
\begin{warn}
Dynamic instantiations refer
to universally quantified parameters of a
subgoal (the dynamic
context) rather than fixed variables
and term
abbreviations of a (static) Isar
context.
\end{warn}
Tactic emulation methods, unlike their ML counterparts, admit simultaneous
instantiation from both dynamic
and static contexts.
If names occur
in both
contexts goal parameters
hide locally fixed variables. Likewise, schematic
variables refer
to term abbreviations,
if present
in the static
context.
Otherwise the schematic variable
is interpreted as a schematic variable
and
left
to be solved
by unification
with certain parts of the subgoal.
Note that the tactic emulation
proof methods
in Isabelle/Isar are
consistently named
‹foo_tac
›.
Note also that variable names occurring on
left hand sides of instantiations must be preceded
by a question mark
if
they coincide
with a keyword or contain dots. This
is consistent
with the
attribute @{attribute
"where"} (see
\secref{sec:pure-meth-att}).
\begin{matharray}{rcl}
@{method_def rule_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def erule_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def drule_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def frule_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def cut_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def thin_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def subgoal_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def rename_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def rotate_tac}
‹🚫*
› & : &
‹method
› \\
@{method_def tactic}
‹🚫*
› & : &
‹method
› \\
@{method_def raw_tactic}
‹🚫*
› & : &
‹method
› \\
\end{matharray}
🚫‹
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
@@{method frule_tac} | @@{method cut_tac}) @{
syntax goal_spec}?
🍋
(@{
syntax named_insts} @{
syntax for_fixes} @
'in' @{
syntax thm} | @{
syntax thms} )
;
@@{method thin_tac} @{
syntax goal_spec}? @{
syntax prop} @{
syntax for_fixes}
;
@@{method subgoal_tac} @{
syntax goal_spec}? (@{
syntax prop} +) @{
syntax for_fixes}
;
@@{method rename_tac} @{
syntax goal_spec}? (@{
syntax name} +)
;
@@{method rotate_tac} @{
syntax goal_spec}? @{
syntax int}?
;
(@@{method tactic} | @@{method raw_tactic}) @{
syntax text}
›
🚫 @{method rule_tac} etc. do resolution of rules
with explicit
instantiation. This works the same way as the ML tactics
🚫‹Rule_Insts.res_inst_tac
› etc.
\ (
see 🍋‹"isabelle-implementation"›).
Multiple rules may be only given if there is no instantiation; then @{method
rule_tac} is the same as 🚫‹resolve_tac› in ML (see 🍋‹"isabelle-implementation"›).
🚫 @{method cut_tac} inserts facts into the proof state as assumption of a
subgoal; instantiations may be given as well. Note that the scope of
schematic variables is spread over the main goal statement and rule premises
are turned into new subgoals. This is in contrast to the regular method
@{method insert} which inserts closed rule statements.
🚫 @{method thin_tac}~‹φ› deletes the specified premise from a subgoal. Note
that ‹φ› may contain schematic variables, to abbreviate the intended
proposition; the first matching subgoal premise will be deleted. Removing
useless premises from a subgoal increases its readability and can make
search tactics run faster.
🚫 @{method subgoal_tac}~‹φ🚫1 … φ🚫n› adds the propositions ‹φ🚫1 … φ🚫n› as
local premises to a subgoal, and poses the same as new subgoals (in the
original context).
🚫 @{method rename_tac}~‹x🚫1 … x🚫n› renames parameters of a goal according to
the list ‹x🚫1, …, x🚫n›, which refers to the 🚫‹suffix› of variables.
🚫 @{method rotate_tac}~‹n› rotates the premises of a subgoal by ‹n›
positions: from right to left if ‹n› is positive, and from left to right if
‹n› is negative; the default value is 1.
🚫 @{method tactic}~‹text› produces a proof method from any ML text of type
🚫‹tactic›. Apart from the usual ML environment and the current proof
context, the ML code may refer to the locally bound values 🚫‹facts›,
which indicates any current facts used for forward-chaining.
🚫 @{method raw_tactic} is similar to @{method tactic}, but presents the goal
state in its raw internal form, where simultaneous subgoals appear as
conjunction of the logical framework instead of the usual split into several
subgoals. While feature this is useful for debugging of complex method
definitions, it should not never appear in production theories.
›
end
