--- a/doc-src/IsarRef/Thy/Framework.thy Mon Feb 09 21:08:59 2009 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy Mon Feb 09 21:09:24 2009 +0100
@@ -51,6 +51,182 @@
set-theory) is being used most of the time; Isabelle/ZF
\cite{isabelle-ZF} is less extensively developed, although it would
probably fit better for classical mathematics.
+
+ \medskip In order to illustrate typical natural deduction reasoning
+ in Isar, we shall refer to the background theory and library of
+ Isabelle/HOL. This includes common notions of predicate logic,
+ naive set-theory etc.\ using fairly standard mathematical notation.
+ From the perspective of generic natural deduction there is nothing
+ special about the logical connectives of HOL (@{text "\<and>"}, @{text
+ "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"}, etc.), only the resulting reasoning
+ principles are relevant to the user. There are similar rules
+ available for set-theory operators (@{text "\<inter>"}, @{text "\<union>"}, @{text
+ "\<Inter>"}, @{text "\<Union>"}, etc.), or any other theory developed in the
+ library (lattice theory, topology etc.).
+
+ Subsequently we briefly review fragments of Isar proof texts
+ corresponding directly to such general natural deduction schemes.
+ The examples shall refer to set-theory, to minimize the danger of
+ understanding connectives of predicate logic as something special.
+
+ \medskip The following deduction performs @{text "\<inter>"}-introduction,
+ working forwards from assumptions towards the conclusion. We give
+ both the Isar text, and depict the primitive rule involved, as
+ determined by unification of the problem against rules from the
+ context.
+*}
+
+text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
+
+(*<*)
+lemma True
+proof
+(*>*)
+ assume "x \<in> A" and "x \<in> B"
+ then have "x \<in> A \<inter> B" ..
+(*<*)
+qed
+(*>*)
+
+text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}
+
+text {*
+ \infer{@{prop "x \<in> A \<inter> B"}}{@{prop "x \<in> A"} & @{prop "x \<in> B"}}
+*}
+
+text_raw {*\end{minipage}*}
+
+text {*
+ \medskip\noindent Note that @{command "assume"} augments the
+ context, @{command "then"} indicates that the current facts shall be
+ used in the next step, and @{command "have"} states a local claim.
+ The two dots ``@{command ".."}'' above refer to a complete proof of
+ the claim, using the indicated facts and a canonical rule from the
+ context. We could have been more explicit here by spelling out the
+ final proof step via the @{command "by"} command:
+*}
+
+(*<*)
+lemma True
+proof
+(*>*)
+ assume "x \<in> A" and "x \<in> B"
+ then have "x \<in> A \<inter> B" by (rule IntI)
+(*<*)
+qed
+(*>*)
+
+text {*
+ \noindent The format of the @{text "\<inter>"}-introduction rule represents
+ the most basic inference, which proceeds from given premises to a
+ conclusion, without any additional context involved.
+
+ \medskip The next example performs backwards introduction on @{term
+ "\<Inter>\<A>"}, the intersection of all sets within a given set. This
+ requires a nested proof of set membership within a local context of
+ an arbitrary-but-fixed member of the collection:
+*}
+
+text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
+
+(*<*)
+lemma True
+proof
+(*>*)
+ have "x \<in> \<Inter>\<A>"
+ proof
+ fix A
+ assume "A \<in> \<A>"
+ show "x \<in> A" sorry
+ qed
+(*<*)
+qed
+(*>*)
+
+text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}
+
+text {*
+ \infer{@{prop "x \<in> \<Inter>\<A>"}}{\infer*{@{prop "x \<in> A"}}{@{text "[A][A \<in> \<A>]"}}}
+*}
+
+text_raw {*\end{minipage}*}
+
+text {*
+ \medskip\noindent This Isar reasoning pattern again refers to the
+ primitive rule depicted above. The system determines it in the
+ ``@{command "proof"}'' step, which could have been spelt out more
+ explicitly as ``@{command "proof"}~@{text "("}@{method rule}~@{fact
+ InterI}@{text ")"}''. Note that this rule involves both a local
+ parameter @{term "A"} and an assumption @{prop "A \<in> \<A>"} in the
+ nested reasoning. This kind of compound rule typically demands a
+ genuine sub-proof in Isar, working backwards rather than forwards as
+ seen before. In the proof body we encounter the @{command
+ "fix"}-@{command "assume"}-@{command "show"} skeleton of nested
+ sub-proofs that is typical for Isar. The final @{command "show"} is
+ like @{command "have"} followed by an additional refinement of the
+ enclosing claim, using the rule derived from the proof body. The
+ @{command "sorry"} command stands for a hole in the proof -- it may
+ be understood as an excuse for not providing a proper proof yet.
+
+ \medskip The next example involves @{term "\<Union>\<A>"}, which can be
+ characterized as the set of all @{term "x"} such that @{prop "\<exists>A. x
+ \<in> A \<and> A \<in> \<A>"}. The elimination rule for @{prop "x \<in> \<Union>\<A>"} does
+ not mention @{text "\<exists>"} and @{text "\<and>"} at all, but admits to obtain
+ directly a local @{term "A"} such that @{prop "x \<in> A"} and @{prop "A
+ \<in> \<A>"} hold. This corresponds to the following Isar proof and
+ inference rule, respectively:
+*}
+
+text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
+
+(*<*)
+lemma True
+proof
+(*>*)
+ assume "x \<in> \<Union>\<A>"
+ then have C
+ proof
+ fix A
+ assume "x \<in> A" and "A \<in> \<A>"
+ show C sorry
+ qed
+(*<*)
+qed
+(*>*)
+
+text_raw {*\end{minipage}\begin{minipage}{0.4\textwidth}*}
+
+text {*
+ \infer{@{prop "C"}}{@{prop "x \<in> \<Union>\<A>"} & \infer*{@{prop "C"}~}{@{text "[A][x \<in> A, A \<in> \<A>]"}}}
+*}
+
+text_raw {*\end{minipage}*}
+
+text {*
+ \medskip\noindent Although the Isar proof follows the natural
+ deduction rule closely, the text reads not as natural as
+ anticipated. There is a double occurrence of an arbitrary
+ conclusion @{prop "C"}, which represents the final result, but is
+ irrelevant for now. This issue arises for any elimination rule
+ involving local parameters. Isar provides the derived language
+ element @{command "obtain"}, which is able to perform the same
+ elimination proof more conveniently:
+*}
+
+(*<*)
+lemma True
+proof
+(*>*)
+ assume "x \<in> \<Union>\<A>"
+ then obtain A where "x \<in> A" and "A \<in> \<A>" ..
+(*<*)
+qed
+(*>*)
+
+text {*
+ \noindent Here we avoid to mention the final conclusion @{prop "C"}
+ and return to plain forward reasoning. The rule involved in the
+ ``@{command ".."}'' proof is the same as before.
*}
end