# HG changeset patch # User nipkow # Date 982660706 -3600 # Node ID 5652018b809a08572531d806d290bf0a353a490e # Parent 0d94005e374c9def038a19029b64add1be4ae38e *** empty log message *** diff -r 0d94005e374c -r 5652018b809a doc-src/TutorialI/Advanced/Partial.thy --- a/doc-src/TutorialI/Advanced/Partial.thy Sat Feb 17 10:43:53 2001 +0100 +++ b/doc-src/TutorialI/Advanced/Partial.thy Tue Feb 20 10:18:26 2001 +0100 @@ -158,17 +158,16 @@ They are initalized with the global @{term x} and @{term"f x"}. At the end @{term fst} selects the local @{term x}. -This looks like we can define at least tail recursive functions -without bothering about termination after all. But there is no free -lunch: when proving properties of functions defined by @{term while}, -termination rears its ugly head again. Here is -@{thm[source]while_rule}, the well known proof rule for total +Although the definition of tail recursive functions via @{term while} avoids +termination proofs, there is no free lunch. When proving properties of +functions defined by @{term while}, termination rears its ugly head +again. Here is @{thm[source]while_rule}, the well known proof rule for total correctness of loops expressed with @{term while}: -@{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be -true of the initial state @{term s} and invariant under @{term c} -(premises 1 and~2). The post-condition @{term Q} must become true when -leaving the loop (premise~3). And each loop iteration must descend -along a well-founded relation @{term r} (premises 4 and~5). +@{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be true of +the initial state @{term s} and invariant under @{term c} (premises 1 +and~2). The post-condition @{term Q} must become true when leaving the loop +(premise~3). And each loop iteration must descend along a well-founded +relation @{term r} (premises 4 and~5). Let us now prove that @{term find2} does indeed find a fixed point. Instead of induction we apply the above while rule, suitably instantiated. diff -r 0d94005e374c -r 5652018b809a doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Sat Feb 17 10:43:53 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Tue Feb 20 10:18:26 2001 +0100 @@ -166,22 +166,21 @@ They are initalized with the global \isa{x} and \isa{f\ x}. At the end \isa{fst} selects the local \isa{x}. -This looks like we can define at least tail recursive functions -without bothering about termination after all. But there is no free -lunch: when proving properties of functions defined by \isa{while}, -termination rears its ugly head again. Here is -\isa{while{\isacharunderscore}rule}, the well known proof rule for total +Although the definition of tail recursive functions via \isa{while} avoids +termination proofs, there is no free lunch. When proving properties of +functions defined by \isa{while}, termination rears its ugly head +again. Here is \isa{while{\isacharunderscore}rule}, the well known proof rule for total correctness of loops expressed with \isa{while}: \begin{isabelle}% \ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline \isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymnot}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\ s{\isacharsemicolon}\ wf\ r{\isacharsemicolon}\isanewline \isaindent{\ \ \ \ \ \ \ \ }{\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}c\ s{\isacharcomma}\ s{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\isanewline \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ Q\ {\isacharparenleft}while\ b\ c\ s{\isacharparenright}% -\end{isabelle} \isa{P} needs to be -true of the initial state \isa{s} and invariant under \isa{c} -(premises 1 and~2). The post-condition \isa{Q} must become true when -leaving the loop (premise~3). And each loop iteration must descend -along a well-founded relation \isa{r} (premises 4 and~5). +\end{isabelle} \isa{P} needs to be true of +the initial state \isa{s} and invariant under \isa{c} (premises 1 +and~2). The post-condition \isa{Q} must become true when leaving the loop +(premise~3). And each loop iteration must descend along a well-founded +relation \isa{r} (premises 4 and~5). Let us now prove that \isa{find{\isadigit{2}}} does indeed find a fixed point. Instead of induction we apply the above while rule, suitably instantiated. diff -r 0d94005e374c -r 5652018b809a doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Sat Feb 17 10:43:53 2001 +0100 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Tue Feb 20 10:18:26 2001 +0100 @@ -267,18 +267,21 @@ grammar, for no good reason, excludes the empty word. That complicates matters just a little bit because we now have 8 instead of our 7 productions. -More importantly, the proof itself is different: rather than separating the -two directions, they perform one induction on the length of a word. This -deprives them of the beauty of rule induction and in the easy direction -(correctness) their reasoning is more detailed than our \isa{auto}. For the -hard part (completeness), they consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of automatically. Then they conclude the proof by saying -about the remaining cases: ``We do this in a manner similar to our method of -proof for part (1); this part is left to the reader''. But this is precisely -the part that requires the intermediate value theorem and thus is not at all -similar to the other cases (which are automatic in Isabelle). We conclude -that the authors are at least cavalier about this point and may even have -overlooked the slight difficulty lurking in the omitted cases. This is not -atypical for pen-and-paper proofs, once analysed in detail.% +More importantly, the proof itself is different: rather than +separating the two directions, they perform one induction on the +length of a word. This deprives them of the beauty of rule induction, +and in the easy direction (correctness) their reasoning is more +detailed than our \isa{auto}. For the hard part (completeness), they +consider just one of the cases that our \isa{simp{\isacharunderscore}all} disposes of +automatically. Then they conclude the proof by saying about the +remaining cases: ``We do this in a manner similar to our method of +proof for part (1); this part is left to the reader''. But this is +precisely the part that requires the intermediate value theorem and +thus is not at all similar to the other cases (which are automatic in +Isabelle). The authors are at least cavalier about this point and may +even have overlooked the slight difficulty lurking in the omitted +cases. This is not atypical for pen-and-paper proofs, once analysed in +detail.% \end{isamarkuptext}% \end{isabellebody}% %%% Local Variables: diff -r 0d94005e374c -r 5652018b809a doc-src/TutorialI/todo.tobias --- a/doc-src/TutorialI/todo.tobias Sat Feb 17 10:43:53 2001 +0100 +++ b/doc-src/TutorialI/todo.tobias Tue Feb 20 10:18:26 2001 +0100 @@ -1,6 +1,8 @@ Implementation ============== +- (#2 * x) = #2 * - x is not proved by arith + Relation: comp -> composition Add map_cong?? (upto 10% slower) @@ -35,6 +37,9 @@ Minor fixes in the tutorial =========================== +I guess we should say "HOL" everywhere, with a remark early on about the +differences between our HOL and the other one. + warning: simp of asms from l to r; may require reordering (rotate_tac) Adjust FP textbook refs: new Bird, Hudak