# HG changeset patch # User nipkow # Date 967554790 -7200 # Node ID 7e51c9f3d5a04344ec4724097355d1fb72b07784 # Parent 3b7b72db57f11234a7f77b5af9e590346540c4ee *** empty log message *** diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 TFL/tfl.sml --- 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) = diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/Tutorial/fp.tex --- 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. diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Datatype/document/ABexpr.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Datatype/document/Fundata.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Datatype/document/Nested.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Datatype/document/unfoldnested.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/IsaMakefile --- 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 diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/ROOT.ML --- 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"; diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/case_splits.thy --- 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 (*>*) diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/cases.thy --- 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 [] \\ [] | y#ys \\ 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 (*>*) diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/Itrev.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/Tree.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/Tree2.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/arith1.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/arith2.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/arith3.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/arith4.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/asm_simp.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/case_splits.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/cases.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/cond_rewr.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/def_rewr.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/fakenat.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/let_rewr.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/natsum.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/pairs.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/prime_def.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/trace_simp.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Misc/document/types.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/Nested2.thy --- 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 diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/Induction.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/Nested0.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/Nested1.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/Nested2.tex --- 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 @@ -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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/examples.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/simplification.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Recdef/document/termination.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/ToyList/document/ToyList.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Trie/document/Option2.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/Trie/document/Trie.tex --- 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" diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 doc-src/TutorialI/fp.tex --- 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}. diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 src/Provers/classical.ML --- 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 => diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 src/Pure/library.ML --- 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) diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 src/Pure/term.ML --- 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 diff -r 3b7b72db57f1 -r 7e51c9f3d5a0 src/Pure/thm.ML --- 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;