--- a/doc-src/TutorialI/Inductive/AB.thy Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy Wed Dec 06 13:22:58 2000 +0100
@@ -104,7 +104,7 @@
intermediate value theorem @{thm[source]nat0_intermed_int_val}
@{thm[display]nat0_intermed_int_val[no_vars]}
where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
-@{term abs} is the absolute value function, and @{term"#1::int"} is the
+@{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
integer 1 (see \S\ref{sec:numbers}).
First we show that the our specific function, the difference between the
@@ -116,15 +116,12 @@
*}
lemma step1: "\<forall>i < size w.
- abs((int(size[x\<in>take (i+1) w. P x]) -
- int(size[x\<in>take (i+1) w. \<not>P x]))
- -
- (int(size[x\<in>take i w. P x]) -
- int(size[x\<in>take i w. \<not>P x]))) \<le> #1";
+ \<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
+ - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> #1"
txt{*\noindent
The lemma is a bit hard to read because of the coercion function
-@{term[source]"int::nat \<Rightarrow> int"}. It is required because @{term size} returns
+@{term[source]"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
a natural number, but @{text-} on @{typ nat} will do the wrong thing.
Function @{term take} is predefined and @{term"take i xs"} is the prefix of
length @{term i} of @{term xs}; below we als need @{term"drop i xs"}, which
@@ -149,17 +146,15 @@
\<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
txt{*\noindent
-This is proved with the help of the intermediate value theorem, instantiated
-appropriately and with its first premise disposed of by lemma
-@{thm[source]step1}.
+This is proved by force with the help of the intermediate value theorem,
+instantiated appropriately and with its first premise disposed of by lemma
+@{thm[source]step1}:
*}
apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
-apply simp;
-by(simp del:int_Suc add:zdiff_eq_eq sym[OF int_Suc]);
+by force;
text{*\noindent
-The additional lemmas are needed to mediate between @{typ nat} and @{typ int}.
Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}.
The suffix @{term"drop i w"} is dealt with in the following easy lemma:
--- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Dec 06 13:22:58 2000 +0100
@@ -100,7 +100,7 @@
\ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
\end{isabelle}
where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
-\isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
+\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
integer 1 (see \S\ref{sec:numbers}).
First we show that the our specific function, the difference between the
@@ -111,15 +111,12 @@
roles of \isa{a}'s and \isa{b}'s interchanged.%
\end{isamarkuptext}%
\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
-\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
-\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
-\ \ \ \ \ \ {\isacharminus}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
-\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
+\ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
+\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
The lemma is a bit hard to read because of the coercion function
-\isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
+\isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
@@ -141,16 +138,14 @@
\ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-This is proved with the help of the intermediate value theorem, instantiated
-appropriately and with its first premise disposed of by lemma
-\isa{step{\isadigit{1}}}.%
+This is proved by force with the help of the intermediate value theorem,
+instantiated appropriately and with its first premise disposed of by lemma
+\isa{step{\isadigit{1}}}:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
-\isacommand{apply}\ simp\isanewline
-\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
+\isacommand{by}\ force%
\begin{isamarkuptext}%
\noindent
-The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Dec 06 13:22:58 2000 +0100
@@ -34,7 +34,7 @@
Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
\isa{Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{nat-numerals}.
+see~\S\ref{sec:numerals}.
\begin{warn}
The constant \ttindexbold{0} and the operations
--- a/doc-src/TutorialI/Misc/natsum.thy Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Wed Dec 06 13:22:58 2000 +0100
@@ -32,7 +32,7 @@
Isabelle does not prove this completely automatically. Note that @{term 1}
and @{term 2} are available as abbreviations for the corresponding
@{term Suc}-expressions. If you need the full set of numerals,
-see~\S\ref{nat-numerals}.
+see~\S\ref{sec:numerals}.
\begin{warn}
The constant \ttindexbold{0} and the operations
--- a/doc-src/TutorialI/Types/Pairs.thy Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy Wed Dec 06 13:22:58 2000 +0100
@@ -11,7 +11,7 @@
problem: pattern matching with tuples.
*}
-subsection{*Notation*}
+subsection{*Pattern matching with tuples*}
text{*
It is possible to use (nested) tuples as patterns in $\lambda$-abstractions,
--- a/doc-src/TutorialI/Types/document/Pairs.tex Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Wed Dec 06 13:22:58 2000 +0100
@@ -15,7 +15,7 @@
problem: pattern matching with tuples.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Notation%
+\isamarkupsubsection{Pattern matching with tuples%
}
%
\begin{isamarkuptext}%
--- a/doc-src/TutorialI/Types/numerics.tex Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Dec 06 13:22:58 2000 +0100
@@ -35,6 +35,7 @@
useful lemmas are shown below.
\subsection{Numeric Literals}
+\label{sec:numerals}
Literals are available for the types of natural numbers, integers
and reals and denote integer values of arbitrary size.
--- a/doc-src/TutorialI/fp.tex Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/fp.tex Wed Dec 06 13:22:58 2000 +0100
@@ -244,7 +244,7 @@
\subsection{Pairs}
\input{Misc/document/pairs.tex}
-\subsection{Datatype \emph{\texttt{option}}}
+\subsection{Datatype {\tt\slshape option}}
\label{sec:option}
\input{Misc/document/Option2.tex}
--- a/doc-src/TutorialI/todo.tobias Wed Dec 06 12:34:40 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias Wed Dec 06 13:22:58 2000 +0100
@@ -1,14 +1,10 @@
Implementation
==============
-Why is comp needed in addition to op O?
-Explain in syntax section!
+Relation: comp -> composition
replace "simp only split" by "split_tac".
-arithmetic: allow mixed nat/int formulae
--> simplify proof of part1 in Inductive/AB.thy
-
Add map_cong?? (upto 10% slower)
Recdef: Get rid of function name in header.
@@ -30,6 +26,9 @@
Induction rules for int: int_le/ge_induct?
Needed for ifak example. But is that example worth it?
+Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
+ein generelles Feature ist, das man vielleicht mal abstellen sollte.
+
proper mutual simplification
defs with = and pattern matching??
@@ -62,8 +61,6 @@
Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
-mention split_split in advanced pair section.
-
recdef with nested recursion: either an example or at least a pointer to the
literature. In Recdef/termination.thy, at the end.
%FIXME, with one exception: nested recursion.