apply. -> by
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jul 28 16:02:51 2000 +0200
@@ -105,7 +105,7 @@
that contains two \isa{case}-expressions over instructions. Thus we add
automatic case splitting as well, which finishes the proof:
*}
-apply(induct_tac xs, simp, simp split: instr.split).;
+by(induct_tac xs, simp, simp split: instr.split);
text{*\noindent
Note that because \isaindex{auto} performs simplification, it can
@@ -116,7 +116,7 @@
lemmas [simp del] = exec_app;
lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)";
(*>*)
-apply(induct_tac xs, auto split: instr.split).;
+by(induct_tac xs, auto split: instr.split);
text{*\noindent
Although this is more compact, it is less clear for the reader of the proof.
@@ -128,6 +128,6 @@
*}
(*<*)
theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
-apply(induct_tac e, auto).;
+by(induct_tac e, auto);
end
(*>*)
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Jul 28 16:02:51 2000 +0200
@@ -94,14 +94,14 @@
that contains two \isa{case}-expressions over instructions. Thus we add
automatic case splitting as well, which finishes the proof:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac~xs,~simp,~simp~split:~instr.split)\isacommand{.}%
+\isacommand{by}(induct\_tac~xs,~simp,~simp~split:~instr.split)%
\begin{isamarkuptext}%
\noindent
Note that because \isaindex{auto} performs simplification, it can
also be modified in the same way \isa{simp} can. Thus the proof can be
rewritten as%
\end{isamarkuptext}%
-\isacommand{apply}(induct\_tac~xs,~auto~split:~instr.split)\isacommand{.}%
+\isacommand{by}(induct\_tac~xs,~auto~split:~instr.split)%
\begin{isamarkuptext}%
\noindent
Although this is more compact, it is less clear for the reader of the proof.
--- a/doc-src/TutorialI/Datatype/ABexpr.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Fri Jul 28 16:02:51 2000 +0200
@@ -101,7 +101,7 @@
The resulting 8 goals (one for each constructor) are proved in one fell swoop:
*}
-apply auto.;
+by auto;
text{*
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Jul 28 16:02:51 2000 +0200
@@ -60,7 +60,7 @@
lemma "subst Var t = (t ::('a,'b)term) \\<and>
substs Var ts = (ts::('a,'b)term list)";
-apply(induct_tac t and ts, auto).;
+by(induct_tac t and ts, auto);
text{*\noindent
Note that \isa{Var} is the identity substitution because by definition it
@@ -88,7 +88,7 @@
(*<*)
lemma "subst s (App f ts) = App f (map (subst s) ts)";
-apply(induct_tac ts, auto).;
+by(induct_tac ts, auto);
end
(*>*)
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Jul 28 16:02:51 2000 +0200
@@ -91,7 +91,7 @@
\noindent
The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
\end{isamarkuptxt}%
-\isacommand{apply}~auto\isacommand{.}%
+\isacommand{by}~auto%
\begin{isamarkuptext}%
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
an inductive proof expects a goal of the form
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Fri Jul 28 16:02:51 2000 +0200
@@ -55,7 +55,7 @@
\end{isamarkuptext}%
\isacommand{lemma}~{"}subst~~Var~t~~=~(t~::('a,'b)term)~~{\isasymand}\isanewline
~~~~~~~~substs~Var~ts~=~(ts::('a,'b)term~list){"}\isanewline
-\isacommand{apply}(induct\_tac~t~\isakeyword{and}~ts,~auto)\isacommand{.}%
+\isacommand{by}(induct\_tac~t~\isakeyword{and}~ts,~auto)%
\begin{isamarkuptext}%
\noindent
Note that \isa{Var} is the identity substitution because by definition it
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Jul 28 16:02:51 2000 +0200
@@ -84,7 +84,7 @@
*}
apply(induct_tac b);
-apply(auto).;
+by(auto);
text{*\noindent
In fact, all proofs in this case study look exactly like this. Hence we do
@@ -127,11 +127,11 @@
"\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
(*<*)
apply(induct_tac b);
-apply(auto).;
+by(auto);
theorem "valif (norm b) env = valif b env";
apply(induct_tac b);
-apply(auto).;
+by(auto);
(*>*)
text{*\noindent
Note that the lemma does not have a name, but is implicitly used in the proof
@@ -153,14 +153,14 @@
normality of \isa{normif}:
*}
-lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
+lemma[simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
(*<*)
apply(induct_tac b);
-apply(auto).;
+by(auto);
theorem "normal(norm b)";
apply(induct_tac b);
-apply(auto).;
+by(auto);
end
(*>*)
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Jul 28 16:02:51 2000 +0200
@@ -74,7 +74,7 @@
The proof is canonical:%
\end{isamarkuptxt}%
\isacommand{apply}(induct\_tac~b)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
In fact, all proofs in this case study look exactly like this. Hence we do
@@ -131,7 +131,7 @@
and prove \isa{normal(norm b)}. Of course, this requires a lemma about
normality of \isa{normif}:%
\end{isamarkuptext}%
-\isacommand{lemma}~[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
+\isacommand{lemma}[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/Itrev.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Fri Jul 28 16:02:51 2000 +0200
@@ -5,7 +5,7 @@
text{*
We define a tail-recursive version of list-reversal,
i.e.\ one that can be compiled into a loop:
-*}
+*};
consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
primrec
@@ -18,13 +18,13 @@
argument when the first one becomes empty.
We need to show that \isa{itrev} does indeed reverse its first argument
provided the second one is empty:
-*}
+*};
lemma "itrev xs [] = rev xs";
txt{*\noindent
There is no choice as to the induction variable, and we immediately simplify:
-*}
+*};
apply(induct_tac xs, auto);
@@ -42,7 +42,7 @@
Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
just not true---the correct generalization is
-*}
+*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys";
@@ -67,7 +67,7 @@
the subgoal, but the induction hypothesis needs to be applied with
\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
for all \isa{ys} instead of a fixed one:
-*}
+*};
(*<*)oops;(*>*)
lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
@@ -82,9 +82,9 @@
provability of the goal. Because it is not always required, and may even
complicate matters in some cases, this heuristic is often not
applied blindly.
-*}
+*};
(*<*)
-oops;
+by(induct_tac xs, simp, simp);
end
(*>*)
--- a/doc-src/TutorialI/Misc/Tree.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Fri Jul 28 16:02:51 2000 +0200
@@ -21,7 +21,7 @@
lemma mirror_mirror: "mirror(mirror t) = t";
(*<*)
apply(induct_tac t);
-apply(auto).;
+by(auto);
end
(*>*)
--- a/doc-src/TutorialI/Misc/arith1.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith1.thy Fri Jul 28 16:02:51 2000 +0200
@@ -3,6 +3,6 @@
(*>*)
lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
(**)(*<*)
-apply(auto).;
+by(auto);
end
(*>*)
--- a/doc-src/TutorialI/Misc/arith2.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith2.thy Fri Jul 28 16:02:51 2000 +0200
@@ -2,7 +2,7 @@
theory arith2 = Main:;
(*>*)
lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
-apply(arith).;
+by(arith);
(**)(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/arith4.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/arith4.thy Fri Jul 28 16:02:51 2000 +0200
@@ -3,6 +3,6 @@
(*>*)
lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
(**)(*<*)
-oops;
+by(arith);
end
(*>*)
--- a/doc-src/TutorialI/Misc/asm_simp.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/asm_simp.thy Fri Jul 28 16:02:51 2000 +0200
@@ -7,7 +7,7 @@
*}
lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
-apply simp.;
+by simp;
text{*\noindent
The second assumption simplifies to \isa{xs = []}, which in turn
@@ -28,7 +28,7 @@
explicitly telling the simplifier to ignore the assumptions:
*}
-apply(simp (no_asm)).;
+by(simp (no_asm));
text{*\noindent
There are three options that influence the treatment of assumptions:
--- a/doc-src/TutorialI/Misc/case_splits.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_splits.thy Fri Jul 28 16:02:51 2000 +0200
@@ -53,7 +53,7 @@
(*<*)
lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
(*>*)
-apply(simp split: list.split).;
+by(simp split: list.split);
text{*\noindent%
which \isacommand{apply}\isa{(simp)} alone will not do.
--- a/doc-src/TutorialI/Misc/cases.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/cases.thy Fri Jul 28 16:02:51 2000 +0200
@@ -14,7 +14,7 @@
which is solved automatically:
*}
-apply(auto).;
+by(auto);
(**)
(*<*)
end
--- a/doc-src/TutorialI/Misc/cond_rewr.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy Fri Jul 28 16:02:51 2000 +0200
@@ -8,7 +8,7 @@
*}
lemma hd_Cons_tl[simp]: "xs \\<noteq> [] \\<Longrightarrow> hd xs # tl xs = xs";
-apply(case_tac xs, simp, simp).;
+by(case_tac xs, simp, simp);
text{*\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
@@ -20,7 +20,7 @@
lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
(*<*)
-apply(simp).
+by(simp);
(*>*)
text{*\noindent
is proved by plain simplification:
--- a/doc-src/TutorialI/Misc/document/arith2.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex Fri Jul 28 16:02:51 2000 +0200
@@ -1,6 +1,6 @@
\begin{isabelle}%
\isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline
-\isacommand{apply}(arith)\isacommand{.}\isanewline
+\isacommand{by}(arith)\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Fri Jul 28 16:02:51 2000 +0200
@@ -5,7 +5,7 @@
as simplification rules and are simplified themselves. For example:%
\end{isamarkuptext}%
\isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline
-\isacommand{apply}~simp\isacommand{.}%
+\isacommand{by}~simp%
\begin{isamarkuptext}%
\noindent
The second assumption simplifies to \isa{xs = []}, which in turn
@@ -24,7 +24,7 @@
nontermination but not this one. The problem can be circumvented by
explicitly telling the simplifier to ignore the assumptions:%
\end{isamarkuptxt}%
-\isacommand{apply}(simp~(no\_asm))\isacommand{.}%
+\isacommand{by}(simp~(no\_asm))%
\begin{isamarkuptext}%
\noindent
There are three options that influence the treatment of assumptions:
--- a/doc-src/TutorialI/Misc/document/case_splits.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex Fri Jul 28 16:02:51 2000 +0200
@@ -43,7 +43,7 @@
in case of recursive datatypes. Again, if the \isa{only:} modifier is
dropped, the above goal is solved,%
\end{isamarkuptext}%
-\isacommand{apply}(simp~split:~list.split)\isacommand{.}%
+\isacommand{by}(simp~split:~list.split)%
\begin{isamarkuptext}%
\noindent%
which \isacommand{apply}\isa{(simp)} alone will not do.
--- a/doc-src/TutorialI/Misc/document/cases.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex Fri Jul 28 16:02:51 2000 +0200
@@ -11,7 +11,7 @@
\end{isabellepar}%
which is solved automatically:%
\end{isamarkuptxt}%
-\isacommand{apply}(auto)\isacommand{.}\isanewline
+\isacommand{by}(auto)\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Fri Jul 28 16:02:51 2000 +0200
@@ -5,7 +5,7 @@
accepts \emph{conditional} equations, for example%
\end{isamarkuptext}%
\isacommand{lemma}~hd\_Cons\_tl[simp]:~{"}xs~{\isasymnoteq}~[]~~{\isasymLongrightarrow}~~hd~xs~\#~tl~xs~=~xs{"}\isanewline
-\isacommand{apply}(case\_tac~xs,~simp,~simp)\isacommand{.}%
+\isacommand{by}(case\_tac~xs,~simp,~simp)%
\begin{isamarkuptext}%
\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Fri Jul 28 16:02:51 2000 +0200
@@ -1,6 +1,6 @@
\begin{isabelle}%
\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
-\isacommand{apply}(simp~add:~Let\_def)\isacommand{.}%
+\isacommand{by}(simp~add:~Let\_def)%
\begin{isamarkuptext}%
If, in a particular context, there is no danger of a combinatorial explosion
of nested \isa{let}s one could even add \isa{Let_def} permanently:%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Jul 28 16:02:51 2000 +0200
@@ -18,7 +18,7 @@
\end{isamarkuptext}%
\isacommand{lemma}~{"}sum~n~+~sum~n~=~n*(Suc~n){"}\isanewline
\isacommand{apply}(induct\_tac~n)\isanewline
-\isacommand{apply}(auto)\isacommand{.}\isanewline
+\isacommand{by}(auto)\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Fri Jul 28 16:02:51 2000 +0200
@@ -1,14 +1,14 @@
\begin{isabelle}%
\isanewline
-~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~((m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
+~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~(m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
\begin{isamarkuptext}%
\noindent\small
where \isa{dvd} means ``divides''.
Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency. (Why?) What you
+right-hand side, which would introduce an inconsistency (why?). What you
should have written is%
\end{isamarkuptext}%
-~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~(m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
+~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/let_rewr.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/let_rewr.thy Fri Jul 28 16:02:51 2000 +0200
@@ -2,7 +2,7 @@
theory let_rewr = Main:;
(*>*)
lemma "(let xs = [] in xs@ys@xs) = ys";
-apply(simp add: Let_def).;
+by(simp add: Let_def);
text{*
If, in a particular context, there is no danger of a combinatorial explosion
--- a/doc-src/TutorialI/Misc/natsum.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Fri Jul 28 16:02:51 2000 +0200
@@ -21,7 +21,7 @@
lemma "sum n + sum n = n*(Suc n)";
apply(induct_tac n);
-apply(auto).;
+by(auto);
(*<*)
end
--- a/doc-src/TutorialI/Misc/prime_def.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Fri Jul 28 16:02:51 2000 +0200
@@ -4,15 +4,15 @@
(*>*)
(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))";
+ "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
text{*\noindent\small
where \isa{dvd} means ``divides''.
Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency. (Why?) What you
+right-hand side, which would introduce an inconsistency (why?). What you
should have written is
*}
(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
+ "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Recdef/Induction.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy Fri Jul 28 16:02:51 2000 +0200
@@ -41,7 +41,7 @@
The rest is pure simplification:
*}
-apply auto.;
+by auto;
text{*
Try proving the above lemma by structural induction, and you find that you
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Fri Jul 28 16:02:51 2000 +0200
@@ -36,7 +36,7 @@
\end{isabellepar}%
The rest is pure simplification:%
\end{isamarkuptxt}%
-\isacommand{apply}~auto\isacommand{.}%
+\isacommand{by}~auto%
\begin{isamarkuptext}%
Try proving the above lemma by structural induction, and you find that you
need an additional case distinction. What is worse, the names of variables
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jul 28 16:02:51 2000 +0200
@@ -79,9 +79,9 @@
derived conditional ones. For \isa{gcd} it means we have to prove%
\end{isamarkuptext}%
\isacommand{lemma}~[simp]:~{"}gcd~(m,~0)~=~m{"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}\isanewline
+\isacommand{by}(simp)\isanewline
\isacommand{lemma}~[simp]:~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~gcd(m,~n)~=~gcd(n,~m~mod~n){"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}%
+\isacommand{by}(simp)%
\begin{isamarkuptext}%
\noindent
after which we can disable the original simplification rule:%
--- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Jul 28 16:02:51 2000 +0200
@@ -31,7 +31,7 @@
It was not proved automatically because of the special nature of \isa{-}
on \isa{nat}. This requires more arithmetic than is tried by default:%
\end{isamarkuptxt}%
-\isacommand{apply}(arith)\isacommand{.}%
+\isacommand{by}(arith)%
\begin{isamarkuptext}%
\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
@@ -48,7 +48,7 @@
rules. Thus we can automatically prove%
\end{isamarkuptext}%
\isacommand{theorem}~wow:~{"}g(1,0)~=~g(1,1){"}\isanewline
-\isacommand{apply}(simp)\isacommand{.}%
+\isacommand{by}(simp)%
\begin{isamarkuptext}%
\noindent
More exciting theorems require induction, which is discussed below.
--- a/doc-src/TutorialI/Recdef/simplification.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Fri Jul 28 16:02:51 2000 +0200
@@ -90,9 +90,9 @@
*}
lemma [simp]: "gcd (m, 0) = m";
-apply(simp).;
+by(simp);
lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
-apply(simp).;
+by(simp);
text{*\noindent
after which we can disable the original simplification rule:
--- a/doc-src/TutorialI/Recdef/termination.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Fri Jul 28 16:02:51 2000 +0200
@@ -36,7 +36,7 @@
on \isa{nat}. This requires more arithmetic than is tried by default:
*}
-apply(arith).;
+by(arith);
text{*\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
@@ -55,7 +55,7 @@
*}
theorem wow: "g(1,0) = g(1,1)";
-apply(simp).;
+by(simp);
text{*\noindent
More exciting theorems require induction, which is discussed below.
--- a/doc-src/TutorialI/ToyList/ToyList.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Fri Jul 28 16:02:51 2000 +0200
@@ -286,7 +286,9 @@
just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
printed out after the final dot) the free variable \isa{xs} has been
replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}.
+\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+followed by a dot, you can simply write \isacommand{by}\indexbold{by},
+which we do most of the time.
Going back to the proof of the first lemma
*}
@@ -324,7 +326,7 @@
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
apply(induct_tac xs);
-apply(auto).;
+by(auto);
text{*
\noindent
@@ -335,7 +337,7 @@
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
apply(induct_tac xs);
-apply(auto).;
+by(auto);
text{*\noindent
and then solve our main theorem:
@@ -343,7 +345,7 @@
theorem rev_rev [simp]: "rev(rev xs) = xs";
apply(induct_tac xs);
-apply(auto).;
+by(auto);
text{*\noindent
The final \isa{end} tells Isabelle to close the current theory because
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jul 28 16:02:51 2000 +0200
@@ -265,7 +265,9 @@
just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
printed out after the final dot) the free variable \isa{xs} has been
replaced by the unknown \isa{?xs}, just as explained in
-\S\ref{sec:variables}.
+\S\ref{sec:variables}. Note that instead of instead of \isacommand{apply}
+followed by a dot, you can simply write \isacommand{by}\indexbold{by},
+which we do most of the time.
Going back to the proof of the first lemma%
\end{isamarkuptext}%
@@ -299,7 +301,7 @@
\end{comment}
\isacommand{lemma}~app\_assoc~[simp]:~{"}(xs~@~ys)~@~zs~=~xs~@~(ys~@~zs){"}\isanewline
\isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
succeeds without further ado.
@@ -308,14 +310,14 @@
\end{isamarkuptext}%
\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline
\isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
and then solve our main theorem:%
\end{isamarkuptext}%
\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}\isanewline
\isacommand{apply}(induct\_tac~xs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
The final \isa{end} tells Isabelle to close the current theory because
--- a/doc-src/TutorialI/ToyList2/ToyList2 Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList2 Fri Jul 28 16:02:51 2000 +0200
@@ -1,17 +1,18 @@
lemma app_Nil2 [simp]: "xs @ [] = xs";
apply(induct_tac xs);
-apply(auto);.;
+apply(auto);
+.;
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
apply(induct_tac xs);
-apply(auto);.;
+by(auto);
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
apply(induct_tac xs);
-apply(auto);.;
+by(auto);
theorem rev_rev [simp]: "rev(rev xs) = xs";
apply(induct_tac xs);
-apply(auto);.;
+by(auto);
end;
--- a/doc-src/TutorialI/Trie/Trie.thy Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Fri Jul 28 16:02:51 2000 +0200
@@ -7,7 +7,7 @@
representation where the subtries are held in an association list, i.e.\ a
list of (letter,trie) pairs. Abstracting over the alphabet \isa{'a} and the
values \isa{'v} we define a trie as follows:
-*}
+*};
datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list";
@@ -16,7 +16,7 @@
association list of subtries. This is an example of nested recursion involving products,
which is fine because products are datatypes as well.
We define two selector functions:
-*}
+*};
consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
@@ -25,7 +25,7 @@
text{*\noindent
Association lists come with a generic lookup function:
-*}
+*};
consts assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
primrec "assoc [] x = None"
@@ -37,7 +37,7 @@
examining the letters of the search string one by one. As
recursion on lists is simpler than on tries, let us express this as primitive
recursion on the search string argument:
-*}
+*};
consts lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
primrec "lookup t [] = value t"
@@ -49,16 +49,16 @@
As a first simple property we prove that looking up a string in the empty
trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
distinguishes the two cases whether the search string is empty or not:
-*}
+*};
lemma [simp]: "lookup (Trie None []) as = None";
-apply(case_tac as, auto).;
+by(case_tac as, auto);
text{*
Things begin to get interesting with the definition of an update function
that adds a new (string,value) pair to a trie, overwriting the old value
associated with that string:
-*}
+*};
consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
primrec
@@ -79,7 +79,7 @@
Before we start on any proofs about \isa{update} we tell the simplifier to
expand all \isa{let}s and to split all \isa{case}-constructs over
options:
-*}
+*};
theorems [simp] = Let_def;
theorems [split] = option.split;
@@ -91,7 +91,7 @@
Our main goal is to prove the correct interaction of \isa{update} and
\isa{lookup}:
-*}
+*};
theorem "\\<forall>t v bs. lookup (update t as v) bs =
(if as=bs then Some v else lookup t bs)";
@@ -104,7 +104,7 @@
if \isa{update} has already been simplified, which can only happen if
\isa{as} is instantiated.
The start of the proof is completely conventional:
-*}
+*};
apply(induct_tac as, auto);
@@ -118,10 +118,10 @@
Clearly, if we want to make headway we have to instantiate \isa{bs} as
well now. It turns out that instead of induction, case distinction
suffices:
-*}
+*};
apply(case_tac[!] bs);
-apply(auto).;
+by(auto);
text{*\noindent
Both \isaindex{case_tac} and \isaindex{induct_tac}
@@ -136,8 +136,8 @@
goals up in such a way that case distinction on \isa{bs} makes sense and
solves the proof. Part~\ref{Isar} shows you how to write readable and stable
proofs.
-*}
+*};
(*<*)
-end
+end;
(*>*)
--- a/doc-src/TutorialI/Trie/document/Trie.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Fri Jul 28 16:02:51 2000 +0200
@@ -44,7 +44,7 @@
distinguishes the two cases whether the search string is empty or not:%
\end{isamarkuptext}%
\isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline
-\isacommand{apply}(case\_tac~as,~auto)\isacommand{.}%
+\isacommand{by}(case\_tac~as,~auto)%
\begin{isamarkuptext}%
Things begin to get interesting with the definition of an update function
that adds a new (string,value) pair to a trie, overwriting the old value
@@ -107,7 +107,7 @@
suffices:%
\end{isamarkuptxt}%
\isacommand{apply}(case\_tac[!]~bs)\isanewline
-\isacommand{apply}(auto)\isacommand{.}%
+\isacommand{by}(auto)%
\begin{isamarkuptext}%
\noindent
Both \isaindex{case_tac} and \isaindex{induct_tac}
--- a/doc-src/TutorialI/fp.tex Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Fri Jul 28 16:02:51 2000 +0200
@@ -472,6 +472,8 @@
\subsection{Using the simplifier}
\label{sec:SimpFeatures}
+\subsubsection{What is simplification}
+
In its most basic form, simplification means repeated application of
equations from left to right. For example, taking the rules for \isa{\at}
and applying them to the term \isa{[0,1] \at\ []} results in a sequence of