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