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

author | nipkow |

Fri, 26 Jan 2001 15:50:28 +0100 | |

changeset 10983 | 59961d32b1ae |

parent 10982 | 55c0f9a8df78 |

child 10984 | 8f49dcbec859 |

*** empty log message ***

--- a/doc-src/TutorialI/CTL/Base.thy Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/CTL/Base.thy Fri Jan 26 15:50:28 2001 +0100 @@ -60,7 +60,7 @@ text{*\noindent Command \isacommand{typedecl} merely declares a new type but without -defining it (see also \S\ref{sec:typedecl}). Thus we know nothing +defining it (see \S\ref{sec:typedecl}). Thus we know nothing about the type other than its existence. That is exactly what we need because @{typ state} really is an implicit parameter of our model. Of course it would have been more generic to make @{typ state} a type

--- a/doc-src/TutorialI/CTL/CTL.thy Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Jan 26 15:50:28 2001 +0100 @@ -17,8 +17,9 @@ | AF formula; text{*\noindent -which stands for "always in the future": -on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy +which stands for ``\emph{A}lways in the \emph{F}uture'': +on all infinite paths, at some point the formula holds. +Formalizing the notion of an infinite path is easy in HOL: it is simply a function from @{typ nat} to @{typ state}. *}; @@ -67,7 +68,7 @@ text{*\noindent Because @{term af} is monotone in its second argument (and also its first, but -that is irrelevant) @{term"af A"} has a least fixed point: +that is irrelevant), @{term"af A"} has a least fixed point: *}; lemma mono_af: "mono(af A)"; @@ -150,8 +151,8 @@ infinite @{term A}-avoiding path starting from @{term s}. The reason is that by unfolding @{term lfp} we find that if @{term s} is not in @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a -direct successor of @{term s} that is again not in @{term"lfp(af -A)"}. Iterating this argument yields the promised infinite +direct successor of @{term s} that is again not in \mbox{@{term"lfp(af +A)"}}. Iterating this argument yields the promised infinite @{term A}-avoiding path. Let us formalize this sketch. The one-step argument in the sketch above @@ -159,7 +160,7 @@ *}; lemma not_in_lfp_afD: - "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))"; + "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))"; apply(erule contrapos_np); apply(rule ssubst[OF lfp_unfold[OF mono_af]]); apply(simp add:af_def); @@ -196,8 +197,8 @@ \<exists>p\<in>Paths s. \<forall>i. Q(p i)"; txt{*\noindent -First we rephrase the conclusion slightly because we need to prove both the path property -and the fact that @{term Q} holds simultaneously: +First we rephrase the conclusion slightly because we need to prove simultaneously +both the path property and the fact that @{term Q} holds: *}; apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> Q(p i))"); @@ -216,7 +217,7 @@ apply(clarsimp); txt{*\noindent -After simplification and clarification the subgoal has the following compact form +After simplification and clarification, the subgoal has the following form @{subgoals[display,indent=0,margin=70,goals_limit=1]} and invites a proof by induction on @{term i}: *}; @@ -225,7 +226,7 @@ apply(simp); txt{*\noindent -After simplification the base case boils down to +After simplification, the base case boils down to @{subgoals[display,indent=0,margin=70,goals_limit=1]} The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"} holds. However, we first have to show that such a @{term t} actually exists! This reasoning @@ -345,8 +346,8 @@ text{* The language defined above is not quite CTL\@. The latter also includes an -until-operator @{term"EU f g"} with semantics ``there exists a path -where @{term f} is true until @{term g} becomes true''. With the help +until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path +where @{term f} is true \emph{U}ntil @{term g} becomes true''. With the help of an auxiliary function *} @@ -360,7 +361,7 @@ text{*\noindent the semantics of @{term EU} is straightforward: -@{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"} +@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"} Note that @{term EU} is not definable in terms of the other operators! Model checking @{term EU} is again a least fixed point construction: @@ -457,10 +458,10 @@ It is clear that if all sets are finite, they can be represented as lists and the usual set operations are easily implemented. Only @{term lfp} requires a little thought. Fortunately, the HOL Library% -\footnote{See theory \isa{While_Combinator_Example}.} +\footnote{See theory \isa{While_Combinator}.} provides a theorem stating that in the case of finite sets and a monotone function~@{term F}, -the value of @{term"lfp F"} can be computed by iterated application of @{term F} to~@{term"{}"} until +the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until a fixed point is reached. It is actually possible to generate executable functional programs from HOL definitions, but that is beyond the scope of the tutorial. *}

