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