--- a/src/HOL/Isar_examples/BasicLogic.thy Sun Sep 17 22:15:08 2000 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Sun Sep 17 22:19:02 2000 +0200
@@ -5,52 +5,52 @@
Basic propositional and quantifier reasoning.
*)
-header {* Basic logical reasoning *};
+header {* Basic logical reasoning *}
-theory BasicLogic = Main:;
+theory BasicLogic = Main:
-subsection {* Pure backward reasoning *};
+subsection {* Pure backward reasoning *}
text {*
In order to get a first idea of how Isabelle/Isar proof documents may
look like, we consider the propositions $I$, $K$, and $S$. The
following (rather explicit) proofs should require little extra
explanations.
-*};
+*}
-lemma I: "A --> A";
-proof;
- assume A;
- show A; by assumption;
-qed;
+lemma I: "A --> A"
+proof
+ assume A
+ show A by assumption
+qed
-lemma K: "A --> B --> A";
-proof;
- assume A;
- show "B --> A";
- proof;
- show A; by assumption;
- qed;
-qed;
+lemma K: "A --> B --> A"
+proof
+ assume A
+ show "B --> A"
+ proof
+ show A by assumption
+ qed
+qed
-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
-proof;
- assume "A --> B --> C";
- show "(A --> B) --> A --> C";
- proof;
- assume "A --> B";
- show "A --> C";
- proof;
- assume A;
- show C;
- proof (rule mp);
- show "B --> C"; by (rule mp);
- show B; by (rule mp);
- qed;
- qed;
- qed;
-qed;
+lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
+proof
+ assume "A --> B --> C"
+ show "(A --> B) --> A --> C"
+ proof
+ assume "A --> B"
+ show "A --> C"
+ proof
+ assume A
+ show C
+ proof (rule mp)
+ show "B --> C" by (rule mp)
+ show B by (rule mp)
+ qed
+ qed
+ qed
+qed
text {*
Isar provides several ways to fine-tune the reasoning, avoiding
@@ -59,13 +59,13 @@
way, even without referring to any automated proof tools yet.
First of all, proof by assumption may be abbreviated as a single dot.
-*};
+*}
-lemma "A --> A";
-proof;
- assume A;
- show A; .;
-qed;
+lemma "A --> A"
+proof
+ assume A
+ show A .
+qed
text {*
In fact, concluding any (sub-)proof already involves solving any
@@ -73,11 +73,11 @@
trivial operation, as proof by assumption may involve full
higher-order unification.}. Thus we may skip the rather vacuous body
of the above proof as well.
-*};
+*}
-lemma "A --> A";
-proof;
-qed;
+lemma "A --> A"
+proof
+qed
text {*
Note that the \isacommand{proof} command refers to the $\idt{rule}$
@@ -85,22 +85,22 @@
single rule, as determined from the syntactic form of the statements
involved. The \isacommand{by} command abbreviates any proof with
empty body, so the proof may be further pruned.
-*};
+*}
-lemma "A --> A";
- by rule;
+lemma "A --> A"
+ by rule
text {*
Proof by a single rule may be abbreviated as double-dot.
-*};
+*}
-lemma "A --> A"; ..;
+lemma "A --> A" ..
text {*
Thus we have arrived at an adequate representation of the proof of a
tautology that holds by a single standard rule.\footnote{Apparently,
the rule here is implication introduction.}
-*};
+*}
text {*
Let us also reconsider $K$. Its statement is composed of iterated
@@ -110,20 +110,20 @@
The $\idt{intro}$ proof method repeatedly decomposes a goal's
conclusion.\footnote{The dual method is $\idt{elim}$, acting on a
goal's premises.}
-*};
+*}
-lemma "A --> B --> A";
-proof intro;
- assume A;
- show A; .;
-qed;
+lemma "A --> B --> A"
+proof intro
+ assume A
+ show A .
+qed
text {*
Again, the body may be collapsed.
-*};
+*}
-lemma "A --> B --> A";
- by intro;
+lemma "A --> B --> A"
+ by intro
text {*
Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof
@@ -140,10 +140,10 @@
terminal steps that solve a goal completely are usually performed by
actual automated proof methods (such as
\isacommand{by}~$\idt{blast}$).
-*};
+*}
-subsection {* Variations of backward vs.\ forward reasoning *};
+subsection {* Variations of backward vs.\ forward reasoning *}
text {*
Certainly, any proof may be performed in backward-style only. On the
@@ -154,17 +154,17 @@
A$.
The first version is purely backward.
-*};
+*}
-lemma "A & B --> B & A";
-proof;
- assume "A & B";
- show "B & A";
- proof;
- show B; by (rule conjunct2);
- show A; by (rule conjunct1);
- qed;
-qed;
+lemma "A & B --> B & A"
+proof
+ assume "A & B"
+ show "B & A"
+ proof
+ show B by (rule conjunct2)
+ show A by (rule conjunct1)
+ qed
+qed
text {*
Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named
@@ -174,17 +174,17 @@
current facts, enabling the use of double-dot proofs. Note that
\isacommand{from} already does forward-chaining, involving the
\name{conjE} rule here.
-*};
+*}
-lemma "A & B --> B & A";
-proof;
- assume "A & B";
- show "B & A";
- proof;
- from prems; show B; ..;
- from prems; show A; ..;
- qed;
-qed;
+lemma "A & B --> B & A"
+proof
+ assume "A & B"
+ show "B & A"
+ proof
+ from prems show B ..
+ from prems show A ..
+ qed
+qed
text {*
In the next version, we move the forward step one level upwards.
@@ -194,48 +194,48 @@
introduction. The resulting proof structure directly corresponds to
that of the $\name{conjE}$ rule, including the repeated goal
proposition that is abbreviated as $\var{thesis}$ below.
-*};
+*}
-lemma "A & B --> B & A";
-proof;
- assume "A & B";
- then; show "B & A";
- proof -- {* rule \name{conjE} of $A \conj B$ *};
- assume A B;
- show ?thesis; .. -- {* rule \name{conjI} of $B \conj A$ *};
- qed;
-qed;
+lemma "A & B --> B & A"
+proof
+ assume "A & B"
+ then show "B & A"
+ proof -- {* rule \name{conjE} of $A \conj B$ *}
+ assume A B
+ show ?thesis .. -- {* rule \name{conjI} of $B \conj A$ *}
+ qed
+qed
text {*
In the subsequent version we flatten the structure of the main body
by doing forward reasoning all the time. Only the outermost
decomposition step is left as backward.
-*};
+*}
-lemma "A & B --> B & A";
-proof;
- assume ab: "A & B";
- from ab; have a: A; ..;
- from ab; have b: B; ..;
- from b a; show "B & A"; ..;
-qed;
+lemma "A & B --> B & A"
+proof
+ assume ab: "A & B"
+ from ab have a: A ..
+ from ab have b: B ..
+ from b a show "B & A" ..
+qed
text {*
We can still push forward-reasoning a bit further, even at the risk
of getting ridiculous. Note that we force the initial proof step to
do nothing here, by referring to the ``-'' proof method.
-*};
+*}
-lemma "A & B --> B & A";
-proof -;
- {;
- assume ab: "A & B";
- from ab; have a: A; ..;
- from ab; have b: B; ..;
- from b a; have "B & A"; ..;
- };
- thus ?thesis; .. -- {* rule \name{impI} *};
-qed;
+lemma "A & B --> B & A"
+proof -
+ {
+ assume ab: "A & B"
+ from ab have a: A ..
+ from ab have b: B ..
+ from b a have "B & A" ..
+ }
+ thus ?thesis .. -- {* rule \name{impI} *}
+qed
text {*
\medskip With these examples we have shifted through a whole range
@@ -252,7 +252,7 @@
etc., rules (and methods) on the one hand vs.\ facts on the other
hand have to be emphasized in an appropriate way. This requires the
proof writer to develop good taste, and some practice, of course.
-*};
+*}
text {*
For our example the most appropriate way of reasoning is probably the
@@ -261,47 +261,47 @@
abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same
vein, \isacommand{hence} abbreviates
\isacommand{then}~\isacommand{have}.}
-*};
+*}
-lemma "A & B --> B & A";
-proof;
- assume "A & B";
- thus "B & A";
- proof;
- assume A B;
- show ?thesis; ..;
- qed;
-qed;
+lemma "A & B --> B & A"
+proof
+ assume "A & B"
+ thus "B & A"
+ proof
+ assume A B
+ show ?thesis ..
+ qed
+qed
-subsection {* A few examples from ``Introduction to Isabelle'' *};
+subsection {* A few examples from ``Introduction to Isabelle'' *}
text {*
We rephrase some of the basic reasoning examples of
\cite{isabelle-intro}, using HOL rather than FOL.
-*};
+*}
-subsubsection {* A propositional proof *};
+subsubsection {* A propositional proof *}
text {*
We consider the proposition $P \disj P \impl P$. The proof below
involves forward-chaining from $P \disj P$, followed by an explicit
case-analysis on the two \emph{identical} cases.
-*};
+*}
-lemma "P | P --> P";
-proof;
- assume "P | P";
- thus P;
+lemma "P | P --> P"
+proof
+ assume "P | P"
+ thus P
proof -- {*
rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
- *};
- assume P; show P; .;
- next;
- assume P; show P; .;
- qed;
-qed;
+ *}
+ assume P show P .
+ next
+ assume P show P .
+ qed
+qed
text {*
Case splits are \emph{not} hardwired into the Isar language as a
@@ -325,34 +325,34 @@
\medskip In our example the situation is even simpler, since the two
cases actually coincide. Consequently the proof may be rephrased as
follows.
-*};
+*}
-lemma "P | P --> P";
-proof;
- assume "P | P";
- thus P;
- proof;
- assume P;
- show P; .;
- show P; .;
- qed;
-qed;
+lemma "P | P --> P"
+proof
+ assume "P | P"
+ thus P
+ proof
+ assume P
+ show P .
+ show P .
+ qed
+qed
text {*
Again, the rather vacuous body of the proof may be collapsed. Thus
the case analysis degenerates into two assumption steps, which are
implicitly performed when concluding the single rule step of the
double-dot proof as follows.
-*};
+*}
-lemma "P | P --> P";
-proof;
- assume "P | P";
- thus P; ..;
-qed;
+lemma "P | P --> P"
+proof
+ assume "P | P"
+ thus P ..
+qed
-subsubsection {* A quantifier proof *};
+subsubsection {* A quantifier proof *}
text {*
To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap
@@ -366,20 +366,20 @@
the \isacommand{fix} command augments the context by some new
``arbitrary, but fixed'' element; the \isacommand{is} annotation
binds term abbreviations by higher-order pattern matching.
-*};
+*}
-lemma "(EX x. P (f x)) --> (EX x. P x)";
-proof;
- assume "EX x. P (f x)";
- thus "EX x. P x";
+lemma "(EX x. P (f x)) --> (EX x. P x)"
+proof
+ assume "EX x. P (f x)"
+ thus "EX x. P x"
proof (rule exE) -- {*
rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
- *};
- fix a;
- assume "P (f a)" (is "P ?witness");
- show ?thesis; by (rule exI [of P ?witness]);
- qed;
-qed;
+ *}
+ fix a
+ assume "P (f a)" (is "P ?witness")
+ show ?thesis by (rule exI [of P ?witness])
+ qed
+qed
text {*
While explicit rule instantiation may occasionally improve
@@ -388,32 +388,32 @@
structural clues for the system to infer both the rules and their
instances (by higher-order unification). Thus we may as well prune
the text as follows.
-*};
+*}
-lemma "(EX x. P (f x)) --> (EX x. P x)";
-proof;
- assume "EX x. P (f x)";
- thus "EX x. P x";
- proof;
- fix a;
- assume "P (f a)";
- show ?thesis; ..;
- qed;
-qed;
+lemma "(EX x. P (f x)) --> (EX x. P x)"
+proof
+ assume "EX x. P (f x)"
+ thus "EX x. P x"
+ proof
+ fix a
+ assume "P (f a)"
+ show ?thesis ..
+ qed
+qed
text {*
Explicit $\exists$-elimination as seen above can become quite
cumbersome in practice. The derived Isar language element
``\isakeyword{obtain}'' provides a more handsome way to do
generalized existence reasoning.
-*};
+*}
-lemma "(EX x. P (f x)) --> (EX x. P x)";
-proof;
- assume "EX x. P (f x)";
- then; obtain a where "P (f a)"; by blast;
- thus "EX x. P x"; ..;
-qed;
+lemma "(EX x. P (f x)) --> (EX x. P x)"
+proof
+ assume "EX x. P (f x)"
+ then obtain a where "P (f a)" by blast
+ thus "EX x. P x" ..
+qed
text {*
Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
@@ -423,29 +423,29 @@
reasoning involved here, any result exported from the context of an
\isakeyword{obtain} statement may \emph{not} refer to the parameters
introduced there.
-*};
+*}
-subsubsection {* Deriving rules in Isabelle *};
+subsubsection {* Deriving rules in Isabelle *}
text {*
We derive the conjunction elimination rule from the corresponding
projections. The proof is quite straight-forward, since
Isabelle/Isar supports non-atomic goals and assumptions fully
transparently.
-*};
+*}
-theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
-proof -;
- assume "A & B";
- assume r: "A ==> B ==> C";
- show C;
- proof (rule r);
- show A; by (rule conjunct1);
- show B; by (rule conjunct2);
- qed;
-qed;
+theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
+proof -
+ assume "A & B"
+ assume r: "A ==> B ==> C"
+ show C
+ proof (rule r)
+ show A by (rule conjunct1)
+ show B by (rule conjunct2)
+ qed
+qed
text {*
Note that classic Isabelle handles higher rules in a slightly
@@ -454,6 +454,6 @@
\texttt{goal} command to decompose the rule into premises and
conclusion. The actual result would then emerge by discharging of
the context at \texttt{qed} time.
-*};
+*}
-end;
+end