--- a/doc-src/TutorialI/CTL/PDL.thy Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/CTL/PDL.thy Fri Jan 26 15:50:28 2001 +0100 @@ -42,8 +42,8 @@ text{*\noindent The first three equations should be self-explanatory. The temporal formula -@{term"AX f"} means that @{term f} is true in all next states whereas -@{term"EF f"} means that there exists some future state in which @{term f} is +@{term"AX f"} means that @{term f} is true in \emph{A}ll ne\emph{X}t states whereas +@{term"EF f"} means that there \emph{E}xists some \emph{F}uture state in which @{term f} is true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive closure. Because of reflexivity, the future includes the present. @@ -68,7 +68,7 @@ fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you find it hard to see that @{term"mc(EF f)"} contains exactly those states from -which there is a path to a state where @{term f} is true, do not worry --- that +which there is a path to a state where @{term f} is true, do not worry --- this will be proved in a moment. First we prove monotonicity of the function inside @{term lfp} @@ -180,7 +180,7 @@ text{* \begin{exercise} @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX} -as that is the ASCII equivalent of @{text"\<exists>"}} +as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}} (``there exists a next state such that'') with the intended semantics @{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"} Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?

--- a/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 26 15:50:28 2001 +0100 @@ -63,7 +63,7 @@ \begin{isamarkuptext}% \noindent Command \isacommand{typedecl} merely declares a new type but without -defining it (see also \S\ref{sec:typedecl}). Thus we know nothing +defining it (see \S\ref{sec:typedecl}). Thus we know nothing about the type other than its existence. That is exactly what we need because \isa{state} really is an implicit parameter of our model. Of course it would have been more generic to make \isa{state} a type

--- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 26 15:50:28 2001 +0100 @@ -15,8 +15,9 @@ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula% \begin{isamarkuptext}% \noindent -which stands for "always in the future": -on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy +which stands for ``\emph{A}lways in the \emph{F}uture'': +on all infinite paths, at some point the formula holds. +Formalizing the notion of an infinite path is easy in HOL: it is simply a function from \isa{nat} to \isa{state}.% \end{isamarkuptext}% \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline @@ -45,7 +46,7 @@ \begin{isamarkuptext}% \noindent Because \isa{af} is monotone in its second argument (and also its first, but -that is irrelevant) \isa{af\ A} has a least fixed point:% +that is irrelevant), \isa{af\ A} has a least fixed point:% \end{isamarkuptext}% \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline @@ -111,14 +112,14 @@ infinite \isa{A}-avoiding path starting from \isa{s}. The reason is that by unfolding \isa{lfp} we find that if \isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a -direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite +direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite \isa{A}-avoiding path. Let us formalize this sketch. The one-step argument in the sketch above is proved by a variant of contraposition:% \end{isamarkuptext}% \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline -\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline +\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline @@ -153,8 +154,8 @@ \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -First we rephrase the conclusion slightly because we need to prove both the path property -and the fact that \isa{Q} holds simultaneously:% +First we rephrase the conclusion slightly because we need to prove simultaneously +both the path property and the fact that \isa{Q} holds:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\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}% \begin{isamarkuptxt}% @@ -170,7 +171,7 @@ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% \begin{isamarkuptxt}% \noindent -After simplification and clarification the subgoal has the following compact form +After simplification and clarification, the subgoal has the following form \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline @@ -182,7 +183,7 @@ \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% \begin{isamarkuptxt}% \noindent -After simplification the base case boils down to +After simplification, the base case boils down to \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M% @@ -281,8 +282,8 @@ \isacommand{done}% \begin{isamarkuptext}% The language defined above is not quite CTL\@. The latter also includes an -until-operator \isa{EU\ f\ g} with semantics ``there exists a path -where \isa{f} is true until \isa{g} becomes true''. With the help +until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path +where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. With the help of an auxiliary function% \end{isamarkuptext}% \isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline @@ -293,7 +294,7 @@ \noindent the semantics of \isa{EU} is straightforward: \begin{isabelle}% -\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ A\ B\ s\ p{\isacharparenright}% +\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}% \end{isabelle} Note that \isa{EU} is not definable in terms of the other operators! @@ -320,10 +321,10 @@ It is clear that if all sets are finite, they can be represented as lists and the usual set operations are easily implemented. Only \isa{lfp} requires a little thought. Fortunately, the HOL Library% -\footnote{See theory \isa{While_Combinator_Example}.} +\footnote{See theory \isa{While_Combinator}.} provides a theorem stating that in the case of finite sets and a monotone function~\isa{F}, -the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until +the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is reached. It is actually possible to generate executable functional programs from HOL definitions, but that is beyond the scope of the tutorial.% \end{isamarkuptext}%

