author nipkow Mon, 08 Jul 2002 18:49:18 +0200 changeset 13317 bb74918cc0dd parent 13316 d16629fd0f95 child 13318 3f475e54875c
*** empty log message ***
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 17:51:56 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 18:49:18 2002 +0200
@@ -42,13 +42,11 @@

text{* We start with a really trivial toy proof to introduce the basic
features of structured proofs. *}
-
lemma "A \<longrightarrow> A"
proof (rule impI)
assume a: "A"
show "A" by(rule a)
qed
-
text{*\noindent
The operational reading: the \isakeyword{assume}-\isakeyword{show} block
proves @{prop"A \<Longrightarrow> A"},
@@ -71,7 +69,6 @@
text{* Trivial proofs, in particular those by assumption, should be trivial
to perform. Method .'' does just that (and a bit more --- see later). Thus
naming of assumptions is often superfluous: *}
-
lemma "A \<longrightarrow> A"
proof
assume "A"
@@ -81,13 +78,11 @@
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: *}
-
lemma "A \<longrightarrow> A \<and> A"
proof
assume A
show "A \<and> A" by(rule conjI)
qed
-
text{*\noindent A drawback of these implicit proofs by assumption is that it
is no longer obvious where an assumption is used.

@@ -101,7 +96,6 @@
assume A
show "A \<and> 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
@@ -113,7 +107,6 @@
@{thm[display,indent=5]conjE[no_vars]}  In the following proof it is applied
by hand, after its first (\emph{major}'') premise has been eliminated via
@{text"[OF AB]"}: *}
-
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume AB: "A \<and> B"
@@ -123,7 +116,6 @@
show ?thesis ..
qed
qed
-
text{*\noindent Note that the term @{text"?thesis"} always stands for the
current goal'', i.e.\ the enclosing \isakeyword{show} (or
\isakeyword{have}).
@@ -159,7 +151,6 @@
The previous proposition can be referred to via the fact @{text this}.
This greatly reduces the need for explicit naming of propositions:
*}
-
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume "A \<and> B"
@@ -176,7 +167,6 @@
\medskip

