*** empty log message ***
authornipkow
Thu Dec 13 16:48:34 2001 +0100 (2001-12-13)
changeset 12489c92e38c3cbaa
parent 12488 83acab8042ad
child 12490 d2a2c479b3cb
*** empty log message ***
NEWS
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/document/CTL.tex
doc-src/TutorialI/Misc/document/simp.tex
doc-src/TutorialI/Misc/simp.thy
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/Sets/Relations.thy
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/preface.tex
doc-src/TutorialI/todo.tobias
doc-src/TutorialI/tutorial.tex
     1.1 --- a/NEWS	Thu Dec 13 16:48:07 2001 +0100
     1.2 +++ b/NEWS	Thu Dec 13 16:48:34 2001 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -224,6 +223,10 @@
     1.9  a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
    1.10  necessary to attach explicit type constraints;
    1.11  
    1.12 +* HOL/Relation: the prefix name of the infix "O" has been changed from "comp"
    1.13 +to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly
    1.14 +(eg "compI" -> "rel_compI").
    1.15 +
    1.16  * HOL: syntax translations now work properly with numerals and records
    1.17  expressions;
    1.18  
     2.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Thu Dec 13 16:48:07 2001 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Dec 13 16:48:34 2001 +0100
     2.3 @@ -203,7 +203,8 @@
     2.4  both the path property and the fact that @{term Q} holds:
     2.5  *};
     2.6  
     2.7 -apply(subgoal_tac "\<exists>p. s = p (0::nat) \<and> (\<forall>i. (p i, p(i+1)) \<in> M \<and> Q(p i))");
     2.8 +apply(subgoal_tac
     2.9 +  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))");
    2.10  
    2.11  txt{*\noindent
    2.12  From this proposition the original goal follows easily:
     3.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Dec 13 16:48:07 2001 +0100
     3.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Thu Dec 13 16:48:34 2001 +0100
     3.3 @@ -221,7 +221,8 @@
     3.4  both the path property and the fact that \isa{Q} holds:%
     3.5  \end{isamarkuptxt}%
     3.6  \isamarkuptrue%
     3.7 -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
     3.8 +\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
     3.9 +\ \ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
    3.10  %
    3.11  \begin{isamarkuptxt}%
    3.12  \noindent
     4.1 --- a/doc-src/TutorialI/Misc/document/simp.tex	Thu Dec 13 16:48:07 2001 +0100
     4.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex	Thu Dec 13 16:48:34 2001 +0100
     4.3 @@ -25,7 +25,7 @@
     4.4  are explained in \S\ref{sec:SimpHow}.
     4.5  
     4.6  The simplification attribute of theorems can be turned on and off:%
     4.7 -\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
     4.8 +\index{*simp del (attribute)}
     4.9  \begin{quote}
    4.10  \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
    4.11  \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}}
    4.12 @@ -237,7 +237,7 @@
    4.13  There is also the special method \isa{unfold}\index{*unfold (method)|bold}
    4.14  which merely unfolds
    4.15  one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
    4.16 -This is can be useful if \isa{simp} does too much.%
    4.17 +This is can be useful in situations where \isa{simp} does too much.%
    4.18  \end{isamarkuptext}%
    4.19  \isamarkuptrue%
    4.20  %
     5.1 --- a/doc-src/TutorialI/Misc/simp.thy	Thu Dec 13 16:48:07 2001 +0100
     5.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Thu Dec 13 16:48:34 2001 +0100
     5.3 @@ -21,7 +21,7 @@
     5.4  are explained in \S\ref{sec:SimpHow}.
     5.5  
     5.6  The simplification attribute of theorems can be turned on and off:%
     5.7 -\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
     5.8 +\index{*simp del (attribute)}
     5.9  \begin{quote}
    5.10  \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
    5.11  \isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
     6.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Thu Dec 13 16:48:07 2001 +0100
     6.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Thu Dec 13 16:48:34 2001 +0100
     6.3 @@ -15,55 +15,56 @@
     6.4  simplification rules.
     6.5  
     6.6  Isabelle may fail to prove the termination condition for some
     6.7 -recursive call.  Let us try the following artificial function:%
     6.8 -\end{isamarkuptext}%
     6.9 -\isamarkuptrue%
    6.10 -\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    6.11 -\isamarkupfalse%
    6.12 -\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
    6.13 -\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
    6.14 -%
    6.15 -\begin{isamarkuptext}%
    6.16 -\noindent This definition fails, and Isabelle prints an error message
    6.17 -showing you what it was unable to prove. You will then have to prove it as a
    6.18 -separate lemma before you attempt the definition of your function once
    6.19 -more. In our case the required lemma is the obvious one:%
    6.20 +recursive call.  Let us try to define Quicksort:%
    6.21  \end{isamarkuptext}%
    6.22  \isamarkuptrue%
    6.23 -\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}\isamarkupfalse%
    6.24 -%
    6.25 -\begin{isamarkuptxt}%
    6.26 -\noindent
    6.27 -It was not proved automatically because of the awkward behaviour of subtraction
    6.28 -on type \isa{nat}. This requires more arithmetic than is tried by default:%
    6.29 -\end{isamarkuptxt}%
    6.30 -\isamarkuptrue%
    6.31 -\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
    6.32 +\isacommand{consts}\ qs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline
    6.33  \isamarkupfalse%
    6.34 -\isacommand{done}\isamarkupfalse%
    6.35 +\isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
    6.36 +\ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
    6.37 +\ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
    6.38  %
    6.39  \begin{isamarkuptext}%
    6.40 -\noindent
    6.41 -Because \isacommand{recdef}'s termination prover involves simplification,
    6.42 -we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
    6.43 -says to use \isa{termi{\isacharunderscore}lem} as a simplification rule.%
    6.44 +\noindent where \isa{filter} is predefined and \isa{filter\ P\ xs}
    6.45 +is the list of elements of \isa{xs} satisfying \isa{P}.
    6.46 +This definition of \isa{qs} fails, and Isabelle prints an error message
    6.47 +showing you what it was unable to prove:
    6.48 +\begin{isabelle}%
    6.49 +\ \ \ \ \ length\ {\isacharparenleft}filter\ {\isachardot}{\isachardot}{\isachardot}\ xs{\isacharparenright}\ {\isacharless}\ Suc\ {\isacharparenleft}length\ xs{\isacharparenright}%
    6.50 +\end{isabelle}
    6.51 +We can either prove this as a separate lemma, or try to figure out which
    6.52 +existing lemmas may help. We opt for the second alternative. The theory of
    6.53 +lists contains the simplification rule \isa{length\ {\isacharparenleft}filter\ P\ xs{\isacharparenright}\ {\isasymle}\ length\ xs},
    6.54 +which is already
    6.55 +close to what we need, except that we still need to turn \mbox{\isa{{\isacharless}\ Suc}}
    6.56 +into
    6.57 +\isa{{\isasymle}} for the simplification rule to apply. Lemma
    6.58 +\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} does just that: \isa{{\isacharparenleft}m\ {\isacharless}\ Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}m\ {\isasymle}\ n{\isacharparenright}}.
    6.59 +
    6.60 +Now we retry the above definition but supply the lemma(s) just found (or
    6.61 +proved). Because \isacommand{recdef}'s termination prover involves
    6.62 +simplification, we include in our second attempt a hint: the
    6.63 +\attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a
    6.64 +simplification rule.%
    6.65  \end{isamarkuptext}%
    6.66  \isamarkuptrue%
    6.67  \isamarkupfalse%
    6.68  \isamarkupfalse%
    6.69 -\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
    6.70 -\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
    6.71 -{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}\isamarkupfalse%
    6.72 +\isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
    6.73 +\ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
    6.74 +\ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    6.75 +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse%
    6.76  \isamarkupfalse%
    6.77  %
    6.78  \begin{isamarkuptext}%
    6.79  \noindent
    6.80 -This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely
    6.81 -the stated recursion equation for \isa{f}, which has been turned into a
    6.82 -simplification rule.  Thus we can automatically prove results such as this one:%
    6.83 +This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely
    6.84 +the stated recursion equations for \isa{qs} and they have become
    6.85 +simplification rules.
    6.86 +Thus we can automatically prove results such as this one:%
    6.87  \end{isamarkuptext}%
    6.88  \isamarkuptrue%
    6.89 -\isacommand{theorem}\ {\isachardoublequote}f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    6.90 +\isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline
    6.91  \isamarkupfalse%
    6.92  \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
    6.93  \isamarkupfalse%
    6.94 @@ -73,10 +74,10 @@
    6.95  \noindent
    6.96  More exciting theorems require induction, which is discussed below.
    6.97  
    6.98 -If the termination proof requires a new lemma that is of general use, you can
    6.99 +If the termination proof requires a lemma that is of general use, you can
   6.100  turn it permanently into a simplification rule, in which case the above
   6.101 -\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
   6.102 -sufficiently general to warrant this distinction.%
   6.103 +\isacommand{hint} is not necessary. But in the case of
   6.104 +\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.%
   6.105  \end{isamarkuptext}%
   6.106  \isamarkuptrue%
   6.107  \isamarkupfalse%
     7.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Thu Dec 13 16:48:07 2001 +0100
     7.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Thu Dec 13 16:48:34 2001 +0100
     7.3 @@ -14,55 +14,57 @@
     7.4  simplification rules.
     7.5  
     7.6  Isabelle may fail to prove the termination condition for some
     7.7 -recursive call.  Let us try the following artificial function:*}
     7.8 +recursive call.  Let us try to define Quicksort:*}
     7.9  
    7.10 -consts f :: "nat\<times>nat \<Rightarrow> nat"
    7.11 -recdef (*<*)(permissive)(*>*)f "measure(\<lambda>(x,y). x-y)"
    7.12 -  "f(x,y) = (if x \<le> y then x else f(x,y+1))"
    7.13 +consts qs :: "nat list \<Rightarrow> nat list"
    7.14 +recdef(*<*)(permissive)(*>*) qs "measure length"
    7.15 + "qs [] = []"
    7.16 + "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
    7.17  
    7.18 -text{*\noindent This definition fails, and Isabelle prints an error message
    7.19 -showing you what it was unable to prove. You will then have to prove it as a
    7.20 -separate lemma before you attempt the definition of your function once
    7.21 -more. In our case the required lemma is the obvious one: *}
    7.22 +text{*\noindent where @{term filter} is predefined and @{term"filter P xs"}
    7.23 +is the list of elements of @{term xs} satisfying @{term P}.
    7.24 +This definition of @{term qs} fails, and Isabelle prints an error message
    7.25 +showing you what it was unable to prove:
    7.26 +@{text[display]"length (filter ... xs) < Suc (length xs)"}
    7.27 +We can either prove this as a separate lemma, or try to figure out which
    7.28 +existing lemmas may help. We opt for the second alternative. The theory of
    7.29 +lists contains the simplification rule @{thm length_filter[no_vars]},
    7.30 +which is already
    7.31 +close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
    7.32 +into
    7.33 +@{text"\<le>"} for the simplification rule to apply. Lemma
    7.34 +@{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
    7.35  
    7.36 -lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
    7.37 +Now we retry the above definition but supply the lemma(s) just found (or
    7.38 +proved). Because \isacommand{recdef}'s termination prover involves
    7.39 +simplification, we include in our second attempt a hint: the
    7.40 +\attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
    7.41 +simplification rule.  *}
    7.42  
    7.43 -txt{*\noindent
    7.44 -It was not proved automatically because of the awkward behaviour of subtraction
    7.45 -on type @{typ"nat"}. This requires more arithmetic than is tried by default:
    7.46 +(*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
    7.47 +recdef qs "measure length"
    7.48 + "qs [] = []"
    7.49 + "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
    7.50 +(hints recdef_simp: less_Suc_eq_le)
    7.51 +(*<*)local(*>*)
    7.52 +text{*\noindent
    7.53 +This time everything works fine. Now @{thm[source]qs.simps} contains precisely
    7.54 +the stated recursion equations for @{text qs} and they have become
    7.55 +simplification rules.
    7.56 +Thus we can automatically prove results such as this one:
    7.57  *}
    7.58  
    7.59 -apply(arith)
    7.60 -done
    7.61 -
    7.62 -text{*\noindent
    7.63 -Because \isacommand{recdef}'s termination prover involves simplification,
    7.64 -we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
    7.65 -says to use @{thm[source]termi_lem} as a simplification rule.  
    7.66 -*}
    7.67 -
    7.68 -(*<*)global consts f :: "nat\<times>nat \<Rightarrow> nat" (*>*)
    7.69 -recdef f "measure(\<lambda>(x,y). x-y)"
    7.70 -  "f(x,y) = (if x \<le> y then x else f(x,y+1))"
    7.71 -(hints recdef_simp: termi_lem)
    7.72 -(*<*)local(*>*)
    7.73 -text{*\noindent
    7.74 -This time everything works fine. Now @{thm[source]f.simps} contains precisely
    7.75 -the stated recursion equation for @{text f}, which has been turned into a
    7.76 -simplification rule.  Thus we can automatically prove results such as this one:
    7.77 -*}
    7.78 -
    7.79 -theorem "f(1,0) = f(1,1)"
    7.80 +theorem "qs[2,3,0] = qs[3,0,2]"
    7.81  apply(simp)
    7.82  done
    7.83  
    7.84  text{*\noindent
    7.85  More exciting theorems require induction, which is discussed below.
    7.86  
    7.87 -If the termination proof requires a new lemma that is of general use, you can
    7.88 +If the termination proof requires a lemma that is of general use, you can
    7.89  turn it permanently into a simplification rule, in which case the above
    7.90 -\isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
    7.91 -sufficiently general to warrant this distinction.
    7.92 +\isacommand{hint} is not necessary. But in the case of
    7.93 +@{thm[source]less_Suc_eq_le} this would be of dubious value.
    7.94  *}
    7.95  (*<*)
    7.96  end
     8.1 --- a/doc-src/TutorialI/Sets/Relations.thy	Thu Dec 13 16:48:07 2001 +0100
     8.2 +++ b/doc-src/TutorialI/Sets/Relations.thy	Thu Dec 13 16:48:34 2001 +0100
     8.3 @@ -12,8 +12,8 @@
     8.4  *}
     8.5  
     8.6  text{*
     8.7 -@{thm[display] comp_def[no_vars]}
     8.8 -\rulename{comp_def}
     8.9 +@{thm[display] rel_comp_def[no_vars]}
    8.10 +\rulename{rel_comp_def}
    8.11  *}
    8.12  
    8.13  text{*
    8.14 @@ -22,8 +22,8 @@
    8.15  *}
    8.16  
    8.17  text{*
    8.18 -@{thm[display] comp_mono[no_vars]}
    8.19 -\rulename{comp_mono}
    8.20 +@{thm[display] rel_comp_mono[no_vars]}
    8.21 +\rulename{rel_comp_mono}
    8.22  *}
    8.23  
    8.24  text{*
    8.25 @@ -32,8 +32,8 @@
    8.26  *}
    8.27  
    8.28  text{*
    8.29 -@{thm[display] converse_comp[no_vars]}
    8.30 -\rulename{converse_comp}
    8.31 +@{thm[display] converse_rel_comp[no_vars]}
    8.32 +\rulename{converse_rel_comp}
    8.33  *}
    8.34  
    8.35  text{*
     9.1 --- a/doc-src/TutorialI/Sets/sets.tex	Thu Dec 13 16:48:07 2001 +0100
     9.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Thu Dec 13 16:48:34 2001 +0100
     9.3 @@ -670,7 +670,7 @@
     9.4  available: 
     9.5  \begin{isabelle}
     9.6  r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
     9.7 -\rulenamedx{comp_def}
     9.8 +\rulenamedx{rel_comp_def}
     9.9  \end{isabelle}
    9.10  %
    9.11  This is one of the many lemmas proved about these concepts: 
    9.12 @@ -686,7 +686,7 @@
    9.13  \isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\
    9.14  \isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\
    9.15  s\isacharprime\ \isasymsubseteq\ r\ O\ s%
    9.16 -\rulename{comp_mono}
    9.17 +\rulename{rel_comp_mono}
    9.18  \end{isabelle}
    9.19  
    9.20  \indexbold{converse!of a relation}%
    9.21 @@ -704,7 +704,7 @@
    9.22  Here is a typical law proved about converse and composition: 
    9.23  \begin{isabelle}
    9.24  (r\ O\ s)\isasyminverse\ =\ s\isasyminverse\ O\ r\isasyminverse
    9.25 -\rulename{converse_comp}
    9.26 +\rulename{converse_rel_comp}
    9.27  \end{isabelle}
    9.28  
    9.29  \indexbold{image!under a relation}%
    10.1 --- a/doc-src/TutorialI/appendix.tex	Thu Dec 13 16:48:07 2001 +0100
    10.2 +++ b/doc-src/TutorialI/appendix.tex	Thu Dec 13 16:48:34 2001 +0100
    10.3 @@ -115,7 +115,7 @@
    10.4  
    10.5  \begin{table}[htbp]
    10.6  \begin{center}
    10.7 -\begin{tabular}{|lllllllll|}
    10.8 +\begin{tabular}{@{}|lllllllll|@{}}
    10.9  \hline
   10.10  \texttt{ALL} &
   10.11  \texttt{BIT} &
    11.1 --- a/doc-src/TutorialI/preface.tex	Thu Dec 13 16:48:07 2001 +0100
    11.2 +++ b/doc-src/TutorialI/preface.tex	Thu Dec 13 16:48:34 2001 +0100
    11.3 @@ -36,4 +36,3 @@
    11.4  GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
    11.5  \textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}
    11.6  project).
    11.7 -
    12.1 --- a/doc-src/TutorialI/todo.tobias	Thu Dec 13 16:48:07 2001 +0100
    12.2 +++ b/doc-src/TutorialI/todo.tobias	Thu Dec 13 16:48:34 2001 +0100
    12.3 @@ -3,28 +3,10 @@
    12.4  Implementation
    12.5  ==============
    12.6  
    12.7 -- (#2 * x) = #2 * - x is not proved by arith
    12.8 +Add map_cong?? (upto 10% slower)
    12.9  
   12.10  a simp command for terms
   12.11  
   12.12 -----------------------------------------------------------------------
   12.13 -primrec 
   12.14 -"(foorec [] []) = []"
   12.15 -"(foorec [] (y # ys)) = (y # (foorec [] ys))"
   12.16 -
   12.17 -*** Primrec definition error:
   12.18 -*** extra variables on rhs: "y", "ys"
   12.19 -*** in
   12.20 -*** "((foorec [] ((y::'a_1) # (ys::'a_1 list))) = (y # (foorec [] ys)))"
   12.21 -*** At command "primrec".
   12.22 -
   12.23 -Bessere Fehlermeldung!
   12.24 -----------------------------------------------------------------------
   12.25 -
   12.26 -Relation: comp -> composition
   12.27 -
   12.28 -Add map_cong?? (upto 10% slower)
   12.29 -
   12.30  Recdef: Get rid of function name in header.
   12.31  Support mutual recursion (Konrad?)
   12.32  
   12.33 @@ -33,9 +15,6 @@
   12.34  better 1 point rules:
   12.35  !x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
   12.36  
   12.37 -use arith_tac in recdef to solve termination conditions?
   12.38 --> new example in Recdef/termination
   12.39 -
   12.40  it would be nice if @term could deal with ?-vars.
   12.41  then a number of (unchecked!) @texts could be converted to @terms.
   12.42  
    13.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Dec 13 16:48:07 2001 +0100
    13.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Dec 13 16:48:34 2001 +0100
    13.3 @@ -69,10 +69,18 @@
    13.4  \input{Advanced/advanced}
    13.5  \input{Protocol/protocol}
    13.6  
    13.7 -%\chapter{Structured Proofs}
    13.8 -%\label{ch:Isar}
    13.9 -%\chapter{Case Study: UNIX File-System Security}
   13.10 -%\chapter{The Tricks of the Trade}
   13.11 +\markboth{}{}
   13.12 +\cleardoublepage
   13.13 +\vspace*{\fill}
   13.14 +\begin{flushright}
   13.15 +\begin{tabular}{l}
   13.16 +{\large\sf\slshape You know my methods. Apply them!}\\[1ex]
   13.17 +Sherlock Holmes
   13.18 +\end{tabular}
   13.19 +\end{flushright}
   13.20 +\vspace*{\fill}
   13.21 +\vspace*{\fill}
   13.22 +
   13.23  \input{appendix}
   13.24  
   13.25  \bibliographystyle{plain}