--- a/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 26 15:50:28 2001 +0100 @@ -43,8 +43,8 @@ \begin{isamarkuptext}% \noindent The first three equations should be self-explanatory. The temporal formula -\isa{AX\ f} means that \isa{f} is true in all next states whereas -\isa{EF\ f} means that there exists some future state in which \isa{f} is +\isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas +\isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the reflexive transitive closure. Because of reflexivity, the future includes the present. @@ -68,7 +68,7 @@ fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from -which there is a path to a state where \isa{f} is true, do not worry --- that +which there is a path to a state where \isa{f} is true, do not worry --- this will be proved in a moment. First we prove monotonicity of the function inside \isa{lfp} @@ -177,7 +177,7 @@ \begin{isamarkuptext}% \begin{exercise} \isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX} -as that is the ASCII equivalent of \isa{{\isasymexists}}} +as that is the \textsc{ascii}-equivalent of \isa{{\isasymexists}}} (``there exists a next state such that'') with the intended semantics \begin{isabelle}% \ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%

--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 26 15:50:28 2001 +0100 @@ -166,7 +166,7 @@ Of course we can also unfold definitions in the middle of a proof. You should normally not turn a definition permanently into a simplification -rule because this defeats the whole purpose of an abbreviation. +rule because this defeats the whole purpose. \begin{warn} If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold

--- a/doc-src/TutorialI/Misc/simp.thy Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Misc/simp.thy Fri Jan 26 15:50:28 2001 +0100 @@ -162,7 +162,7 @@ Of course we can also unfold definitions in the middle of a proof. You should normally not turn a definition permanently into a simplification -rule because this defeats the whole purpose of an abbreviation. +rule because this defeats the whole purpose. \begin{warn} If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold

--- a/doc-src/TutorialI/Rules/rules.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Fri Jan 26 15:50:28 2001 +0100 @@ -966,7 +966,7 @@ \subsection{Definite Descriptions} -In ASCII, we write \isa{SOME} for $\varepsilon$. +In \textsc{ascii}, we write \isa{SOME} for $\varepsilon$. \REMARK{the internal constant is \isa{Eps}} The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite description}: when \isa{P} is satisfied by a unique value,~\isa{a}.

--- a/doc-src/TutorialI/Sets/Functions.thy Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Sets/Functions.thy Fri Jan 26 15:50:28 2001 +0100 @@ -79,7 +79,7 @@ *} lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; - apply (simp add: expand_fun_eq inj_on_def o_def) + apply (simp add: expand_fun_eq inj_on_def) apply (auto) done

