*** empty log message ***
authornipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608620647438780
parent 10607 352f6f209775
child 10609 5cbb6e62c502
*** empty log message ***
doc-src/TutorialI/Inductive/AB.thy
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Types/Pairs.thy
doc-src/TutorialI/Types/document/Pairs.tex
doc-src/TutorialI/Types/numerics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/todo.tobias
     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.37 -\isa{step{\isadigit{1}}}.%
    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.40 +\isa{step{\isadigit{1}}}:%
    2.41  \end{isamarkuptxt}%
    2.42  \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
    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.