# HG changeset patch # User nipkow # Date 1008144260 -3600 # Node ID f41e477576b901b543f05d3a9f1baba6a0a74a85 # Parent 3307149f1ec246f1680fe2d02d4998a34ef09cb7 *** empty log message *** diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTL.thy Wed Dec 12 09:04:20 2001 +0100 @@ -460,7 +460,7 @@ our model checkers. It is clear that if all sets are finite, they can be represented as lists and the usual set operations are easily implemented. Only @{term lfp} requires a little thought. Fortunately, theory -@{text While_Combinator} in the Library~\cite{isabelle-HOL-lib} provides a +@{text While_Combinator} in the Library~\cite{HOL-Library} provides a theorem stating that in the case of finite sets and a monotone function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until a fixed point is diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Dec 12 09:04:20 2001 +0100 @@ -469,7 +469,7 @@ our model checkers. It is clear that if all sets are finite, they can be represented as lists and the usual set operations are easily implemented. Only \isa{lfp} requires a little thought. Fortunately, theory -\isa{While{\isacharunderscore}Combinator} in the Library~\cite{isabelle-HOL-lib} provides a +\isa{While{\isacharunderscore}Combinator} in the Library~\cite{HOL-Library} provides a theorem stating that in the case of finite sets and a monotone function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Dec 12 09:04:20 2001 +0100 @@ -232,7 +232,12 @@ occurrences of $f$ with at least two arguments. This may be helpful for unfolding $f$ selectively, but it may also get in the way. Defining $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$. -\end{warn}% +\end{warn} + +There is also the special method \isa{unfold}\index{*unfold (method)|bold} +which merely unfolds +one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}. +This is can be useful if \isa{simp} does too much.% \end{isamarkuptext}% \isamarkuptrue% % diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Misc/simp.thy --- a/doc-src/TutorialI/Misc/simp.thy Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Misc/simp.thy Wed Dec 12 09:04:20 2001 +0100 @@ -197,6 +197,11 @@ $f$ selectively, but it may also get in the way. Defining $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$. \end{warn} + +There is also the special method \isa{unfold}\index{*unfold (method)|bold} +which merely unfolds +one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}. +This is can be useful in situations where \isa{simp} does too much. *} subsection{*Simplifying {\tt\slshape let}-Expressions*} diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Dec 12 09:04:20 2001 +0100 @@ -23,7 +23,7 @@ According to the measure function, the second argument should decrease with each recursive call. The resulting termination condition \begin{isabelle}% -\ \ \ \ \ n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n% +\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n% \end{isabelle} is proved automatically because it is already present as a lemma in HOL\@. Thus the recursion equation becomes a simplification @@ -70,7 +70,7 @@ \begin{isamarkuptext}% \noindent The order of equations is important: it hides the side condition -\isa{n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. Unfortunately, in general the case distinction +\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction may not be expressible by pattern matching. A simple alternative is to replace \isa{if} by \isa{case}, diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Dec 12 09:04:20 2001 +0100 @@ -59,7 +59,7 @@ \begin{isamarkuptext}% \noindent This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely -the stated recursion equation for \isa{{\isacharquery}{\isacharquery}{\isachardot}f}, which has been stored as a +the stated recursion equation for \isa{f}, which has been turned into a simplification rule. Thus we can automatically prove results such as this one:% \end{isamarkuptext}% \isamarkuptrue% diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Recdef/simplification.thy --- a/doc-src/TutorialI/Recdef/simplification.thy Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Recdef/simplification.thy Wed Dec 12 09:04:20 2001 +0100 @@ -19,7 +19,7 @@ text{*\noindent According to the measure function, the second argument should decrease with each recursive call. The resulting termination condition -@{term[display]"n ~= 0 ==> m mod n < n"} +@{term[display]"n ~= (0::nat) ==> m mod n < n"} is proved automatically because it is already present as a lemma in HOL\@. Thus the recursion equation becomes a simplification rule. Of course the equation is nonterminating if we are allowed to unfold @@ -58,7 +58,7 @@ text{*\noindent The order of equations is important: it hides the side condition -@{prop"n ~= 0"}. Unfortunately, in general the case distinction +@{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction may not be expressible by pattern matching. A simple alternative is to replace @{text if} by @{text case}, diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Recdef/termination.thy --- a/doc-src/TutorialI/Recdef/termination.thy Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Recdef/termination.thy Wed Dec 12 09:04:20 2001 +0100 @@ -48,7 +48,7 @@ (*<*)local(*>*) text{*\noindent This time everything works fine. Now @{thm[source]f.simps} contains precisely -the stated recursion equation for @{term f}, which has been stored as a +the stated recursion equation for @{text f}, which has been turned into a simplification rule. Thus we can automatically prove results such as this one: *} diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Sets/sets.tex --- a/doc-src/TutorialI/Sets/sets.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Wed Dec 12 09:04:20 2001 +0100 @@ -965,7 +965,7 @@ the well-founded relation used to prove termination. The \bfindex{multiset ordering}, useful for hard termination proofs, is -available in the Library~\cite{isabelle-HOL-lib}. +available in the Library~\cite{HOL-Library}. Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it. \medskip diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Types/Typedefs.thy --- a/doc-src/TutorialI/Types/Typedefs.thy Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Types/Typedefs.thy Wed Dec 12 09:04:20 2001 +0100 @@ -69,13 +69,14 @@ It is easily represented by the first three natural numbers: *} -typedef three = "{n::nat. n \ 2}" +typedef three = "{0::nat, 1, 2}" txt{*\noindent In order to enforce that the representing set on the right-hand side is non-empty, this definition actually starts a proof to that effect: @{subgoals[display,indent=0]} -Fortunately, this is easy enough to show: take 0 as a witness. +Fortunately, this is easy enough to show, even \isa{auto} could do it. +In general, one has to provide a witness, in our case 0: *} apply(rule_tac x = 0 in exI) @@ -127,7 +128,7 @@ % From this example it should be clear what \isacommand{typedef} does in general given a name (here @{text three}) and a set -(here @{term"{n::nat. n\2}"}). +(here @{term"{0::nat,1,2}"}). Our next step is to define the basic functions expected on the new type. Although this depends on the type at hand, the following strategy works well: @@ -161,17 +162,30 @@ and that they exhaust the type. In processing our \isacommand{typedef} declaration, -Isabelle helpfully proves several lemmas. -One, @{thm[source]Abs_three_inject}, -expresses that @{term Abs_three} is injective on the representing subset: +Isabelle proves several helpful lemmas. The first two +express injectivity of @{term Rep_three} and @{term Abs_three}: \begin{center} -@{thm Abs_three_inject[no_vars]} +\begin{tabular}{@ {}r@ {\qquad}l@ {}} +@{thm Rep_three_inject[no_vars]} & (@{thm[source]Rep_three_inject}) \\ +\begin{tabular}{@ {}l@ {}} +@{text"\x \ three; y \ three \"} \\ +@{text"\ (Abs_three x = Abs_three y) = (x = y)"} +\end{tabular} & (@{thm[source]Abs_three_inject}) \\ +\end{tabular} \end{center} -Another, @{thm[source]Rep_three_inject}, expresses that the representation -function is also injective: +The following ones allow to replace some @{text"x::three"} by +@{text"Abs_three(y::nat)"}, and conversely @{term y} by @{term"Rep_three x"}: \begin{center} -@{thm Rep_three_inject[no_vars]} +\begin{tabular}{@ {}r@ {\qquad}l@ {}} +@{thm Rep_three_cases[no_vars]} & (@{thm[source]Rep_three_cases}) \\ +@{thm Abs_three_cases[no_vars]} & (@{thm[source]Abs_three_cases}) \\ +@{thm Rep_three_induct[no_vars]} & (@{thm[source]Rep_three_induct}) \\ +@{thm Abs_three_induct[no_vars]} & (@{thm[source]Abs_three_induct}) \\ +\end{tabular} \end{center} +These theorems are proved for any type definition, with @{term three} +replaced by the name of the type in question. + Distinctness of @{term A}, @{term B} and @{term C} follows immediately if we expand their definitions and rewrite with the injectivity of @{term Abs_three}: @@ -181,57 +195,26 @@ by(simp add: Abs_three_inject A_def B_def C_def three_def) text{*\noindent -Of course we rely on the simplifier to solve goals like @{prop"0 \ 1"}. +Of course we rely on the simplifier to solve goals like @{prop"(0::nat) \ 1"}. The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is best phrased as a case distinction theorem: if you want to prove @{prop"P x"} (where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"}, -@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the -representation: *} - -lemma cases_lemma: "\ Q 0; Q 1; Q 2; n \ three \ \ Q n" - -txt{*\noindent -Expanding @{thm[source]three_def} yields the premise @{prop"n\2"}. Repeated -elimination with @{thm[source]le_SucE} -@{thm[display]le_SucE} -reduces @{prop"n\2"} to the three cases @{prop"n\0"}, @{prop"n=1"} and -@{prop"n=2"} which are trivial for simplification: -*} - -apply(simp add: three_def numerals) (* FIXME !? *) -apply((erule le_SucE)+) -apply simp_all -done - -text{* -Now the case distinction lemma on type @{typ three} is easy to derive if you -know how: -*} +@{prop"P B"} and @{prop"P C"}: *} lemma three_cases: "\ P A; P B; P C \ \ P x" -txt{*\noindent -We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}: -*} - -apply(rule subst[OF Rep_three_inverse]) +txt{*\noindent Again this follows easily from a pre-proved general theorem:*} -txt{*\noindent -This substitution step worked nicely because there was just a single -occurrence of a term of type @{typ three}, namely @{term x}. -When we now apply @{thm[source]cases_lemma}, @{term Q} becomes @{term"\n. P(Abs_three -n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}: -*} - -apply(rule cases_lemma) +apply(rule_tac x = x in Abs_three_induct) txt{* @{subgoals[display,indent=0]} -The resulting subgoals are easily solved by simplification: -*} +Simplification with @{thm[source]three_def} leads to the disjunction @{prop"y += 0 \ y = 1 \ y = (2::nat)"} which \isa{auto} separates into three +subgoals, each of which is easily solved by simplification: *} -apply(simp_all add:A_def B_def C_def Rep_three) +apply(auto simp add: three_def A_def B_def C_def) done text{*\noindent @@ -253,7 +236,7 @@ example to demonstrate \isacommand{typedef} because its simplicity makes the key concepts particularly easy to grasp. If you would like to see a non-trivial example that cannot be defined more directly, we recommend the -definition of \emph{finite multisets} in the Library~\cite{isabelle-HOL-lib}. +definition of \emph{finite multisets} in the Library~\cite{HOL-Library}. Let us conclude by summarizing the above procedure for defining a new type. Given some abstract axiomatic description $P$ of a type $ty$ in terms of a diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Types/document/Typedefs.tex --- a/doc-src/TutorialI/Types/document/Typedefs.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/Types/document/Typedefs.tex Wed Dec 12 09:04:20 2001 +0100 @@ -86,16 +86,17 @@ It is easily represented by the first three natural numbers:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% +\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse% % \begin{isamarkuptxt}% \noindent In order to enforce that the representing set on the right-hand side is non-empty, this definition actually starts a proof to that effect: \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}% \end{isabelle} -Fortunately, this is easy enough to show: take 0 as a witness.% +Fortunately, this is easy enough to show, even \isa{auto} could do it. +In general, one has to provide a witness, in our case 0:% \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline @@ -117,7 +118,7 @@ \end{center} where constant \isa{three} is explicitly defined as the representing set: \begin{center} -\isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def}) +\isa{three\ {\isasymequiv}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def}) \end{center} The situation is best summarized with the help of the following diagram, where squares are types and circles are sets: @@ -147,7 +148,7 @@ % From this example it should be clear what \isacommand{typedef} does in general given a name (here \isa{three}) and a set -(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}). +(here \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}). Our next step is to define the basic functions expected on the new type. Although this depends on the type at hand, the following strategy works well: @@ -179,17 +180,30 @@ and that they exhaust the type. In processing our \isacommand{typedef} declaration, -Isabelle helpfully proves several lemmas. -One, \isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}, -expresses that \isa{Abs{\isacharunderscore}three} is injective on the representing subset: +Isabelle proves several helpful lemmas. The first two +express injectivity of \isa{Rep{\isacharunderscore}three} and \isa{Abs{\isacharunderscore}three}: \begin{center} -\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} +\begin{tabular}{@ {}r@ {\qquad}l@ {}} +\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}) \\ +\begin{tabular}{@ {}l@ {}} +\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}} \\ +\isa{{\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} +\end{tabular} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}) \\ +\end{tabular} \end{center} -Another, \isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}, expresses that the representation -function is also injective: +The following ones allow to replace some \isa{x{\isacharcolon}{\isacharcolon}three} by +\isa{Abs{\isacharunderscore}three{\isacharparenleft}y{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}, and conversely \isa{y} by \isa{Rep{\isacharunderscore}three\ x}: \begin{center} -\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} +\begin{tabular}{@ {}r@ {\qquad}l@ {}} +\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ y\ {\isacharequal}\ Rep{\isacharunderscore}three\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}cases}) \\ +\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}cases}) \\ +\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}induct}) \\ +\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}induct}) \\ +\end{tabular} \end{center} +These theorems are proved for any type definition, with \isa{three} +replaced by the name of the type in question. + Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately if we expand their definitions and rewrite with the injectivity of \isa{Abs{\isacharunderscore}three}:% @@ -201,70 +215,31 @@ % \begin{isamarkuptext}% \noindent -Of course we rely on the simplifier to solve goals like \isa{{\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}}. +Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}. The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is best phrased as a case distinction theorem: if you want to prove \isa{P\ x} (where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A}, -\isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the -representation:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}\isamarkupfalse% -% -\begin{isamarkuptxt}% -\noindent -Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated -elimination with \isa{le{\isacharunderscore}SucE} -\begin{isabelle}% -{\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R% -\end{isabelle} -reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and -\isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ numerals{\isacharparenright}\ \ \ \isanewline -\isamarkupfalse% -\isacommand{apply}{\isacharparenleft}{\isacharparenleft}erule\ le{\isacharunderscore}SucE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline -\isamarkupfalse% -\isacommand{apply}\ simp{\isacharunderscore}all\isanewline -\isamarkupfalse% -\isacommand{done}\isamarkupfalse% -% -\begin{isamarkuptext}% -Now the case distinction lemma on type \isa{three} is easy to derive if you -know how:% +\isa{P\ B} and \isa{P\ C}:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}\isamarkupfalse% % \begin{isamarkuptxt}% -\noindent -We start by replacing the \isa{x} by \isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}}:% +\noindent Again this follows easily from a pre-proved general theorem:% \end{isamarkuptxt}% \isamarkuptrue% -\isacommand{apply}{\isacharparenleft}rule\ subst{\isacharbrackleft}OF\ Rep{\isacharunderscore}three{\isacharunderscore}inverse{\isacharbrackright}{\isacharparenright}\isamarkupfalse% -% -\begin{isamarkuptxt}% -\noindent -This substitution step worked nicely because there was just a single -occurrence of a term of type \isa{three}, namely \isa{x}. -When we now apply \isa{cases{\isacharunderscore}lemma}, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:% -\end{isamarkuptxt}% -\isamarkuptrue% -\isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline -\ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline -\ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}% \end{isabelle} -The resulting subgoals are easily solved by simplification:% +Simplification with \isa{three{\isacharunderscore}def} leads to the disjunction \isa{y\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{2}}} which \isa{auto} separates into three +subgoals, each of which is easily solved by simplification:% \end{isamarkuptxt}% \isamarkuptrue% -\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ Rep{\isacharunderscore}three{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def{\isacharparenright}\isanewline \isamarkupfalse% \isacommand{done}\isamarkupfalse% % @@ -289,7 +264,7 @@ example to demonstrate \isacommand{typedef} because its simplicity makes the key concepts particularly easy to grasp. If you would like to see a non-trivial example that cannot be defined more directly, we recommend the -definition of \emph{finite multisets} in the Library~\cite{isabelle-HOL-lib}. +definition of \emph{finite multisets} in the Library~\cite{HOL-Library}. Let us conclude by summarizing the above procedure for defining a new type. Given some abstract axiomatic description $P$ of a type $ty$ in terms of a diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/basics.tex Wed Dec 12 09:04:20 2001 +0100 @@ -89,9 +89,9 @@ Unless you know what you are doing, always include \isa{Main} as a direct or indirect parent of all your theories. \end{warn} -There is also a growing Library~\cite{isabelle-library}\index{Library} +There is also a growing Library~\cite{HOL-Library}\index{Library} of useful theories that are not part of \isa{Main} but can to be included -among the parents of a theory and will then be included automatically.% +among the parents of a theory and will then be loaded automatically.% \index{theories|)} diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/fp.tex Wed Dec 12 09:04:20 2001 +0100 @@ -527,7 +527,6 @@ \subsection{Simplification and Recursive Functions} \label{sec:recdef-simplification} - \input{Recdef/document/simplification.tex} \subsection{Induction and Recursive Functions} diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/todo.tobias --- a/doc-src/TutorialI/todo.tobias Tue Dec 11 17:07:45 2001 +0100 +++ b/doc-src/TutorialI/todo.tobias Wed Dec 12 09:04:20 2001 +0100 @@ -36,9 +36,6 @@ use arith_tac in recdef to solve termination conditions? -> new example in Recdef/termination -a tactic for replacing a specific occurrence: -apply(subst [2] thm) - it would be nice if @term could deal with ?-vars. then a number of (unchecked!) @texts could be converted to @terms. @@ -60,49 +57,16 @@ Minor fixes in the tutorial =========================== -1/2 no longer abbrevs for Suc. -Warning: needs simplification to turn 1 into Suc 0. arith does so -automatically. - -recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes) -say something about how conditions are proved? -No, better show failed proof attempts. - -Advanced recdef: explain recdef_tc? No. Adjust recdef! - -Adjust FP textbook refs: new Bird, Hudak -Discrete math textbook: Rosen? - -adjust type of ^ in tab:overloading - -an example of induction: !y. A --> B --> C ?? - -Explain type_definition and mention pre-proved thms in subset.thy? --> Types/typedef - Appendix: Lexical: long ids. Warning: infixes automatically become reserved words! -Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof? - -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. - Syntax section: syntax annotations not just for consts but also for constdefs and datatype. Appendix with list functions. All theory sources on the web? - -Minor additions to the tutorial, unclear where -============================================== - -unfold? - - Possible exercises ==================