--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Sep 05 13:53:39 2000 +0200
@@ -2,7 +2,9 @@
theory CodeGen = Main:
(*>*)
-text{*\noindent
+section{*Case study: compiling expressions*}
+
+text{*\label{sec:ExprCompiler}
The task is to develop a compiler from a generic type of expressions (built
up from variables, constants and binary operations) to a stack machine. This
generic type of expressions is a generalization of the boolean expressions in
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Sep 05 13:53:39 2000 +0200
@@ -1,8 +1,10 @@
%
\begin{isabellebody}%
%
+\isamarkupsection{Case study: compiling expressions}
+%
\begin{isamarkuptext}%
-\noindent
+\label{sec:ExprCompiler}
The task is to develop a compiler from a generic type of expressions (built
up from variables, constants and binary operations) to a stack machine. This
generic type of expressions is a generalization of the boolean expressions in
--- a/doc-src/TutorialI/IsaMakefile Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Tue Sep 05 13:53:39 2000 +0200
@@ -100,9 +100,8 @@
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
Misc/prime_def.thy Misc/case_exprs.thy \
- Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
- Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
- Misc/trace_simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/asm_simp.thy
+ Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy \
+ Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
@rm -f tutorial.dvi
--- a/doc-src/TutorialI/Misc/Itrev.thy Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Sep 05 13:53:39 2000 +0200
@@ -2,7 +2,32 @@
theory Itrev = Main:;
(*>*)
-text{*
+section{*Induction heuristics*}
+
+text{*\label{sec:InductionHeuristics}
+The purpose of this section is to illustrate some simple heuristics for
+inductive proofs. The first one we have already mentioned in our initial
+example:
+\begin{quote}
+\emph{Theorems about recursive functions are proved by induction.}
+\end{quote}
+In case the function has more than one argument
+\begin{quote}
+\emph{Do induction on argument number $i$ if the function is defined by
+recursion in argument number $i$.}
+\end{quote}
+When we look at the proof of @{term[source]"(xs @ ys) @ zs = xs @ (ys @ zs)"}
+in \S\ref{sec:intro-proof} we find (a) @{text"@"} is recursive in
+the first argument, (b) @{term xs} occurs only as the first argument of
+@{text"@"}, and (c) both @{term ys} and @{term zs} occur at least once as
+the second argument of @{text"@"}. Hence it is natural to perform induction
+on @{term xs}.
+
+The key heuristic, and the main point of this section, is to
+generalize the goal before induction. The reason is simple: if the goal is
+too specific, the induction hypothesis is too weak to allow the induction
+step to go through. Let us now illustrate the idea with an example.
+
Function @{term"rev"} has quadratic worst-case running time
because it calls function @{text"@"} for each element of the list and
@{text"@"} is linear in its first argument. A linear time version of
@@ -36,7 +61,7 @@
txt{*\noindent
Unfortunately, this is not a complete success:
-\begin{isabelle}
+\begin{isabelle}\makeatother
~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
\end{isabelle}
Just as predicted above, the overall goal, and hence the induction
@@ -62,7 +87,7 @@
Although we now have two variables, only @{term"xs"} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabelle}
+\begin{isabelle}\makeatother
~1.~{\isasymAnd}a~list.\isanewline
~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
@@ -75,8 +100,11 @@
*};
(*<*)oops;(*>*)
lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
+(*<*)
+by(induct_tac xs, simp_all);
+(*>*)
-txt{*\noindent
+text{*\noindent
This time induction on @{term"xs"} followed by simplification succeeds. This
leads to another heuristic for generalization:
\begin{quote}
@@ -94,9 +122,19 @@
the problem at hand and is beyond simple rules of thumb. In a nutshell: you
will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
to learn about some advanced techniques for inductive proofs.
-*};
+A final point worth mentioning is the orientation of the equation we just
+proved: the more complex notion (@{term itrev}) is on the left-hand
+side, the simpler one (@{term rev}) on the right-hand side. This constitutes
+another, albeit weak heuristic that is not restricted to induction:
+\begin{quote}
+ \emph{The right-hand side of an equation should (in some sense) be simpler
+ than the left-hand side.}
+\end{quote}
+This heuristic is tricky to apply because it is not obvious that
+@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
+happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
+*}
(*<*)
-by(induct_tac xs, simp_all);
end
(*>*)
--- a/doc-src/TutorialI/Misc/ROOT.ML Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Sep 05 13:53:39 2000 +0200
@@ -7,15 +7,9 @@
use_thy "arith1";
use_thy "arith2";
use_thy "arith3";
-use_thy "arith4";
use_thy "pairs";
use_thy "types";
use_thy "prime_def";
-use_thy "def_rewr";
-use_thy "let_rewr";
-use_thy "cond_rewr";
-use_thy "case_splits";
-use_thy "trace_simp";
+use_thy "simp";
use_thy "Itrev";
use_thy "AdvancedInd";
-use_thy "asm_simp";
--- a/doc-src/TutorialI/Misc/arith4.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*<*)
-theory arith4 = Main:;
-(*>*)
-lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
-(**)(*<*)
-by(arith);
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/asm_simp.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(*<*)
-theory asm_simp = Main:;
-
-(*>*)text{*
-By default, assumptions are part of the simplification process: they are used
-as simplification rules and are simplified themselves. For example:
-*}
-
-lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
-by simp;
-
-text{*\noindent
-The second assumption simplifies to @{term"xs = []"}, which in turn
-simplifies the first assumption to @{term"zs = ys"}, thus reducing the
-conclusion to @{term"ys = ys"} and hence to @{term"True"}.
-
-In some cases this may be too much of a good thing and may lead to
-nontermination:
-*}
-
-lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []";
-
-txt{*\noindent
-cannot be solved by an unmodified application of @{text"simp"} because the
-simplification rule @{term"f x = g (f (g x))"} extracted from the assumption
-does not terminate. Isabelle notices certain simple forms of
-nontermination but not this one. The problem can be circumvented by
-explicitly telling the simplifier to ignore the assumptions:
-*}
-
-by(simp (no_asm));
-
-text{*\noindent
-There are three options that influence the treatment of assumptions:
-\begin{description}
-\item[@{text"(no_asm)"}]\indexbold{*no_asm}
- means that assumptions are completely ignored.
-\item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}
- means that the assumptions are not simplified but
- are used in the simplification of the conclusion.
-\item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use}
- means that the assumptions are simplified but are not
- used in the simplification of each other or the conclusion.
-\end{description}
-Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify
-the above problematic subgoal.
-
-Note that only one of the above options is allowed, and it must precede all
-other arguments.
-*}
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Misc/case_splits.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*<*)
-theory case_splits = Main:;
-(*>*)
-
-text{*
-Goals containing @{text"if"}-expressions are usually proved by case
-distinction on the condition of the @{text"if"}. For example the goal
-*}
-
-lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []";
-
-txt{*\noindent
-can be split into
-\begin{isabelle}
-~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
-\end{isabelle}
-by a degenerate form of simplification
-*}
-
-apply(simp only: split: split_if);
-(*<*)oops;(*>*)
-
-text{*\noindent
-where no simplification rules are included (@{text"only:"} is followed by the
-empty list of theorems) but the rule \isaindexbold{split_if} for
-splitting @{text"if"}s is added (via the modifier @{text"split:"}). Because
-case-splitting on @{text"if"}s is almost always the right proof strategy, the
-simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
-on the initial goal above.
-
-This splitting idea generalizes from @{text"if"} to \isaindex{case}:
-*}
-
-lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
-txt{*\noindent
-becomes
-\begin{isabelle}
-~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
-\end{isabelle}
-by typing
-*}
-
-apply(simp only: split: list.split);
-(*<*)oops;(*>*)
-
-text{*\noindent
-In contrast to @{text"if"}-expressions, the simplifier does not split
-@{text"case"}-expressions by default because this can lead to nontermination
-in case of recursive datatypes. Again, if the @{text"only:"} modifier is
-dropped, the above goal is solved,
-*}
-(*<*)
-lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
-(*>*)
-by(simp split: list.split);
-
-text{*\noindent%
-which \isacommand{apply}@{text"(simp)"} alone will not do.
-
-In general, every datatype $t$ comes with a theorem
-$t$@{text".split"} which can be declared to be a \bfindex{split rule} either
-locally as above, or by giving it the @{text"split"} attribute globally:
-*}
-
-lemmas [split] = list.split;
-
-text{*\noindent
-The @{text"split"} attribute can be removed with the @{text"del"} modifier,
-either locally
-*}
-(*<*)
-lemma "dummy=dummy";
-(*>*)
-apply(simp split del: split_if);
-(*<*)
-oops;
-(*>*)
-text{*\noindent
-or globally:
-*}
-lemmas [split del] = list.split;
-
-text{*
-The above split rules intentionally only affect the conclusion of a
-subgoal. If you want to split an @{text"if"} or @{text"case"}-expression in
-the assumptions, you have to apply @{thm[source]split_if_asm} or
-$t$@{text".split_asm"}:
-*}
-
-lemma "if xs = [] then ys ~= [] else ys = [] ==> xs @ ys ~= []"
-apply(simp only: split: split_if_asm);
-
-txt{*\noindent
-In contrast to splitting the conclusion, this actually creates two
-separate subgoals (which are solved by @{text"simp_all"}):
-\begin{isabelle}
-\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
-\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
-\end{isabelle}
-If you need to split both in the assumptions and the conclusion,
-use $t$@{text".splits"} which subsumes $t$@{text".split"} and
-$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
-*}
-
-(*<*)
-by(simp_all)
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/cond_rewr.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(*<*)
-theory cond_rewr = Main:;
-(*>*)
-
-text{*
-So far all examples of rewrite rules were equations. The simplifier also
-accepts \emph{conditional} equations, for example
-*}
-
-lemma hd_Cons_tl[simp]: "xs \\<noteq> [] \\<Longrightarrow> hd xs # tl xs = xs";
-by(case_tac xs, simp, simp);
-
-text{*\noindent
-Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
-sequence of methods. Assuming that the simplification rule
-@{term"(rev xs = []) = (xs = [])"}
-is present as well,
-*}
-
-lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
-(*<*)
-by(simp);
-(*>*)
-text{*\noindent
-is proved by plain simplification:
-the conditional equation @{thm[source]hd_Cons_tl} above
-can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
-because the corresponding precondition @{term"rev xs ~= []"}
-simplifies to @{term"xs ~= []"}, which is exactly the local
-assumption of the subgoal.
-*}
-(*<*)
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/def_rewr.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*<*)
-theory def_rewr = Main:;
-
-(*>*)text{*\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
-be used as simplification rules, but by default they are not. Hence the
-simplifier does not expand them automatically, just as it should be:
-definitions are introduced for the purpose of abbreviating complex
-concepts. Of course we need to expand the definitions initially to derive
-enough lemmas that characterize the concept sufficiently for us to forget the
-original definition. For example, given
-*}
-
-constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool"
- "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)";
-
-text{*\noindent
-we may want to prove
-*}
-
-lemma "exor A (\\<not>A)";
-
-txt{*\noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}
-*}
-
-apply(simp only:exor_def);
-
-txt{*\noindent
-In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
-\end{isabelle}
-can be proved by simplification. Thus we could have proved the lemma outright
-*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
-by(simp add: exor_def)
-
-text{*\noindent
-Of course we can also unfold definitions in the middle of a proof.
-
-You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.
-*}
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Sep 05 13:53:39 2000 +0200
@@ -1,7 +1,33 @@
%
\begin{isabellebody}%
%
+\isamarkupsection{Induction heuristics}
+%
\begin{isamarkuptext}%
+\label{sec:InductionHeuristics}
+The purpose of this section is to illustrate some simple heuristics for
+inductive proofs. The first one we have already mentioned in our initial
+example:
+\begin{quote}
+\emph{Theorems about recursive functions are proved by induction.}
+\end{quote}
+In case the function has more than one argument
+\begin{quote}
+\emph{Do induction on argument number $i$ if the function is defined by
+recursion in argument number $i$.}
+\end{quote}
+When we look at the proof of \isa{{\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}}
+in \S\ref{sec:intro-proof} we find (a) \isa{{\isacharat}} is recursive in
+the first argument, (b) \isa{xs} occurs only as the first argument of
+\isa{{\isacharat}}, and (c) both \isa{ys} and \isa{zs} occur at least once as
+the second argument of \isa{{\isacharat}}. Hence it is natural to perform induction
+on \isa{xs}.
+
+The key heuristic, and the main point of this section, is to
+generalize the goal before induction. The reason is simple: if the goal is
+too specific, the induction hypothesis is too weak to allow the induction
+step to go through. Let us now illustrate the idea with an example.
+
Function \isa{rev} has quadratic worst-case running time
because it calls function \isa{{\isacharat}} for each element of the list and
\isa{{\isacharat}} is linear in its first argument. A linear time version of
@@ -32,7 +58,7 @@
\begin{isamarkuptxt}%
\noindent
Unfortunately, this is not a complete success:
-\begin{isabelle}
+\begin{isabelle}\makeatother
~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
\end{isabelle}
Just as predicted above, the overall goal, and hence the induction
@@ -57,7 +83,7 @@
Although we now have two variables, only \isa{xs} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabelle}
+\begin{isabelle}\makeatother
~1.~{\isasymAnd}a~list.\isanewline
~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
@@ -69,7 +95,7 @@
for all \isa{ys} instead of a fixed one:%
\end{isamarkuptxt}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
-\begin{isamarkuptxt}%
+\begin{isamarkuptext}%
\noindent
This time induction on \isa{xs} followed by simplification succeeds. This
leads to another heuristic for generalization:
@@ -87,8 +113,20 @@
need to generalize your proposition even further. This requires insight into
the problem at hand and is beyond simple rules of thumb. In a nutshell: you
will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
-to learn about some advanced techniques for inductive proofs.%
-\end{isamarkuptxt}%
+to learn about some advanced techniques for inductive proofs.
+
+A final point worth mentioning is the orientation of the equation we just
+proved: the more complex notion (\isa{itrev}) is on the left-hand
+side, the simpler one (\isa{rev}) on the right-hand side. This constitutes
+another, albeit weak heuristic that is not restricted to induction:
+\begin{quote}
+ \emph{The right-hand side of an equation should (in some sense) be simpler
+ than the left-hand side.}
+\end{quote}
+This heuristic is tricky to apply because it is not obvious that
+\isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
+happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!%
+\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Misc/document/arith4.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-%
-\begin{isabellebody}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-By default, assumptions are part of the simplification process: they are used
-as simplification rules and are simplified themselves. For example:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ xs\ {\isacharat}\ zs\ {\isacharequal}\ ys\ {\isacharat}\ xs{\isacharsemicolon}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ {\isacharequal}\ zs{\isachardoublequote}\isanewline
-\isacommand{by}\ simp%
-\begin{isamarkuptext}%
-\noindent
-The second assumption simplifies to \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}}, which in turn
-simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
-conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
-
-In some cases this may be too much of a good thing and may lead to
-nontermination:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption
-does not terminate. Isabelle notices certain simple forms of
-nontermination but not this one. The problem can be circumvented by
-explicitly telling the simplifier to ignore the assumptions:%
-\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-There are three options that influence the treatment of assumptions:
-\begin{description}
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
- means that assumptions are completely ignored.
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}
- means that the assumptions are not simplified but
- are used in the simplification of the conclusion.
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}
- means that the assumptions are simplified but are not
- used in the simplification of each other or the conclusion.
-\end{description}
-Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify
-the above problematic subgoal.
-
-Note that only one of the above options is allowed, and it must precede all
-other arguments.%
-\end{isamarkuptext}%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/case_splits.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,92 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-Goals containing \isa{if}-expressions are usually proved by case
-distinction on the condition of the \isa{if}. For example the goal%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-can be split into
-\begin{isabelle}
-~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])
-\end{isabelle}
-by a degenerate form of simplification%
-\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-where no simplification rules are included (\isa{only{\isacharcolon}} is followed by the
-empty list of theorems) but the rule \isaindexbold{split_if} for
-splitting \isa{if}s is added (via the modifier \isa{split{\isacharcolon}}). Because
-case-splitting on \isa{if}s is almost always the right proof strategy, the
-simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
-on the initial goal above.
-
-This splitting idea generalizes from \isa{if} to \isaindex{case}:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-becomes
-\begin{isabelle}
-~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
-~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)
-\end{isabelle}
-by typing%
-\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-In contrast to \isa{if}-expressions, the simplifier does not split
-\isa{case}-expressions by default because this can lead to nontermination
-in case of recursive datatypes. Again, if the \isa{only{\isacharcolon}} modifier is
-dropped, the above goal is solved,%
-\end{isamarkuptext}%
-\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent%
-which \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not do.
-
-In general, every datatype $t$ comes with a theorem
-$t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
-locally as above, or by giving it the \isa{split} attribute globally:%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
-\begin{isamarkuptext}%
-\noindent
-The \isa{split} attribute can be removed with the \isa{del} modifier,
-either locally%
-\end{isamarkuptext}%
-\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-or globally:%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split%
-\begin{isamarkuptext}%
-The above split rules intentionally only affect the conclusion of a
-subgoal. If you want to split an \isa{if} or \isa{case}-expression in
-the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or
-$t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ xs\ {\isacharat}\ ys\ {\isachartilde}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
-\begin{isamarkuptxt}%
-\noindent
-In contrast to splitting the conclusion, this actually creates two
-separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
-\begin{isabelle}
-\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ \mbox{ys}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
-\ \isadigit{2}{\isachardot}\ {\isasymlbrakk}\mbox{xs}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ \mbox{ys}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ \mbox{xs}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}
-\end{isabelle}
-If you need to split both in the assumptions and the conclusion,
-use $t$\isa{{\isachardot}splits} which subsumes $t$\isa{{\isachardot}split} and
-$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.%
-\end{isamarkuptxt}%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-So far all examples of rewrite rules were equations. The simplifier also
-accepts \emph{conditional} equations, for example%
-\end{isamarkuptext}%
-\isacommand{lemma}\ hd{\isacharunderscore}Cons{\isacharunderscore}tl{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ \ {\isasymLongrightarrow}\ \ hd\ xs\ {\isacharhash}\ tl\ xs\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
-sequence of methods. Assuming that the simplification rule
-\isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
-is present as well,%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-is proved by plain simplification:
-the conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
-can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs}
-because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
-simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local
-assumption of the subgoal.%
-\end{isamarkuptext}%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
-be used as simplification rules, but by default they are not. Hence the
-simplifier does not expand them automatically, just as it should be:
-definitions are introduced for the purpose of abbreviating complex
-concepts. Of course we need to expand the definitions initially to derive
-enough lemmas that characterize the concept sufficiently for us to forget the
-original definition. For example, given%
-\end{isamarkuptext}%
-\isacommand{constdefs}\ exor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
-\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-we may want to prove%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}exor\ A\ {\isacharparenleft}{\isasymnot}A{\isacharparenright}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
-get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}%
-\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}exor{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptxt}%
-\noindent
-In this particular case, the resulting goal
-\begin{isabelle}
-~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
-\end{isabelle}
-can be proved by simplification. Thus we could have proved the lemma outright%
-\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-Of course we can also unfold definitions in the middle of a proof.
-
-You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.%
-\end{isamarkuptext}%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\isamarkupsubsubsection{Simplifying let-expressions}
-%
-\begin{isamarkuptext}%
-\index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
-requires the \isa{let}-con\-structs to be expanded at some point. Since
-\isa{let}-\isa{in} is just syntactic sugar for a predefined constant
-(called \isa{Let}), expanding \isa{let}-constructs means rewriting with
-\isa{Let{\isacharunderscore}def}:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
-\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{\isacharunderscore}def} permanently:%
-\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Tue Sep 05 13:53:39 2000 +0200
@@ -1,15 +1,27 @@
%
\begin{isabellebody}%
-\isanewline
-\ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+%
\begin{isamarkuptext}%
-\noindent\small
+\begin{warn}
+A common mistake when writing definitions is to introduce extra free
+variables on the right-hand side as in the following fictitious definition:
+%
+\begin{isabelle}%
+\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
+\end{isabelle}%
+
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
-should have written is%
+should have written is
+%
+\begin{isabelle}%
+\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
+\end{isabelle}%
+
+\end{warn}%
\end{isamarkuptext}%
-\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-%
-\begin{isabellebody}%
-%
-\begin{isamarkuptext}%
-Using the simplifier effectively may take a bit of experimentation. Set the
-\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
-on:%
-\end{isamarkuptext}%
-\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
-\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
-\begin{isamarkuptxt}%
-\noindent
-produces the trace
-
-\begin{ttbox}
-Applying instance of rewrite rule:
-rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
-Rewriting:
-rev [x] == rev [] @ [x]
-Applying instance of rewrite rule:
-rev [] == []
-Rewriting:
-rev [] == []
-Applying instance of rewrite rule:
-[] @ ?y == ?y
-Rewriting:
-[] @ [x] == [x]
-Applying instance of rewrite rule:
-?x3 \# ?t3 = ?t3 == False
-Rewriting:
-[x] = [] == False
-\end{ttbox}
-
-In more complicated cases, the trace can be quite lenghty, especially since
-invocations of the simplifier are often nested (e.g.\ when solving conditions
-of rewrite rules). Thus it is advisable to reset it:%
-\end{isamarkuptxt}%
-\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Misc/let_rewr.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*<*)
-theory let_rewr = Main:;
-(*>*)
-
-subsubsection{*Simplifying let-expressions*}
-
-text{*\index{simplification!of let-expressions}
-Proving a goal containing \isaindex{let}-expressions almost invariably
-requires the @{text"let"}-con\-structs to be expanded at some point. Since
-@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
-(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
-@{thm[source]Let_def}:
-*}
-
-lemma "(let xs = [] in xs@ys@xs) = ys";
-by(simp add: Let_def);
-
-text{*
-If, in a particular context, there is no danger of a combinatorial explosion
-of nested @{text"let"}s one could even add @{thm[source]Let_def} permanently:
-*}
-lemmas [simp] = Let_def;
-(*<*)
-end
-(*>*)
--- a/doc-src/TutorialI/Misc/prime_def.thy Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Tue Sep 05 13:53:39 2000 +0200
@@ -2,17 +2,18 @@
theory prime_def = Main:;
consts prime :: "nat \\<Rightarrow> bool"
(*>*)
-(*<*)term(*>*)
-
- "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
-text{*\noindent\small
+text{*
+\begin{warn}
+A common mistake when writing definitions is to introduce extra free
+variables on the right-hand side as in the following fictitious definition:
+@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
where @{text"dvd"} means ``divides''.
Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
right-hand side, which would introduce an inconsistency (why?). What you
should have written is
+@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
+\end{warn}
*}
-(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/trace_simp.thy Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*<*)
-theory trace_simp = Main:;
-(*>*)
-
-text{*
-Using the simplifier effectively may take a bit of experimentation. Set the
-\isaindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
-on:
-*}
-ML "set trace_simp";
-lemma "rev [a] = []";
-apply(simp);
-
-txt{*\noindent
-produces the trace
-
-\begin{ttbox}
-Applying instance of rewrite rule:
-rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
-Rewriting:
-rev [x] == rev [] @ [x]
-Applying instance of rewrite rule:
-rev [] == []
-Rewriting:
-rev [] == []
-Applying instance of rewrite rule:
-[] @ ?y == ?y
-Rewriting:
-[] @ [x] == [x]
-Applying instance of rewrite rule:
-?x3 \# ?t3 = ?t3 == False
-Rewriting:
-[x] = [] == False
-\end{ttbox}
-
-In more complicated cases, the trace can be quite lenghty, especially since
-invocations of the simplifier are often nested (e.g.\ when solving conditions
-of rewrite rules). Thus it is advisable to reset it:
-*}
-
-ML "reset trace_simp";
-
-(*<*)
-oops;
-end
-(*>*)
--- a/doc-src/TutorialI/fp.tex Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Tue Sep 05 13:53:39 2000 +0200
@@ -370,11 +370,7 @@
Section~\S\ref{sec:Simplification} explains how definitions are used
in proofs.
-\begin{warn}%
-A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side as in the following fictitious definition:
-\input{Misc/document/prime_def.tex}%
-\end{warn}
+\input{Misc/document/prime_def.tex}
\chapter{More Functional Programming}
@@ -425,181 +421,17 @@
to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
because the terms do not necessarily become simpler in the process.
-\subsubsection{Simplification rules}
-\indexbold{simplification rules}
-
-To facilitate simplification, theorems can be declared to be simplification
-rules (with the help of the attribute \isa{[simp]}\index{*simp
- (attribute)}), in which case proofs by simplification make use of these
-rules automatically. In addition the constructs \isacommand{datatype} and
-\isacommand{primrec} (and a few others) invisibly declare useful
-simplification rules. Explicit definitions are \emph{not} declared
-simplification rules automatically!
-
-Not merely equations but pretty much any theorem can become a simplification
-rule. The simplifier will try to make sense of it. For example, a theorem
-\isasymnot$P$ is automatically turned into \isa{$P$ = False}. The details
-are explained in \S\ref{sec:SimpHow}.
-
-The simplification attribute of theorems can be turned on and off as follows:
-\begin{ttbox}
-lemmas [simp] = \(list of theorem names\);
-lemmas [simp del] = \(list of theorem names\);
-\end{ttbox}
-As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) =
- xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification
-rules. Those of a more specific nature (e.g.\ distributivity laws, which
-alter the structure of terms considerably) should only be used selectively,
-i.e.\ they should not be default simplification rules. Conversely, it may
-also happen that a simplification rule needs to be disabled in certain
-proofs. Frequent changes in the simplification status of a theorem may
-indicate a badly designed theory.
-\begin{warn}
- Simplification may not terminate, for example if both $f(x) = g(x)$ and
- $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
- to include simplification rules that can lead to nontermination, either on
- their own or in combination with other simplification rules.
-\end{warn}
-
-\subsubsection{The simplification method}
-\index{*simp (method)|bold}
-
-The general format of the simplification method is
-\begin{ttbox}
-simp \(list of modifiers\)
-\end{ttbox}
-where the list of \emph{modifiers} helps to fine tune the behaviour and may
-be empty. Most if not all of the proofs seen so far could have been performed
-with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
-only the first subgoal and may thus need to be repeated---use \isaindex{simp_all}
-to simplify all subgoals.
-Note that \isa{simp} fails if nothing changes.
-
-\subsubsection{Adding and deleting simplification rules}
-
-If a certain theorem is merely needed in a few proofs by simplification,
-we do not need to make it a global simplification rule. Instead we can modify
-the set of simplification rules used in a simplification step by adding rules
-to it and/or deleting rules from it. The two modifiers for this are
-\begin{ttbox}
-add: \(list of theorem names\)
-del: \(list of theorem names\)
-\end{ttbox}
-In case you want to use only a specific list of theorems and ignore all
-others:
-\begin{ttbox}
-only: \(list of theorem names\)
-\end{ttbox}
-
-
-\subsubsection{Assumptions}
-\index{simplification!with/of assumptions}
-
-{\makeatother\input{Misc/document/asm_simp.tex}}
-
-\subsubsection{Rewriting with definitions}
-\index{simplification!with definitions}
-
-\input{Misc/document/def_rewr.tex}
-
-\begin{warn}
- If you have defined $f\,x\,y~\isasymequiv~t$ then you can only expand
- occurrences of $f$ with at least two arguments. Thus it is safer to define
- $f$~\isasymequiv~\isasymlambda$x\,y.\;t$.
-\end{warn}
-
-\input{Misc/document/let_rewr.tex}
-
-\subsubsection{Conditional equations}
-
-\input{Misc/document/cond_rewr.tex}
-
-
-\subsubsection{Automatic case splits}
-\indexbold{case splits}
-\index{*split|(}
-
-{\makeatother\input{Misc/document/case_splits.tex}}
-\index{*split|)}
-
-\begin{warn}
- The simplifier merely simplifies the condition of an \isa{if} but not the
- \isa{then} or \isa{else} parts. The latter are simplified only after the
- condition reduces to \isa{True} or \isa{False}, or after splitting. The
- same is true for \isaindex{case}-expressions: only the selector is
- simplified at first, until either the expression reduces to one of the
- cases or it is split.
-\end{warn}
-
-\subsubsection{Arithmetic}
-\index{arithmetic}
-
-The simplifier routinely solves a small class of linear arithmetic formulae
-(over type \isa{nat} and other numeric types): it only takes into account
-assumptions and conclusions that are (possibly negated) (in)equalities
-(\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus
-
-\input{Misc/document/arith1.tex}%
-is proved by simplification, whereas the only slightly more complex
-
-\input{Misc/document/arith4.tex}%
-is not proved by simplification and requires \isa{arith}.
-
-\subsubsection{Tracing}
-\indexbold{tracing the simplifier}
-
-{\makeatother\input{Misc/document/trace_simp.tex}}
+\input{Misc/document/simp.tex}
\index{simplification|)}
-\section{Induction heuristics}
-\label{sec:InductionHeuristics}
-
-The purpose of this section is to illustrate some simple heuristics for
-inductive proofs. The first one we have already mentioned in our initial
-example:
-\begin{quote}
-\emph{Theorems about recursive functions are proved by induction.}
-\end{quote}
-In case the function has more than one argument
-\begin{quote}
-\emph{Do induction on argument number $i$ if the function is defined by
-recursion in argument number $i$.}
-\end{quote}
-When we look at the proof of {\makeatother\isa{(xs @ ys) @ zs = xs @ (ys @
- zs)}} in \S\ref{sec:intro-proof} we find (a) \isa{\at} is recursive in
-the first argument, (b) \isa{xs} occurs only as the first argument of
-\isa{\at}, and (c) both \isa{ys} and \isa{zs} occur at least once as
-the second argument of \isa{\at}. Hence it is natural to perform induction
-on \isa{xs}.
-
-The key heuristic, and the main point of this section, is to
-generalize the goal before induction. The reason is simple: if the goal is
-too specific, the induction hypothesis is too weak to allow the induction
-step to go through. Let us now illustrate the idea with an example.
-
-{\makeatother\input{Misc/document/Itrev.tex}}
-
-A final point worth mentioning is the orientation of the equation we just
-proved: the more complex notion (\isa{itrev}) is on the left-hand
-side, the simpler \isa{rev} on the right-hand side. This constitutes
-another, albeit weak heuristic that is not restricted to induction:
-\begin{quote}
- \emph{The right-hand side of an equation should (in some sense) be simpler
- than the left-hand side.}
-\end{quote}
-This heuristic is tricky to apply because it is not obvious that
-\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
-happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
+\input{Misc/document/Itrev.tex}
\begin{exercise}
\input{Misc/document/Tree2.tex}%
\end{exercise}
-\section{Case study: compiling expressions}
-\label{sec:ExprCompiler}
-
-{\makeatother\input{CodeGen/document/CodeGen.tex}}
+\input{CodeGen/document/CodeGen.tex}
\section{Advanced datatypes}