--- 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.
--- 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.
--- 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:
--- 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