75 indicate \textbf{schematic variables} (also called |
75 indicate \textbf{schematic variables} (also called |
76 \textbf{unknowns}):\index{unknowns|bold} they may |
76 \textbf{unknowns}):\index{unknowns|bold} they may |
77 be replaced by arbitrary formulas. If we use the rule backwards, Isabelle |
77 be replaced by arbitrary formulas. If we use the rule backwards, Isabelle |
78 tries to unify the current subgoal with the conclusion of the rule, which |
78 tries to unify the current subgoal with the conclusion of the rule, which |
79 has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, |
79 has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, |
80 \S\ref{sec:unification}.) If successful, |
80 {\S}\ref{sec:unification}.) If successful, |
81 it yields new subgoals given by the formulas assigned to |
81 it yields new subgoals given by the formulas assigned to |
82 \isa{?P} and \isa{?Q}. |
82 \isa{?P} and \isa{?Q}. |
83 |
83 |
84 The following trivial proof illustrates this point. |
84 The following trivial proof illustrates this point. |
85 \begin{isabelle} |
85 \begin{isabelle} |
173 \isacommand{apply}\ (rule\ disjI1)\isanewline |
173 \isacommand{apply}\ (rule\ disjI1)\isanewline |
174 \isacommand{apply}\ assumption |
174 \isacommand{apply}\ assumption |
175 \end{isabelle} |
175 \end{isabelle} |
176 We assume \isa{P\ \isasymor\ Q} and |
176 We assume \isa{P\ \isasymor\ Q} and |
177 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction |
177 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction |
178 elimination rule, \isa{disjE}\@. We invoke it using \isaindex{erule}, a |
178 elimination rule, \isa{disjE}\@. We invoke it using \methdx{erule}, a |
179 method designed to work with elimination rules. It looks for an assumption that |
179 method designed to work with elimination rules. It looks for an assumption that |
180 matches the rule's first premise. It deletes the matching assumption, |
180 matches the rule's first premise. It deletes the matching assumption, |
181 regards the first premise as proved and returns subgoals corresponding to |
181 regards the first premise as proved and returns subgoals corresponding to |
182 the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two |
182 the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two |
183 subgoals result. This is better than applying it using \isa{rule} |
183 subgoals result. This is better than applying it using \isa{rule} |
406 deduction rules are straightforward, but additional rules seem |
406 deduction rules are straightforward, but additional rules seem |
407 necessary in order to handle negated assumptions gracefully. This section |
407 necessary in order to handle negated assumptions gracefully. This section |
408 also illustrates the \isa{intro} method: a convenient way of |
408 also illustrates the \isa{intro} method: a convenient way of |
409 applying introduction rules. |
409 applying introduction rules. |
410 |
410 |
411 Negation introduction deduces $\neg P$ if assuming $P$ leads to a |
411 Negation introduction deduces $\lnot P$ if assuming $P$ leads to a |
412 contradiction. Negation elimination deduces any formula in the |
412 contradiction. Negation elimination deduces any formula in the |
413 presence of $\neg P$ together with~$P$: |
413 presence of $\lnot P$ together with~$P$: |
414 \begin{isabelle} |
414 \begin{isabelle} |
415 (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% |
415 (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% |
416 \rulenamedx{notI}\isanewline |
416 \rulenamedx{notI}\isanewline |
417 \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% |
417 \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% |
418 \rulenamedx{notE} |
418 \rulenamedx{notE} |
419 \end{isabelle} |
419 \end{isabelle} |
420 % |
420 % |
421 Classical logic allows us to assume $\neg P$ |
421 Classical logic allows us to assume $\lnot P$ |
422 when attempting to prove~$P$: |
422 when attempting to prove~$P$: |
423 \begin{isabelle} |
423 \begin{isabelle} |
424 (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% |
424 (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% |
425 \rulenamedx{classical} |
425 \rulenamedx{classical} |
426 \end{isabelle} |
426 \end{isabelle} |
427 |
427 |
428 \index{contrapositives|(}% |
428 \index{contrapositives|(}% |
429 The implications $P\imp Q$ and $\neg Q\imp\neg P$ are logically |
429 The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically |
430 equivalent, and each is called the |
430 equivalent, and each is called the |
431 \textbf{contrapositive} of the other. Four further rules support |
431 \textbf{contrapositive} of the other. Four further rules support |
432 reasoning about contrapositives. They differ in the placement of the |
432 reasoning about contrapositives. They differ in the placement of the |
433 negation symbols: |
433 negation symbols: |
434 \begin{isabelle} |
434 \begin{isabelle} |
448 assumption and the goal's conclusion.% |
448 assumption and the goal's conclusion.% |
449 \index{contrapositives|)} |
449 \index{contrapositives|)} |
450 |
450 |
451 The most important of these is \isa{contrapos_np}. It is useful |
451 The most important of these is \isa{contrapos_np}. It is useful |
452 for applying introduction rules to negated assumptions. For instance, |
452 for applying introduction rules to negated assumptions. For instance, |
453 the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we |
453 the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we |
454 might want to use conjunction introduction on it. |
454 might want to use conjunction introduction on it. |
455 Before we can do so, we must move that assumption so that it |
455 Before we can do so, we must move that assumption so that it |
456 becomes the conclusion. The following proof demonstrates this |
456 becomes the conclusion. The following proof demonstrates this |
457 technique: |
457 technique: |
458 \begin{isabelle} |
458 \begin{isabelle} |
584 replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an |
584 replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an |
585 $n$th subgoal is like the original one but has an additional assumption: an |
585 $n$th subgoal is like the original one but has an additional assumption: an |
586 instance of~$Q$. It is appropriate for destruction rules. |
586 instance of~$Q$. It is appropriate for destruction rules. |
587 \item |
587 \item |
588 Method \isa{frule\ R} is like \isa{drule\ R} except that the matching |
588 Method \isa{frule\ R} is like \isa{drule\ R} except that the matching |
589 assumption is not deleted. (See \S\ref{sec:frule} below.) |
589 assumption is not deleted. (See {\S}\ref{sec:frule} below.) |
590 \end{itemize} |
590 \end{itemize} |
591 |
591 |
592 Other methods apply a rule while constraining some of its |
592 Other methods apply a rule while constraining some of its |
593 variables. The typical form is |
593 variables. The typical form is |
594 \begin{isabelle} |
594 \begin{isabelle} |
845 the third unchanged. With this instantiation, backtracking is neither necessary |
845 the third unchanged. With this instantiation, backtracking is neither necessary |
846 nor possible. |
846 nor possible. |
847 |
847 |
848 An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem |
848 An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem |
849 modified using~\isa{of}, described in |
849 modified using~\isa{of}, described in |
850 \S\ref{sec:forward} below. An advantage of \isa{rule_tac} is that the |
850 {\S}\ref{sec:forward} below. An advantage of \isa{rule_tac} is that the |
851 instantiations may refer to |
851 instantiations may refer to |
852 \isasymAnd-bound variables in the current subgoal.% |
852 \isasymAnd-bound variables in the current subgoal.% |
853 \index{substitution|)} |
853 \index{substitution|)} |
854 |
854 |
855 |
855 |
1144 Isabelle makes the correct choice automatically, constructing the term by |
1144 Isabelle makes the correct choice automatically, constructing the term by |
1145 unification. In other cases, the required term is not obvious and we must |
1145 unification. In other cases, the required term is not obvious and we must |
1146 specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac} |
1146 specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac} |
1147 and \isa{erule_tac}. |
1147 and \isa{erule_tac}. |
1148 |
1148 |
1149 We have seen (just above, \S\ref{sec:frule}) a proof of this lemma: |
1149 We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma: |
1150 \begin{isabelle} |
1150 \begin{isabelle} |
1151 \isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\ |
1151 \isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\ |
1152 \isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \ |
1152 \isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \ |
1153 \isasymLongrightarrow \ P(h\ (h\ a))" |
1153 \isasymLongrightarrow \ P(h\ (h\ a))" |
1154 \end{isabelle} |
1154 \end{isabelle} |
1263 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the |
1263 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the |
1264 description) and proceed to prove other facts. |
1264 description) and proceed to prove other facts. |
1265 |
1265 |
1266 A more challenging example illustrates how Isabelle/HOL defines the least number |
1266 A more challenging example illustrates how Isabelle/HOL defines the least number |
1267 operator, which denotes the least \isa{x} satisfying~\isa{P}:% |
1267 operator, which denotes the least \isa{x} satisfying~\isa{P}:% |
1268 \index{least number operator} |
1268 \index{least number operator|see{\protect\isa{LEAST}}} |
1269 \begin{isabelle} |
1269 \begin{isabelle} |
1270 (LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ |
1270 (LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ |
1271 P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)) |
1271 P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)) |
1272 \end{isabelle} |
1272 \end{isabelle} |
1273 % |
1273 % |
1274 Let us prove the counterpart of \isa{some_equality} for \isa{LEAST}\@. |
1274 Let us prove the counterpart of \isa{some_equality} for \sdx{LEAST}\@. |
1275 The first step merely unfolds the definitions (\isa{LeastM} is a |
1275 The first step merely unfolds the definitions (\isa{LeastM} is a |
1276 auxiliary operator): |
1276 auxiliary operator): |
1277 \begin{isabelle} |
1277 \begin{isabelle} |
1278 \isacommand{theorem}\ Least_equality:\isanewline |
1278 \isacommand{theorem}\ Least_equality:\isanewline |
1279 \ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline |
1279 \ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline |
1773 an equation, so it too is a forward step. |
1773 an equation, so it too is a forward step. |
1774 |
1774 |
1775 \subsection{Modifying a Theorem using {\tt\slshape of} and {\tt\slshape THEN}} |
1775 \subsection{Modifying a Theorem using {\tt\slshape of} and {\tt\slshape THEN}} |
1776 |
1776 |
1777 Let us reproduce our examples in Isabelle. Recall that in |
1777 Let us reproduce our examples in Isabelle. Recall that in |
1778 \S\ref{sec:recdef-simplification} we declared the recursive function |
1778 {\S}\ref{sec:recdef-simplification} we declared the recursive function |
1779 \isa{gcd}:\index{*gcd (constant)|(} |
1779 \isa{gcd}:\index{*gcd (constant)|(} |
1780 \begin{isabelle} |
1780 \begin{isabelle} |
1781 \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline |
1781 \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline |
1782 \isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline |
1782 \isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline |
1783 \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" |
1783 \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" |
1904 attribute such as |
1904 attribute such as |
1905 \isa{[of "?k*m"]} will be rejected. |
1905 \isa{[of "?k*m"]} will be rejected. |
1906 \end{warn} |
1906 \end{warn} |
1907 |
1907 |
1908 \begin{exercise} |
1908 \begin{exercise} |
1909 In \S\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How |
1909 In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied. How |
1910 can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}? |
1910 can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}? |
1911 % answer rule (mult_commute [THEN ssubst]) |
1911 % answer rule (mult_commute [THEN ssubst]) |
1912 \end{exercise} |
1912 \end{exercise} |
1913 |
1913 |
1914 \subsection{Modifying a Theorem using {\tt\slshape OF}} |
1914 \subsection{Modifying a Theorem using {\tt\slshape OF}} |
2392 Let us prove that \isa{gcd} computes the greatest common |
2392 Let us prove that \isa{gcd} computes the greatest common |
2393 divisor of its two arguments. |
2393 divisor of its two arguments. |
2394 % |
2394 % |
2395 We use induction: \isa{gcd.induct} is the |
2395 We use induction: \isa{gcd.induct} is the |
2396 induction rule returned by \isa{recdef}. We simplify using |
2396 induction rule returned by \isa{recdef}. We simplify using |
2397 rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the |
2397 rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the |
2398 definition of \isa{gcd} can loop. |
2398 definition of \isa{gcd} can loop. |
2399 \begin{isabelle} |
2399 \begin{isabelle} |
2400 \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ |
2400 \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ |
2401 n)" |
2401 n)" |
2402 \end{isabelle} |
2402 \end{isabelle} |