author lcp Mon, 11 Jul 1994 18:26:57 +0200 changeset 459 03b445551763 parent 458 877704b91847 child 460 5d91bd2db00a
minor edits
 doc-src/Intro/advanced.tex file | annotate | diff | comparison | revisions doc-src/Intro/theorems.txt file | annotate | diff | comparison | revisions
--- a/doc-src/Intro/advanced.tex	Mon Jul 11 17:50:34 1994 +0200
+++ b/doc-src/Intro/advanced.tex	Mon Jul 11 18:26:57 1994 +0200
@@ -864,14 +864,14 @@
\begin{ttbox}
goal Nat.thy "~ (Suc(k) = k)";
{\out Level 0}
-{\out ~Suc(k) = k}
-{\out  1. ~Suc(k) = k}
+{\out Suc(k) ~= k}
+{\out  1. Suc(k) ~= k}
\ttbreak
by (res_inst_tac [("n","k")] induct 1);
{\out Level 1}
-{\out ~Suc(k) = k}
-{\out  1. ~Suc(0) = 0}
-{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
+{\out Suc(k) ~= k}
+{\out  1. Suc(0) ~= 0}
+{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
\end{ttbox}
We should check that Isabelle has correctly applied induction.  Subgoal~1
is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
@@ -881,14 +881,14 @@
\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 2}
-{\out ~Suc(k) = k}
+{\out Suc(k) ~= k}
{\out  1. Suc(0) = 0 ==> False}
-{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
+{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
\ttbreak
by (eresolve_tac [Suc_neq_0] 1);
{\out Level 3}
-{\out ~Suc(k) = k}
-{\out  1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
+{\out Suc(k) ~= k}
+{\out  1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
\end{ttbox}
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
@@ -896,17 +896,17 @@
\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 4}
-{\out ~Suc(k) = k}
-{\out  1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
+{\out Suc(k) ~= k}
+{\out  1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
\ttbreak
by (eresolve_tac [notE] 1);
{\out Level 5}
-{\out ~Suc(k) = k}
+{\out Suc(k) ~= k}
{\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
\ttbreak
by (eresolve_tac [Suc_inject] 1);
{\out Level 6}
-{\out ~Suc(k) = k}
+{\out Suc(k) ~= k}
{\out No subgoals!}
\end{ttbox}

@@ -983,7 +983,7 @@
insert the equations proved in the previous section, namely
$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
\begin{ttbox}
\end{ttbox}
We state the goal for associativity of addition, and
use \ttindex{res_inst_tac} to invoke induction on~$k$:
--- a/doc-src/Intro/theorems.txt	Mon Jul 11 17:50:34 1994 +0200
+++ b/doc-src/Intro/theorems.txt	Mon Jul 11 18:26:57 1994 +0200
@@ -58,7 +58,7 @@

(*tactics *)

-goal cla_thy "P|P --> P";
+goal FOL.thy "P|P --> P";
by (resolve_tac [impI] 1);
by (resolve_tac [disjE] 1);
by (assume_tac 3);
@@ -67,7 +67,7 @@
val mythm = prth(result());

-goal cla_thy "(P & Q) | R  --> (P | R)";
+goal FOL.thy "(P & Q) | R  --> (P | R)";
by (resolve_tac [impI] 1);
by (eresolve_tac [disjE] 1);
by (dresolve_tac [conjunct1] 1);
@@ -76,7 +76,7 @@
by (REPEAT (assume_tac 1));

-- goal cla_thy "(P & Q) | R  --> (P | R)";
+- goal FOL.thy "(P & Q) | R  --> (P | R)";
Level 0
P & Q | R --> P | R
1. P & Q | R --> P | R
@@ -110,7 +110,7 @@
No subgoals!

-goal cla_thy "(P | Q) | R  -->  P | (Q | R)";
+goal FOL.thy "(P | Q) | R  -->  P | (Q | R)";
by (resolve_tac [impI] 1);
by (eresolve_tac [disjE] 1);
by (eresolve_tac [disjE] 1);