(*:maxLineLen=78:*)
theory Proof
imports Main Base
begin
chapter ‹Proofs
\label{ch:proofs}
›
text ‹
Proof commands perform
transitions of Isar/VM machine configurations, which
are block-structured, consisting of a stack of nodes
with three main
components: logical
proof context, current facts,
and open goals. Isar/VM
transitions are typed according
to the following three different modes of
operation:
🚫 ‹proof(prove)
› means that a new goal has just been stated that
is now
to
be
🚫‹proven
›; the
next command may refine it
by some
proof method,
and
enter a sub-proof
to establish the actual result.
🚫 ‹proof(state)
› is like a nested
theory mode: the
context may be
augmented
by 🚫‹stating
› additional assumptions, intermediate results etc.
🚫 ‹proof(chain)
› is intermediate between
‹proof(state)
› and
‹proof(prove)
›: existing facts (i.e.
\ the contents of the special
@{fact_ref this} register)
have been just picked up
in order
to be used
when refining the goal claimed
next.
The
proof mode indicator may be understood as an instruction
to the writer,
telling what kind of operation may be performed
next. The corresponding
typings of
proof commands restricts the shape of well-formed
proof texts
to
particular command sequences. So dynamic arrangements of commands eventually
turn out as static texts of a certain
structure.
\Appref{ap:refcard} gives a simplified grammar of the (extensible) language
emerging that way
from the different
types of
proof commands. The main ideas
of the overall Isar framework are explained
in \chref{ch:isar-framework}.
›
section
‹Proof structure›
subsection
‹Formal notepad
›
text ‹
\begin{matharray}{rcl}
@{command_def
"notepad"} & : &
‹local_theory
→ proof(state)
› \\
\end{matharray}
🚫‹
@@{command notepad} @
'begin'
;
@@{command
end}
›
🚫 @{command
"notepad"}~@{keyword
"begin"} opens a
proof state without any
goal statement. This allows
to experiment
with Isar, without producing any
persistent result. The notepad
is closed
by @{command
"end"}.
›
subsection
‹Blocks
›
text ‹
\begin{matharray}{rcl}
@{command_def
"next"} & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"{"} & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"}"} & : &
‹proof(state)
→ proof(state)
› \\
\end{matharray}
While Isar
is inherently block-structured, opening
and closing blocks
is
mostly handled rather casually,
with little explicit user-intervention. Any
local goal statement automatically opens
🚫‹two
› internal blocks, which are
closed again when concluding the sub-proof (
by @{command
"qed"} etc.).
Sections of different
context within a sub-proof may be switched via
@{command
"next"}, which
is just a single block-close followed
by block-open
again. The effect of @{command
"next"}
is to reset the
local proof context;
there
is no goal focus involved here!
For slightly more
advanced applications, there are explicit block
parentheses as well. These typically achieve a stronger forward style of
reasoning.
🚫 @{command
"next"} switches
to a fresh block within a sub-proof, resetting
the
local context to the initial one.
🚫 @{command
"{"}
and @{command
"}"} explicitly
open and close blocks. Any
current facts pass through ``@{command
"{"}
'' unchanged, while ``@{command
"}"}
'' causes any result
to be
🚫‹exported
› into the enclosing
context.
Thus
fixed variables are generalized, assumptions discharged,
and local
definitions unfolded (cf.
\ \secref{sec:proof-context}). There
is no
difference of @{command
"assume"}
and @{command
"presume"}
in this mode of
forward reasoning ---
in contrast
to plain backward reasoning
with the
result exported at @{command
"show"} time.
›
subsection
‹Omitting proofs
›
text ‹
\begin{matharray}{rcl}
@{command_def
"oops"} & : &
‹proof → local_theory |
theory› \\
\end{matharray}
The @{command
"oops"} command discontinues the current
proof attempt, while
considering the partial
proof text as properly processed. This
is
conceptually quite different
from ``faking
'' actual proofs via @{command_ref
"sorry"} (see
\secref{sec:proof-steps}): @{command
"oops"} does not observe
the
proof structure at all, but goes
back right
to the
theory level.
Furthermore, @{command
"oops"} does not produce any result
theorem --- there
is no intended claim
to be able
to complete the
proof in any way.
A typical application of @{command
"oops"}
is to explain Isar proofs
🚫‹within
› the system itself,
in conjunction
with the document preparation
tools of Isabelle described
in \chref{ch:document-prep}.
Thus partial or
even wrong
proof attempts can be discussed
in a logically sound manner.
Note
that the Isabelle {
\LaTeX} macros can be easily adapted
to print something
like ``
‹…›'' instead of the keyword ``@{command
"oops"}
''.
›
section
‹Statements
›
subsection
‹Context elements
\label{sec:proof-context}
›
text ‹
\begin{matharray}{rcl}
@{command_def
"fix"} & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"assume"} & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"presume"} & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"define"} & : &
‹proof(state)
→ proof(state)
› \\
\end{matharray}
The logical
proof context consists of fixed variables
and assumptions. The
former closely correspond
to Skolem constants, or meta-level universal
quantification as provided
by the Isabelle/Pure logical framework.
Introducing some
🚫‹arbitrary, but fixed
› variable via ``@{command
"fix"}~
‹x
›'' results
in a
local value that may be used
in the subsequent
proof as any other variable or constant. Furthermore, any result
‹⊨ φ[x]
›
exported
from the
context will be universally closed wrt.
\ ‹x
› at the
outermost level:
‹⊨ ∧x. φ[x]
› (this
is expressed
in normal form
using
Isabelle
's meta-variables).
Similarly, introducing some assumption
‹χ
› has two effects. On the one hand,
a
local theorem is created that may be used as a fact
in subsequent
proof
steps. On the other hand, any result
‹χ
⊨ φ
› exported
from the
context
becomes conditional wrt.
\ the assumption:
‹⊨ χ
==> φ
›.
Thus, solving an
enclosing goal
using such a result would basically introduce a new subgoal
stemming
from the assumption. How this situation
is handled depends on the
version of assumption command used: while @{command
"assume"} insists on
solving the subgoal
by unification
with some premise of the goal, @{command
"presume"} leaves the subgoal unchanged
in order
to be proved later
by the
user.
Local definitions, introduced
by ``
🚫‹define x
where x = t
›'', are achieved
by combining ``@{command
"fix"}~
‹x
›'' with another version of assumption
that causes any hypothetical equation
‹x
≡ t
› to be eliminated
by the
reflexivity rule.
Thus, exporting some result
‹x
≡ t
⊨ φ[x]
› yields
‹⊨
φ[t]
›.
🚫‹
@@{command
fix} @{
syntax vars}
;
(@@{command
assume} | @@{command
presume}) concl prems @{
syntax for_fixes}
;
concl: (@{
syntax props} + @
'and')
;
prems: (@
'if' (@{
syntax props
'} + @'and'))?
;
@@{command define} @{
syntax vars} @
'where'
(@{
syntax props} + @
'and') @{
syntax for_fixes}
›
🚫 @{command
"fix"}~
‹x
› introduces a
local variable
‹x
› that
is 🚫‹arbitrary,
but fixed
›.
🚫 @{command
"assume"}~
‹a: φ
› and @{command
"presume"}~
‹a: φ
› introduce a
local fact
‹φ
⊨ φ
› by assumption. Subsequent results applied
to an enclosing
goal (e.g.
\ by @{command_ref
"show"}) are handled as follows: @{command
"assume"} expects
to be able
to unify
with existing premises
in the goal,
while @{command
"presume"} leaves
‹φ
› as new subgoals.
Several lists of assumptions may be given (separated
by @{keyword_ref
"and"}; the resulting list of current facts consists of all of these
concatenated.
A structured assumption like
🚫‹assume "B x" if "A x" for x
› is equivalent
to
🚫‹assume "\x. A x \ B x"›, but vacuous quantification
is avoided: a
for-context only effects propositions according
to actual
use of variables.
🚫 🚫‹define x
where "x = t"› introduces a
local (non-polymorphic)
definition.
In results that are exported
from the
context,
‹x
› is replaced
by ‹t
›.
Internally, equational assumptions are added
to the
context in Pure form,
using ‹x
≡ t
› instead of
‹x = t
› or
‹x
⟷ t
› from the object-logic. When
exporting results
from the
context,
‹x
› is generalized
and the assumption
discharged
by reflexivity, causing the replacement
by ‹t
›.
The default name
for the definitional fact
is ‹x_def
›. Several simultaneous
definitions may be given as well,
with a collective default name.
🚫
It
is also possible
to abstract over
local parameters as follows:
🚫‹define f
::
"'a \ 'b" where "f x = t" for x ::
'a\.
›
subsection
‹Term abbreviations
\label{sec:term-abbrev}
›
text ‹
\begin{matharray}{rcl}
@{command_def
"let"} & : &
‹proof(state)
→ proof(state)
› \\
@{keyword_def
"is"} & : &
syntax \\
\end{matharray}
Abbreviations may be either bound
by explicit @{command
"let"}~
‹p
≡ t
›
statements, or
by annotating assumptions or goal statements
with a list of
patterns ``
🚫‹(
is p
🚫1
… p
🚫n)
›''.
In both cases, higher-order matching
is
invoked
to bind extra-logical
term variables, which may be either named
schematic variables of the form
‹?x
›, or nameless dummies ``@{variable _}
''
(underscore).
Note that
in the @{command
"let"} form the patterns occur on
the left-hand side, while the @{keyword
"is"} patterns are
in postfix
position.
Polymorphism of
term bindings
is handled
in Hindley-Milner style, similar
to
ML. Type variables referring
to local assumptions or
open goal statements
are
🚫‹fixed
›, while those of finished results or bound
by @{command
"let"}
may occur
in 🚫‹arbitrary
› instances later. Even though actual polymorphism
should be rarely used
in practice, this mechanism
is essential
to achieve
proper incremental type-inference, as the user proceeds
to build up the Isar
proof text from left
to right.
🚫
Term abbreviations are quite different
from local definitions as introduced
via @{command
"define"} (see
\secref{sec:proof-context}). The latter are
visible within the logic as actual equations, while abbreviations disappear
during the input process just after type checking.
Also note that @{command
"define"} does not support polymorphism.
🚫‹
@@{command
let} ((@{
syntax term} + @
'and')
'=' @{
syntax term} + @
'and')
›
The
syntax of @{keyword
"is"} patterns follows @{
syntax term_pat} or
@{
syntax prop_pat} (see
\secref{sec:term-decls}).
🚫 🚫‹let p
🚫1 = t
🚫1
and … p
🚫n = t
🚫n
› binds any
text variables
in patterns
‹p
🚫1,
…, p
🚫n
› by simultaneous higher-order matching against terms
‹t
🚫1,
…,
t
🚫n
›.
🚫 🚫‹(
is p
🚫1
… p
🚫n)
› resembles @{command
"let"}, but matches
‹p
🚫1,
…, p
🚫n
›
against the preceding statement.
Also note that @{keyword
"is"}
is not a
separate command, but part of others (such as @{command
"assume"},
@{command
"have"} etc.).
Some
🚫‹implicit
› term abbreviations
\index{
term abbreviations}
for goals
and
facts are available as well.
For any
open goal, @{variable_ref thesis}
refers
to its object-level statement, abstracted over any meta-level
parameters (
if present). Likewise, @{variable_ref this}
is bound
for fact
statements resulting
from assumptions or finished goals.
In case @{variable
this} refers
to an object-logic statement that
is an application
‹f t
›,
then
‹t
› is bound
to the special
text variable ``@{variable
"\"}
'' (three dots).
The canonical application of this convenience are calculational proofs (see
\secref{sec:calculation}).
›
subsection
‹Facts
and forward chaining
\label{sec:proof-facts}
›
text ‹
\begin{matharray}{rcl}
@{command_def
"note"} & : &
‹proof(state)
→ proof(state)
› \\
@{command_def
"then"} & : &
‹proof(state)
→ proof(chain)
› \\
@{command_def
"from"} & : &
‹proof(state)
→ proof(chain)
› \\
@{command_def
"with"} & : &
‹proof(state)
→ proof(chain)
› \\
@{command_def
"using"} & : &
‹proof(prove)
→ proof(prove)
› \\
@{command_def
"unfolding"} & : &
‹proof(prove)
→ proof(prove)
› \\
@{method_def
"use"} & : &
‹method
› \\
@{fact_def
"method_facts"} & : &
‹fact
› \\
\end{matharray}
New facts are established either
by assumption or
proof of
local statements.
Any fact will usually be involved
in further proofs, either as explicit
arguments of
proof methods, or when forward chaining towards the
next goal
via @{command
"then"} (
and variants); @{command
"from"}
and @{command
"with"} are composite forms involving @{command
"note"}. The @{command
"using"} elements augments the collection of used facts
🚫‹after
› a goal has
been stated.
Note that the special
theorem name @{fact_ref this} refers
to
the most recently established facts, but only
🚫‹before
› issuing a follow-up
claim.
🚫‹
@@{command
note} (@{
syntax thmdef}? @{
syntax thms} + @
'and')
;
(@@{command
from} | @@{command
with} | @@{command
using} | @@{command
unfolding})
(@{
syntax thms} + @
'and')
;
@{method
use} @{
syntax thms} @
'in' @{
syntax method}
›
🚫 @{command
"note"}~
‹a = b
🚫1
… b
🚫n
› recalls existing facts
‹b
🚫1,
…, b
🚫n
›,
binding the result as
‹a
›.
Note that attributes may be involved as well,
both on the left
and right hand sides.
🚫 @{command
"then"} indicates forward chaining
by the current facts
in order
to establish the goal
to be claimed
next. The initial
proof method invoked
to refine that will be offered the facts
to do ``anything appropriate
'' (see
also \secref{sec:proof-steps}).
For example, method @{method (Pure) rule}
(see
\secref{sec:pure-meth-att}) would typically do an elimination rather
than an introduction. Automatic methods usually insert the facts into the
goal state before operation. This provides a simple scheme
to control
relevance of facts
in automated
proof search.
🚫 @{command
"from"}~
‹b
› abbreviates ``@{command
"note"}~
‹b
›~@{command
"then"}
'';
thus @{command
"then"}
is equivalent
to ``@{command
"from"}~
‹this
›''.
🚫 @{command
"with"}~
‹b
🚫1
… b
🚫n
› abbreviates ``@{command
"from"}~
‹b
🚫1
… b
🚫n
🚫 this
›'';
thus the forward chaining
is from earlier facts together
with the current ones.
🚫 @{command
"using"}~
‹b
🚫1
… b
🚫n
› augments the facts
to be used
by a
subsequent refinement step (such as @{command_ref
"apply"} or @{command_ref
"proof"}).
🚫 @{command
"unfolding"}~
‹b
🚫1
… b
🚫n
› is structurally similar
to @{command
"using"}, but unfolds definitional equations
‹b
🚫1
… b
🚫n
› throughout the goal
state
and facts. See
also the
proof method @{method_ref unfold}.
🚫 🚫‹(
use b
🚫1
… b
🚫n
in method)
› uses the facts
in the given method
expression. The facts provided
by the
proof state (via @{command
"using"}
etc.) are ignored, but it
is possible
to refer
to @{fact method_facts}
explicitly.
🚫 @{fact method_facts}
is a dynamic fact that refers
to the currently used
facts of the goal state.
Forward chaining
with an empty list of
theorems is the same as not chaining
at all.
Thus ``@{command
"from"}~
‹nothing
›'' has no effect apart
from
entering
‹prove(chain)
› mode, since @{fact_ref nothing}
is bound
to the
empty list of
theorems.
Basic
proof methods (such as @{method_ref (Pure) rule}) expect multiple
facts
to be given
in their proper order, corresponding
to a prefix of the
premises of the rule involved.
Note that positions may be easily skipped
using something like @{command
"from"}~
‹_
🚫 a
🚫 b
›,
for example.
This involves the trivial rule
‹PROP ψ
==> PROP ψ
›, which
is bound
in
Isabelle/Pure as ``@{fact_ref
"_"}
'' (underscore).
Automated methods (such as @{method simp} or @{method auto}) just insert any
given facts before their usual operation. Depending on the kind of procedure
involved, the order of facts
is less significant here.
›
subsection
‹Goals
\label{sec:goals}
›
text ‹
\begin{matharray}{rcl}
@{command_def
"lemma"} & : &
‹local_theory
→ proof(prove)
› \\
@{command_def
"theorem"} & : &
‹local_theory
→ proof(prove)
› \\
@{command_def
"corollary"} & : &
‹local_theory
→ proof(prove)
› \\
@{command_def
"proposition"} & : &
‹local_theory
→ proof(prove)
› \\
@{command_def
"schematic_goal"} & : &
‹local_theory
→ proof(prove)
› \\
@{command_def
"have"} & : &
‹proof(state) |
proof(chain)
→ proof(prove)
› \\
@{command_def
"show"} & : &
‹proof(state) |
proof(chain)
→ proof(prove)
› \\
@{command_def
"hence"} & : &
‹proof(state)
→ proof(prove)
› \\
@{command_def
"thus"} & : &
‹proof(state)
→ proof(prove)
› \\
@{command_def
"print_statement"}
‹🚫*
› & : &
‹context →› \\
\end{matharray}
From a
theory context,
proof mode
is entered
by an initial goal command such
as @{command
"lemma"}. Within a
proof context, new claims may be introduced
locally; there are variants
to interact
with the overall
proof structure
specifically, such as @{command
have} or @{command
show}.
Goals may consist of multiple statements, resulting
in a list of facts
eventually. A pending multi-goal
is internally represented as a meta-level
conjunction (
‹&&&
›), which
is usually split into the correspo
nding number of
sub-goals prior to an initial method application, via @{command_ref "proof"}
(\secref{sec:proof-steps}) or @{command_ref "apply"}
(\secref{sec:tactic-commands}). The @{method_ref induct} method covered in
\secref{sec:cases-induct} acts on multiple claims simultaneously.
Claims at the theory level may be either in short or long form. A short goal
merely consists of several simultaneous propositions (often just one). A
long goal includes an explicit context specification for the subsequent
conclusion, involving local parameters and assumptions. Here the role of
each part of the statement is explicitly marked by separate keywords (see
also \secref{sec:locale}); the local assumptions being introduced here are
available as @{fact_ref assms} in the proof. Moreover, there are two kinds
of conclusions: @{element_def "shows"} states several simultaneous
propositions (essentially a big conjunction), while @{element_def "obtains"}
claims several simultaneous contexts --- essentially a big disjunction of
eliminated parameters and assumptions (see \secref{sec:obtain}).
🚫‹
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
@@{command proposition} | @@{command schematic_goal})
(long_statement | short_statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
stmt cond_stmt @{syntax for_fixes}
;
@@{command print_statement} @{syntax modes}? @{syntax thms}
;
stmt: (@{syntax props} + @'and')
;
cond_stmt: ((@'if' | @'when') stmt)?
;
short_statement: stmt (@'if' stmt)? @{syntax for_fixes}
;
long_statement: @{syntax thmdecl}? context conclusion
;
context: (@{syntax_ref "includes"}?) (@{syntax context_elem} *)
;
conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
;
@{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
;
@{syntax_def obtain_case}: (@{syntax vars} @'where')?
(@{syntax thmdecl}? (@{syntax prop}+) + @'and')
›
🚫 @{command "lemma"}~‹a: φ› enters proof mode with ‹φ› as main goal,
eventually resulting in some fact ‹⊨ φ› to be put back into the target
context.
A @{syntax long_statement} may build up an initial proof context for the
subsequent claim, potentially including local definitions and syntax; see
also @{syntax "includes"} in \secref{sec:bundle} and @{syntax context_elem}
in \secref{sec:locale}.
A @{syntax short_statement} consists of propositions as conclusion, with an
option context of premises and parameters, via 🍋‹if›/🍋‹for› in postfix
notation, corresponding to 🍋‹assumes›/🍋‹fixes› in the long prefix notation.
Local premises (if present) are called ``‹assms›'' for @{syntax
long_statement}, and ``‹that›'' for @{syntax short_statement}.
🚫 @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}
are the same as @{command "lemma"}. The different command names merely serve
as a formal comment in the theory source.
🚫 @{command "schematic_goal"} is similar to @{command "theorem"}, but allows
the statement to contain unbound schematic variables.
Under normal circumstances, an Isar proof text needs to specify claims
explicitly. Schematic goals are more like goals in Prolog, where certain
results are synthesized in the course of reasoning. With schematic
statements, the inherent compositionality of Isar proofs is lost, which also
impacts performance, because proof checking is forced into sequential mode.
🚫 @{command "have"}~‹a: φ› claims a local goal, eventually resulting in a
fact within the current logical context. This operation is completely
independent of any pending sub-goals of an enclosing goal statements, so
@{command "have"} may be freely used for experimental exploration of
potential results within a proof body.
🚫 @{command "show"}~‹a: φ› is like @{command "have"}~‹a: φ› plus a second
stage to refine some pending sub-goal for each one of the finished result,
after having been exported into the corresponding context (at the head of
the sub-proof of this @{command "show"} command).
To accommodate interactive debugging, resulting rules are printed before
being applied internally. Even more, interactive execution of @{command
"show"} predicts potential failure and displays the resulting error as a
warning beforehand. Watch out for the following message:
@{verbatim [display] ‹Local statement fails to refine any pending goal›}
🚫 @{command "hence"} expands to ``@{command "then"}~@{command "have"}'' and
@{command "thus"} expands to ``@{command "then"}~@{command "show"}''. These
conflations are left-over from early history of Isar. The expanded syntax is
more orthogonal and improves readability and maintainability of proofs.
🚫 @{command "print_statement"}~‹a› prints facts from the current theory or
proof context in long statement form, according to the syntax for @{command
"lemma"} given above.
Any goal statement causes some term abbreviations (such as @{variable_ref
"?thesis"}) to be bound automatically, see also \secref{sec:term-abbrev}.
Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
"when"} define the special fact @{fact_ref that} to refer to these
assumptions in the proof body. The user may provide separate names according
to the syntax of the statement.
›
section ‹Calculational reasoning \label{sec:calculation}›
text ‹
\begin{matharray}{rcl}
@{command_def "also"} & : & ‹proof(state) → proof(state)› \\
@{command_def "finally"} & : & ‹proof(state) → proof(chain)› \\
@{command_def "moreover"} & : & ‹proof(state) → proof(state)› \\
@{command_def "ultimately"} & : & ‹proof(state) → proof(chain)› \\
@{command_def "print_trans_rules"}‹🚫*› & : & ‹context →› \\
@{attribute_def trans} & : & ‹attribute› \\
@{attribute_def sym} & : & ‹attribute› \\
@{attribute_def symmetric} & : & ‹attribute› \\
\end{matharray}
Calculational proof is forward reasoning with implicit application of
transitivity rules (such those of ‹=›, ‹≤›, ‹<›). Isabelle/Isar maintains an
auxiliary fact register @{fact_ref calculation} for accumulating results
obtained by transitivity composed with the current result. Command @{command
"also"} updates @{fact calculation} involving @{fact this}, while @{command
"finally"} exhibits the final @{fact calculation} by forward chaining
towards the next goal statement. Both commands require valid current facts,
i.e.\ may occur only after commands that produce theorems such as @{command
"assume"}, @{command "note"}, or some finished proof of @{command "have"},
@{command "show"} etc. The @{command "moreover"} and @{command "ultimately"}
commands are similar to @{command "also"} and @{command "finally"}, but only
collect further results in @{fact calculation} without applying any rules
yet.
Also note that the implicit term abbreviation ``‹…›'' has its canonical
application with calculational proofs. It refers to the argument of the
preceding statement. (The argument of a curried infix expression happens to
be its right-hand side.)
Isabelle/Isar calculations are implicitly subject to block structure in the
sense that new threads of calculational reasoning are commenced for any new
block (as opened by a local goal, for example). This means that, apart from
being able to nest calculations, there is no separate 🚫‹begin-calculation›
command required.
🚫
The Isar calculation proof commands may be defined as follows:🚫‹We suppress
internal bookkeeping such as proper handling of block-structure.›
\begin{matharray}{rcl}
@{command "also"}‹🚫0› & \equiv & @{command "note"}~‹calculation = this› \\
@{command "also"}‹🚫n🚫+🚫1› & \equiv & @{command "note"}~‹calculation = trans [OF calculation this]› \\[0.5ex]
@{command "finally"} & \equiv & @{command "also"}~@{command "from"}~‹calculation› \\[0.5ex]
@{command "moreover"} & \equiv & @{command "note"}~‹calculation = calculation this› \\
@{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~‹calculation› \\
\end{matharray}
🚫‹
(@@{command also} | @@{command finally}) ('(' @{syntax thms} ')')?
;
@@{attribute trans} (() | 'add' | 'del')
›
🚫 @{command "also"}~‹(a🚫1 … a🚫n)› maintains the auxiliary @{fact
calculation} register as follows. The first occurrence of @{command "also"}
in some calculational thread initializes @{fact calculation} by @{fact
this}. Any subsequent @{command "also"} on the same level of block-structure
updates @{fact calculation} by some transitivity rule applied to @{fact
calculation} and @{fact this} (in that order). Transitivity rules are picked
from the current context, unless alternative rules are given as explicit
arguments.
🚫 @{command "finally"}~‹(a🚫1 … a🚫n)› maintains @{fact calculation} in the
same way as @{command "also"} and then concludes the current calculational
thread. The final result is exhibited as fact for forward chaining towards
the next goal. Basically, @{command "finally"} abbreviates @{command
"also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding
calculational proofs are ``@{command "finally"}~@{command
"show"}~‹?thesis›~@{command "."}'' and ``@{command "finally"}~@{command
"have"}~‹φ›~@{command "."}''.
🚫 @{command "moreover"} and @{command "ultimately"} are analogous to
@{command "also"} and @{command "finally"}, but collect results only,
without applying rules.
🚫 @{command "print_trans_rules"} prints the list of transitivity rules (for
calculational commands @{command "also"} and @{command "finally"}) and
symmetry rules (for the @{attribute symmetric} operation and single step
elimination patters) of the current context.
🚫 @{attribute trans} declares theorems as transitivity rules.
🚫 @{attribute sym} declares symmetry rules, as well as @{attribute
"Pure.elim"}‹?› rules.
🚫 @{attribute symmetric} resolves a theorem with some rule declared as
@{attribute sym} in the current context. For example, ``@{command
"assume"}~‹[symmetric]: x = y›'' produces a swapped fact derived from that
assumption.
In structured proof texts it is often more appropriate to use an explicit
single-step elimination proof, such as ``@{command "assume"}~‹x =
y›~@{command "then"}~@{command "have"}~‹y = x›~@{command ".."}''.
›
section ‹Refinement steps›
subsection ‹Proof method expressions \label{sec:proof-meth}›
text ‹
Proof methods are either basic ones, or expressions composed of methods via
``🍋‹,›'' (sequential composition), ``🍋‹;›'' (structural composition),
``🍋‹|›'' (alternative choices), ``🍋‹?›'' (try), ``🍋‹+›'' (repeat at least
once), ``🍋‹[›‹n›🍋‹]›'' (restriction to first ‹n› subgoals). In practice,
proof methods are usually just a comma separated list of @{syntax
name}~@{syntax args} specifications. Note that parentheses may be dropped
for single method specifications (with no arguments). The syntactic
precedence of method combinators is 🍋‹|› 🍋‹;› 🍋‹,› 🍋‹[]› 🍋‹+› 🍋‹?› (from low
to high).
🚫‹
@{syntax_def method}:
(@{syntax name} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
;
methods: (@{syntax name} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
›
Regular Isar proof methods do 🚫‹not› admit direct goal addressing, but refer
to the first subgoal or to all subgoals uniformly. Nonetheless, the
subsequent mechanisms allow to imitate the effect of subgoal addressing that
is known from ML tactics.
🚫
Goal 🚫‹restriction› means the proof state is wrapped-up in a way that
certain subgoals are exposed, and other subgoals are ``parked'' elsewhere.
Thus a proof method has no other chance than to operate on the subgoals that
are presently exposed.
Structural composition ``‹m🚫1›🍋‹;›~‹m🚫2›'' means that method ‹m🚫1› is
applied with restriction to the first subgoal, then ‹m🚫2› is applied
consecutively with restriction to each subgoal that has newly emerged due to
‹m🚫1›. This is analogous to the tactic combinator 🚫‹THEN_ALL_NEW› in
Isabelle/ML, see also 🍋‹"isabelle-implementation"›. For example, ‹(rule
r; blast)› applies rule ‹r› and then solves all new subgoals by ‹blast›.
Moreover, the explicit goal restriction operator ``‹[n]›'' exposes only the
first ‹n› subgoals (which need to exist), with default ‹n = 1›. For example,
the method expression ``‹simp_all[3]›'' simplifies the first three subgoals,
while ``‹(rule r, simp_all)[]›'' simplifies all new goals that emerge from
applying rule ‹r› to the originally first one.
🚫
Improper methods, notably tactic emulations, offer low-level goal addressing
as explicit argument to the individual tactic being involved. Here ``‹[!]›''
refers to all goals, and ``‹[n-]›'' to all goals starting from ‹n›.
🚫‹
@{syntax_def goal_spec}:
'[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
›
›
subsection ‹Initial and terminal proof steps \label{sec:proof-steps}›
text ‹
\begin{matharray}{rcl}
@{command_def "proof"} & : & ‹proof(prove) → proof(state)› \\
@{command_def "qed"} & : & ‹proof(state) → proof(state) | local_theory | theory› \\
@{command_def "by"} & : & ‹proof(prove) → proof(state) | local_theory | theory› \\
@{command_def ".."} & : & ‹proof(prove) → proof(state) | local_theory | theory› \\
@{command_def "."} & : & ‹proof(prove) → proof(state) | local_theory | theory› \\
@{command_def "sorry"} & : & ‹proof(prove) → proof(state) | local_theory | theory› \\
@{method_def standard} & : & ‹method› \\
\end{matharray}
Arbitrary goal refinement via tactics is considered harmful. Structured
proof composition in Isar admits proof methods to be invoked in two places
only.
🚫 An 🚫‹initial› refinement step @{command_ref "proof"}~‹m🚫1› reduces a
newly stated goal to a number of sub-goals that are to be solved later.
Facts are passed to ‹m🚫1› for forward chaining, if so indicated by
‹proof(chain)› mode.
🚫 A 🚫‹terminal› conclusion step @{command_ref "qed"}~‹m🚫2› is intended to
solve remaining goals. No facts are passed to ‹m🚫2›.
The only other (proper) way to affect pending goals in a proof body is by
@{command_ref "show"}, which involves an explicit statement of what is to be
solved eventually. Thus we avoid the fundamental problem of unstructured
tactic scripts that consist of numerous consecutive goal transformations,
with invisible effects.
🚫
As a general rule of thumb for good proof style, initial proof methods
should either solve the goal completely, or constitute some well-understood
reduction to new sub-goals. Arbitrary automatic proof tools that are prone
leave a large number of badly structured sub-goals are no help in continuing
the proof document in an intelligible manner.
Unless given explicitly by the user, the default initial method is @{method
standard}, which subsumes at least @{method_ref (Pure) rule} or its
classical variant @{method_ref (HOL) rule}. These methods apply a single
standard elimination or introduction rule according to the topmost logical
connective involved. There is no separate default terminal method. Any
remaining goals are always solved by assumption in the very last step.
🚫‹
@@{command proof} method?
;
@@{command qed} method?
;
@@{command "by"} method method?
;
(@@{command "."} | @@{command ".."} | @@{command sorry})
›
🚫 @{command "proof"}~‹m🚫1› refines the goal by proof method ‹m🚫1›; facts for
forward chaining are passed if so indicated by ‹proof(chain)› mode.
🚫 @{command "qed"}~‹m🚫2› refines any remaining goals by proof method ‹m🚫2›
and concludes the sub-proof by assumption. If the goal had been ‹show›, some
pending sub-goal is solved as well by the rule resulting from the result
🚫‹exported› into the enclosing goal context. Thus ‹qed› may fail for two
reasons: either ‹m🚫2› fails, or the resulting rule does not fit to any
pending goal🚫‹This includes any additional ``strong'' assumptions as
introduced by @{command "assume"}.› of the enclosing context. Debugging such
a situation might involve temporarily changing @{command "show"} into
@{command "have"}, or weakening the local context by replacing occurrences
of @{command "assume"} by @{command "presume"}.
🚫 @{command "by"}~‹m🚫1 m🚫2› is a 🚫‹terminal proof›\index{proof!terminal}; it
abbreviates @{command "proof"}~‹m🚫1›~@{command "qed"}~‹m🚫2›, but with
backtracking across both methods. Debugging an unsuccessful @{command
"by"}~‹m🚫1 m🚫2› command can be done by expanding its definition; in many
cases @{command "proof"}~‹m🚫1› (or even ‹apply›~‹m🚫1›) is already sufficient
to see the problem.
🚫 ``@{command ".."}'' is a 🚫‹standard proof›\index{proof!standard}; it
abbreviates @{command "by"}~‹standard›.
🚫 ``@{command "."}'' is a 🚫‹trivial proof›\index{proof!trivial}; it
abbreviates @{command "by"}~‹this›.
🚫 @{command "sorry"} is a 🚫‹fake proof›\index{proof!fake} pretending to
solve the pending claim without further ado. This only works in interactive
development, or if the @{attribute quick_and_dirty} is enabled. Facts
emerging from fake proofs are not the real thing. Internally, the derivation
object is tainted by an oracle invocation, which may be inspected via the
command @{command "thm_oracles"} (\secref{sec:oracles}).
The most important application of @{command "sorry"} is to support
experimentation and top-down proof development.
🚫 @{method standard} refers to the default refinement step of some Isar
language elements (notably @{command proof} and ``@{command ".."}''). It is
🚫‹dynamically scoped›, so the behaviour depends on the application
environment.
In Isabelle/Pure, @{method standard} performs elementary introduction~/
elimination steps (@{method_ref (Pure) rule}), introduction of type classes
(@{method_ref intro_classes}) and locales (@{method_ref intro_locales}).
In Isabelle/HOL, @{method standard} also takes classical rules into account
(cf.\ \secref{sec:classical}).
›
subsection ‹Fundamental methods and attributes \label{sec:pure-meth-att}›
text ‹
The following proof methods and attributes refer to basic logical operations
of Isar. Further methods and attributes are provided by several generic and
object-logic specific tools and packages (see \chref{ch:gen-tools} and
\partref{part:hol}).
\begin{matharray}{rcl}
@{command_def "print_rules"}‹🚫*› & : & ‹context →› \\[0.5ex]
@{method_def "-"} & : & ‹method› \\
@{method_def "goal_cases"} & : & ‹method› \\
@{method_def "subproofs"} & : & ‹method› \\
@{method_def "fact"} & : & ‹method› \\
@{method_def "assumption"} & : & ‹method› \\
@{method_def "this"} & : & ‹method› \\
@{method_def (Pure) "rule"} & : & ‹method› \\
@{attribute_def (Pure) "intro"} & : & ‹attribute› \\
@{attribute_def (Pure) "elim"} & : & ‹attribute› \\
@{attribute_def (Pure) "dest"} & : & ‹attribute› \\
@{attribute_def (Pure) "rule"} & : & ‹attribute› \\[0.5ex]
@{attribute_def "OF"} & : & ‹attribute› \\
@{attribute_def "of"} & : & ‹attribute› \\
@{attribute_def "where"} & : & ‹attribute› \\
\end{matharray}
🚫‹
@@{method goal_cases} (@{syntax name}*)
;
@@{method subproofs} @{syntax method}
;
@@{method fact} @{syntax thms}?
;
@@{method (Pure) rule} @{syntax thms}?
;
rulemod: ('intro' | 'elim' | 'dest')
((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thms}
;
(@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
('!' | () | '?') @{syntax nat}?
;
@@{attribute (Pure) rule} 'del'
;
@@{attribute OF} @{syntax thms}
;
@@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
;
@@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}
›
🚫 @{command "print_rules"} prints rules declared via attributes @{attribute
(Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of
Isabelle/Pure.
See also the analogous @{command "print_claset"} command for similar rule
declarations of the classical reasoner (\secref{sec:classical}).
🚫 ``@{method "-"}'' (minus) inserts the forward chaining facts as premises
into the goal, and nothing else.
Note that command @{command_ref "proof"} without any method actually
performs a single reduction step using the @{method_ref (Pure) rule} method;
thus a plain 🚫‹do-nothing› proof step would be ``@{command "proof"}~‹-›''
rather than @{command "proof"} alone.
🚫 @{method "goal_cases"}~‹a🚫1 … a🚫n› turns the current subgoals into cases
within the context (see also \secref{sec:cases-induct}). The specified case
names are used if present; otherwise cases are numbered starting from 1.
Invoking cases in the subsequent proof body via the @{command_ref case}
command will @{command fix} goal parameters, @{command assume} goal
premises, and @{command let} variable @{variable_ref ?case} refer to the
conclusion.
🚫 @{method "subproofs"}~‹m› applies the method expression ‹m› consecutively
to each subgoal, constructing individual subproofs internally (analogous to
``🚫‹show goal by m›'' for each subgoal of the proof state). Search
alternatives of ‹m› are truncated: the method is forced to be deterministic.
This method combinator impacts the internal construction of proof terms: it
makes a cascade of let-expressions within the derivation tree and may thus
improve scalability.
🚫 @{method "fact"}~‹a🚫1 … a🚫n› composes some fact from ‹a🚫1, …, a🚫n› (or
implicitly from the current proof context) modulo unification of schematic
type and term variables. The rule structure is not taken into account, i.e.java.lang.NullPointerException
meta-level implication is considered atomic. This is the same principle
underlying literal facts (cf.\ \secref{sec:syn-att}): ``@{command
"have"}~‹φ›~@{command "by"}~‹fact›'' is equivalent to ``@{command
"note"}~🍋‹`›‹φ›🍋‹`›'' provided that ‹⊨ φ› is an instance of some known ‹⊨ φ›
in the proof context.
🚫 @{method assumption} solves some goal by a single assumption step. All
given facts are guaranteed to participate in the refinement; this means
there may be only 0 or 1 in the first place. Recall that @{command "qed"}
(\secref{sec:proof-steps}) already concludes any remaining sub-goals by
assumption, so structured proofs usually need not quote the @{method
assumption} method at all.
🚫 @{method this} applies all of the current facts directly as rules. Recall
that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~‹this›''.
🚫 @{method (Pure) rule}~‹a🚫1 … a🚫n› applies some rule given as argument in
backward manner; facts are used to reduce the rule before applying it to the
goal. Thus @{method (Pure) rule} without facts is plain introduction, while
with facts it becomes elimination.
When no arguments are given, the @{method (Pure) rule} method tries to pick
appropriate rules automatically, as declared in the current context using
the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
dest} attributes (see below). This is included in the standard behaviour of
@{command "proof"} and ``@{command ".."}'' (double-dot) steps (see
\secref{sec:proof-steps}).
🚫 @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute
(Pure) dest} declare introduction, elimination, and destruct rules, to be
used with method @{method (Pure) rule}, and similar tools. Note that the
latter will ignore rules declared with ``‹?›'', while ``‹!›'' are used most
aggressively.
The classical reasoner (see \secref{sec:classical}) introduces its own
variants of these attributes; use qualified names to access the present
versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}.
🚫 @{attribute (Pure) rule}~‹del› undeclares introduction, elimination, or
destruct rules.
🚫 @{attribute OF}~‹a🚫1 … a🚫n› applies some theorem to all of the given rules
‹a🚫1, …, a🚫n› in canonical right-to-left order, which means that premises
stemming from the ‹a🚫i› emerge in parallel in the result, without
interfering with each other. In many practical situations, the ‹a🚫i› do not
have premises themselves, so ‹rule [OF a🚫1 … a🚫n]› can be actually read as
functional application (modulo unification).
Argument positions may be effectively skipped by using ``‹_›'' (underscore),
which refers to the propositional identity rule in the Pure theory.
🚫 @{attribute of}~‹t🚫1 … t🚫n› performs positional instantiation of term
variables. The terms ‹t🚫1, …, t🚫n› are substituted for any schematic
variables occurring in a theorem from left to right; ``‹_›'' (underscore)
indicates to skip a position. Arguments following a ``‹concl:›''
specification refer to positions of the conclusion of a rule.
An optional context of local variables ‹🚫 x🚫1 … x🚫m› may be specified:
the instantiated theorem is exported, and these variables become schematic
(usually with some shifting of indices).
🚫 @{attribute "where"}~‹x🚫1 = t🚫1 🚫 … x🚫n = t🚫n› performs named
instantiation of schematic type and term variables occurring in a theorem.
Schematic variables have to be specified on the left-hand side (e.g.java.lang.NullPointerException
‹?x1.3›). The question mark may be omitted if the variable name is a plain
identifier without index. As type instantiations are inferred from term
instantiations, explicit type instantiations are seldom necessary.
An optional context of local variables ‹🚫 x🚫1 … x🚫m› may be specified
as for @{attribute "of"} above.
›
subsection ‹Defining proof methods›
text ‹
\begin{matharray}{rcl}
@{command_def "method_setup"} & : & ‹local_theory → local_theory› \\
\end{matharray}
🚫‹
@@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
›
🚫 @{command "method_setup"}~‹name = text description› defines a proof method
in the current context. The given ‹text› has to be an ML expression of type
🚫‹(Proof.context -> Proof.method) context_parser›, cf.\ basic
parsers defined in structure 🚫‹Args› and 🚫‹Attrib›. There are also combinators like 🚫‹METHOD› and 🚫‹SIMPLE_METHOD› to turn certain tactic forms into official proof methods; the
primed versions refer to tactics with explicit goal addressing.
Here are some example method definitions:
›
(*<*)experiment begin(*>*)
method_setup my_method1 =
‹Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\
"my first method (without any arguments)"
method_setup my_method2 =
‹Scan.succeed (fn ctxt: Proof.context =>
SIMPLE_METHOD' (fn i: int => no_tac))\
"my second method (with context)"
method_setup my_method3 =
‹Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
SIMPLE_METHOD' (fn i: int => no_tac))\
"my third method (with theorem arguments and context)"
(*<*)end(*>*)
section ‹Proof by cases and induction \label{sec:cases-induct}›
subsection ‹Rule contexts›
text ‹
\begin{matharray}{rcl}
@{command_def "case"} & : & ‹proof(state) → proof(state)› \\
@{command_def "print_cases"}‹🚫*› & : & ‹context →› \\
@{attribute_def case_names} & : & ‹attribute› \\
@{attribute_def case_conclusion} & : & ‹attribute› \\
@{attribute_def params} & : & ‹attribute› \\
@{attribute_def consumes} & : & ‹attribute› \\
\end{matharray}
The puristic way to build up Isar proof contexts is by explicit language
elements like @{command "fix"}, @{command "assume"}, @{command "let"} (see
\secref{sec:proof-context}). This is adequate for plain natural deduction,
but easily becomes unwieldy in concrete verification tasks, which typically
involve big induction rules with several cases.
The @{command "case"} command provides a shorthand to refer to a local
context symbolically: certain proof methods provide an environment of named
``cases'' of the form ‹c: x🚫1, …, x🚫m, φ🚫1, …, φ🚫n›; the effect of
``@{command "case"}~‹c›'' is then equivalent to ``@{command "fix"}~‹x🚫1 …
x🚫m›~@{command "assume"}~‹c: φ🚫1 … φ🚫n›''. Term bindings may be covered as
well, notably @{variable ?case} for the main conclusion.
By default, the ``terminology'' ‹x🚫1, …, x🚫m› of a case value is marked as
hidden, i.e.\ there is no way to refer to such parameters in the subsequent
proof text. After all, original rule parameters stem from somewhere outside
of the current proof text. By using the explicit form ``@{command
"case"}~‹(c y🚫1 … y🚫m)›'' instead, the proof author is able to chose local
names that fit nicely into the current context.
🚫
It is important to note that proper use of @{command "case"} does not
provide means to peek at the current goal state, which is not directly
observable in Isar! Nonetheless, goal refinement commands do provide named
cases ‹goal🚫i› for each subgoal ‹i = 1, …, n› of the resulting goal state.
Using this extra feature requires great care, because some bits of the
internal tactical machinery intrude the proof text. In particular, parameter
names stemming from the left-over of automated reasoning tools are usually
quite unpredictable.
Under normal circumstances, the text of cases emerge from standard
elimination or induction rules, which in turn are derived from previous
theory specifications in a canonical way (say from @{command "inductive"}
definitions).
🚫
Proper cases are only available if both the proof method and the rules
involved support this. By using appropriate attributes, case names,
conclusions, and parameters may be also declared by hand. Thus variant
versions of rules that have been derived manually become ready to use in
advanced case analysis later.
🚫‹
@@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')')
;
@@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) *) ']' ) ? ) +)
;
@@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
;
@@{attribute params} ((@{syntax name} * ) + @'and')
;
@@{attribute consumes} @{syntax int}?
›
🚫 @{command "case"}~‹a: (c x🚫1 … x🚫m)› invokes a named local context ‹c:
x🚫1, …, x🚫m, φ🚫1, …, φ🚫m›, as provided by an appropriate proof method (such
as @{method_ref cases} and @{method_ref induct}). The command ``@{command
"case"}~‹a: (c x🚫1 … x🚫m)›'' abbreviates ``@{command "fix"}~‹x🚫1 …
x🚫m›~@{command "assume"}~‹a.c: φ🚫1 … φ🚫n›''. Each local fact is qualified by
the prefix ‹a›, and all such facts are collectively bound to the name ‹a›.
The fact name is specification ‹a› is optional, the default is to re-use
‹c›. So @{command "case"}~‹(c x🚫1 … x🚫m)› is the same as @{command
"case"}~‹c: (c x🚫1 … x🚫m)›.
🚫 @{command "print_cases"} prints all local contexts of the current state,
using Isar proof language notation.
🚫 @{attribute case_names}~‹c🚫1 … c🚫k› declares names for the local contexts
of premises of a theorem; ‹c🚫1, …, c🚫k› refers to the 🚫‹prefix› of the list
of premises. Each of the cases ‹c🚫i› can be of the form ‹c[h🚫1 … h🚫n]› where
the ‹h🚫1 … h🚫n› are the names of the hypotheses in case ‹c🚫i› from left to
right.
🚫 @{attribute case_conclusion}~‹c d🚫1 … d🚫k› declares names for the
conclusions of a named premise ‹c›; here ‹d🚫1, …, d🚫k› refers to the prefix
of arguments of a logical formula built by nesting a binary connective
(e.g.\ ‹∨›).
Note that proof methods such as @{method induct} and @{method coinduct}
already provide a default name for the conclusion as a whole. The need to
name subformulas only arises with cases that split into several sub-cases,
as in common co-induction rules.
🚫 @{attribute params}~‹p🚫1 … p🚫m 🚫 … q🚫1 … q🚫n› renames the innermost
parameters of premises ‹1, …, n› of some theorem. An empty list of names may
be given to skip positions, leaving the present parameters unchanged.
Note that the default usage of case rules does 🚫‹not› directly expose
parameters to the proof context.
🚫 @{attribute consumes}~‹n› declares the number of ``major premises'' of a
rule, i.e.\ the number of facts to be consumed when it is applied by an
appropriate proof method. The default value of @{attribute consumes} is ‹n =
1›, which is appropriate for the usual kind of cases and induction rules for
inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
@{attribute consumes} declaration given are treated as if @{attribute
consumes}~‹0› had been specified.
A negative ‹n› is interpreted relatively to the total number of premises of
the rule in the target context. Thus its absolute value specifies the
remaining number of premises, after subtracting the prefix of major premises
as indicated above. This form of declaration has the technical advantage of
being stable under more morphisms, notably those that export the result from
a nested @{command_ref context} with additional assumptions.
Note that explicit @{attribute consumes} declarations are only rarely
needed; this is already taken care of automatically by the higher-level
@{attribute cases}, @{attribute induct}, and @{attribute coinduct}
declarations.
›
subsection ‹Proof methods›
text ‹
\begin{matharray}{rcl}
@{method_def cases} & : & ‹method› \\
@{method_def induct} & : & ‹method› \\
@{method_def induction} & : & ‹method› \\
@{method_def coinduct} & : & ‹method› \\
\end{matharray}
The @{method cases}, @{method induct}, @{method induction}, and @{method
coinduct} methods provide a uniform interface to common proof techniques
over datatypes, inductive predicates (or sets), recursive functions etc. The
corresponding rules may be specified and instantiated in a casual manner.
Furthermore, these methods provide named local contexts that may be invoked
via the @{command "case"} proof command within the subsequent proof text.
This accommodates compact proof texts even when reasoning about large
specifications.
The @{method induct} method also provides some infrastructure to work with
structured statements (either using explicit meta-level connectives, or
including facts and parameters separately). This avoids cumbersome encoding
of ``strengthened'' inductive statements within the object-logic.
Method @{method induction} differs from @{method induct} only in the names
of the facts in the local context invoked by the @{command "case"} command.
🚫‹
@@{method cases} ('(' 'no_simp' ')')? 🍋
(@{syntax insts} * @'and') rule?
;
(@@{method induct} | @@{method induction})
('(' 'no_simp' ')')? (definsts * @'and') 🍋 arbitrary? taking? rule?
;
@@{method coinduct} @{syntax insts} taking rule?
;
rule: ('type' | 'pred' | 'set') ':' (@{syntax name} +) | 'rule' ':' (@{syntax thm} +)
;
definst: @{syntax name} ('==' | '\') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst}
;
definsts: ( definst * )
;
arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
;
taking: 'taking' ':' @{syntax insts}
›
🚫 @{method cases}~‹insts R› applies method @{method rule} with an
appropriate case distinction theorem, instantiated to the subjects ‹insts›.
Symbolic case names are bound according to the rule's local contexts.
The rule is determined as follows, according to the facts and arguments
passed to the @{method cases} method:
🚫
\begin{tabular}{llll}
facts & & arguments & rule \\\hline
‹⊨ R› & @{method cases} & & implicit rule ‹R› \\
& @{method cases} & & classical case split \\
& @{method cases} & ‹t› & datatype exhaustion (type of ‹t›) \\
‹⊨ A t› & @{method cases} & ‹…› & inductive predicate/set elimination (of ‹A›) \\
‹…› & @{method cases} & ‹… rule: R› & explicit rule ‹R› \\
\end{tabular}
🚫
Several instantiations may be given, referring to the 🚫‹suffix› of premises
of the case rule; within each premise, the 🚫‹prefix› of variables is
instantiated. In most situations, only a single term needs to be specified;
this refers to the first variable of the last premise (it is usually the
same for all cases). The ‹(no_simp)› option can be used to disable
pre-simplification of cases (see the description of @{method induct} below
for details).
🚫 @{method induct}~‹insts R› and @{method induction}~‹insts R› are analogous
to the @{method cases} method, but refer to induction rules, which are
determined as follows:
🚫
\begin{tabular}{llll}
facts & & arguments & rule \\\hline
& @{method induct} & ‹P x› & datatype induction (type of ‹x›) \\
‹⊨ A x› & @{method induct} & ‹…› & predicate/set induction (of ‹A›) \\
‹…› & @{method induct} & ‹… rule: R› & explicit rule ‹R› \\
\end{tabular}
🚫
Several instantiations may be given, each referring to some part of a mutual
inductive definition or datatype --- only related partial induction rules
may be used together, though. Any of the lists of terms ‹P, x, …› refers to
the 🚫‹suffix› of variables present in the induction rule. This enables the
writer to specify only induction variables, or both predicates and
variables, for example.
Instantiations may be definitional: equations ‹x ≡ t› introduce local
definitions, which are inserted into the claim and discharged after applying
the induction rule. Equalities reappear in the inductive cases, but have
been transformed according to the induction principle being involved here.
In order to achieve practically useful induction hypotheses, some variables
occurring in ‹t› need to generalized (see below). Instantiations of
the form ‹t›, where ‹t› is not a variable, are taken as a shorthand for ‹x ≡
t›, where ‹x› is a fresh variable. If this is not intended, ‹t› has to be
enclosed in parentheses. By default, the equalities generated by
definitional instantiations are pre-simplified using a specific set of
rules, usually consisting of distinctness and injectivity theorems for
datatypes. This pre-simplification may cause some of the parameters of an
inductive case to disappear, or may even completely delete some of the
inductive cases, if one of the equalities occurring in their premises can be
simplified to ‹False›. The ‹(no_simp)› option can be used to disable
pre-simplification. Additional rules to be used in pre-simplification can be
declared using the @{attribute_def induct_simp} attribute.
The optional ``‹arbitrary: x🚫1 … x🚫m›'' specification generalizes variables
‹x🚫1, …, x🚫m› of the original goal before applying induction. It is possible
to separate variables by ``‹and›'' to generalize in goals other than
the first. Thus induction hypotheses may become sufficiently general to get
the proof through. Together with definitional instantiations, one may
effectively perform induction over expressions of a certain structure.
--> --------------------
--> maximum size reached
--> --------------------
