# HG changeset patch # User nipkow # Date 976105378 -3600 # Node ID 620647438780e2ca3cd256f1c47192057158a12a # Parent 352f6f209775b3b2fccba42568459f2ef3226541 *** empty log message *** diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Inductive/AB.thy --- 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 \ int"}, @{typ int} are the integers, -@{term abs} is the absolute value function, and @{term"#1::int"} is the +@{text"\.\"} 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: "\i < size w. - abs((int(size[x\take (i+1) w. P x]) - - int(size[x\take (i+1) w. \P x])) - - - (int(size[x\take i w. P x]) - - int(size[x\take i w. \P x]))) \ #1"; + \(int(size[x\take (i+1) w. P x])-int(size[x\take (i+1) w. \P x])) + - (int(size[x\take i w. P x])-int(size[x\take i w. \P x]))\ \ #1" txt{*\noindent The lemma is a bit hard to read because of the coercion function -@{term[source]"int::nat \ int"}. It is required because @{term size} returns +@{term[source]"int :: nat \ 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 @@ \i\size w. size[x\take i w. P x] = size[x\take i w. \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: diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Inductive/document/AB.tex --- 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:% diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Misc/document/natsum.tex --- 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 diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Misc/natsum.thy --- 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 diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Types/Pairs.thy --- 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, diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Types/document/Pairs.tex --- 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}% diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/Types/numerics.tex --- 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. diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/fp.tex --- 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} diff -r 352f6f209775 -r 620647438780 doc-src/TutorialI/todo.tobias --- 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.