--- a/TFL/tfl.sml Tue Aug 29 12:28:48 2000 +0200
+++ b/TFL/tfl.sml Tue Aug 29 15:13:10 2000 +0200
@@ -47,9 +47,8 @@
fun add_cong(congs,thm) =
let val c = cong_hd thm
- in case assoc(congs,c) of None => (c,thm)::congs
- | _ => (warning ("Overwriting congruence rule for " ^ quote c);
- overwrite (congs, (c,thm)))
+ in overwrite_warn (congs,(c,thm))
+ ("Overwriting congruence rule for " ^ quote c)
end
fun del_cong(congs,thm) =
--- a/doc-src/Tutorial/fp.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/Tutorial/fp.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1029,7 +1029,7 @@
Nevertheless the simplifier can be instructed to perform \texttt{case}-splits
by adding the appropriate rule to the simpset:
\begin{ttbox}
-by(simp_tac (simpset() addsplits [split_list_case]) 1);
+by(simp_tac (simpset() addsplits [list.split]) 1);
\end{ttbox}\indexbold{*addsplits}
solves the initial goal outright, which \texttt{Simp_tac} alone will not do.
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
@@ -112,7 +111,7 @@
However, this is unnecessary because the generalized version fully subsumes
its instance.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Sometimes it is necessary to define two datatypes that depend on each
@@ -112,7 +111,7 @@
it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
\end{exercise}%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent Parameter \isa{'a} is the type of values stored in
@@ -50,7 +49,7 @@
~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
\end{isabellepar}%%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
So far, all datatypes had the property that on the right-hand side of their
@@ -122,7 +121,7 @@
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
expressions as its argument: \isa{Sum "'a aexp list"}.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,7 +1,6 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
-\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}%
+\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\subsubsection{How can we model boolean expressions?}
@@ -132,7 +131,7 @@
and prove \isa{normal(norm b)}. Of course, this requires a lemma about
normality of \isa{normif}:%
\end{isamarkuptext}%
-\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/IsaMakefile Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Tue Aug 29 15:13:10 2000 +0200
@@ -98,7 +98,8 @@
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy Misc/cases.thy \
- Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.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
--- a/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 29 15:13:10 2000 +0200
@@ -1,6 +1,7 @@
use_thy "Tree";
use_thy "Tree2";
use_thy "cases";
+use_thy "case_exprs";
use_thy "fakenat";
use_thy "natsum";
use_thy "arith1";
--- a/doc-src/TutorialI/Misc/case_splits.thy Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_splits.thy Tue Aug 29 15:13:10 2000 +0200
@@ -81,6 +81,27 @@
*}
lemmas [split del] = list.split;
+text{*
+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\_if\_asm} or $t$\isa{.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 \isa{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$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.
+*}
+
(*<*)
+by(simp_all)
end
(*>*)
--- a/doc-src/TutorialI/Misc/cases.thy Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/cases.thy Tue Aug 29 15:13:10 2000 +0200
@@ -2,6 +2,19 @@
theory "cases" = Main:;
(*>*)
+subsection{*Structural induction and case distinction*}
+
+text{*
+\indexbold{structural induction}
+\indexbold{induction!structural}
+\indexbold{case distinction}
+Almost all the basic laws about a datatype are applied automatically during
+simplification. Only induction is invoked by hand via \isaindex{induct_tac},
+which works for any datatype. In some cases, induction is overkill and a case
+distinction over all constructors of the datatype suffices. This is performed
+by \isaindexbold{case_tac}. A trivial example:
+*}
+
lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
apply(case_tac xs);
@@ -14,8 +27,13 @@
which is solved automatically:
*}
-by(auto);
-(**)
+by(auto)
+
+text{*
+Note that we do not need to give a lemma a name if we do not intend to refer
+to it explicitly in the future.
+*}
+
(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
@@ -272,7 +271,7 @@
For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}.
For details see the library.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Function \isa{rev} has quadratic worst-case running time
@@ -89,7 +88,7 @@
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}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
@@ -17,7 +16,7 @@
Define a function \isa{flatten} that flattens a tree into a list
by traversing it in infix order. Prove%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent In Exercise~\ref{ex:Tree} we defined a function
@@ -12,7 +11,7 @@
\begin{isamarkuptext}%
\noindent Define \isa{flatten2} and prove%
\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/arith1.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith1.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,7 +1,6 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/arith2.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,8 +1,7 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/arith3.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith3.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,7 +1,6 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/arith4.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith4.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,7 +1,6 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
By default, assumptions are part of the simplification process: they are used
@@ -45,7 +44,7 @@
Note that only one of the above options is allowed, and it must precede all
other arguments.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Goals containing \isaindex{if}-expressions are usually proved by case
@@ -64,8 +63,26 @@
\noindent
or globally:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split\isanewline
-\end{isabellebody}%
+\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\_if\_asm} or $t$\isa{.split_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\_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{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.%
+\end{isamarkuptxt}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,6 +1,17 @@
+\begin{isabelle}%
%
-\begin{isabellebody}%
-\isanewline
+\isamarkupsubsection{Structural induction and case distinction}
+%
+\begin{isamarkuptext}%
+\indexbold{structural induction}
+\indexbold{induction!structural}
+\indexbold{case distinction}
+Almost all the basic laws about a datatype are applied automatically during
+simplification. Only induction is invoked by hand via \isaindex{induct_tac},
+which works for any datatype. In some cases, induction is overkill and a case
+distinction over all constructors of the datatype suffices. This is performed
+by \isaindexbold{case_tac}. A trivial example:%
+\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -12,8 +23,12 @@
\end{isabellepar}%
which is solved automatically:%
\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\end{isabellebody}%
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
+\begin{isamarkuptext}%
+Note that we do not need to give a lemma a name if we do not intend to refer
+to it explicitly in the future.%
+\end{isamarkuptext}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
So far all examples of rewrite rules were equations. The simplifier also
@@ -24,7 +23,7 @@
simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local
assumption of the subgoal.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
@@ -39,7 +38,7 @@
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}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,12 +1,11 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural
numbers is predefined and behaves like%
\end{isamarkuptext}%
-\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabellebody}%
+\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,12 +1,11 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\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_def} permanently:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}%
+\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/natsum.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
@@ -23,7 +22,7 @@
\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/pairs.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
@@ -21,7 +20,7 @@
\end{quote}
Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\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}%
@@ -9,7 +8,7 @@
right-hand side, which would introduce an inconsistency (why?). What you
should have written is%
\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}%
+\ {\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{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Using the simplifier effectively may take a bit of experimentation. Set the
@@ -37,7 +36,7 @@
of rewrite rules). Thus it is advisable to reset it:%
\end{isamarkuptxt}%
\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Misc/document/types.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
@@ -39,7 +38,7 @@
in which case the default name of each definition is \isa{$f$_def}, where
$f$ is the name of the defined constant.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/Nested2.thy Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Tue Aug 29 15:13:10 2000 +0200
@@ -34,10 +34,21 @@
both of which are solved by simplification:
*};
-by(simp_all del:map_compose add:sym[OF map_compose] rev_map);
+by(simp_all add:rev_map sym[OF map_compose]);
text{*\noindent
-If this surprises you, see Datatype/Nested2......
+If the proof of the induction step mystifies you, we recommend to go through
+the chain of simplification steps in detail, probably with the help of
+\isa{trace\_simp}.
+%\begin{quote}
+%{term[display]"trev(trev(App f ts))"}\\
+%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
+%{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
+%{term[display]"App f (map trev (map trev ts))"}\\
+%{term[display]"App f (map (trev o trev) ts)"}\\
+%{term[display]"App f (map (%x. x) ts)"}\\
+%{term[display]"App f ts"}
+%\end{quote}
The above definition of @{term"trev"} is superior to the one in \S\ref{sec:nested-datatype}
because it brings @{term"rev"} into play, about which already know a lot, in particular
@@ -48,19 +59,22 @@
because they determine the complexity of your proofs.}
\end{quote}
-Let us now return to the question of how \isacommand{recdef} can come up with sensible termination
-conditions in the presence of higher-order functions like @{term"map"}. For a start, if nothing
-were known about @{term"map"}, @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms,
-and thus \isacommand{recdef} would try to prove the unprovable
-@{term"size t < Suc (term_size ts)"}, without any assumption about \isa{t}.
-Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}:
+Let us now return to the question of how \isacommand{recdef} can come up with
+sensible termination conditions in the presence of higher-order functions
+like @{term"map"}. For a start, if nothing were known about @{term"map"},
+@{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
+\isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
+(term_size ts)"}, without any assumption about \isa{t}. Therefore
+\isacommand{recdef} has been supplied with the congruence theorem
+\isa{map\_cong}:
\begin{quote}
@{thm[display,margin=50]"map_cong"[no_vars]}
\end{quote}
-Its second premise expresses (indirectly) that the second argument of @{term"map"} is only applied
-to elements of its third argument. Congruence rules for other higher-order functions on lists would
-look very similar but have not been proved yet because they were never needed.
-If you get into a situation where you need to supply \isacommand{recdef} with new congruence
+Its second premise expresses (indirectly) that the second argument of
+@{term"map"} is only applied to elements of its third argument. Congruence
+rules for other higher-order functions on lists would look very similar but
+have not been proved yet because they were never needed. If you get into a
+situation where you need to supply \isacommand{recdef} with new congruence
rules, you can either append the line
\begin{ttbox}
congs <congruence rules>
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Assuming we have defined our function such that Isabelle could prove
@@ -63,7 +62,7 @@
empty list, the singleton list, and the list with at least two elements
(in which case you may assume it holds for the tail of that list).%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
In \S\ref{sec:nested-datatype} we defined the datatype of terms%
@@ -17,7 +16,7 @@
FIXME: declare trev now!%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
@@ -39,7 +38,7 @@
We will now prove the termination condition and continue with our definition.
Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
\noindent
@@ -32,10 +31,21 @@
\end{quote}
both of which are solved by simplification:%
\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}map{\isacharunderscore}compose\ add{\isacharcolon}sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ rev{\isacharunderscore}map{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-If this surprises you, see Datatype/Nested2......
+If the proof of the induction step mystifies you, we recommend to go through
+the chain of simplification steps in detail, probably with the help of
+\isa{trace\_simp}.
+%\begin{quote}
+%{term[display]"trev(trev(App f ts))"}\\
+%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
+%{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
+%{term[display]"App f (map trev (map trev ts))"}\\
+%{term[display]"App f (map (trev o trev) ts)"}\\
+%{term[display]"App f (map (%x. x) ts)"}\\
+%{term[display]"App f ts"}
+%\end{quote}
The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype}
because it brings \isa{rev} into play, about which already know a lot, in particular
@@ -46,12 +56,13 @@
because they determine the complexity of your proofs.}
\end{quote}
-Let us now return to the question of how \isacommand{recdef} can come up with sensible termination
-conditions in the presence of higher-order functions like \isa{map}. For a start, if nothing
-were known about \isa{map}, \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms,
-and thus \isacommand{recdef} would try to prove the unprovable
-\isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}.
-Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}:
+Let us now return to the question of how \isacommand{recdef} can come up with
+sensible termination conditions in the presence of higher-order functions
+like \isa{map}. For a start, if nothing were known about \isa{map},
+\isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, and thus
+\isacommand{recdef} would try to prove the unprovable \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}. Therefore
+\isacommand{recdef} has been supplied with the congruence theorem
+\isa{map\_cong}:
\begin{quote}
\begin{isabelle}%
@@ -60,10 +71,11 @@
\end{isabelle}%
\end{quote}
-Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied
-to elements of its third argument. Congruence rules for other higher-order functions on lists would
-look very similar but have not been proved yet because they were never needed.
-If you get into a situation where you need to supply \isacommand{recdef} with new congruence
+Its second premise expresses (indirectly) that the second argument of
+\isa{map} is only applied to elements of its third argument. Congruence
+rules for other higher-order functions on lists would look very similar but
+have not been proved yet because they were never needed. If you get into a
+situation where you need to supply \isacommand{recdef} with new congruence
rules, you can either append the line
\begin{ttbox}
congs <congruence rules>
@@ -78,7 +90,7 @@
declaring a congruence rule for the simplifier does not make it
available to \isacommand{recdef}, and vice versa. This is intentional.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Here is a simple example, the Fibonacci function:%
@@ -78,7 +77,7 @@
For non-recursive functions the termination measure degenerates to the empty
set \isa{\{\}}.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
Once we have succeeded in proving all termination conditions, the recursion
@@ -101,7 +100,7 @@
after which we can disable the original simplification rule:%
\end{isamarkuptext}%
\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
When a function is defined via \isacommand{recdef}, Isabelle tries to prove
@@ -87,7 +86,7 @@
For details see the manual~\cite{isabelle-HOL} and the examples in the
library.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
\begin{isamarkuptext}%
\noindent
@@ -325,7 +324,7 @@
we are finished with its development:%
\end{isamarkuptext}%
\isacommand{end}\isanewline
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Trie/document/Option2.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,7 +1,6 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
\isanewline
-\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
+\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 15:13:10 2000 +0200
@@ -1,5 +1,4 @@
-%
-\begin{isabellebody}%
+\begin{isabelle}%
%
\begin{isamarkuptext}%
To minimize running time, each node of a trie should contain an array that maps
@@ -123,7 +122,7 @@
solves the proof. Part~\ref{Isar} shows you how to write readable and stable
proofs.%
\end{isamarkuptext}%
-\end{isabellebody}%
+\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/fp.tex Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Tue Aug 29 15:13:10 2000 +0200
@@ -214,66 +214,7 @@
\input{Misc/document/Tree.tex}%
\end{exercise}
-\subsection{Case expressions}
-\label{sec:case-expressions}
-
-HOL also features \isaindexbold{case}-expressions for analyzing
-elements of a datatype. For example,
-% case xs of [] => 0 | y#ys => y
-\begin{isabellepar}%
-~~~case~xs~of~[]~{\isasymRightarrow}~0~|~y~\#~ys~{\isasymRightarrow}~y
-\end{isabellepar}%
-evaluates to \isa{0} if \isa{xs} is \isa{[]} and to \isa{y} if
-\isa{xs} is \isa{y\#ys}. (Since the result in both branches must be of
-the same type, it follows that \isa{y::nat} and hence
-\isa{xs::(nat)list}.)
-
-In general, if $e$ is a term of the datatype $t$ defined in
-\S\ref{sec:general-datatype} above, the corresponding
-\isa{case}-expression analyzing $e$ is
-\[
-\begin{array}{rrcl}
-\isa{case}~e~\isa{of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\
- \vdots \\
- \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m
-\end{array}
-\]
-
-\begin{warn}
-{\em All} constructors must be present, their order is fixed, and nested
-patterns are not supported. Violating these restrictions results in strange
-error messages.
-\end{warn}
-\noindent
-Nested patterns can be simulated by nested \isa{case}-expressions: instead
-of
-% case xs of [] => 0 | [x] => x | x#(y#zs) => y
-\begin{isabellepar}%
-~~~case~xs~of~[]~{\isasymRightarrow}~0~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
-\end{isabellepar}%
-write
-% term(latex xsymbols symbols)"case xs of [] => 0 | x#ys => (case ys of [] => x | y#zs => y)";
-\begin{isabellepar}%
-~~~case~xs~of~[]~{\isasymRightarrow}~0~|~x~\#~ys~{\isasymRightarrow}~(case~ys~of~[]~{\isasymRightarrow}~x~|~y~\#~zs~{\isasymRightarrow}~y)%
-\end{isabellepar}%
-Note that \isa{case}-expressions should be enclosed in parentheses to
-indicate their scope.
-
-\subsection{Structural induction and case distinction}
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:
-
-\input{Misc/document/cases.tex}%
-
-Note that we do not need to give a lemma a name if we do not intend to refer
-to it explicitly in the future.
+\input{Misc/document/case_exprs.tex}
\begin{warn}
Induction is only allowed on free (or \isasymAnd-bound) variables that
@@ -592,7 +533,6 @@
\index{*split|(}
{\makeatother\input{Misc/document/case_splits.tex}}
-
\index{*split|)}
\begin{warn}
@@ -620,10 +560,10 @@
\subsubsection{Permutative rewrite rules}
-A rewrite rule is {\bf permutative} if the left-hand side and right-hand side
-are the same up to renaming of variables. The most common permutative rule
-is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$. Such
-rules are problematic because once they apply, they can be used forever.
+A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
+side are the same up to renaming of variables. The most common permutative
+rule is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$.
+Such rules are problematic because once they apply, they can be used forever.
The simplifier is aware of this danger and treats permutative rules
separately. For details see~\cite{isabelle-ref}.
--- a/src/Provers/classical.ML Tue Aug 29 12:28:48 2000 +0200
+++ b/src/Provers/classical.ML Tue Aug 29 15:13:10 2000 +0200
@@ -683,15 +683,13 @@
(*Add/replace a safe wrapper*)
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers =>
- (case assoc_string (swrappers,(fst new_swrapper)) of None =>()
- | Some x => warning("overwriting safe wrapper "^fst new_swrapper);
- overwrite (swrappers, new_swrapper)));
+ overwrite_warn (swrappers, new_swrapper)
+ ("Overwriting safe wrapper " ^ fst new_swrapper));
(*Add/replace an unsafe wrapper*)
fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
- (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>()
- | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper);
- overwrite (uwrappers, new_uwrapper)));
+ overwrite_warn (uwrappers, new_uwrapper)
+ ("Overwriting unsafe wrapper "^fst new_uwrapper));
(*Remove a safe wrapper*)
fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
--- a/src/Pure/library.ML Tue Aug 29 12:28:48 2000 +0200
+++ b/src/Pure/library.ML Tue Aug 29 15:13:10 2000 +0200
@@ -188,6 +188,7 @@
val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
+ val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list
val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
(*generic tables*)
@@ -1204,6 +1205,10 @@
(** misc **)
+fun overwrite_warn (args as (alist,(a,_))) text =
+ (if is_none(assoc(alist,a)) then () else warning text;
+ overwrite args);
+
(*use the keyfun to make a list of (x, key) pairs*)
fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
let fun keypair x = (x, keyfun x)
--- a/src/Pure/term.ML Tue Aug 29 12:28:48 2000 +0200
+++ b/src/Pure/term.ML Tue Aug 29 15:13:10 2000 +0200
@@ -638,16 +638,14 @@
| subst_atomic (instl: (term*term) list) t =
let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
| subst (f$t') = subst f $ subst t'
- | subst t = (case assoc(instl,t) of
- Some u => u | None => t)
+ | subst t = if_none (assoc(instl,t)) t
in subst t end;
(*Substitute for type Vars in a type*)
fun typ_subst_TVars iTs T = if null iTs then T else
let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
| subst(T as TFree _) = T
- | subst(T as TVar(ixn,_)) =
- (case assoc(iTs,ixn) of None => T | Some(U) => U)
+ | subst(T as TVar(ixn,_)) = if_none (assoc(iTs,ixn)) T
in subst T end;
(*Substitute for type Vars in a term*)
@@ -655,8 +653,7 @@
(*Substitute for Vars in a term; see also envir/norm_term*)
fun subst_Vars itms t = if null itms then t else
- let fun subst(v as Var(ixn,_)) =
- (case assoc(itms,ixn) of None => v | Some t => t)
+ let fun subst(v as Var(ixn,_)) = if_none (assoc(itms,ixn)) v
| subst(Abs(a,T,t)) = Abs(a,T,subst t)
| subst(f$t) = subst f $ subst t
| subst(t) = t
--- a/src/Pure/thm.ML Tue Aug 29 12:28:48 2000 +0200
+++ b/src/Pure/thm.ML Tue Aug 29 15:13:10 2000 +0200
@@ -1363,8 +1363,7 @@
else Var((y,i),T)
| None=> t)
| rename(Abs(x,T,t)) =
- Abs(case assoc_string(al,x) of Some(y) => y | None => x,
- T, rename t)
+ Abs(if_none(assoc_string(al,x)) x, T, rename t)
| rename(f$t) = rename f $ rename t
| rename(t) = t;
fun strip_ren Ai = strip_apply rename (Ai,B)
@@ -1835,10 +1834,11 @@
val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
raise SIMPLIFIER ("Congruence must start with a constant", thm);
val (alist,weak) = congs
+ val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
+ ("Overwriting congruence rule for " ^ quote a);
val weak2 = if is_full_cong thm then weak else a::weak
in
- mk_mss (rules, ((a, {lhs = lhs, thm = thm}) :: alist, weak2),
- procs, bounds, prems, mk_rews, termless)
+ mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
end;
val (op add_congs) = foldl add_cong;
@@ -1969,7 +1969,7 @@
fun ren_inst(insts,prop,pat,obj) =
let val ren = match_bvs(pat,obj,[])
fun renAbs(Abs(x,T,b)) =
- Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b))
+ Abs(if_none(assoc_string(ren,x)) x, T, renAbs(b))
| renAbs(f$t) = renAbs(f) $ renAbs(t)
| renAbs(t) = t
in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;