--- a/doc-src/TutorialI/Sets/sets.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Fri Jan 26 15:50:28 2001 +0100 @@ -96,7 +96,7 @@ \isacommand{by}\ blast \end{isabelle} % -This is the same example using ASCII syntax, illustrating a pitfall: +This is the same example using \textsc{ascii} syntax, illustrating a pitfall: \begin{isabelle} \isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -A)" \end{isabelle} @@ -287,8 +287,8 @@ \end{isabelle} Unions can be formed over the values of a given set. The syntax is -\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN -x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law: +\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN +x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law: \begin{isabelle} (b\ \isasymin\ (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\ @@ -320,12 +320,12 @@ over a \emph{type}: \begin{isabelle} \ \ \ \ \ -({\isasymUnion}x.\ B\ x)\ {==}\ +({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\ ({\isasymUnion}x{\isasymin}UNIV.\ B\ x) \end{isabelle} Abbreviations work as you might expect. The term on the left-hand side of the -\isa{==} symbol is automatically translated to the right-hand side when the +\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the term is parsed, the reverse translation being done when the term is displayed. @@ -523,7 +523,7 @@ Theorems involving these concepts can be hard to prove. The following example is easy, but it cannot be proved automatically. To begin -with, we need a law that relates the quality of functions to +with, we need a law that relates the equality of functions to equality over all arguments: \begin{isabelle} (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x) @@ -535,7 +535,7 @@ side of function composition: \begin{isabelle} \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline -\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline +\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline \isacommand{apply}\ auto\isanewline \isacommand{done} \end{isabelle} @@ -593,7 +593,7 @@ abbreviates an application of image to {\isa{UNIV}}: \begin{isabelle} \ \ \ \ \ range\ f\ -{==}\ f`UNIV +{\isasymrightleftharpoons}\ f`UNIV \end{isabelle} % Few theorems are proved specifically @@ -845,7 +845,7 @@ Induction comes in many forms, including traditional mathematical induction, structural induction on lists and induction on size. More general than these is induction over a well-founded relation. -Such A relation expresses the notion of a terminating process. +Such a relation expresses the notion of a terminating process. Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no infinite descending chains \[ \cdots \prec a@2 \prec a@1 \prec a@0. \] @@ -944,9 +944,9 @@ \section{Fixed Point Operators} -Fixed point operators define sets recursively. Most users invoke -them by making an inductive definition, as discussed in -Chap.\ts\ref{chap:inductive} below. However, they can be used directly. +Fixed point operators define sets recursively. They are invoked +implicitly when making an inductive definition, as discussed in +Chap.\ts\ref{chap:inductive} below. However, they can be used directly, too. The \relax{least} or \relax{strongest} fixed point yields an inductive definition; the \relax{greatest} or \relax{weakest} fixed point yields a @@ -954,7 +954,7 @@ existence of these fixed points is guaranteed by the Knaster-Tarski theorem. -The theory works applies only to monotonic functions. Isabelle's +The theory applies only to monotonic functions. Isabelle's definition of monotone is overloaded over all orderings: \begin{isabelle} mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%

--- a/doc-src/TutorialI/Types/Typedef.thy Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Types/Typedef.thy Fri Jan 26 15:50:28 2001 +0100 @@ -96,8 +96,10 @@ @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"} \end{tabular} \end{center} -Constant @{term three} is just an abbreviation (@{thm[source]three_def}): -@{thm[display]three_def} +Constant @{term three} is explicitly defined as the representing set: +\begin{center} +@{thm three_def}\hfill(@{thm[source]three_def}) +\end{center} The situation is best summarized with the help of the following diagram, where squares are types and circles are sets: \begin{center} @@ -118,10 +120,10 @@ surjective on the subset @{term three} and @{term Abs_three} and @{term Rep_three} are inverses of each other: \begin{center} -\begin{tabular}{rl} -@{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\ -@{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\ -@{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse}) +\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}} +@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\ +@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\ +@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse}) \end{tabular} \end{center} %

--- a/doc-src/TutorialI/Types/document/Typedef.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Types/document/Typedef.tex Fri Jan 26 15:50:28 2001 +0100 @@ -102,10 +102,10 @@ \isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three} \end{tabular} \end{center} -Constant \isa{three} is just an abbreviation (\isa{three{\isacharunderscore}def}): -\begin{isabelle}% -three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}% -\end{isabelle} +Constant \isa{three} is explicitly defined as the representing set: +\begin{center} +\isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def}) +\end{center} The situation is best summarized with the help of the following diagram, where squares are types and circles are sets: \begin{center} @@ -125,10 +125,10 @@ Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other: \begin{center} -\begin{tabular}{rl} -\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} &~~ (\isa{Rep{\isacharunderscore}three}) \\ -\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} &~~ (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\ -\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} &~~ (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}) +\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}} +\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\ +\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\ +\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}) \end{tabular} \end{center} %

--- a/doc-src/TutorialI/Types/numerics.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Fri Jan 26 15:50:28 2001 +0100 @@ -270,7 +270,7 @@ \begin{warn} The absolute value bars shown above cannot be typed on a keyboard. They -can be entered using the X-symbol package. In ASCII, type \isa{abs x} to +can be entered using the X-symbol package. In \textsc{ascii}, type \isa{abs x} to get \isa{\isasymbar x\isasymbar}. \end{warn}

--- a/doc-src/TutorialI/appendix.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/appendix.tex Fri Jan 26 15:50:28 2001 +0100 @@ -98,9 +98,9 @@ \hline \end{tabular} \end{center} -\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes} +\caption{Mathematical symbols, their \textsc{ascii}-equivalents and X-symbol codes} \label{tab:ascii} -\end{table}\indexbold{ASCII symbols} +\end{table}\indexbold{ASCII@\textsc{ascii} symbols} \input{Misc/document/appendix.tex}

