summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 17 Apr 2001 16:54:38 +0200 | |

changeset 11256 | 49afcce3bada |

parent 11255 | ca546b170471 |

child 11257 | 622331bbdb7f |

*** empty log message ***

--- a/doc-src/TutorialI/Advanced/Partial.thy Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/Advanced/Partial.thy Tue Apr 17 16:54:38 2001 +0200 @@ -29,7 +29,7 @@ text{* The rest of this section is devoted to the question of how to define -partial recursive functions by other means that non-exhaustive pattern +partial recursive functions by other means than non-exhaustive pattern matching. *}

--- a/doc-src/TutorialI/Advanced/document/Partial.tex Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Tue Apr 17 16:54:38 2001 +0200 @@ -29,7 +29,7 @@ {\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}% \begin{isamarkuptext}% The rest of this section is devoted to the question of how to define -partial recursive functions by other means that non-exhaustive pattern +partial recursive functions by other means than non-exhaustive pattern matching.% \end{isamarkuptext}% %

--- a/doc-src/TutorialI/Datatype/Nested.thy Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Tue Apr 17 16:54:38 2001 +0200 @@ -5,7 +5,9 @@ text{* So far, all datatypes had the property that on the right-hand side of their definition they occurred only at the top-level, i.e.\ directly below a -constructor. This is not the case any longer for the following model of terms +constructor. Now we consider \emph{nested recursion}, where the recursive +datatupe occurs nested in some other datatype (but not inside itself!). +Consider the following model of terms where function symbols can be applied to a list of arguments: *} (*<*)hide const Var(*>*) @@ -126,4 +128,4 @@ *} (*<*) end -(*>*) \ No newline at end of file +(*>*)

--- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Apr 17 16:54:38 2001 +0200 @@ -5,7 +5,9 @@ \begin{isamarkuptext}% So far, all datatypes had the property that on the right-hand side of their definition they occurred only at the top-level, i.e.\ directly below a -constructor. This is not the case any longer for the following model of terms +constructor. Now we consider \emph{nested recursion}, where the recursive +datatupe occurs nested in some other datatype (but not inside itself!). +Consider the following model of terms where function symbols can be applied to a list of arguments:% \end{isamarkuptext}% \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}%

