# HG changeset patch # User nipkow # Date 964792971 -7200 # Node ID c613cd06d5cfcc150dc2da809e5d516b84940964 # Parent 966974a7a5b32c33b7fb8a553806654c7b010a30 apply. -> by diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/CodeGen/CodeGen.thy --- 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]: "\\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 "\\vs. exec (comp e) s vs = (value e s) # vs"; -apply(induct_tac e, auto).; +by(induct_tac e, auto); end (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/CodeGen/document/CodeGen.tex --- 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. diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Datatype/ABexpr.thy --- 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$, diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Datatype/Nested.thy --- 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) \\ 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 (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Datatype/document/ABexpr.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Datatype/document/Nested.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Ifexpr/Ifexpr.thy --- 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 @@ "\\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]: "\\t e. normal(normif b t e) = (normal t \\ normal e)"; +lemma[simp]: "\\t e. normal(normif b t e) = (normal t \\ normal e)"; (*<*) apply(induct_tac b); -apply(auto).; +by(auto); theorem "normal(norm b)"; apply(induct_tac b); -apply(auto).; +by(auto); end (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- 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" diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/Itrev.thy --- 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 \\ 'a list \\ '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 "\\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 (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/Tree.thy --- 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 (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/arith1.thy --- 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 "\\ \\ m < n; m < n+1 \\ \\ m = n"; (**)(*<*) -apply(auto).; +by(auto); end (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/arith2.thy --- 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 (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/arith4.thy --- 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 "\\ m < n \\ m < n+1 \\ m = n"; (**)(*<*) -oops; +by(arith); end (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/asm_simp.thy --- 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 "\\ xs @ zs = ys @ xs; [] @ xs = [] @ [] \\ \\ 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: diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/case_splits.thy --- 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 [] \\ zs | y#ys \\ 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. diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/cases.thy --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/cond_rewr.thy --- 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 \\ [] \\ 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 \\ [] \\ hd(rev xs) # tl(rev xs) = rev xs"; (*<*) -apply(simp). +by(simp); (*>*) text{*\noindent is proved by plain simplification: diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/arith2.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/asm_simp.tex --- 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: diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/case_splits.tex --- 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. diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/cases.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/cond_rewr.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/let_rewr.tex --- 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:% diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/natsum.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/prime_def.tex --- 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" diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/let_rewr.thy --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/natsum.thy --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/prime_def.thy --- 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) \\ 1 < p \\ ((m dvd p) \\ (m=1 \\ m=p))"; + "prime(p) \\ 1 < p \\ (m dvd p \\ (m=1 \\ 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) \\ 1 < p \\ (\\m. (m dvd p) \\ (m=1 \\ m=p))" + "prime(p) \\ 1 < p \\ (\\m. m dvd p \\ (m=1 \\ m=p))" (*<*) end (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/Induction.thy --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/document/Induction.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/document/simplification.tex --- 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:% diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/document/termination.tex --- 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. diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/simplification.thy --- 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 \\ 0 \\ gcd(m, n) = gcd(n, m mod n)"; -apply(simp).; +by(simp); text{*\noindent after which we can disable the original simplification rule: diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Recdef/termination.thy --- 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. diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/ToyList/ToyList.thy --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/ToyList/document/ToyList.tex --- 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 diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/ToyList2/ToyList2 --- 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; diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Trie/Trie.thy --- 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 \\ 'v option" alist :: "('a,'v)trie \\ ('a * ('a,'v)trie)list"; @@ -25,7 +25,7 @@ text{*\noindent Association lists come with a generic lookup function: -*} +*}; consts assoc :: "('key * 'val)list \\ 'key \\ '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 \\ 'a list \\ '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 \\ 'a list \\ 'v \\ ('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 "\\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; (*>*) diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Trie/document/Trie.tex --- 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} diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/fp.tex --- 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