# HG changeset patch # User wenzelm # Date 1230844808 -3600 # Node ID ddee494212800086b4f593cdba2e527fa4afe338 # Parent 62e0f892e525b214c0ed7c86ff89a906490be78d eliminated implicit use of prems; unified fact names: a, b, ab; diff -r 62e0f892e525 -r ddee49421280 doc-src/IsarOverview/Isar/Logic.thy --- a/doc-src/IsarOverview/Isar/Logic.thy Thu Jan 01 21:30:13 2009 +0100 +++ b/doc-src/IsarOverview/Isar/Logic.thy Thu Jan 01 22:20:08 2009 +0100 @@ -34,54 +34,51 @@ be enclosed in double quotes. However, we will continue to do so for uniformity. -Trivial proofs, in particular those by assumption, should be trivial -to perform. Proof ``.'' does just that (and a bit more). Thus -naming of assumptions is often superfluous: *} +Instead of applying fact @{text a} via the @{text rule} method, we can +also push it directly onto our goal. The proof is then immediate, +which is formally written as ``.'' in Isar: *} lemma "A \ A" proof - assume "A" - show "A" . + assume a: "A" + from a show "A" . qed -text{* To hide proofs by assumption further, \isakeyword{by}@{text"(method)"} -first applies @{text method} and then tries to solve all remaining subgoals -by assumption: *} +text{* We can also push several facts towards a goal, and put another +rule in between to establish some result that is one step further +removed. We illustrate this by introducing a trivial conjunction: *} lemma "A \ A \ A" proof - assume "A" - show "A \ A" by(rule conjI) + assume a: "A" + from a and a show "A \ A" by(rule conjI) qed text{*\noindent Rule @{thm[source]conjI} is of course @{thm conjI}. -A drawback of implicit proofs by assumption is that it -is no longer obvious where an assumption is used. Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} -can be abbreviated to ``..'' if \emph{name} refers to one of the +can be abbreviated to ``..'' if \emph{name} refers to one of the predefined introduction rules (or elimination rules, see below): *} lemma "A \ A \ A" proof - assume "A" - show "A \ A" .. + assume a: "A" + from a and a show "A \ A" .. qed text{*\noindent This is what happens: first the matching introduction rule @{thm[source]conjI} -is applied (first ``.''), then the two subgoals are solved by assumption -(second ``.''). *} +is applied (first ``.''), the remaining problem is solved immediately (second ``.''). *} subsubsection{*Elimination rules*} text{*A typical elimination rule is @{thm[source]conjE}, $\land$-elimination: @{thm[display,indent=5]conjE} In the following proof it is applied by hand, after its first (\emph{major}) premise has been eliminated via -@{text"[OF AB]"}: *} +@{text"[OF ab]"}: *} lemma "A \ B \ B \ A" proof - assume AB: "A \ B" + assume ab: "A \ B" show "B \ A" - proof (rule conjE[OF AB]) -- {*@{text"conjE[OF AB]"}: @{thm conjE[OF AB]} *} - assume "A" "B" - show ?thesis .. + proof (rule conjE[OF ab]) -- {*@{text"conjE[OF ab]"}: @{thm conjE[OF ab]} *} + assume a: "A" and b: "B" + from b and a show ?thesis .. qed qed text{*\noindent Note that the term @{text"?thesis"} always stands for the @@ -106,11 +103,11 @@ lemma "A \ B \ B \ A" proof - assume AB: "A \ B" - from AB show "B \ A" + assume ab: "A \ B" + from ab show "B \ A" proof - assume "A" "B" - show ?thesis .. + assume a: "A" and b: "B" + from b and a show ?thesis .. qed qed @@ -120,15 +117,16 @@ such that the proof of each proposition builds on the previous proposition. \end{quote} The previous proposition can be referred to via the fact @{text this}. -This greatly reduces the need for explicit naming of propositions: +This greatly reduces the need for explicit naming of propositions. We also +rearrange the additional inner assumptions into proper order for immediate use: *} lemma "A \ B \ B \ A" proof assume "A \ B" from this show "B \ A" proof - assume "A" "B" - show ?thesis .. + assume "B" "A" + from this show ?thesis .. qed qed @@ -199,11 +197,11 @@ assume nn: "\ (\ A \ \ B)" have "\ A" proof - assume "A" + assume a: "A" have "\ B" proof - assume "B" - have "A \ B" .. + assume b: "B" + from a and b have "A \ B" .. with n show False .. qed hence "\ A \ \ B" .. @@ -282,28 +280,28 @@ \isakeyword{assumes} and \isakeyword{shows} elements which allow direct naming of assumptions: *} -lemma assumes AB: "large_A \ large_B" +lemma assumes ab: "large_A \ large_B" shows "large_B \ large_A" (is "?B \ ?A") proof - from AB show "?B" .. + from ab show "?B" .. next - from AB show "?A" .. + from ab show "?A" .. qed text{*\noindent Note the difference between @{text ?AB}, a term, and -@{text AB}, a fact. +@{text ab}, a fact. Finally we want to start the proof with $\land$-elimination so we don't have to perform it twice, as above. Here is a slick way to achieve this: *} -lemma assumes AB: "large_A \ large_B" +lemma assumes ab: "large_A \ large_B" shows "large_B \ large_A" (is "?B \ ?A") -using AB +using ab proof - assume "?A" "?B" show ?thesis .. + assume "?B" "?A" thus ?thesis .. qed text{*\noindent Command \isakeyword{using} can appear before a proof -and adds further facts to those piped into the proof. Here @{text AB} +and adds further facts to those piped into the proof. Here @{text ab} is the only such fact and it triggers $\land$-elimination. Another frequent idiom is as follows: \begin{center} @@ -319,23 +317,23 @@ not be what we had in mind. A simple ``@{text"-"}'' prevents this \emph{faux pas}: *} -lemma assumes AB: "A \ B" shows "B \ A" +lemma assumes ab: "A \ B" shows "B \ A" proof - - from AB show ?thesis + from ab show ?thesis proof - assume A show ?thesis .. + assume A thus ?thesis .. next - assume B show ?thesis .. + assume B thus ?thesis .. qed qed text{*\noindent Alternatively one can feed @{prop"A \ B"} directly into the proof, thus triggering the elimination rule: *} -lemma assumes AB: "A \ B" shows "B \ A" -using AB +lemma assumes ab: "A \ B" shows "B \ A" +using ab proof - assume A show ?thesis .. + assume A thus ?thesis .. next - assume B show ?thesis .. + assume B thus ?thesis .. qed text{* \noindent Remember that eliminations have priority over introductions. @@ -416,7 +414,7 @@ proof -- "@{thm[source]exE}: @{thm exE}" fix x assume "P(f x)" - show ?thesis .. -- "@{thm[source]exI}: @{thm exI}" + thus ?thesis .. -- "@{thm[source]exI}: @{thm exI}" qed qed text{*\noindent Explicit $\exists$-elimination as seen above can become @@ -499,12 +497,12 @@ assume "y \ ?S" hence "y \ f y" by simp hence "y \ ?S" by(simp add: `?S = f y`) - thus False by contradiction + with `y \ ?S` show False by contradiction next assume "y \ ?S" hence "y \ f y" by simp hence "y \ ?S" by(simp add: `?S = f y`) - thus False by contradiction + with `y \ ?S` show False by contradiction qed qed qed