author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10607 352f6f209775 child 10609 5cbb6e62c502
*** empty log message ***
 doc-src/TutorialI/Inductive/AB.thy file | annotate | diff | revisions doc-src/TutorialI/Inductive/document/AB.tex file | annotate | diff | revisions doc-src/TutorialI/Misc/document/natsum.tex file | annotate | diff | revisions doc-src/TutorialI/Misc/natsum.thy file | annotate | diff | revisions doc-src/TutorialI/Types/Pairs.thy file | annotate | diff | revisions doc-src/TutorialI/Types/document/Pairs.tex file | annotate | diff | revisions doc-src/TutorialI/Types/numerics.tex file | annotate | diff | revisions doc-src/TutorialI/fp.tex file | annotate | diff | revisions doc-src/TutorialI/todo.tobias file | annotate | diff | revisions
     1.1 --- a/doc-src/TutorialI/Inductive/AB.thy	Wed Dec 06 12:34:40 2000 +0100
1.2 +++ b/doc-src/TutorialI/Inductive/AB.thy	Wed Dec 06 13:22:58 2000 +0100
1.3 @@ -104,7 +104,7 @@
1.4  intermediate value theorem @{thm[source]nat0_intermed_int_val}
1.5  @{thm[display]nat0_intermed_int_val[no_vars]}
1.6  where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
1.7 -@{term abs} is the absolute value function, and @{term"#1::int"} is the
1.8 +@{text"\<bar>.\<bar>"} is the absolute value function, and @{term"#1::int"} is the
1.9  integer 1 (see \S\ref{sec:numbers}).
1.10
1.11  First we show that the our specific function, the difference between the
1.12 @@ -116,15 +116,12 @@
1.13  *}
1.14
1.15  lemma step1: "\<forall>i < size w.
1.16 -  abs((int(size[x\<in>take (i+1) w.  P x]) -
1.17 -       int(size[x\<in>take (i+1) w. \<not>P x]))
1.18 -      -
1.19 -      (int(size[x\<in>take i w.  P x]) -
1.20 -       int(size[x\<in>take i w. \<not>P x]))) \<le> #1";
1.21 +  \<bar>(int(size[x\<in>take (i+1) w. P x])-int(size[x\<in>take (i+1) w. \<not>P x]))
1.22 +   - (int(size[x\<in>take i w. P x])-int(size[x\<in>take i w. \<not>P x]))\<bar> \<le> #1"
1.23
1.24  txt{*\noindent
1.25  The lemma is a bit hard to read because of the coercion function
1.26 -@{term[source]"int::nat \<Rightarrow> int"}. It is required because @{term size} returns
1.27 +@{term[source]"int :: nat \<Rightarrow> int"}. It is required because @{term size} returns
1.28  a natural number, but @{text-} on @{typ nat} will do the wrong thing.
1.29  Function @{term take} is predefined and @{term"take i xs"} is the prefix of
1.30  length @{term i} of @{term xs}; below we als need @{term"drop i xs"}, which
1.31 @@ -149,17 +146,15 @@
1.32    \<exists>i\<le>size w. size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1";
1.33
1.34  txt{*\noindent
1.35 -This is proved with the help of the intermediate value theorem, instantiated
1.36 -appropriately and with its first premise disposed of by lemma
1.37 -@{thm[source]step1}.
1.38 +This is proved by force with the help of the intermediate value theorem,
1.39 +instantiated appropriately and with its first premise disposed of by lemma
1.40 +@{thm[source]step1}:
1.41  *}
1.42
1.43  apply(insert nat0_intermed_int_val[OF step1, of "P" "w" "#1"]);
1.44 -apply simp;
1.45 -by(simp del:int_Suc add:zdiff_eq_eq sym[OF int_Suc]);
1.46 +by force;
1.47
1.48  text{*\noindent
1.49 -The additional lemmas are needed to mediate between @{typ nat} and @{typ int}.
1.50
1.51  Lemma @{thm[source]part1} tells us only about the prefix @{term"take i w"}.
1.52  The suffix @{term"drop i w"} is dealt with in the following easy lemma:

     2.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Dec 06 12:34:40 2000 +0100
2.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Dec 06 13:22:58 2000 +0100
2.3 @@ -100,7 +100,7 @@
2.4  \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
2.5  \end{isabelle}
2.6  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
2.7 -\isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
2.8 +\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
2.9  integer 1 (see \S\ref{sec:numbers}).
2.10
2.11  First we show that the our specific function, the difference between the
2.12 @@ -111,15 +111,12 @@
2.13  roles of \isa{a}'s and \isa{b}'s interchanged.%
2.14  \end{isamarkuptext}%
2.15  \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
2.16 -\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
2.17 -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
2.18 -\ \ \ \ \ \ {\isacharminus}\isanewline
2.19 -\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
2.20 -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
2.21 +\ \ {\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
2.22 +\ \ \ {\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}%
2.23  \begin{isamarkuptxt}%
2.24  \noindent
2.25  The lemma is a bit hard to read because of the coercion function
2.26 -\isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
2.27 +\isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
2.28  a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
2.29  Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
2.30  length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
2.31 @@ -141,16 +138,14 @@
2.32  \ \ {\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}%
2.33  \begin{isamarkuptxt}%
2.34  \noindent
2.35 -This is proved with the help of the intermediate value theorem, instantiated
2.36 -appropriately and with its first premise disposed of by lemma
2.38 +This is proved by force with the help of the intermediate value theorem,
2.39 +instantiated appropriately and with its first premise disposed of by lemma
2.41  \end{isamarkuptxt}%
2.43 -\isacommand{apply}\ simp\isanewline
2.44 -\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
2.45 +\isacommand{by}\ force%
2.46  \begin{isamarkuptext}%
2.47  \noindent
2.48 -The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
2.49
2.50  Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
2.51  The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%

     3.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Dec 06 12:34:40 2000 +0100
3.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Dec 06 13:22:58 2000 +0100
3.3 @@ -34,7 +34,7 @@
3.4  Isabelle does not prove this completely automatically. Note that \isa{{\isadigit{1}}}
3.5  and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
3.6  \isa{Suc}-expressions. If you need the full set of numerals,
3.7 -see~\S\ref{nat-numerals}.
3.8 +see~\S\ref{sec:numerals}.
3.9
3.10  \begin{warn}
3.11    The constant \ttindexbold{0} and the operations

     4.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Wed Dec 06 12:34:40 2000 +0100
4.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Dec 06 13:22:58 2000 +0100
4.3 @@ -32,7 +32,7 @@
4.4  Isabelle does not prove this completely automatically. Note that @{term 1}
4.5  and @{term 2} are available as abbreviations for the corresponding
4.6  @{term Suc}-expressions. If you need the full set of numerals,
4.7 -see~\S\ref{nat-numerals}.
4.8 +see~\S\ref{sec:numerals}.
4.9
4.10  \begin{warn}
4.11    The constant \ttindexbold{0} and the operations

     5.1 --- a/doc-src/TutorialI/Types/Pairs.thy	Wed Dec 06 12:34:40 2000 +0100
5.2 +++ b/doc-src/TutorialI/Types/Pairs.thy	Wed Dec 06 13:22:58 2000 +0100
5.3 @@ -11,7 +11,7 @@
5.4  problem: pattern matching with tuples.
5.5  *}
5.6
5.7 -subsection{*Notation*}
5.8 +subsection{*Pattern matching with tuples*}
5.9
5.10  text{*
5.11  It is possible to use (nested) tuples as patterns in $\lambda$-abstractions,

     6.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex	Wed Dec 06 12:34:40 2000 +0100
6.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex	Wed Dec 06 13:22:58 2000 +0100
6.3 @@ -15,7 +15,7 @@
6.4  problem: pattern matching with tuples.%
6.5  \end{isamarkuptext}%
6.6  %
6.7 -\isamarkupsubsection{Notation%
6.8 +\isamarkupsubsection{Pattern matching with tuples%
6.9  }
6.10  %
6.11  \begin{isamarkuptext}%

     7.1 --- a/doc-src/TutorialI/Types/numerics.tex	Wed Dec 06 12:34:40 2000 +0100
7.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Wed Dec 06 13:22:58 2000 +0100
7.3 @@ -35,6 +35,7 @@
7.4  useful lemmas are shown below.
7.5
7.6  \subsection{Numeric Literals}
7.7 +\label{sec:numerals}
7.8
7.9  Literals are available for the types of natural numbers, integers
7.10  and reals and denote integer values of arbitrary size.

     8.1 --- a/doc-src/TutorialI/fp.tex	Wed Dec 06 12:34:40 2000 +0100
8.2 +++ b/doc-src/TutorialI/fp.tex	Wed Dec 06 13:22:58 2000 +0100
8.3 @@ -244,7 +244,7 @@
8.4  \subsection{Pairs}
8.5  \input{Misc/document/pairs.tex}
8.6
8.7 -\subsection{Datatype \emph{\texttt{option}}}
8.8 +\subsection{Datatype {\tt\slshape option}}
8.9  \label{sec:option}
8.10  \input{Misc/document/Option2.tex}
8.11

     9.1 --- a/doc-src/TutorialI/todo.tobias	Wed Dec 06 12:34:40 2000 +0100
9.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Dec 06 13:22:58 2000 +0100
9.3 @@ -1,14 +1,10 @@
9.4  Implementation
9.5  ==============
9.6
9.7 -Why is comp needed in addition to op O?
9.8 -Explain in syntax section!
9.9 +Relation: comp -> composition
9.10
9.11  replace "simp only split" by "split_tac".
9.12
9.13 -arithmetic: allow mixed nat/int formulae
9.14 --> simplify proof of part1 in Inductive/AB.thy
9.15 -
9.16  Add map_cong?? (upto 10% slower)
9.17
9.18  Recdef: Get rid of function name in header.
9.19 @@ -30,6 +26,9 @@
9.20  Induction rules for int: int_le/ge_induct?
9.21  Needed for ifak example. But is that example worth it?
9.22
9.23 +Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
9.24 +ein generelles Feature ist, das man vielleicht mal abstellen sollte.
9.25 +
9.26  proper mutual simplification
9.27
9.28  defs with = and pattern matching??
9.29 @@ -62,8 +61,6 @@
9.30
9.31  Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
9.32
9.33 -mention split_split in advanced pair section.
9.34 -
9.35  recdef with nested recursion: either an example or at least a pointer to the
9.36  literature. In Recdef/termination.thy, at the end.
9.37  %FIXME, with one exception: nested recursion.