Here is an alternative proof that operates purely by forward reasoning: *}
-
lemma "A \<and> B \<longrightarrow> B \<and> A"
proof
assume ab: "A \<and> B"
@@ -184,7 +174,6 @@
from ab have b: B ..
from b a show "B \<and> A" ..
qed
-
text{*\noindent
It is worth examining this text in detail because it exhibits a number of new features.

@@ -246,7 +235,6 @@
qed
qed
qed;
-
text{*\noindent Apart from demonstrating the strangeness of classical
arguments by contradiction, this example also introduces a new language
feature to deal with multiple subgoals: \isakeyword{next}.  When showing
@@ -259,13 +247,11 @@
text{* So far our examples have been a bit unnatural: normally we want to
prove rules expressed with @{text"\<Longrightarrow>"}, not @{text"\<longrightarrow>"}. Here is an example:
*}
-
lemma "(A \<Longrightarrow> False) \<Longrightarrow> \<not> A"
proof
assume "A \<Longrightarrow> False" "A"
thus False .
qed
-
text{*\noindent The \isakeyword{proof} always works on the conclusion,
@{prop"\<not>A"} in our case, thus selecting $\neg$-introduction. Hence we can
additionally assume @{prop"A"}. Why does .'' prove @{prop False}? Because
@@ -283,7 +269,6 @@
assume "?P \<Longrightarrow> False" ?P
thus False .
qed
-
text{*\noindent Any formula may be followed by
@{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern
to be matched against the formula, instantiating the @{text"?"}-variables in
@@ -300,7 +285,6 @@
assume ?P
with A show False .
qed
-
text{*\noindent Here we have used the abbreviation
\begin{center}
@@ -322,6 +306,7 @@
qed
qed

+
subsection{*Predicate calculus*}

text{* Command \isakeyword{fix} introduces new local variables into a
@@ -329,13 +314,11 @@
meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
@{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are
applied implictly: *}
-
lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P(f x)"
proof  -- "@{thm[source]allI}: @{thm allI[no_vars]}"
fix a
from P show "P(f a)" ..  --"@{thm[source]allE}: @{thm allE[no_vars]}"
qed
-
text{*\noindent Note that in the proof we have chosen to call the bound
variable @{term a} instead of @{term x} merely to show that the choice of
names is irrelevant.
@@ -352,21 +335,17 @@
show ?thesis ..  --"@{thm[source]exI}: @{thm exI[no_vars]}"
qed
qed
-
-text {*\noindent
-Explicit $\exists$-elimination as seen above can become
+text{*\noindent Explicit $\exists$-elimination as seen above can become
cumbersome in practice.  The derived Isar language element
-\isakeyword{obtain} provides a more handsome way to perform
-generalized existence reasoning:
-*}
+\isakeyword{obtain} provides a more handsome way to perform generalized
+existence reasoning: *}

lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y"
proof -
from Pf obtain a where "P(f a)" ..
thus "\<exists>y. P y" ..
qed
-
-text {*\noindent Note how the proof text follows the usual mathematical style
+text{*\noindent Note how the proof text follows the usual mathematical style
of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$
as a new local variable.  Technically, \isakeyword{obtain} is similar to
\isakeyword{fix} and \isakeyword{assume} together with a soundness proof of
@@ -389,7 +368,6 @@
powerful automatic methods can be used just as well. Here is an example,
Cantor's theorem that there is no surjective function from a set to its
powerset: *}
-
theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
proof
let ?S = "{x. x \<notin> f x}"
@@ -407,7 +385,6 @@
qed
qed
qed
-
text{*\noindent
For a start, the example demonstrates two new language elements:
\begin{itemize}
@@ -447,8 +424,7 @@
qed
qed
qed
-
-text {*\noindent Method @{text contradiction} succeeds if both $P$ and
+text{*\noindent Method @{text contradiction} succeeds if both $P$ and
$\neg P$ are among the assumptions and the facts fed into that step.

As it happens, Cantor's theorem can be proved automatically by best-first
@@ -458,7 +434,6 @@

theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
by best
-
text{*\noindent Of course this only works in the context of HOL's carefully
constructed introduction and elimination rules for set theory.

@@ -475,11 +450,9 @@
apply assumption
done
qed
-
text{*\noindent You may need to resort to this technique if an automatic step
fails to prove the desired proposition. *}

-
section{*Case distinction and induction*}

@@ -487,14 +460,12 @@

text{* We have already met the @{text cases} method for performing
binary case splits. Here is another example: *}
-
lemma "P \<or> \<not> P"
proof cases
assume "P" thus ?thesis ..
next
assume "\<not> P" thus ?thesis ..
qed
-
text{*\noindent As always, the cases can be tackled in any order.

This form is appropriate if @{term P} is textually small.  However, if
@@ -507,7 +478,6 @@
next
case False thus ?thesis ..
qed
-
text{*\noindent which is simply a shorthand for the previous
proof. More precisely, the phrases \isakeyword{case}~@{prop
True}/@{prop False} abbreviate the corresponding assumptions @{prop P}
@@ -515,14 +485,15 @@

The same game can be played with other datatypes, for example lists:
*}
+
(*<*)declare length_tl[simp del](*>*)
+
lemma "length(tl xs) = length xs - 1"
proof (cases xs)
case Nil thus ?thesis by simp
next
case Cons thus ?thesis by simp
qed
-
text{*\noindent Here \isakeyword{case}~@{text Nil} abbreviates
\isakeyword{assume}~@{prop"x = []"} and \isakeyword{case}~@{text Cons}
abbreviates \isakeyword{assume}~@{text"xs = _ # _"}. The names of the head
@@ -544,25 +515,21 @@
by simp
thus ?thesis by simp
qed
-
text{* New case distincion rules can be declared any time, even with
named cases. *}

-
subsection{*Induction*}

subsubsection{*Structural induction*}

text{* We start with a simple inductive proof where both cases are proved automatically: *}
-
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
by (induct n, simp_all)

text{*\noindent If we want to expose more of the structure of the
proof, we can use pattern matching to avoid having to repeat the goal
statement: *}
-
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n")
proof (induct n)
show "?P 0" by simp
@@ -574,7 +541,6 @@
text{* \noindent We could refine this further to show more of the equational
proof. Instead we explore the same avenue as for case distinctions:
introducing context via the \isakeyword{case} command: *}
-
lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)"
proof (induct n)
case 0 show ?case by simp
@@ -590,7 +556,6 @@
in the induction step because it has not been introduced via \isakeyword{fix}
(in contrast to the previous proof). The solution is the same as above:
replace @{term Suc} by @{text"(Suc i)"}: *}
-
lemma fixes n::nat shows "n < n*n + 1"
proof (induct n)
case 0 show ?case by simp
@@ -606,7 +571,6 @@
@{prop[display,indent=5]"(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n) \<Longrightarrow> P n"}
via structural induction. It is well known that one needs to prove
something more general first: *}
-
lemma cind_lemma:
assumes A: "(\<And>n. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n)"
shows "\<And>m. m < n \<Longrightarrow> P(m::nat)"
@@ -625,7 +589,6 @@
with Suc show "P m" by blast
qed
qed
-
text{* \noindent Let us first examine the statement of the lemma.
In contrast to the style advertized in the
Tutorial~\cite{LNCS2283}, structured Isar proofs do not need to
@@ -655,7 +618,6 @@

text{* We define our own version of reflexive transitive closure of a
relation *}
-
consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
inductive "r*"
intros
@@ -663,7 +625,15 @@
step:  "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"

text{* \noindent and prove that @{term"r*"} is indeed transitive: *}
-
+lemma assumes A: "(x,y) \<in> r*"
+  shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" (is "PROP ?P x y")
+using A
+proof induct
+  case refl thus ?case .
+next
+  case step thus ?case by(blast intro: rtc.step)
+qed
+(*
lemma assumes A: "(x,y) \<in> r*"
shows "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" (is "PROP ?P x y")
proof -
@@ -672,12 +642,12 @@
fix x show "PROP ?P x x" .
next
fix x' x y
-    assume "(x',x) \<in> r" and
-           "PROP ?P x y" -- "The induction hypothesis"
+    assume "(x',x) \<in> r"
+           "PROP ?P x y"   -- "induction hypothesis"
thus "PROP ?P x' y" by(blast intro: rtc.step)
qed
qed
-
+*)
text{*\noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) \in R$
piped into the proof, here \isakeyword{from}~@{text A}. The proof itself
follows the two rules of the inductive definition very closely.  The only