1.1 --- a/doc-src/IsarOverview/Isar/Logic.thy Thu Jan 01 21:30:13 2009 +0100
1.2 +++ b/doc-src/IsarOverview/Isar/Logic.thy Thu Jan 01 22:20:08 2009 +0100
1.3 @@ -34,54 +34,51 @@
1.4 be enclosed in double quotes. However, we will continue to do so for
1.5 uniformity.
1.6
1.7 -Trivial proofs, in particular those by assumption, should be trivial
1.8 -to perform. Proof ``.'' does just that (and a bit more). Thus
1.9 -naming of assumptions is often superfluous: *}
1.10 +Instead of applying fact @{text a} via the @{text rule} method, we can
1.11 +also push it directly onto our goal. The proof is then immediate,
1.12 +which is formally written as ``.'' in Isar: *}
1.13 lemma "A \<longrightarrow> A"
1.14 proof
1.15 - assume "A"
1.16 - show "A" .
1.17 + assume a: "A"
1.18 + from a show "A" .
1.19 qed
1.20
1.21 -text{* To hide proofs by assumption further, \isakeyword{by}@{text"(method)"}
1.22 -first applies @{text method} and then tries to solve all remaining subgoals
1.23 -by assumption: *}
1.24 +text{* We can also push several facts towards a goal, and put another
1.25 +rule in between to establish some result that is one step further
1.26 +removed. We illustrate this by introducing a trivial conjunction: *}
1.27 lemma "A \<longrightarrow> A \<and> A"
1.28 proof
1.29 - assume "A"
1.30 - show "A \<and> A" by(rule conjI)
1.31 + assume a: "A"
1.32 + from a and a show "A \<and> A" by(rule conjI)
1.33 qed
1.34 text{*\noindent Rule @{thm[source]conjI} is of course @{thm conjI}.
1.35 -A drawback of implicit proofs by assumption is that it
1.36 -is no longer obvious where an assumption is used.
1.37
1.38 Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"}
1.39 -can be abbreviated to ``..'' if \emph{name} refers to one of the
1.40 +can be abbreviated to ``..'' if \emph{name} refers to one of the
1.41 predefined introduction rules (or elimination rules, see below): *}
1.42
1.43 lemma "A \<longrightarrow> A \<and> A"
1.44 proof
1.45 - assume "A"
1.46 - show "A \<and> A" ..
1.47 + assume a: "A"
1.48 + from a and a show "A \<and> A" ..
1.49 qed
1.50 text{*\noindent
1.51 This is what happens: first the matching introduction rule @{thm[source]conjI}
1.52 -is applied (first ``.''), then the two subgoals are solved by assumption
1.53 -(second ``.''). *}
1.54 +is applied (first ``.''), the remaining problem is solved immediately (second ``.''). *}
1.55
1.56 subsubsection{*Elimination rules*}
1.57
1.58 text{*A typical elimination rule is @{thm[source]conjE}, $\land$-elimination:
1.59 @{thm[display,indent=5]conjE} In the following proof it is applied
1.60 by hand, after its first (\emph{major}) premise has been eliminated via
1.61 -@{text"[OF AB]"}: *}
1.62 +@{text"[OF ab]"}: *}
1.63 lemma "A \<and> B \<longrightarrow> B \<and> A"
1.64 proof
1.65 - assume AB: "A \<and> B"
1.66 + assume ab: "A \<and> B"
1.67 show "B \<and> A"
1.68 - proof (rule conjE[OF AB]) -- {*@{text"conjE[OF AB]"}: @{thm conjE[OF AB]} *}
1.69 - assume "A" "B"
1.70 - show ?thesis ..
1.71 + proof (rule conjE[OF ab]) -- {*@{text"conjE[OF ab]"}: @{thm conjE[OF ab]} *}
1.72 + assume a: "A" and b: "B"
1.73 + from b and a show ?thesis ..
1.74 qed
1.75 qed
1.76 text{*\noindent Note that the term @{text"?thesis"} always stands for the
1.77 @@ -106,11 +103,11 @@
1.78
1.79 lemma "A \<and> B \<longrightarrow> B \<and> A"
1.80 proof
1.81 - assume AB: "A \<and> B"
1.82 - from AB show "B \<and> A"
1.83 + assume ab: "A \<and> B"
1.84 + from ab show "B \<and> A"
1.85 proof
1.86 - assume "A" "B"
1.87 - show ?thesis ..
1.88 + assume a: "A" and b: "B"
1.89 + from b and a show ?thesis ..
1.90 qed
1.91 qed
1.92
1.93 @@ -120,15 +117,16 @@
1.94 such that the proof of each proposition builds on the previous proposition.
1.95 \end{quote}
1.96 The previous proposition can be referred to via the fact @{text this}.
1.97 -This greatly reduces the need for explicit naming of propositions:
1.98 +This greatly reduces the need for explicit naming of propositions. We also
1.99 +rearrange the additional inner assumptions into proper order for immediate use:
1.100 *}
1.101 lemma "A \<and> B \<longrightarrow> B \<and> A"
1.102 proof
1.103 assume "A \<and> B"
1.104 from this show "B \<and> A"
1.105 proof
1.106 - assume "A" "B"
1.107 - show ?thesis ..
1.108 + assume "B" "A"
1.109 + from this show ?thesis ..
1.110 qed
1.111 qed
1.112
1.113 @@ -199,11 +197,11 @@
1.114 assume nn: "\<not> (\<not> A \<or> \<not> B)"
1.115 have "\<not> A"
1.116 proof
1.117 - assume "A"
1.118 + assume a: "A"
1.119 have "\<not> B"
1.120 proof
1.121 - assume "B"
1.122 - have "A \<and> B" ..
1.123 + assume b: "B"
1.124 + from a and b have "A \<and> B" ..
1.125 with n show False ..
1.126 qed
1.127 hence "\<not> A \<or> \<not> B" ..
1.128 @@ -282,28 +280,28 @@
1.129 \isakeyword{assumes} and \isakeyword{shows} elements which allow direct
1.130 naming of assumptions: *}
1.131
1.132 -lemma assumes AB: "large_A \<and> large_B"
1.133 +lemma assumes ab: "large_A \<and> large_B"
1.134 shows "large_B \<and> large_A" (is "?B \<and> ?A")
1.135 proof
1.136 - from AB show "?B" ..
1.137 + from ab show "?B" ..
1.138 next
1.139 - from AB show "?A" ..
1.140 + from ab show "?A" ..
1.141 qed
1.142 text{*\noindent Note the difference between @{text ?AB}, a term, and
1.143 -@{text AB}, a fact.
1.144 +@{text ab}, a fact.
1.145
1.146 Finally we want to start the proof with $\land$-elimination so we
1.147 don't have to perform it twice, as above. Here is a slick way to
1.148 achieve this: *}
1.149
1.150 -lemma assumes AB: "large_A \<and> large_B"
1.151 +lemma assumes ab: "large_A \<and> large_B"
1.152 shows "large_B \<and> large_A" (is "?B \<and> ?A")
1.153 -using AB
1.154 +using ab
1.155 proof
1.156 - assume "?A" "?B" show ?thesis ..
1.157 + assume "?B" "?A" thus ?thesis ..
1.158 qed
1.159 text{*\noindent Command \isakeyword{using} can appear before a proof
1.160 -and adds further facts to those piped into the proof. Here @{text AB}
1.161 +and adds further facts to those piped into the proof. Here @{text ab}
1.162 is the only such fact and it triggers $\land$-elimination. Another
1.163 frequent idiom is as follows:
1.164 \begin{center}
1.165 @@ -319,23 +317,23 @@
1.166 not be what we had in mind.
1.167 A simple ``@{text"-"}'' prevents this \emph{faux pas}: *}
1.168
1.169 -lemma assumes AB: "A \<or> B" shows "B \<or> A"
1.170 +lemma assumes ab: "A \<or> B" shows "B \<or> A"
1.171 proof -
1.172 - from AB show ?thesis
1.173 + from ab show ?thesis
1.174 proof
1.175 - assume A show ?thesis ..
1.176 + assume A thus ?thesis ..
1.177 next
1.178 - assume B show ?thesis ..
1.179 + assume B thus ?thesis ..
1.180 qed
1.181 qed
1.182 text{*\noindent Alternatively one can feed @{prop"A \<or> B"} directly
1.183 into the proof, thus triggering the elimination rule: *}
1.184 -lemma assumes AB: "A \<or> B" shows "B \<or> A"
1.185 -using AB
1.186 +lemma assumes ab: "A \<or> B" shows "B \<or> A"
1.187 +using ab
1.188 proof
1.189 - assume A show ?thesis ..
1.190 + assume A thus ?thesis ..
1.191 next
1.192 - assume B show ?thesis ..
1.193 + assume B thus ?thesis ..
1.194 qed
1.195 text{* \noindent Remember that eliminations have priority over
1.196 introductions.
1.197 @@ -416,7 +414,7 @@
1.198 proof -- "@{thm[source]exE}: @{thm exE}"
1.199 fix x
1.200 assume "P(f x)"
1.201 - show ?thesis .. -- "@{thm[source]exI}: @{thm exI}"
1.202 + thus ?thesis .. -- "@{thm[source]exI}: @{thm exI}"
1.203 qed
1.204 qed
1.205 text{*\noindent Explicit $\exists$-elimination as seen above can become
1.206 @@ -499,12 +497,12 @@
1.207 assume "y \<in> ?S"
1.208 hence "y \<notin> f y" by simp
1.209 hence "y \<notin> ?S" by(simp add: `?S = f y`)
1.210 - thus False by contradiction
1.211 + with `y \<in> ?S` show False by contradiction
1.212 next
1.213 assume "y \<notin> ?S"
1.214 hence "y \<in> f y" by simp
1.215 hence "y \<in> ?S" by(simp add: `?S = f y`)
1.216 - thus False by contradiction
1.217 + with `y \<notin> ?S` show False by contradiction
1.218 qed
1.219 qed
1.220 qed