# HG changeset patch # User paulson # Date 990267563 -7200 # Node ID 51e70b7bc315dab630dababd2040ce5702e3df62 # Parent d666f11ca2d41cb427ba4dee6e9549e179806194 spelling check diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Advanced/Partial.thy --- a/doc-src/TutorialI/Advanced/Partial.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Advanced/Partial.thy Sat May 19 12:19:23 2001 +0200 @@ -2,8 +2,8 @@ text{*\noindent Throughout the tutorial we have emphasized the fact that all functions in HOL are total. Hence we cannot hope to define -truly partial functions but must totalize them. A straightforward -totalization is to lift the result type of the function from $\tau$ to +truly partial functions, but must make them total. A straightforward +method is to lift the result type of the function from $\tau$ to $\tau$~@{text option} (see \ref{sec:option}), where @{term None} is returned if the function is applied to an argument not in its domain. Function @{term assoc} in \S\ref{sec:Trie} is a simple example. @@ -165,7 +165,7 @@ text{*\noindent The loop operates on two ``local variables'' @{term x} and @{term x'} containing the ``current'' and the ``next'' value of function @{term f}. -They are initalized with the global @{term x} and @{term"f x"}. At the +They are initialized with the global @{term x} and @{term"f x"}. At the end @{term fst} selects the local @{term x}. Although the definition of tail recursive functions via @{term while} avoids @@ -206,7 +206,7 @@ text{* Let us conclude this section on partial functions by a discussion of the merits of the @{term while} combinator. We have already seen that the advantage (if it is one) of not having to -provide a termintion argument when defining a function via @{term +provide a termination argument when defining a function via @{term while} merely puts off the evil hour. On top of that, tail recursive functions tend to be more complicated to reason about. So why use @{term while} at all? The only reason is executability: the recursion diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Sat May 19 12:19:23 2001 +0200 @@ -5,8 +5,8 @@ \begin{isamarkuptext}% \noindent Throughout the tutorial we have emphasized the fact that all functions in HOL are total. Hence we cannot hope to define -truly partial functions but must totalize them. A straightforward -totalization is to lift the result type of the function from $\tau$ to +truly partial functions, but must make them total. A straightforward +method is to lift the result type of the function from $\tau$ to $\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is returned if the function is applied to an argument not in its domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example. @@ -172,7 +172,7 @@ \noindent The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}} containing the ``current'' and the ``next'' value of function \isa{f}. -They are initalized with the global \isa{x} and \isa{f\ x}. At the +They are initialized with the global \isa{x} and \isa{f\ x}. At the end \isa{fst} selects the local \isa{x}. Although the definition of tail recursive functions via \isa{while} avoids @@ -215,7 +215,7 @@ Let us conclude this section on partial functions by a discussion of the merits of the \isa{while} combinator. We have already seen that the advantage (if it is one) of not having to -provide a termintion argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive +provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive functions tend to be more complicated to reason about. So why use \isa{while} at all? The only reason is executability: the recursion equation for \isa{while} is a directly executable functional diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Sat May 19 12:19:23 2001 +0200 @@ -6,7 +6,7 @@ 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. Now we consider \emph{nested recursion}, where the recursive -datatupe occurs nested in some other datatype (but not inside itself!). +datatype 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: *} diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Sat May 19 12:19:23 2001 +0200 @@ -6,7 +6,7 @@ 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. Now we consider \emph{nested recursion}, where the recursive -datatupe occurs nested in some other datatype (but not inside itself!). +datatype 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}% diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Sat May 19 12:19:23 2001 +0200 @@ -285,7 +285,7 @@ text{* We conclude this section with a comparison of our proof with -Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook grammar, for no good reason, excludes the empty word, thus complicating matters just a little bit: they have 8 instead of our 7 productions. diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Sat May 19 12:19:23 2001 +0200 @@ -266,7 +266,7 @@ \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}% \begin{isamarkuptext}% We conclude this section with a comparison of our proof with -Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook grammar, for no good reason, excludes the empty word, thus complicating matters just a little bit: they have 8 instead of our 7 productions. diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Misc/Option2.thy --- a/doc-src/TutorialI/Misc/Option2.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Misc/Option2.thy Sat May 19 12:19:23 2001 +0200 @@ -11,7 +11,7 @@ datatype 'a option = None | Some 'a; text{*\noindent -Frequently one needs to add a distiguished element to some existing type. +Frequently one needs to add a distinguished element to some existing type. For example, type @{text"t option"} can model the result of a computation that may either terminate with an error (represented by @{term None}) or return some value @{term v} (represented by @{term"Some v"}). diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Misc/Translations.thy --- a/doc-src/TutorialI/Misc/Translations.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Misc/Translations.thy Sat May 19 12:19:23 2001 +0200 @@ -22,7 +22,7 @@ and @{text"\"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown} for uni-directional translations, which only affect parsing or printing. We do not want to cover the details of -translations at this point. We haved mentioned the concept merely because it +translations at this point. We have mentioned the concept merely because it crops up occasionally: a number of HOL's built-in constructs are defined via translations. Translations are preferable to definitions when the new concept is a trivial variation on an existing one. For example, we diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Misc/document/Option2.tex --- a/doc-src/TutorialI/Misc/document/Option2.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/Option2.tex Sat May 19 12:19:23 2001 +0200 @@ -9,7 +9,7 @@ \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a% \begin{isamarkuptext}% \noindent -Frequently one needs to add a distiguished element to some existing type. +Frequently one needs to add a distinguished element to some existing type. For example, type \isa{t\ option} can model the result of a computation that may either terminate with an error (represented by \isa{None}) or return some value \isa{v} (represented by \isa{Some\ v}). diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Misc/document/Translations.tex --- a/doc-src/TutorialI/Misc/document/Translations.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/Translations.tex Sat May 19 12:19:23 2001 +0200 @@ -24,7 +24,7 @@ and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown} for uni-directional translations, which only affect parsing or printing. We do not want to cover the details of -translations at this point. We haved mentioned the concept merely because it +translations at this point. We have mentioned the concept merely because it crops up occasionally: a number of HOL's built-in constructs are defined via translations. Translations are preferable to definitions when the new concept is a trivial variation on an existing one. For example, we diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Protocol/Event.thy Sat May 19 12:19:23 2001 +0200 @@ -27,7 +27,7 @@ knows :: "agent => event list => msg set" -(*"spies" is retained for compability's sake*) +(*"spies" is retained for compatibility's sake*) syntax spies :: "event list => msg set" diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Types/Overloading0.thy --- a/doc-src/TutorialI/Types/Overloading0.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Types/Overloading0.thy Sat May 19 12:19:23 2001 +0200 @@ -29,7 +29,7 @@ left it is @{typ"'a \ 'b \ 'a \ 'b"} but on the right @{typ"'a \ 'a"} and @{typ"'b \ 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that the definitions do intentionally define @{term[source]inverse} only at -instances of its declared type @{typ"'a \ 'a"} --- this merely supresses +instances of its declared type @{typ"'a \ 'a"} --- this merely suppresses warnings to that effect. However, there is nothing to prevent the user from forming terms such as diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Types/Overloading1.thy --- a/doc-src/TutorialI/Types/Overloading1.thy Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Types/Overloading1.thy Sat May 19 12:19:23 2001 +0200 @@ -66,5 +66,5 @@ by(simp add: le_bool_def) text{*\noindent -whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped +whereas @{text"[] <<= []"} is not even well-typed. In order to make it well-typed we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*) diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Types/document/Overloading0.tex --- a/doc-src/TutorialI/Types/document/Overloading0.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex Sat May 19 12:19:23 2001 +0200 @@ -33,7 +33,7 @@ left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that the definitions do intentionally define \isa{inverse} only at -instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses +instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses warnings to that effect. However, there is nothing to prevent the user from forming terms such as diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Types/document/Overloading1.tex --- a/doc-src/TutorialI/Types/document/Overloading1.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex Sat May 19 12:19:23 2001 +0200 @@ -62,7 +62,7 @@ \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% \noindent -whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped +whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. In order to make it well-typed we need to make lists a type of class \isa{ordrel}:% \end{isamarkuptext}% \end{isabellebody}% diff -r d666f11ca2d4 -r 51e70b7bc315 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Fri May 18 17:18:43 2001 +0200 +++ b/src/HOL/Auth/Event.thy Sat May 19 12:19:23 2001 +0200 @@ -27,7 +27,7 @@ knows :: "agent => event list => msg set" -(*"spies" is retained for compability's sake*) +(*"spies" is retained for compatibility's sake*) syntax spies :: "event list => msg set" @@ -37,8 +37,8 @@ axioms (*Spy has access to his own key for spoof messages, but Server is secure*) - Spy_in_bad [iff] : "Spy \ bad" - Server_not_bad [iff] : "Server \ bad" + Spy_in_bad [iff] : "Spy \\ bad" + Server_not_bad [iff] : "Server \\ bad" primrec knows_Nil: "knows A [] = initState A" @@ -49,7 +49,7 @@ Says A' B X => insert X (knows Spy evs) | Gets A' X => knows Spy evs | Notes A' X => - if A' \ bad then insert X (knows Spy evs) else knows Spy evs) + if A' \\ bad then insert X (knows Spy evs) else knows Spy evs) else (case ev of Says A' B X => @@ -84,6 +84,6 @@ method_setup analz_mono_contra = {* Method.no_args (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *} - "for proving theorems of the form X \ analz (knows Spy evs) --> P" + "for proving theorems of the form X \\ analz (knows Spy evs) --> P" end