--- a/doc-src/TutorialI/basics.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/basics.tex Fri Jan 26 15:50:28 2001 +0100 @@ -8,12 +8,14 @@ HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step following the equation \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] -We assume that the reader is familiar with the basic concepts of both fields. -For excellent introductions to functional programming consult the textbooks -by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although -this tutorial initially concentrates on functional programming, do not be -misled: HOL can express most mathematical concepts, and functional -programming is just one particularly simple and ubiquitous instance. +We do not assume that the reader is familiar with mathematical logic but that +(s)he is used to logical and set theoretic notation. In contrast, we do assume +that the reader is familiar with the basic concepts of functional programming. +For excellent introductions consult the textbooks by Bird and +Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although this +tutorial initially concentrates on functional programming, do not be +misled: HOL can express most mathematical concepts, and functional programming +is just one particularly simple and ubiquitous instance. Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has influenced some of HOL's concrete syntax but is otherwise @@ -233,7 +235,7 @@ \end{itemize} For the sake of readability the usual mathematical symbols are used throughout -the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in +the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in the appendix. @@ -278,7 +280,7 @@ General}~\cite{Aspinall:TACAS:2000,proofgeneral}. Some interfaces (including the shell level) offer special fonts with -mathematical symbols. For those that do not, remember that ASCII-equivalents +mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in the appendix. Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} @@ -295,7 +297,7 @@ starts the default logic, which usually is already \texttt{HOL}. This is controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual} for more details.} This presents you with Isabelle's most -basic ASCII interface. In addition you need to open an editor window to +basic \textsc{ascii} interface. In addition you need to open an editor window to create theory files. While you are developing a theory, we recommend to type each command into the file first and then enter it into Isabelle by copy-and-paste, thus ensuring that you have a complete record of your theory.

--- a/doc-src/TutorialI/fp.tex Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/fp.tex Fri Jan 26 15:50:28 2001 +0100 @@ -1,16 +1,18 @@ \chapter{Functional Programming in HOL} Although on the surface this chapter is mainly concerned with how to write -functional programs in HOL and how to verify them, most of the -constructs and proof procedures introduced are general purpose and recur in -any specification or verification task. +functional programs in HOL and how to verify them, most of the constructs and +proof procedures introduced are general purpose and recur in any specification +or verification task. In fact, it we should really speak of functional +\emph{modelling} rather than \emph{programming} because our aim is not +primarily to write programs but to design abstract models of systems. HOL is +a specification language that goes well beyond what can be expressed as a +program. However, for the time being we concentrate on the computable. The dedicated functional programmer should be warned: HOL offers only -\emph{total functional programming} --- all functions in HOL must be total; -lazy data structures are not directly available. On the positive side, -functions in HOL need not be computable: HOL is a specification language that -goes well beyond what can be expressed as a program. However, for the time -being we concentrate on the computable. +\emph{total functional programming} --- all functions in HOL must be total, +i.e.\ they must terminate for all inputs; lazy data structures are not +directly available. \section{An Introductory Theory} \label{sec:intro-theory}

--- a/doc-src/TutorialI/todo.tobias Fri Jan 26 15:02:04 2001 +0100 +++ b/doc-src/TutorialI/todo.tobias Fri Jan 26 15:50:28 2001 +0100 @@ -35,15 +35,12 @@ Minor fixes in the tutorial =========================== -adjust type of ^ in tab:overloading - -explanation of term "contrapositive"/contraposition in Rules? -Index the notion and maybe the rules contrapos_xy +Adjust FP textbook refs: new Bird, Hudak +Discrete math textbook: Rosen? -get rid of use_thy in tutorial? +say something about "abbreviations" when defs are introduced. -Orderings on numbers (with hint that it is overloaded): -bounded quantifers ALL x<y, <=. +adjust type of ^ in tab:overloading an example of induction: !y. A --> B --> C ?? @@ -74,16 +71,6 @@ unfold? -Tacticals: , ? + -Note: + is used in typedef section! - -A list of further useful commands (rules? tricks?) -prefer, defer, print_simpset (-> print_simps?) - -demonstrate x : set xs in Sets. Or Tricks chapter? - -Appendix with HOL and Isar keywords. - Possible exercises ==================