minor edits
authorlcp
Mon Jul 11 18:26:57 1994 +0200 (1994-07-11)
changeset 45903b445551763
parent 458 877704b91847
child 460 5d91bd2db00a
minor edits
doc-src/Intro/advanced.tex
doc-src/Intro/theorems.txt
     1.1 --- a/doc-src/Intro/advanced.tex	Mon Jul 11 17:50:34 1994 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Mon Jul 11 18:26:57 1994 +0200
     1.3 @@ -864,14 +864,14 @@
     1.4  \begin{ttbox}
     1.5  goal Nat.thy "~ (Suc(k) = k)";
     1.6  {\out Level 0}
     1.7 -{\out ~Suc(k) = k}
     1.8 -{\out  1. ~Suc(k) = k}
     1.9 +{\out Suc(k) ~= k}
    1.10 +{\out  1. Suc(k) ~= k}
    1.11  \ttbreak
    1.12  by (res_inst_tac [("n","k")] induct 1);
    1.13  {\out Level 1}
    1.14 -{\out ~Suc(k) = k}
    1.15 -{\out  1. ~Suc(0) = 0}
    1.16 -{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
    1.17 +{\out Suc(k) ~= k}
    1.18 +{\out  1. Suc(0) ~= 0}
    1.19 +{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
    1.20  \end{ttbox}
    1.21  We should check that Isabelle has correctly applied induction.  Subgoal~1
    1.22  is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
    1.23 @@ -881,14 +881,14 @@
    1.24  \begin{ttbox}
    1.25  by (resolve_tac [notI] 1);
    1.26  {\out Level 2}
    1.27 -{\out ~Suc(k) = k}
    1.28 +{\out Suc(k) ~= k}
    1.29  {\out  1. Suc(0) = 0 ==> False}
    1.30 -{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
    1.31 +{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
    1.32  \ttbreak
    1.33  by (eresolve_tac [Suc_neq_0] 1);
    1.34  {\out Level 3}
    1.35 -{\out ~Suc(k) = k}
    1.36 -{\out  1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
    1.37 +{\out Suc(k) ~= k}
    1.38 +{\out  1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
    1.39  \end{ttbox}
    1.40  The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
    1.41  Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
    1.42 @@ -896,17 +896,17 @@
    1.43  \begin{ttbox}
    1.44  by (resolve_tac [notI] 1);
    1.45  {\out Level 4}
    1.46 -{\out ~Suc(k) = k}
    1.47 -{\out  1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
    1.48 +{\out Suc(k) ~= k}
    1.49 +{\out  1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
    1.50  \ttbreak
    1.51  by (eresolve_tac [notE] 1);
    1.52  {\out Level 5}
    1.53 -{\out ~Suc(k) = k}
    1.54 +{\out Suc(k) ~= k}
    1.55  {\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
    1.56  \ttbreak
    1.57  by (eresolve_tac [Suc_inject] 1);
    1.58  {\out Level 6}
    1.59 -{\out ~Suc(k) = k}
    1.60 +{\out Suc(k) ~= k}
    1.61  {\out No subgoals!}
    1.62  \end{ttbox}
    1.63  
    1.64 @@ -983,7 +983,7 @@
    1.65  insert the equations proved in the previous section, namely
    1.66  $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
    1.67  \begin{ttbox}
    1.68 -val add_ss = FOL_ss addrews [add_0, add_Suc];
    1.69 +val add_ss = FOL_ss addsimps [add_0, add_Suc];
    1.70  \end{ttbox}
    1.71  We state the goal for associativity of addition, and
    1.72  use \ttindex{res_inst_tac} to invoke induction on~$k$:
     2.1 --- a/doc-src/Intro/theorems.txt	Mon Jul 11 17:50:34 1994 +0200
     2.2 +++ b/doc-src/Intro/theorems.txt	Mon Jul 11 18:26:57 1994 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4  
     2.5  (*tactics *)
     2.6  
     2.7 -goal cla_thy "P|P --> P";
     2.8 +goal FOL.thy "P|P --> P";
     2.9  by (resolve_tac [impI] 1);
    2.10  by (resolve_tac [disjE] 1);
    2.11  by (assume_tac 3);
    2.12 @@ -67,7 +67,7 @@
    2.13  val mythm = prth(result());
    2.14  
    2.15  
    2.16 -goal cla_thy "(P & Q) | R  --> (P | R)";
    2.17 +goal FOL.thy "(P & Q) | R  --> (P | R)";
    2.18  by (resolve_tac [impI] 1);
    2.19  by (eresolve_tac [disjE] 1);
    2.20  by (dresolve_tac [conjunct1] 1);
    2.21 @@ -76,7 +76,7 @@
    2.22  by (REPEAT (assume_tac 1));
    2.23  
    2.24  
    2.25 -- goal cla_thy "(P & Q) | R  --> (P | R)";
    2.26 +- goal FOL.thy "(P & Q) | R  --> (P | R)";
    2.27  Level 0
    2.28  P & Q | R --> P | R
    2.29   1. P & Q | R --> P | R
    2.30 @@ -110,7 +110,7 @@
    2.31  No subgoals!
    2.32  
    2.33  
    2.34 -goal cla_thy "(P | Q) | R  -->  P | (Q | R)";
    2.35 +goal FOL.thy "(P | Q) | R  -->  P | (Q | R)";
    2.36  by (resolve_tac [impI] 1);
    2.37  by (eresolve_tac [disjE] 1);
    2.38  by (eresolve_tac [disjE] 1);