--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Apr 17 16:54:38 2001 +0200 @@ -124,7 +124,16 @@ consts f :: "nat \<Rightarrow> nat"; axioms f_ax: "f(f(n)) < f(Suc(n))"; -text{*\noindent +text{* +\begin{warn} +We discourage the use of axioms because of the danger of +inconsistencies. Axiom @{text f_ax} does +not introduce an inconsistency because, for example, the identity function +satisfies it. Axioms can be useful in exploratory developments, say when +you assume some well-known theorems so that you can quickly demonstrate some +point about methodology. If your example turns into a substantial proof +development, you should replace axioms by theorems. +\end{warn}\noindent The axiom for @{term"f"} implies @{prop"n <= f n"}, which can be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined above, we have to phrase the proposition as follows to allow induction: @@ -197,40 +206,31 @@ (*<*)oops;(*>*) text{* -\begin{warn} -We discourage the use of axioms because of the danger of -inconsistencies. Axiom @{text f_ax} does -not introduce an inconsistency because, for example, the identity function -satisfies it. Axioms can be useful in exploratory developments, say when -you assume some well-known theorems so that you can quickly demonstrate some -point about methodology. If your example turns into a substantial proof -development, you should replace the axioms by proofs. -\end{warn} +\begin{exercise} +From the axiom and lemma for @{term"f"}, show that @{term"f"} is the +identity function. +\end{exercise} -\bigskip -In general, @{text induct_tac} can be applied with any rule $r$ +Method @{text induct_tac} can be applied with any rule $r$ whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the format is \begin{quote} \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"} \end{quote}\index{*induct_tac}% where $y@1, \dots, y@n$ are variables in the first subgoal. -A further example of a useful induction rule is @{thm[source]length_induct}, -induction on the length of a list:\indexbold{*length_induct} -@{thm[display]length_induct[no_vars]} - -In fact, @{text"induct_tac"} even allows the conclusion of -$r$ to be an (iterated) conjunction of formulae of the above form, in -which case the application is +The conclusion of $r$ can even be an (iterated) conjunction of formulae of +the above form in which case the application is \begin{quote} \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"} \end{quote} -\begin{exercise} -From the axiom and lemma for @{term"f"}, show that @{term"f"} is the -identity function. -\end{exercise} -*}; +A further useful induction rule is @{thm[source]length_induct}, +induction on the length of a list\indexbold{*length_induct} +@{thm[display]length_induct[no_vars]} +which is a special case of @{thm[source]measure_induct} +@{thm[display]measure_induct[no_vars]} +where @{term f} may be any function into type @{typ nat}. +*} subsection{*Derivation of New Induction Schemas*}; @@ -259,9 +259,9 @@ @{thm[display]"less_SucE"[no_vars]} Now it is straightforward to derive the original version of -@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma: -instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and -remove the trivial condition @{prop"n < Suc n"}. Fortunately, this +@{thm[source]nat_less_induct} by manipulating the conclusion of the above +lemma: instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} +and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this happens automatically when we add the lemma as a new premise to the desired goal: *};

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Apr 17 16:54:38 2001 +0200 @@ -120,7 +120,15 @@ \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% -\noindent +\begin{warn} +We discourage the use of axioms because of the danger of +inconsistencies. Axiom \isa{f{\isacharunderscore}ax} does +not introduce an inconsistency because, for example, the identity function +satisfies it. Axioms can be useful in exploratory developments, say when +you assume some well-known theorems so that you can quickly demonstrate some +point about methodology. If your example turns into a substantial proof +development, you should replace axioms by theorems. +\end{warn}\noindent The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined above, we have to phrase the proposition as follows to allow induction:% @@ -193,41 +201,34 @@ \end{isamarkuptext}% \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}% \begin{isamarkuptext}% -\begin{warn} -We discourage the use of axioms because of the danger of -inconsistencies. Axiom \isa{f{\isacharunderscore}ax} does -not introduce an inconsistency because, for example, the identity function -satisfies it. Axioms can be useful in exploratory developments, say when -you assume some well-known theorems so that you can quickly demonstrate some -point about methodology. If your example turns into a substantial proof -development, you should replace the axioms by proofs. -\end{warn} +\begin{exercise} +From the axiom and lemma for \isa{f}, show that \isa{f} is the +identity function. +\end{exercise} -\bigskip -In general, \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$ +Method \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$ whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the format is \begin{quote} \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}} \end{quote}\index{*induct_tac}% where $y@1, \dots, y@n$ are variables in the first subgoal. -A further example of a useful induction rule is \isa{length{\isacharunderscore}induct}, -induction on the length of a list:\indexbold{*length_induct} -\begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs% -\end{isabelle} - -In fact, \isa{induct{\isacharunderscore}tac} even allows the conclusion of -$r$ to be an (iterated) conjunction of formulae of the above form, in -which case the application is +The conclusion of $r$ can even be an (iterated) conjunction of formulae of +the above form in which case the application is \begin{quote} \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}} \end{quote} -\begin{exercise} -From the axiom and lemma for \isa{f}, show that \isa{f} is the -identity function. -\end{exercise}% +A further useful induction rule is \isa{length{\isacharunderscore}induct}, +induction on the length of a list\indexbold{*length_induct} +\begin{isabelle}% +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs% +\end{isabelle} +which is a special case of \isa{measure{\isacharunderscore}induct} +\begin{isabelle}% +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a% +\end{isabelle} +where \isa{f} may be any function into type \isa{nat}.% \end{isamarkuptext}% % \isamarkupsubsection{Derivation of New Induction Schemas% @@ -259,9 +260,9 @@ \end{isabelle} Now it is straightforward to derive the original version of -\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma: -instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and -remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this +\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above +lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} +and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this happens automatically when we add the lemma as a new premise to the desired goal:% \end{isamarkuptext}%

--- a/doc-src/TutorialI/todo.tobias Tue Apr 17 15:03:41 2001 +0200 +++ b/doc-src/TutorialI/todo.tobias Tue Apr 17 16:54:38 2001 +0200 @@ -54,8 +54,10 @@ =========================== recdef: failed tcs no longer shown! +say something about how conditions are proved? +No, better show failed proof attempts. -Advanced recdef: explain recdef_tc? +Advanced recdef: explain recdef_tc? No. Adjust recdef! Adjust FP textbook refs: new Bird, Hudak Discrete math textbook: Rosen?