doc-src/TutorialI/Rules/rules.tex
author paulson
Mon, 23 Oct 2000 16:25:04 +0200
changeset 10295 8eb12693cead
child 10301 8a5aa26c125f
permissions -rw-r--r--
the Rules chapter and theories
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10295
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     1
\chapter{The Rules of the Game}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     2
\label{chap:rules}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     3
 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     4
Until now, we have proved everything using only induction and simplification.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     5
Substantial proofs require more elaborate forms of inference.  This chapter
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     6
outlines the concepts and techniques that underlie reasoning in Isabelle. The examples
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     7
are mainly drawn from predicate logic.  The first examples in this
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     8
chapter will consist of detailed, low-level proof steps.  Later, we shall
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     9
see how to automate such reasoning using the methods \isa{blast},
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    10
\isa{auto} and others. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    11
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    12
\section{Natural deduction}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    13
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    14
In Isabelle, proofs are constructed using inference rules. The 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    15
most familiar inference rule is probably \emph{modus ponens}: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    16
\[ \infer{Q}{P\imp Q & P} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    17
This rule says that from $P\imp Q$ and $P$  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    18
we may infer~$Q$.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    19
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    20
%Early logical formalisms had this  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    21
%rule and at most one or two others, along with many complicated 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    22
%axioms. Any desired theorem could be obtained by applying \emph{modus 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    23
%ponens} or other rules to the axioms, but proofs were 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    24
%hard to find. For example, a standard inference system has 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    25
%these two axioms (amongst others): 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    26
%\begin{gather*}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    27
%  P\imp(Q\imp P) \tag{K}\\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    28
%  (P\imp(Q\imp R))\imp ((P\imp Q)\imp(P\imp R))  \tag{S}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    29
%\end{gather*}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    30
%Try proving the trivial fact $P\imp P$ using these axioms and \emph{modus
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    31
%ponens}!
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    32
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    33
\textbf{Natural deduction} is an attempt to formalize logic in a way 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    34
that mirrors human reasoning patterns. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    35
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    36
%Instead of having a few 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    37
%inference rules and many axioms, it has many inference rules 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    38
%and few axioms. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    39
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    40
For each logical symbol (say, $\conj$), there 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    41
are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    42
The introduction rules allow us to infer this symbol (say, to 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    43
infer conjunctions). The elimination rules allow us to deduce 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    44
consequences from this symbol. Ideally each rule should mention 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    45
one symbol only.  For predicate logic this can be 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    46
done, but when users define their own concepts they typically 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    47
have to refer to other symbols as well.  It is best not be dogmatic.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    48
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    49
Natural deduction generally deserves its name.  It is easy to use.  Each
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    50
proof step consists of identifying the outermost symbol of a formula and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    51
applying the corresponding rule.  It creates new subgoals in
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    52
an obvious way from parts of the chosen formula.  Expanding the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    53
definitions of constants can blow up the goal enormously.  Deriving natural
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    54
deduction rules for such constants lets us reason in terms of their key
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    55
properties, which might otherwise be obscured by the technicalities of its
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    56
definition.  Natural deduction rules also lend themselves to automation.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    57
Isabelle's
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    58
\textbf{classical  reasoner} accepts any suitable  collection of natural deduction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    59
rules and uses them to search for proofs automatically.  Isabelle is designed around
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    60
natural deduction and many of its  tools use the terminology of introduction and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    61
elimination rules.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    62
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    63
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    64
\section{Introduction rules}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    65
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    66
An \textbf{introduction} rule tells us when we can infer a formula 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    67
containing a specific logical symbol. For example, the conjunction 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    68
introduction rule says that if we have $P$ and if we have $Q$ then 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    69
we have $P\conj Q$. In a mathematics text, it is typically shown 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    70
like this:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    71
\[  \infer{P\conj Q}{P & Q} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    72
The rule introduces the conjunction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    73
symbol~($\conj$) in its conclusion.  Of course, in Isabelle proofs we
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    74
mainly  reason backwards.  When we apply this rule, the subgoal already has
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    75
the form of a conjunction; the proof step makes this conjunction symbol
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    76
disappear. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    77
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    78
In Isabelle notation, the rule looks like this:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    79
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    80
\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    81
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    82
Carefully examine the syntax.  The premises appear to the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    83
left of the arrow and the conclusion to the right.  The premises (if 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    84
more than one) are grouped using the fat brackets.  The question marks
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    85
indicate \textbf{schematic variables} (also called \textbf{unknowns}): they may
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    86
be replaced by arbitrary formulas.  If we use the rule backwards, Isabelle
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    87
tries to unify the current subgoal with the conclusion of the rule, which
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    88
has the form \isa{?P\ \isasymand\ ?Q}.  (Unification is discussed below,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    89
\S\ref{sec:unification}.)  If successful,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    90
it yields new subgoals given by the formulas assigned to 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    91
\isa{?P} and \isa{?Q}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    92
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    93
The following trivial proof illustrates this point. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    94
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    95
\isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    96
Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    97
(Q\ \isasymand\ P){"}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    98
\isacommand{apply}\ (rule\ conjI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    99
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   100
\isacommand{apply}\ (rule\ conjI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   101
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   102
\isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   103
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   104
At the start, Isabelle presents 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   105
us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   106
\isa{P\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   107
(Q\ \isasymand\ P)}.  We are working backwards, so when we
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   108
apply conjunction introduction, the rule removes the outermost occurrence
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   109
of the \isa{\isasymand} symbol.  To apply a  rule to a subgoal, we apply
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   110
the proof method {\isa{rule}} --- here with {\isa{conjI}}, the  conjunction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   111
introduction rule. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   112
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   113
%{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   114
%\isasymand\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   115
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   116
\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   117
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   118
Isabelle leaves two new subgoals: the two halves of the original conjunction. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   119
The first is simply \isa{P}, which is trivial, since \isa{P} is among 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   120
the assumptions.  We can apply the {\isa{assumption}} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   121
method, which proves a subgoal by finding a matching assumption.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   122
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   123
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   124
Q\ \isasymand\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   125
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   126
We are left with the subgoal of proving  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   127
\isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}.  We apply
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   128
\isa{rule conjI} again. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   129
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   130
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   131
\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   132
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   133
We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   134
using the {\isa{assumption}} method. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   135
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   136
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   137
\section{Elimination rules}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   138
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   139
\textbf{Elimination} rules work in the opposite direction from introduction 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   140
rules. In the case of conjunction, there are two such rules. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   141
From $P\conj Q$ we infer $P$. also, from $P\conj Q$  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   142
we infer $Q$:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   143
\[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q}  \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   144
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   145
Now consider disjunction. There are two introduction rules, which resemble inverted forms of the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   146
conjunction elimination rules:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   147
\[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q}  \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   148
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   149
What is the disjunction elimination rule?  The situation is rather different from 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   150
conjunction.  From $P\disj Q$ we cannot conclude  that $P$ is true and we
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   151
cannot conclude that $Q$ is true; there are no direct
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   152
elimination rules of the sort that we have seen for conjunction.  Instead,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   153
there is an elimination  rule that works indirectly.  If we are trying  to prove
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   154
something else, say $R$, and we know that $P\disj Q$ holds,  then we have to consider
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   155
two cases.  We can assume that $P$ is true  and prove $R$ and then assume that $Q$ is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   156
true and prove $R$ a second  time.  Here we see a fundamental concept used in natural
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   157
deduction:  that of the \textbf{assumptions}. We have to prove $R$ twice, under
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   158
different assumptions.  The assumptions are local to these subproofs and are visible 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   159
nowhere else. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   160
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   161
In a logic text, the disjunction elimination rule might be shown 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   162
like this:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   163
\[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   164
The assumptions $[P]$ and $[Q]$ are bracketed 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   165
to emphasize that they are local to their subproofs.  In Isabelle 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   166
notation, the already-familiar \isa\isasymLongrightarrow syntax serves the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   167
same  purpose:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   168
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   169
\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   170
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   171
When we use this sort of elimination rule backwards, it produces 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   172
a case split.  (We have this before, in proofs by induction.)  The following  proof
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   173
illustrates the use of disjunction elimination.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   174
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   175
\isacommand{lemma}\ disj_swap:\ {"}P\ \isasymor\ Q\ 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   176
\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   177
\isacommand{apply}\ (erule\ disjE)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   178
\ \isacommand{apply}\ (rule\ disjI2)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   179
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   180
\isacommand{apply}\ (rule\ disjI1)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   181
\isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   182
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   183
We assume \isa{P\ \isasymor\ Q} and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   184
must prove \isa{Q\ \isasymor\ P}\@.  Our first step uses the disjunction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   185
elimination rule, \isa{disjE}.  The method {\isa{erule}}  applies an
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   186
elimination rule to the assumptions, searching for one that matches the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   187
rule's first premise.  Deleting that assumption, it
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   188
return the subgoals for the remaining premises.  Most of the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   189
time, this is  the best way to use elimination rules; only rarely is there
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   190
any  point in keeping the assumption.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   191
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   192
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   193
%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   194
\ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   195
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   196
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   197
Here it leaves us with two subgoals.  The first assumes \isa{P} and the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   198
second assumes \isa{Q}.  Tackling the first subgoal, we need to 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   199
show \isa{Q\ \isasymor\ P}\@.  The second introduction rule (\isa{disjI2})
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   200
can reduce this  to \isa{P}, which matches the assumption. So, we apply the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   201
{\isa{rule}}  method with \isa{disjI2} \ldots
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   202
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   203
\ 1.\ P\ \isasymLongrightarrow\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   204
\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   205
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   206
\ldots and finish off with the {\isa{assumption}} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   207
method.  We are left with the other subgoal, which 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   208
assumes \isa{Q}.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   209
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   210
\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   211
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   212
Its proof is similar, using the introduction 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   213
rule \isa{disjI1}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   214
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   215
The result of this proof is a new inference rule \isa{disj_swap}, which is neither 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   216
an introduction nor an elimination rule, but which might 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   217
be useful.  We can use it to replace any goal of the form $Q\disj P$
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   218
by a one of the form $P\disj Q$.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   219
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   220
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   221
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   222
\section{Destruction rules: some examples}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   223
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   224
Now let us examine the analogous proof for conjunction. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   225
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   226
\isacommand{lemma}\ conj_swap:\ {"}P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   227
\isacommand{apply}\ (rule\ conjI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   228
\ \isacommand{apply}\ (drule\ conjunct2)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   229
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   230
\isacommand{apply}\ (drule\ conjunct1)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   231
\isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   232
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   233
Recall that the conjunction elimination rules --- whose Isabelle names are 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   234
\isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   235
of a conjunction.  Rules of this sort (where the conclusion is a subformula of a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   236
premise) are called \textbf{destruction} rules, by analogy with the destructor
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   237
functions of functional pr§gramming.%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   238
\footnote{This Isabelle terminology has no counterpart in standard logic texts, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   239
although the distinction between the two forms of elimination rule is well known. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   240
Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules are very
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   241
bad.  What is catastrophic about them is the parasitic presence of a formula [$R$]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   242
which has no structural link with the formula which is eliminated.''}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   243
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   244
The first proof step applies conjunction introduction, leaving 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   245
two subgoals: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   246
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   247
%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   248
\ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   249
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   250
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   251
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   252
To invoke the elimination rule, we apply a new method, \isa{drule}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   253
Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   254
you prefer).   Applying the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   255
second conjunction rule using \isa{drule} replaces the assumption 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   256
\isa{P\ \isasymand\ Q} by \isa{Q}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   257
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   258
\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   259
\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   260
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   261
The resulting subgoal can be proved by applying \isa{assumption}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   262
The other subgoal is similarly proved, using the \isa{conjunct1} rule and the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   263
\isa{assumption} method.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   264
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   265
Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   266
you.  Isabelle does not attempt to work out whether a rule 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   267
is an introduction rule or an elimination rule.  The 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   268
method determines how the rule will be interpreted. Many rules 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   269
can be used in more than one way.  For example, \isa{disj_swap} can 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   270
be applied to assumptions as well as to goals; it replaces any
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   271
assumption of the form
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   272
$P\disj Q$ by a one of the form $Q\disj P$.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   273
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   274
Destruction rules are simpler in form than indirect rules such as \isa{disjE},
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   275
but they can be inconvenient.  Each of the conjunction rules discards half 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   276
of the formula, when usually we want to take both parts of the conjunction as new
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   277
assumptions.  The easiest way to do so is by using an 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   278
alternative conjunction elimination rule that resembles \isa{disjE}.  It is seldom,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   279
if ever, seen in logic books.  In Isabelle syntax it looks like this: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   280
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   281
\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   282
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   283
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   284
\begin{exercise}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   285
Use the rule {\isa{conjE}} to shorten the proof above. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   286
\end{exercise}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   287
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   288
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   289
\section{Implication}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   290
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   291
At the start of this chapter, we saw the rule \textit{modus ponens}.  It is, in fact,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   292
a destruction rule. The matching introduction rule looks like this 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   293
in Isabelle: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   294
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   295
(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   296
\isasymlongrightarrow\ ?Q\rulename{impI}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   297
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   298
And this is \textit{modus ponens}:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   299
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   300
\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   301
\isasymLongrightarrow\ ?Q
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   302
\rulename{mp}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   303
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   304
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   305
Here is a proof using the rules for implication.  This 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   306
lemma performs a sort of uncurrying, replacing the two antecedents 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   307
of a nested implication by a conjunction. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   308
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   309
\isacommand{lemma}\ imp_uncurry:\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   310
{"}P\ \isasymlongrightarrow\ (Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   311
\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   312
\isasymand\ Q\ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   313
R"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   314
\isacommand{apply}\ (rule\ impI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   315
\isacommand{apply}\ (erule\ conjE)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   316
\isacommand{apply}\ (drule\ mp)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   317
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   318
\isacommand{apply}\ (drule\ mp)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   319
\ \ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   320
\ \isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   321
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   322
First, we state the lemma and apply implication introduction (\isa{rule impI}), 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   323
which moves the conjunction to the assumptions. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   324
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   325
%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   326
%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   327
\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   328
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   329
Next, we apply conjunction elimination (\isa{erule conjE}), which splits this
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   330
conjunction into two  parts. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   331
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   332
\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   333
Q\isasymrbrakk\ \isasymLongrightarrow\ R
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   334
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   335
Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   336
\isasymlongrightarrow\ R)}, where the parentheses have been inserted for
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   337
clarity.  The nested implication requires two applications of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   338
\textit{modus ponens}: \isa{drule mp}.  The first use  yields the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   339
implication \isa{Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   340
\isasymlongrightarrow\ R}, but first we must prove the extra subgoal 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   341
\isa{P}, which we do by assumption. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   342
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   343
\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   344
\ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   345
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   346
Repeating these steps for \isa{Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   347
\isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   348
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   349
\ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   350
\isasymLongrightarrow\ R
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   351
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   352
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   353
The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   354
both stand for implication, but they differ in many respects.  Isabelle
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   355
uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   356
built-in and Isabelle's inference mechanisms treat it specially.  On the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   357
other hand, \isa{\isasymlongrightarrow} is just one of the many connectives
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   358
available in higher-order logic.  We reason about it using inference rules
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   359
such as \isa{impI} and \isa{mp}, just as we reason about the other
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   360
connectives.  You will have to use \isa{\isasymlongrightarrow} in any
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   361
context that requires a formula of higher-order logic.  Use
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   362
\isa{\isasymLongrightarrow} to separate a theorem's preconditions from its
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   363
conclusion.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   364
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   365
When using induction, often the desired theorem results in an induction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   366
hypothesis that is too weak.  In such cases you may have to invent a more
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   367
complicated induction formula, typically involving
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   368
\isa{\isasymlongrightarrow} and \isa{\isasymforall}.  From this lemma you
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   369
derive the desired theorem , typically involving
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   370
\isa{\isasymLongrightarrow}.  We shall see an example below,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   371
\S\ref{sec:proving-euclid}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   372
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   373
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   374
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   375
\remark{negation: notI, notE, ccontr, swap, contrapos?}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   376
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   377
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   378
\section{Unification and substitution}\label{sec:unification}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   379
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   380
As we have seen, Isabelle rules involve variables that begin  with a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   381
question mark. These are called \textbf{schematic} variables  and act as
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   382
placeholders for terms. \textbf{Unification} refers to  the process of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   383
making two terms identical, possibly by replacing  their variables by
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   384
terms. The simplest case is when the two terms  are already the same. Next
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   385
simplest is when the variables in only one of the term
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   386
 are replaced; this is called \textbf{pattern-matching}.  The
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   387
{\isa{rule}} method typically  matches the rule's conclusion
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   388
against the current subgoal.  In the most complex case,  variables in both
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   389
terms are replaced; the {\isa{rule}} method can do this the goal
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   390
itself contains schematic variables.  Other occurrences of the variables in
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   391
the rule or proof state are updated at the same time.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   392
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   393
Schematic variables in goals are sometimes called \textbf{unknowns}.  They
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   394
are useful because they let us proceed with a proof even  when we do not
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   395
know what certain terms should be --- as when the goal is $\exists x.\,P$. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   396
They can be  filled in later, often automatically. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   397
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   398
 Unification is well known to Prolog programmers. Isabelle uses \textbf{higher-order} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   399
unification, which is unification in the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   400
typed $\lambda$-calculus.  The general case is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   401
undecidable, but for our purposes, the differences from ordinary
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   402
unification are straightforward.  It handles bound  variables
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   403
correctly, avoiding capture.  The two terms \isa{{\isasymlambda}x.\ ?P} and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   404
\isa{{\isasymlambda}x.\ t x}  are not unifiable; replacing \isa{?P} by
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   405
\isa{t x} is forbidden because the free occurrence of~\isa{x} would become
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   406
bound.  The two terms
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   407
\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   408
trivially unifiable because they differ only by a bound variable renaming.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   409
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   410
Higher-order unification sometimes must invent
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   411
$\lambda$-terms to replace function  variables,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   412
which can lead to a combinatorial explosion. However,  Isabelle proofs tend
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   413
to involve easy cases where there are few possibilities for the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   414
$\lambda$-term being constructed. In the easiest case, the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   415
function variable is applied only to bound variables, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   416
as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   417
\isa{{\isasymlambda}x\ y.\ f(x+y+a)}.  The only solution is to replace
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   418
\isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}.  Such cases admit at most
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   419
one unifier, like ordinary unification.  A harder case is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   420
unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h},
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   421
namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   422
Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   423
exponential in the number of occurrences of~\isa{a} in the second term.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   424
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   425
Isabelle also uses function variables to express \textbf{substitution}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   426
A typical substitution rule allows us to replace one term by 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   427
another if we know that two terms are equal. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   428
\[ \infer{P[t/x]}{s=t & P[s/x]} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   429
The conclusion uses a notation for substitution: $P[t/x]$ is the result of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   430
replacing $x$ by~$t$ in~$P$.  The rule only substitutes in the positions
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   431
designated by~$x$, which gives it additional power. For example, it can
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   432
derive symmetry of equality from reflexivity.  Using $x=s$ for~$P$
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   433
replaces just the first $s$ in $s=s$ by~$t$.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   434
\[ \infer{t=s}{s=t & \infer{s=s}{}} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   435
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   436
The Isabelle version of the substitution rule looks like this: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   437
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   438
\isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   439
?t
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   440
\rulename{ssubst}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   441
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   442
Crucially, \isa{?P} is a function 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   443
variable: it can be replaced by a $\lambda$-expression 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   444
involving one bound variable whose occurrences identify the places 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   445
in which $s$ will be replaced by~$t$.  The proof above requires
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   446
\isa{{\isasymlambda}x.~x=s}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   447
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   448
The \isa{simp} method replaces equals by equals, but using the substitution
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   449
rule gives us more control. Consider this proof: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   450
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   451
\isacommand{lemma}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   452
"{\isasymlbrakk}\ x\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   453
=\ f\ x;\ odd(f\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   454
x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   455
x"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   456
\isacommand{apply}\ (erule\ ssubst)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   457
\isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   458
\isacommand{done}\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   459
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   460
The simplifier might loop, replacing \isa{x} by \isa{f x} and then by
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   461
\isa{f(f x)} and so forth. (Actually, \isa{simp} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   462
sees the danger and re-orients this equality, but in more complicated cases
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   463
it can be fooled.) When we apply substitution,  Isabelle replaces every
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   464
\isa{x} in the subgoal by \isa{f x} just once: it cannot loop.  The
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   465
resulting subgoal is trivial by assumption. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   466
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   467
We are using the \isa{erule} method it in a novel way. Hitherto, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   468
the conclusion of the rule was just a variable such as~\isa{?R}, but it may
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   469
be any term. The conclusion is unified with the subgoal just as 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   470
it would be with the \isa{rule} method. At the same time \isa{erule} looks 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   471
for an assumption that matches the rule's first premise, as usual.  With
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   472
\isa{ssubst} the effect is to find, use and delete an equality 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   473
assumption.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   474
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   475
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   476
Higher-order unification can be tricky, as this example indicates: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   477
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   478
\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   479
f\ x;\ triple\ (f\ x)\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   480
(f\ x)\ x\ \isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   481
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   482
\isacommand{apply}\ (erule\ ssubst)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   483
\isacommand{back}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   484
\isacommand{back}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   485
\isacommand{back}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   486
\isacommand{back}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   487
\isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   488
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   489
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   490
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   491
By default, Isabelle tries to substitute for all the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   492
occurrences.  Applying \isa{erule\ ssubst} yields this subgoal:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   493
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   494
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   495
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   496
The substitution should have been done in the first two occurrences 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   497
of~\isa{x} only. Isabelle has gone too far. The \isa{back} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   498
method allows us to reject this possibility and get a new one: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   499
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   500
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   501
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   502
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   503
Now Isabelle has left the first occurrence of~\isa{x} alone. That is 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   504
promising but it is not the desired combination. So we use \isa{back} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   505
again:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   506
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   507
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   508
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   509
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   510
This also is wrong, so we use \isa{back} again: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   511
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   512
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   513
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   514
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   515
And this one is wrong too. Looking carefully at the series 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   516
of alternatives, we see a binary countdown with reversed bits: 111,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   517
011, 101, 001.  Invoke \isa{back} again: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   518
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   519
\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   520
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   521
At last, we have the right combination!  This goal follows by assumption.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   522
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   523
Never use {\isa{back}} in the final version of a proof. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   524
It should only be used for exploration. One way to get rid of {\isa{back}} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   525
to combine two methods in a single \textbf{apply} command. Isabelle 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   526
applies the first method and then the second. If the second method 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   527
fails then Isabelle automatically backtracks. This process continues until 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   528
the first method produces an output that the second method can 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   529
use. We get a one-line proof of our example: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   530
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   531
\isacommand{lemma}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   532
"{\isasymlbrakk}\ x\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   533
=\ f\ x;\ triple\ (f\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   534
x)\ (f\ x)\ x\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   535
\isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   536
\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   537
\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   538
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   539
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   540
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   541
The most general way to get rid of the {\isa{back}} command is 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   542
to instantiate variables in the rule.  The method {\isa{rule\_tac}} is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   543
similar to \isa{rule}, but it
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   544
makes some of the rule's variables  denote specified terms.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   545
Also available are {\isa{drule\_tac}}  and \isa{erule\_tac}.  Here we need
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   546
\isa{erule\_tac} since above we used
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   547
\isa{erule}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   548
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   549
\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   550
\isacommand{apply}\ (erule_tac\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   551
P={"}{\isasymlambda}u.\ triple\ u\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   552
u\ x"\ \isakeyword{in}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   553
ssubst)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   554
\isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   555
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   556
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   557
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   558
To specify a desired substitution 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   559
requires instantiating the variable \isa{?P} with a $\lambda$-expression. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   560
The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   561
u\ x} indicate that the first two arguments have to be substituted, leaving
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   562
the third unchanged.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   563
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   564
An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   565
{\isa{of}}  directive, described in \S\ref{sec:forward} below.   An
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   566
advantage  of {\isa{rule\_tac}} is that the instantiations may refer to 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   567
variables bound in the current subgoal.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   568
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   569
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   570
\section{Negation}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   571
 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   572
Negation causes surprising complexity in proofs.  Its natural 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   573
deduction rules are straightforward, but additional rules seem 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   574
necessary in order to handle negated assumptions gracefully. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   575
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   576
Negation introduction deduces $\neg P$ if assuming $P$ leads to a 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   577
contradiction. Negation elimination deduces any formula in the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   578
presence of $\neg P$ together with~$P$: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   579
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   580
(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   581
\rulename{notI}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   582
\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   583
\rulename{notE}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   584
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   585
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   586
Classical logic allows us to assume $\neg P$ 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   587
when attempting to prove~$P$: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   588
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   589
(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   590
\rulename{classical}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   591
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   592
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   593
Three further rules are variations on the theme of contrapositive. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   594
They differ in the placement of the negation symbols: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   595
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   596
\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   597
\rulename{contrapos_pp}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   598
\isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   599
\rulename{contrapos_np}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   600
\isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   601
\rulename{contrapos_nn}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   602
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   603
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   604
These rules are typically applied using the {\isa{erule}} method, where 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   605
their effect is to form a contrapositive from an 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   606
assumption and the goal's conclusion.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   607
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   608
The most important of these is \isa{contrapos_np}.  It is useful
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   609
for applying introduction rules to negated assumptions.  For instance, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   610
the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   611
might want to use conjunction introduction on it. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   612
Before we can do so, we must move that assumption so that it 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   613
becomes the conclusion. The following proof demonstrates this 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   614
technique: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   615
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   616
\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   617
\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   618
R"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   619
\isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   620
contrapos_np)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   621
\isacommand{apply}\ intro\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   622
\isacommand{apply}\ (erule\ notE,\ assumption)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   623
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   624
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   625
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   626
There are two negated assumptions and we need to exchange the conclusion with the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   627
second one.  The method \isa{erule contrapos_np} would select the first assumption,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   628
which we do not want.  So we specify the desired assumption explicitly, using
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   629
\isa{erule_tac}.  This is the resulting subgoal: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   630
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   631
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   632
R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   633
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   634
The former conclusion, namely \isa{R}, now appears negated among the assumptions,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   635
while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   636
conclusion.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   637
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   638
We can now apply introduction rules.  We use the {\isa{intro}} method, which
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   639
repeatedly  applies built-in introduction rules.  Here its effect is equivalent
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   640
to \isa{rule impI}.\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   641
\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   642
R\isasymrbrakk\ \isasymLongrightarrow\ Q%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   643
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   644
We can see a contradiction in the form of assumptions \isa{\isasymnot\ R}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   645
and~\isa{R}, which suggests using negation elimination.  If applied on its own,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   646
however, it will select the first negated assumption, which is useless.   Instead,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   647
we combine the rule with  the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   648
\isa{assumption} method:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   649
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   650
\ \ \ \ \ (erule\ notE,\ assumption)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   651
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   652
Now when Isabelle selects the first assumption, it tries to prove \isa{P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   653
\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   654
assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption.  That
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   655
concludes the proof.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   656
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   657
\medskip
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   658
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   659
Here is another example. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   660
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   661
\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   662
\isasymLongrightarrow\ P\ \isasymor\ Q\ \isasymand\ R"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   663
\isacommand{apply}\ intro%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   664
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   665
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   666
\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   667
\ \isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   668
\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   669
\isacommand{apply}\ (erule\ contrapos_np,\ rule\ conjI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   670
\ \ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   671
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   672
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   673
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   674
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   675
The first proof step applies the {\isa{intro}} method, which repeatedly 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   676
uses built-in introduction rules.  Here it creates the negative assumption \isa{\isasymnot\ (Q\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   677
R)}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   678
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   679
\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   680
R)\isasymrbrakk\ \isasymLongrightarrow\ P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   681
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   682
It comes from \isa{disjCI},  a disjunction introduction rule that is more
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   683
powerful than the separate rules  \isa{disjI1} and  \isa{disjI2}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   684
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   685
Next we apply the {\isa{elim}} method, which repeatedly applies 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   686
elimination rules; here, the elimination rules given 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   687
in the command.  One of the subgoals is trivial, leaving us with one other:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   688
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   689
\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   690
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   691
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   692
Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion.  The
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   693
combination 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   694
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   695
\ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   696
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   697
is robust: the \isa{conjI} forces the \isa{erule} to select a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   698
conjunction.  The two subgoals are the ones we would expect from appling
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   699
conjunction introduction to
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   700
\isa{Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   701
\isasymand\ R}:  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   702
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   703
\ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   704
Q\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   705
\ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   706
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   707
The rest of the proof is trivial.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   708
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   709
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   710
\section{The universal quantifier}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   711
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   712
Quantifiers require formalizing syntactic substitution and the notion of \textbf{arbitrary
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   713
value}.  Consider the universal quantifier.  In a logic book, its
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   714
introduction  rule looks like this: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   715
\[ \infer{\forall x.\,P}{P} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   716
Typically, a proviso written in English says that $x$ must not
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   717
occur in the assumptions.  This proviso guarantees that $x$ can be regarded as
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   718
arbitrary, since it has not been assumed to satisfy any special conditions. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   719
Isabelle's  underlying formalism, called the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   720
\textbf{meta-logic}, eliminates the  need for English.  It provides its own universal
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   721
quantifier (\isasymAnd) to express the notion of an arbitrary value.  We have
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   722
already seen  another symbol of the meta-logic, namely
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   723
\isa\isasymLongrightarrow, which expresses  inference rules and the treatment of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   724
assumptions. The only other  symbol in the meta-logic is \isa\isasymequiv, which
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   725
can be used to define constants.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   726
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   727
Returning to the universal quantifier, we find that having a similar quantifier
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   728
as part of the meta-logic makes the introduction rule trivial to express:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   729
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   730
({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   731
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   732
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   733
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   734
The following trivial proof demonstrates how the universal introduction 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   735
rule works. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   736
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   737
\isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   738
\isacommand{apply}\ (rule\ allI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   739
\isacommand{apply}\ (rule\ impI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   740
\isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   741
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   742
The first step invokes the rule by applying the method \isa{rule allI}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   743
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   744
%{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   745
\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   746
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   747
Note  that the resulting proof state has a bound variable,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   748
namely~\bigisa{x}.  The rule has replaced the universal quantifier of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   749
higher-order  logic by Isabelle's meta-level quantifier.  Our goal is to
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   750
prove
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   751
\isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   752
an implication, so we apply the corresponding introduction rule (\isa{impI}). 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   753
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   754
\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   755
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   756
The {\isa{assumption}} method proves this last subgoal. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   757
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   758
\medskip
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   759
Now consider universal elimination. In a logic text, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   760
the rule looks like this: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   761
\[ \infer{P[t/x]}{\forall x.\,P} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   762
The conclusion is $P$ with $t$ substituted for the variable~$x$.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   763
Isabelle expresses substitution using a function variable: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   764
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   765
{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   766
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   767
This destruction rule takes a 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   768
universally quantified formula and removes the quantifier, replacing 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   769
the bound variable \bigisa{x} by the schematic variable \bigisa{?x}.  Recall that a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   770
schematic variable starts with a question mark and acts as a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   771
placeholder: it can be replaced by any term. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   772
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   773
To see how this works, let us derive a rule about reducing 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   774
the scope of a universal quantifier.  In mathematical notation we write
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   775
\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   776
with the proviso `$x$ not free in~$P$.'  Isabelle's treatment of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   777
substitution makes the proviso unnecessary.  The conclusion is expressed as
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   778
\isa{P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   779
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   780
variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   781
bound variable capture.  Here is the isabelle proof in full:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   782
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   783
\isacommand{lemma}\ "({\isasymforall}x.\ P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   784
\isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   785
\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x){"}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   786
\isacommand{apply}\ (rule\ impI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   787
\isacommand{apply}\ (rule\ allI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   788
\isacommand{apply}\ (drule\ spec)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   789
\isacommand{apply}\ (drule\ mp)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   790
\ \ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   791
\ \isacommand{apply}\ assumption
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   792
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   793
First we apply implies introduction (\isa{rule impI}), 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   794
which moves the \isa{P} from the conclusion to the assumptions. Then 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   795
we apply universal introduction (\isa{rule allI}).  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   796
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   797
%{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   798
%\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   799
\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   800
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   801
As before, it replaces the HOL 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   802
quantifier by a meta-level quantifier, producing a subgoal that 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   803
binds the variable~\bigisa{x}.  The leading bound variables
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   804
(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   805
\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   806
conclusion, here \isa{Q\ x}.  At each proof step, the subgoals inherit the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   807
previous context, though some context elements may be added or deleted. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   808
Applying \isa{erule} deletes an assumption, while many natural deduction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   809
rules add bound variables or assumptions.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   810
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   811
Now, to reason from the universally quantified 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   812
assumption, we apply the elimination rule using the {\isa{drule}} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   813
method.  This rule is called \isa{spec} because it specializes a universal formula
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   814
to a particular term.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   815
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   816
\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   817
x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   818
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   819
Observe how the context has changed.  The quantified formula is gone,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   820
replaced by a new assumption derived from its body.  Informally, we have
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   821
removed the quantifier.  The quantified variable
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   822
has been replaced by the curious term 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   823
\bigisa{?x2~x}; it acts as a placeholder that may be replaced 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   824
by any term that can be built up from~\bigisa{x}.  (Formally, \bigisa{?x2} is an
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   825
unknown of function type, applied to the argument~\bigisa{x}.)  This new assumption is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   826
an implication, so we can  use \emph{modus ponens} on it. As before, it requires
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   827
proving the  antecedent (in this case \isa{P}) and leaves us with the consequent. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   828
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   829
\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   830
\isasymLongrightarrow\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   831
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   832
The consequent is \isa{Q} applied to that placeholder.  It may be replaced by any
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   833
term built from~\bigisa{x}, and here 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   834
it should simply be~\bigisa{x}.  The \isa{assumption} method will do this.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   835
The assumption need not be identical to the conclusion, provided the two formulas are
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   836
unifiable.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   837
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   838
\medskip
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   839
Note that \isa{drule spec} removes the universal quantifier and --- as
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   840
usual with elimination rules --- discards the original formula.  Sometimes, a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   841
universal formula has to be kept so that it can be used again.  Then we use a new
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   842
method: \isa{frule}.  It acts like \isa{drule} but copies rather than replaces
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   843
the selected assumption.  The \isa{f} is for `forward.'
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   844
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   845
In this example, we intuitively see that to go from \isa{P\ a} to \isa{P(f\ (f\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   846
a))} requires two uses of the quantified assumption, one for each
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   847
additional~\isa{f}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   848
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   849
\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   850
\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(f\ (f\ a))"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   851
\isacommand{apply}\ (frule\ spec)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   852
\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   853
\isacommand{apply}\ (drule\ spec)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   854
\isacommand{apply}\ (drule\ mp,\ assumption,\ assumption)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   855
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   856
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   857
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   858
Applying \isa{frule\ spec} leaves this subgoal:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   859
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   860
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (f\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a))
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   861
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   862
It is just what  \isa{drule} would have left except that the quantified
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   863
assumption is still present.  The next step is to apply \isa{mp} to the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   864
implication and the assumption \isa{P\ a}, which leaves this subgoal:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   865
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   866
\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ (f\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a))
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   867
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   868
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   869
We have created the assumption \isa{P(f\ a)}, which is progress.  To finish the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   870
proof, we apply \isa{spec} one last time, using \isa{drule}.  One final trick: if
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   871
we then apply
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   872
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   873
\ \ \ \ \ (drule\ mp,\ assumption)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   874
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   875
it will add a second copy of \isa{P(f\ a)} instead of the desired \isa{P(f\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   876
(f\ a))}.  Bundling both \isa{assumption} calls with \isa{drule mp} causes
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   877
Isabelle to backtrack and find the correct one.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   878
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   879
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   880
\section{The existential quantifier}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   881
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   882
The concepts just presented also apply to the existential quantifier,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   883
whose introduction rule looks like this in Isabelle: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   884
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   885
?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   886
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   887
If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   888
P(x)$ is also true. It is essentially a dual of the universal elimination rule, and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   889
logic texts present it using the same notation for substitution.  The existential
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   890
elimination rule looks like this
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   891
in a logic text: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   892
\[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   893
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   894
It looks like this in Isabelle: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   895
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   896
\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ {\isasymAnd}x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   897
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   898
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   899
Given an existentially quantified theorem and some
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   900
formula $Q$ to prove, it creates a new assumption by removing the quantifier.  As with
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   901
the universal introduction  rule, the textbook version imposes a proviso on the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   902
quantified variable, which Isabelle expresses using its meta-logic.  Note that it is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   903
enough to have a universal quantifier in the meta-logic; we do not need an existential
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   904
quantifier to be built in as well.\remark{EX example needed?}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   905
 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   906
Isabelle/HOL also provides Hilbert's
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   907
$\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   908
true, provided such a value exists.  Using this operator, we can express an
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   909
existential destruction rule:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   910
\[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   911
This rule is seldom used, for it can cause exponential blow-up.  The
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   912
main use of $\epsilon x. P(x)$ is in definitions when $P(x)$ characterizes $x$
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   913
uniquely.  For instance, we can define the cardinality of a finite set~$A$ to be that
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   914
$n$ such that $A$ is in one-to-one correspondance with $\{1,\ldots,n\}$.  We can then
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   915
prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   916
description) and proceed to prove other facts.\remark{SOME theorems
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   917
and example}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   918
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   919
\begin{exercise}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   920
Prove the lemma
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   921
\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   922
\emph{Hint}: the proof is similar 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   923
to the one just above for the universal quantifier. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   924
\end{exercise}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   925
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   926
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   927
\section{Some proofs that fail}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   928
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   929
Most of the examples in this tutorial involve proving theorems.  But not every 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   930
conjecture is true, and it can be instructive to see how  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   931
proofs fail. Here we attempt to prove a distributive law involving 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   932
the existential quantifier and conjunction. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   933
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   934
\isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   935
\isacommand{apply}\ (erule\ conjE)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   936
\isacommand{apply}\ (erule\ exE)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   937
\isacommand{apply}\ (erule\ exE)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   938
\isacommand{apply}\ (rule\ exI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   939
\isacommand{apply}\ (rule\ conjI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   940
\ \isacommand{apply}\ assumption\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   941
\isacommand{oops}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   942
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   943
The first steps are  routine.  We apply conjunction elimination (\isa{erule
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   944
conjE}) to split the assumption  in two, leaving two existentially quantified
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   945
assumptions.  Applying existential elimination  (\isa{erule exE}) removes one of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   946
the quantifiers. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   947
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   948
%({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   949
%\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   950
\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   951
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   952
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   953
When we remove the other quantifier, we get a different bound 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   954
variable in the subgoal.  (The name \isa{xa} is generated automatically.)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   955
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   956
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   957
\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   958
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   959
The proviso of the existential elimination rule has forced the variables to
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   960
differ: we can hardly expect two arbitrary values to be equal!  There is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   961
no way to prove this subgoal.  Removing the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   962
conclusion's existential quantifier yields two
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   963
identical placeholders, which can become  any term involving the variables \bigisa{x}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   964
and~\bigisa{xa}.  We need one to become \bigisa{x}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   965
and the other to become~\bigisa{xa}, but Isabelle requires all instances of a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   966
placeholder to be identical. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   967
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   968
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   969
\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   970
\ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   971
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   972
We can prove either subgoal 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   973
using the \isa{assumption} method.  If we prove the first one, the placeholder
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   974
changes  into~\bigisa{x}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   975
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   976
\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   977
\isasymLongrightarrow\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   978
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   979
We are left with a subgoal that cannot be proved, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   980
because there is no way to prove that \bigisa{x}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   981
equals~\bigisa{xa}.  Applying the \isa{assumption} method results in an
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   982
error message:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   983
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   984
*** empty result sequence -- proof command failed
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   985
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   986
We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   987
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   988
\medskip 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   989
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   990
Here is another abortive proof, illustrating the interaction between 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   991
bound variables and unknowns.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   992
If $R$ is a reflexive relation, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   993
is there an $x$ such that $R\,x\,y$ holds for all $y$?  Let us see what happens when
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   994
we attempt to prove it. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   995
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   996
\isacommand{lemma}\ "{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   997
{\isasymexists}x.\ {\isasymforall}y.\ R\ x\ y"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   998
\isacommand{apply}\ (rule\ exI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
   999
\isacommand{apply}\ (rule\ allI)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1000
\isacommand{apply}\ (drule\ spec)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1001
\isacommand{oops}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1002
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1003
First, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1004
we remove the existential quantifier. The new proof state has 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1005
an unknown, namely~\bigisa{?x}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1006
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1007
%{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1008
%{\isasymforall}y.\ R\ x\ y\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1009
\ 1.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymforall}y.\ R\ ?x\ y
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1010
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1011
Next, we remove the universal quantifier 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1012
from the conclusion, putting the bound variable~\isa{y} into the subgoal. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1013
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1014
\ 1.\ {\isasymAnd}y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1015
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1016
Finally, we try to apply our reflexivity assumption.  We obtain a 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1017
new assumption whose identical placeholders may be replaced by 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1018
any term involving~\bigisa{y}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1019
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1020
\ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1021
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1022
This subgoal can only be proved by putting \bigisa{y} for all the placeholders,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1023
making the assumption and conclusion become \isa{R\ y\ y}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1024
But Isabelle refuses to substitute \bigisa{y}, a bound variable, for
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1025
\bigisa{?x}; that would be a bound variable capture.  The proof fails.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1026
Note that Isabelle can replace \bigisa{?z2~y} by \bigisa{y}; this involves
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1027
instantiating
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1028
\bigisa{?z2} to the identity function.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1029
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1030
This example is typical of how Isabelle enforces sound quantifier reasoning. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1031
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1032
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1033
\section{Proving theorems using the \emph{\texttt{blast}} method}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1034
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1035
It is hard to prove substantial theorems using the methods 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1036
described above. A proof may be dozens or hundreds of steps long.  You 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1037
may need to search among different ways of proving certain 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1038
subgoals. Often a choice that proves one subgoal renders another 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1039
impossible to prove.  There are further complications that we have not
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1040
discussed, concerning negation and disjunction.  Isabelle's
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1041
\textbf{classical reasoner} is a family of tools that perform such
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1042
proofs automatically.  The most important of these is the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1043
{\isa{blast}} method. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1044
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1045
In this section, we shall first see how to use the classical 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1046
reasoner in its default mode and then how to insert additional 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1047
rules, enabling it to work in new problem domains. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1048
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1049
 We begin with examples from pure predicate logic. The following 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1050
example is known as Andrew's challenge. Peter Andrews designed 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1051
it to be hard to prove by automatic means.%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1052
\footnote{Pelletier~\cite{pelletier86} describes it and many other
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1053
problems for automatic theorem provers.}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1054
The nested biconditionals cause an exponential explosion: the formal
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1055
proof is  enormous.  However, the {\isa{blast}} method proves it in
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1056
a fraction  of a second. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1057
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1058
\isacommand{lemma}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1059
"(({\isasymexists}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1060
{\isasymforall}y.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1061
p(x){=}p(y){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1062
=\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1063
(({\isasymexists}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1064
q(x){)}=({\isasymforall}y.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1065
p(y){)}){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1066
\ \ =\ \ \ \ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1067
\ \ \ \ \ \ \ \
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1068
(({\isasymexists}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1069
{\isasymforall}y.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1070
q(x){=}q(y){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1071
=\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1072
(({\isasymexists}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1073
p(x){)}=({\isasymforall}y.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1074
q(y){)}){)}"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1075
\isacommand{apply}\ blast\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1076
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1077
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1078
The next example is a logic problem composed by Lewis Carroll. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1079
The {\isa{blast}} method finds it trivial. Moreover, it turns out 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1080
that not all of the assumptions are necessary. We can easily 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1081
experiment with variations of this formula and see which ones 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1082
can be proved. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1083
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1084
\isacommand{lemma}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1085
"({\isasymforall}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1086
honest(x)\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1087
industrious(x)\ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1088
healthy(x){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1089
\isasymand\ \ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1090
\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1091
grocer(x)\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1092
healthy(x){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1093
\isasymand\ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1094
\ \ \ \ \ \ \ \ ({\isasymforall}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1095
industrious(x)\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1096
grocer(x)\ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1097
honest(x){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1098
\isasymand\ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1099
\ \ \ \ \ \ \ \ ({\isasymforall}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1100
cyclist(x)\ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1101
industrious(x){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1102
\isasymand\ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1103
\ \ \ \ \ \ \ \ ({\isasymforall}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1104
{\isasymnot}healthy(x)\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1105
cyclist(x)\ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1106
{\isasymnot}honest(x){)}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1107
\ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1108
\ \ \ \ \ \ \ \ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1109
({\isasymforall}x.\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1110
grocer(x)\ \isasymlongrightarrow\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1111
{\isasymnot}cyclist(x){)}"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1112
\isacommand{apply}\ blast\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1113
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1114
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1115
The {\isa{blast}} method is also effective for set theory, which is
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1116
described in the next chapter.  This formula below may look horrible, but
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1117
the \isa{blast} method proves it easily. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1118
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1119
\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i){)}\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j){)}\ =\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1120
\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j){)}"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1121
\isacommand{apply}\ blast\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1122
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1123
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1124
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1125
Few subgoals are couched purely in predicate logic and set theory.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1126
We can extend the scope of the classical reasoner by giving it new rules. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1127
Extending it effectively requires understanding the notions of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1128
introduction, elimination and destruction rules.  Moreover, there is a
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1129
distinction between  safe and unsafe rules. A \textbf{safe} rule is one
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1130
that can be applied  backwards without losing information; an
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1131
\textbf{unsafe} rule loses  information, perhaps transforming the subgoal
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1132
into one that cannot be proved.  The safe/unsafe
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1133
distinction affects the proof search: if a proof attempt fails, the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1134
classical reasoner backtracks to the most recent unsafe rule application
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1135
and makes another choice. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1136
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1137
An important special case avoids all these complications.  A logical 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1138
equivalence, which in higher-order logic is an equality between 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1139
formulas, can be given to the classical 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1140
reasoner and simplifier by using the attribute {\isa{iff}}.  You 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1141
should do so if the right hand side of the equivalence is  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1142
simpler than the left-hand side.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1143
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1144
For example, here is a simple fact about list concatenation. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1145
The result of appending two lists is empty if and only if both 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1146
of the lists are themselves empty. Obviously, applying this equivalence 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1147
will result in a simpler goal. When stating this lemma, we include 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1148
the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1149
will make it known to the classical reasoner (and to the simplifier). 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1150
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1151
\isacommand{lemma}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1152
[iff]{:}\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1153
"(xs{\isacharat}ys\ =\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1154
\isacharbrackleft{]})\ =\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1155
(xs=[]\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1156
\isacharampersand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1157
ys=[]{)}"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1158
\isacommand{apply}\ (induct_tac\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1159
xs)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1160
\isacommand{apply}\ (simp_all)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1161
\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1162
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1163
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1164
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1165
This fact about multiplication is also appropriate for 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1166
the {\isa{iff}} attribute:\remark{the ?s are ugly here but we need
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1167
them again when talking about \isa{of}; we need a consistent style}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1168
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1169
(\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1170
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1171
A product is zero if and only if one of the factors is zero.  The
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1172
reasoning  involves a logical \textsc{or}.  Proving new rules for
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1173
disjunctive reasoning  is hard, but translating to an actual disjunction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1174
works:  the classical reasoner handles disjunction properly.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1175
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1176
In more detail, this is how the {\isa{iff}} attribute works.  It converts
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1177
the equivalence $P=Q$ to a pair of rules: the introduction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1178
rule $Q\Imp P$ and the destruction rule $P\Imp Q$.  It gives both to the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1179
classical reasoner as safe rules, ensuring that all occurrences of $P$ in
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1180
a subgoal are replaced by~$Q$.  The simplifier performs the same
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1181
replacement, since \isa{iff} gives $P=Q$ to the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1182
simplifier.  But classical reasoning is different from
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1183
simplification.  Simplification is deterministic: it applies rewrite rules
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1184
repeatedly, as long as possible, in order to \emph{transform} a goal.  Classical
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1185
reasoning uses search and backtracking in order to \emph{prove} a goal. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1186
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1187
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1188
\section{Proving the correctness of Euclid's algorithm}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1189
\label{sec:proving-euclid}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1190
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1191
A brief development will illustrate advanced use of  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1192
\isa{blast}.  In \S\ref{sec:recdef-simplification}, we declared the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1193
recursive function {\isa{gcd}}:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1194
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1195
\isacommand{consts}\ gcd\ :{:}\ {"}nat{\isacharasterisk}nat={\isachargreater}nat"\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1196
\isacommand{recdef}\ gcd\ {"}measure\ ((\isasymlambda(m{,}n){.}n)\ :{:}nat{\isacharasterisk}nat={\isachargreater}nat){"}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1197
\ \ \ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n){)}"%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1198
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1199
Let us prove that it computes the greatest common
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1200
divisor of its two arguments.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1201
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1202
%The declaration yields a recursion
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1203
%equation  for {\isa{gcd}}.  Simplifying with this equation can 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1204
%cause looping, expanding to ever-larger expressions of if-then-else 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1205
%and {\isa{gcd}} calls.  To prevent this, we prove separate simplification rules
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1206
%for $n=0$\ldots
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1207
%\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1208
%\isacommand{lemma}\ gcd_0\ [simp]{:}\ {"}gcd(m,0)\ =\ m"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1209
%\isacommand{apply}\ (simp)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1210
%\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1211
%\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1212
%\ldots{} and for $n>0$:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1213
%\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1214
%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m{,}n)\ =\ gcd\ (n,\ m\ mod\ n){"}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1215
%\isacommand{apply}\ (simp)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1216
%\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1217
%\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1218
%This second rule is similar to the original equation but
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1219
%does not loop because it is conditional.  It can be applied only
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1220
%when the second argument is known to be non-zero.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1221
%Armed with our two new simplification rules, we now delete the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1222
%original {\isa{gcd}} recursion equation. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1223
%\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1224
%\isacommand{declare}\ gcd{.}simps\ [simp\ del]
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1225
%\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1226
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1227
%Now we can prove  some interesting facts about the {\isa{gcd}} function,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1228
%for exampe, that it computes a common divisor of its arguments.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1229
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1230
The theorem is expressed in terms of the familiar
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1231
\textbf{divides} relation from number theory: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1232
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1233
?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1234
\rulename{dvd_def}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1235
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1236
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1237
A simple induction proves the theorem.  Here \isa{gcd.induct} refers to the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1238
induction rule returned by \isa{recdef}.  The proof relies on the simplification
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1239
rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1240
definition of \isa{gcd} can cause looping.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1241
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1242
\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m{,}n)\ dvd\ m)\ \isasymand\ (gcd(m{,}n)\ dvd\ n){"}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1243
\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd{.}induct)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1244
\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1245
\isacommand{apply}\ (simp_all)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1246
\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1247
\isacommand{done}%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1248
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1249
Notice that the induction formula 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1250
is a conjunction.  This is necessary: in the inductive step, each 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1251
half of the conjunction establishes the other. The first three proof steps 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1252
are applying induction, performing a case analysis on \isa{n}, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1253
and simplifying.  Let us pass over these quickly and consider
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1254
the use of {\isa{blast}}.  We have reached the following 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1255
subgoal: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1256
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1257
%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1258
\ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1259
 \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1260
\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1261
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1262
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1263
One of the assumptions, the induction hypothesis, is a conjunction. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1264
The two divides relationships it asserts are enough to prove 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1265
the conclusion, for we have the following theorem at our disposal: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1266
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1267
\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1268
\rulename{dvd_mod_imp_dvd}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1269
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1270
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1271
This theorem can be applied in various ways.  As an introduction rule, it
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1272
would cause backward chaining from  the conclusion (namely
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1273
\isa{?k\ dvd\ ?m}) to the two premises, which 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1274
also involve the divides relation. This process does not look promising
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1275
and could easily loop.  More sensible is  to apply the rule in the forward
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1276
direction; each step would eliminate  the \isa{mod} symboi from an
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1277
assumption, so the process must terminate.  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1278
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1279
So the final proof step applies the \isa{blast} method.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1280
Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1281
to use it as destruction rule: in the forward direction.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1282
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1283
\medskip
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1284
We have proved a conjunction.  Now, let us give names to each of the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1285
two halves:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1286
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1287
\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1288
\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1289
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1290
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1291
Several things are happening here. The keyword \isacommand{lemmas}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1292
tells Isabelle to transform a theorem in some way and to
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1293
give a name to the resulting theorem.  Attributes can be given,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1294
here \isa{iff}, which supplies the new theorems to the classical reasoner
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1295
and the simplifier.  The directive {\isa{THEN}}, which will be explained
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1296
below, supplies the lemma 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1297
\isa{gcd_dvd_both} to the
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1298
destruction rule \isa{conjunct1} in order to extract the first part.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1299
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1300
\ \ \ \ \ gcd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1301
(?m1,\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1302
?n1)\ dvd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1303
?m1%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1304
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1305
The variable names \isa{?m1} and \isa{?n1} arise because
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1306
Isabelle renames schematic variables to prevent 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1307
clashes.  The second \isacommand{lemmas} declaration yields
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1308
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1309
\ \ \ \ \ gcd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1310
(?m1,\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1311
?n1)\ dvd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1312
?n1%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1313
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1314
Later, we shall explore this type of forward reasoning in detail. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1315
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1316
To complete the verification of the {\isa{gcd}} function, we must 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1317
prove that it returns the greatest of all the common divisors 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1318
of its arguments.  The proof is by induction and simplification.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1319
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1320
\isacommand{lemma}\ gcd_greatest\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1321
[rule_format]{:}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1322
\ \ \ \ \ \ \ "(k\ dvd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1323
m)\ \isasymlongrightarrow\ (k\ dvd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1324
n)\ \isasymlongrightarrow\ k\ dvd\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1325
gcd(m{,}n)"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1326
\isacommand{apply}\ (induct_tac\ m\ n\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1327
rule:\ gcd{.}induct)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1328
\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1329
\isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1330
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1331
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1332
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1333
Note that the theorem has been expressed using HOL implication,
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1334
\isa{\isasymlongrightarrow}, because the induction affects the two
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1335
preconditions.  The directive \isa{rule_format} tells Isabelle to replace
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1336
each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1337
storing the theorem we have proved.  This directive also removes outer
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1338
universal quantifiers, converting a theorem into the usual format for
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1339
inference rules.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1340
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1341
The facts proved above can be summarized as a single logical 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1342
equivalence.  This step gives us a chance to see another application
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1343
of \isa{blast}, and it is worth doing for sound logical reasons.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1344
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1345
\isacommand{theorem}\ gcd_greatest_iff\ [iff]{:}\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1346
\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m{,}n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1347
\isacommand{apply}\ (blast\ intro!{:}\ gcd_greatest\ intro:\ dvd_trans)\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1348
\isacommand{done}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1349
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1350
This theorem concisely expresses the correctness of the {\isa{gcd}} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1351
function. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1352
We state it with the {\isa{iff}} attribute so that 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1353
Isabelle can use it to remove some occurrences of {\isa{gcd}}. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1354
The theorem has a one-line 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1355
proof using {\isa{blast}} supplied with four introduction 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1356
rules: note the {\isa{intro}} attribute. The exclamation mark 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1357
({\isa{intro}}{\isa{!}})\ signifies safe rules, which are 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1358
applied aggressively.  Rules given without the exclamation mark 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1359
are applied reluctantly and their uses can be undone if 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1360
the search backtracks.  Here the unsafe rule expresses transitivity  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1361
of the divides relation:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1362
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1363
\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1364
\rulename{dvd_trans}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1365
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1366
Applying \isa{dvd_trans} as 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1367
an introduction rule entails a risk of looping, for it multiplies 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1368
occurrences of the divides symbol. However, this proof relies 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1369
on transitivity reasoning.  The rule {\isa{gcd\_greatest}} is safe to apply 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1370
aggressively because it yields simpler subgoals.  The proof implicitly
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1371
uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1372
declared using \isa{iff}.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1373
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1374
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1375
\section{Other classical reasoning methods}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1376
 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1377
The {\isa{blast}} method is our main workhorse for proving theorems 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1378
automatically. Other components of the classical reasoner interact 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1379
with the simplifier. Still others perform classical reasoning 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1380
to a limited extent, giving the user fine control over the proof. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1381
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1382
Of the latter methods, the most useful is {\isa{clarify}}. It performs 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1383
all obvious reasoning steps without splitting the goal into multiple 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1384
parts. It does not apply rules that could render the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1385
goal unprovable (so-called unsafe rules). By performing the obvious 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1386
steps, {\isa{clarify}} lays bare the difficult parts of the problem, 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1387
where human intervention is necessary. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1388
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1389
For example, the following conjecture is false:
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1390
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1391
\isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1392
({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1393
\isasymand\ Q\ x)"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1394
\isacommand{apply}\ clarify
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1395
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1396
The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1397
a subgoal that helps us see why we cannot continue the proof. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1398
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1399
\ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1400
xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1401
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1402
The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1403
refer to distinct bound variables.  To reach this state, \isa{clarify} applied
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1404
the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1405
and the elimination rule for ~\isa{\isasymand}.  It did not apply the introduction
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1406
rule for  \isa{\isasymand} because of its policy never to split goals.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1407
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1408
Also available is {\isa{clarsimp}}, a method that interleaves {\isa{clarify}}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1409
and {\isa{simp}}.  Also there is \isa{safe}, which like \isa{clarify} performs
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1410
obvious steps and even applies those that split goals.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1411
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1412
The {\isa{force}} method applies the classical reasoner and simplifier 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1413
to one goal. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1414
\remark{example needed? most
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1415
things done by blast, simp or auto can also be done by force, so why add a new
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1416
one?}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1417
Unless it can prove the goal, it fails. Contrast 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1418
that with the auto method, which also combines classical reasoning 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1419
with simplification. The latter's purpose is to prove all the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1420
easy subgoals and parts of subgoals. Unfortunately, it can produce 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1421
large numbers of new subgoals; also, since it proves some subgoals 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1422
and splits others, it obscures the structure of the proof tree. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1423
The {\isa{force}} method does not have these drawbacks. Another 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1424
difference: {\isa{force}} tries harder than {\isa{auto}} to prove 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1425
its goal, so it can take much longer to terminate.
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1426
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1427
Older components of the classical reasoner have largely been 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1428
superseded by {\isa{blast}}, but they still have niche applications. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1429
Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}} 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1430
searches for proofs using a built-in first-order reasoner, these 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1431
earlier methods search for proofs using standard Isabelle inference. 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1432
That makes them slower but enables them to work correctly in the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1433
presence of the more unusual features of Isabelle rules, such 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1434
as type classes and function unknowns. For example, the introduction rule
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1435
for Hilbert's epsilon-operator has the following form: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1436
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1437
?P\ ?x\ \isasymLongrightarrow\ ?P\ (Eps\ ?P)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1438
\rulename{someI}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1439
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1440
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1441
The repeated occurrence of the variable \isa{?P} makes this rule tricky 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1442
to apply. Consider this contrived example: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1443
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1444
\isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1445
\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1446
\isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1447
\isacommand{apply}\ (rule\ someI)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1448
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1449
%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1450
We can apply rule \isa{someI} explicitly.  It yields the 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1451
following subgoal: 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1452
\begin{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1453
\ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1454
\isasymand\ Q\ ?x%
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1455
\end{isabelle}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
  1456