188 The key characteristics of both @{text simp} and @{text auto} are |
188 The key characteristics of both @{text simp} and @{text auto} are |
189 \begin{itemize} |
189 \begin{itemize} |
190 \item They show you were they got stuck, giving you an idea how to continue. |
190 \item They show you were they got stuck, giving you an idea how to continue. |
191 \item They perform the obvious steps but are highly incomplete. |
191 \item They perform the obvious steps but are highly incomplete. |
192 \end{itemize} |
192 \end{itemize} |
193 A proof method is \concept{complete} if it can prove all true formulas. |
193 A proof method is \conceptnoidx{complete} if it can prove all true formulas. |
194 There is no complete proof method for HOL, not even in theory. |
194 There is no complete proof method for HOL, not even in theory. |
195 Hence all our proof methods only differ in how incomplete they are. |
195 Hence all our proof methods only differ in how incomplete they are. |
196 |
196 |
197 A proof method that is still incomplete but tries harder than @{text auto} is |
197 A proof method that is still incomplete but tries harder than @{text auto} is |
198 @{text fastforce}. It either succeeds or fails, it acts on the first |
198 @{text fastforce}. It either succeeds or fails, it acts on the first |
329 to the proof state. We will now examine the details of this process. |
329 to the proof state. We will now examine the details of this process. |
330 |
330 |
331 \subsection{Instantiating Unknowns} |
331 \subsection{Instantiating Unknowns} |
332 |
332 |
333 We had briefly mentioned earlier that after proving some theorem, |
333 We had briefly mentioned earlier that after proving some theorem, |
334 Isabelle replaces all free variables @{text x} by so called \concept{unknowns} |
334 Isabelle replaces all free variables @{text x} by so called \conceptidx{unknowns}{unknown} |
335 @{text "?x"}. We can see this clearly in rule @{thm[source] conjI}. |
335 @{text "?x"}. We can see this clearly in rule @{thm[source] conjI}. |
336 These unknowns can later be instantiated explicitly or implicitly: |
336 These unknowns can later be instantiated explicitly or implicitly: |
337 \begin{itemize} |
337 \begin{itemize} |
338 \item By hand, using \concept{@{text of}}. |
338 \item By hand, using \indexed{@{text of}}{of}. |
339 The expression @{text"conjI[of \"a=b\" \"False\"]"} |
339 The expression @{text"conjI[of \"a=b\" \"False\"]"} |
340 instantiates the unknowns in @{thm[source] conjI} from left to right with the |
340 instantiates the unknowns in @{thm[source] conjI} from left to right with the |
341 two formulas @{text"a=b"} and @{text False}, yielding the rule |
341 two formulas @{text"a=b"} and @{text False}, yielding the rule |
342 @{thm[display,mode=Rule]conjI[of "a=b" False]} |
342 @{thm[display,mode=Rule]conjI[of "a=b" False]} |
343 |
343 |
344 In general, @{text"th[of string\<^sub>1 \<dots> string\<^sub>n]"} instantiates |
344 In general, @{text"th[of string\<^sub>1 \<dots> string\<^sub>n]"} instantiates |
345 the unknowns in the theorem @{text th} from left to right with the terms |
345 the unknowns in the theorem @{text th} from left to right with the terms |
346 @{text string\<^sub>1} to @{text string\<^sub>n}. |
346 @{text string\<^sub>1} to @{text string\<^sub>n}. |
347 |
347 |
348 \item By unification. \concept{Unification} is the process of making two |
348 \item By unification. \conceptidx{Unification}{unification} is the process of making two |
349 terms syntactically equal by suitable instantiations of unknowns. For example, |
349 terms syntactically equal by suitable instantiations of unknowns. For example, |
350 unifying @{text"?P \<and> ?Q"} with \mbox{@{prop"a=b \<and> False"}} instantiates |
350 unifying @{text"?P \<and> ?Q"} with \mbox{@{prop"a=b \<and> False"}} instantiates |
351 @{text "?P"} with @{prop "a=b"} and @{text "?Q"} with @{prop False}. |
351 @{text "?P"} with @{prop "a=b"} and @{text "?Q"} with @{prop False}. |
352 \end{itemize} |
352 \end{itemize} |
353 We need not instantiate all unknowns. If we want to skip a particular one we |
353 We need not instantiate all unknowns. If we want to skip a particular one we |
354 can just write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}. |
354 can just write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}. |
355 Unknowns can also be instantiated by name using \concept{@{text "where"}}, for example |
355 Unknowns can also be instantiated by name using \indexed{@{text "where"}}{where}, for example |
356 @{text "conjI[where ?P = \"a=b\""} \isacom{and} @{text"?Q = \"False\"]"}. |
356 @{text "conjI[where ?P = \"a=b\""} \isacom{and} @{text"?Q = \"False\"]"}. |
357 |
357 |
358 |
358 |
359 \subsection{Rule Application} |
359 \subsection{Rule Application} |
360 |
360 |
361 \concept{Rule application} means applying a rule backwards to a proof state. |
361 \conceptidx{Rule application}{rule application} means applying a rule backwards to a proof state. |
362 For example, applying rule @{thm[source]conjI} to a proof state |
362 For example, applying rule @{thm[source]conjI} to a proof state |
363 \begin{quote} |
363 \begin{quote} |
364 @{text"1. \<dots> \<Longrightarrow> A \<and> B"} |
364 @{text"1. \<dots> \<Longrightarrow> A \<and> B"} |
365 \end{quote} |
365 \end{quote} |
366 results in two subgoals, one for each premise of @{thm[source]conjI}: |
366 results in two subgoals, one for each premise of @{thm[source]conjI}: |
383 This is also called \concept{backchaining} with rule @{text xyz}. |
383 This is also called \concept{backchaining} with rule @{text xyz}. |
384 |
384 |
385 \subsection{Introduction Rules} |
385 \subsection{Introduction Rules} |
386 |
386 |
387 Conjunction introduction (@{thm[source] conjI}) is one example of a whole |
387 Conjunction introduction (@{thm[source] conjI}) is one example of a whole |
388 class of rules known as \concept{introduction rules}. They explain under which |
388 class of rules known as \conceptidx{introduction rules}{introduction rule}. They explain under which |
389 premises some logical construct can be introduced. Here are some further |
389 premises some logical construct can be introduced. Here are some further |
390 useful introduction rules: |
390 useful introduction rules: |
391 \[ |
391 \[ |
392 \inferrule*[right=\mbox{@{text impI}}]{\mbox{@{text"?P \<Longrightarrow> ?Q"}}}{\mbox{@{text"?P \<longrightarrow> ?Q"}}} |
392 \inferrule*[right=\mbox{@{text impI}}]{\mbox{@{text"?P \<Longrightarrow> ?Q"}}}{\mbox{@{text"?P \<longrightarrow> ?Q"}}} |
393 \qquad |
393 \qquad |
436 \label{sec:forward-proof} |
436 \label{sec:forward-proof} |
437 |
437 |
438 Forward proof means deriving new theorems from old theorems. We have already |
438 Forward proof means deriving new theorems from old theorems. We have already |
439 seen a very simple form of forward proof: the @{text of} operator for |
439 seen a very simple form of forward proof: the @{text of} operator for |
440 instantiating unknowns in a theorem. The big brother of @{text of} is |
440 instantiating unknowns in a theorem. The big brother of @{text of} is |
441 \concept{@{text OF}} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called |
441 \indexed{@{text OF}}{OF} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called |
442 @{text r} and a theorem @{text A'} called @{text r'}, the theorem @{text |
442 @{text r} and a theorem @{text A'} called @{text r'}, the theorem @{text |
443 "r[OF r']"} is the result of applying @{text r} to @{text r'}, where @{text |
443 "r[OF r']"} is the result of applying @{text r} to @{text r'}, where @{text |
444 r} should be viewed as a function taking a theorem @{text A} and returning |
444 r} should be viewed as a function taking a theorem @{text A} and returning |
445 @{text B}. More precisely, @{text A} and @{text A'} are unified, thus |
445 @{text B}. More precisely, @{text A} and @{text A'} are unified, thus |
446 instantiating the unknowns in @{text B}, and the result is the instantiated |
446 instantiating the unknowns in @{text B}, and the result is the instantiated |
780 @{text "\<lbrakk> I a\<^sub>1; P a\<^sub>1; \<dots>; I a\<^sub>n; P a\<^sub>n \<rbrakk> \<Longrightarrow> P a"} |
780 @{text "\<lbrakk> I a\<^sub>1; P a\<^sub>1; \<dots>; I a\<^sub>n; P a\<^sub>n \<rbrakk> \<Longrightarrow> P a"} |
781 \end{quote} |
781 \end{quote} |
782 |
782 |
783 The above format for inductive definitions is simplified in a number of |
783 The above format for inductive definitions is simplified in a number of |
784 respects. @{text I} can have any number of arguments and each rule can have |
784 respects. @{text I} can have any number of arguments and each rule can have |
785 additional premises not involving @{text I}, so-called \concept{side |
785 additional premises not involving @{text I}, so-called \conceptidx{side |
786 conditions}. In rule inductions, these side-conditions appear as additional |
786 conditions}{side condition}. In rule inductions, these side conditions appear as additional |
787 assumptions. The \isacom{for} clause seen in the definition of the reflexive |
787 assumptions. The \isacom{for} clause seen in the definition of the reflexive |
788 transitive closure merely simplifies the form of the induction rule. |
788 transitive closure merely simplifies the form of the induction rule. |
789 |
789 |
790 |
790 |
791 \subsection*{Exercises} |
791 \subsection*{Exercises} |