# HG changeset patch # User nipkow # Date 978776829 -3600 # Node ID 2d4c058749a74900abb8bbb08dadbb6818006f3d # Parent ea69ee7e117bef170eeda5bf91341cd3b0828b3e *** empty log message *** diff -r ea69ee7e117b -r 2d4c058749a7 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Sat Jan 06 10:36:19 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTL.thy Sat Jan 06 11:27:09 2001 +0100 @@ -62,7 +62,7 @@ "mc(Neg f) = -mc f" "mc(And f g) = mc f \ mc g" "mc(AX f) = {s. \t. (s,t) \ M \ t \ mc f}" -"mc(EF f) = lfp(\T. mc f \ M^-1 ^^ T)"(*>*) +"mc(EF f) = lfp(\T. mc f \ M^-1 ``` T)"(*>*) "mc(AF f) = lfp(af(mc f))"; text{*\noindent @@ -75,12 +75,12 @@ apply blast; done (*<*) -lemma mono_ef: "mono(\T. A \ M^-1 ^^ T)"; +lemma mono_ef: "mono(\T. A \ M^-1 ``` T)"; apply(rule monoI); by(blast); lemma EF_lemma: - "lfp(\T. A \ M^-1 ^^ T) = {s. \t. (s,t) \ M^* \ t \ A}"; + "lfp(\T. A \ M^-1 ``` T) = {s. \t. (s,t) \ M^* \ t \ A}"; apply(rule equalityI); apply(rule subsetI); apply(simp); @@ -366,7 +366,7 @@ Note that @{term EU} is not definable in terms of the other operators! Model checking @{term EU} is again a least fixed point construction: -@{text[display]"mc(EU f g) = lfp(\T. mc g \ mc f \ (M^-1 ^^ T))"} +@{text[display]"mc(EU f g) = lfp(\T. mc g \ mc f \ (M^-1 ``` T))"} \begin{exercise} Extend the datatype of formulae by the above until operator @@ -382,7 +382,7 @@ (*<*) constdefs eufix :: "state set \ state set \ state set \ state set" -"eufix A B T \ B \ A \ (M^-1 ^^ T)" +"eufix A B T \ B \ A \ (M^-1 ``` T)" lemma "lfp(eufix A B) \ eusem A B" apply(rule lfp_lowerbound) diff -r ea69ee7e117b -r 2d4c058749a7 doc-src/TutorialI/CTL/PDL.thy --- a/doc-src/TutorialI/CTL/PDL.thy Sat Jan 06 10:36:19 2001 +0100 +++ b/doc-src/TutorialI/CTL/PDL.thy Sat Jan 06 11:27:09 2001 +0100 @@ -58,14 +58,14 @@ "mc(Neg f) = -mc f" "mc(And f g) = mc f \ mc g" "mc(AX f) = {s. \t. (s,t) \ M \ t \ mc f}" -"mc(EF f) = lfp(\T. mc f \ M^-1 ^^ T)" +"mc(EF f) = lfp(\T. mc f \ M^-1 ``` T)" text{*\noindent Only the equation for @{term EF} deserves some comments. Remember that the -postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the +postfix @{text"^-1"} and the infix @{text"```"} are predefined and denote the converse of a relation and the application of a relation to a set. Thus -@{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least -fixed point (@{term lfp}) of @{term"\T. mc f \ M^-1 ^^ T"} is the least set +@{term "M^-1 ``` T"} is the set of all predecessors of @{term T} and the least +fixed point (@{term lfp}) of @{term"\T. mc f \ M^-1 ``` 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 @@ -74,7 +74,7 @@ First we prove monotonicity of the function inside @{term lfp} *} -lemma mono_ef: "mono(\T. A \ M^-1 ^^ T)" +lemma mono_ef: "mono(\T. A \ M^-1 ``` T)" apply(rule monoI) apply blast done @@ -87,7 +87,7 @@ *} lemma EF_lemma: - "lfp(\T. A \ M^-1 ^^ T) = {s. \t. (s,t) \ M^* \ t \ A}" + "lfp(\T. A \ M^-1 ``` T) = {s. \t. (s,t) \ M^* \ t \ A}" txt{*\noindent The equality is proved in the canonical fashion by proving that each set diff -r ea69ee7e117b -r 2d4c058749a7 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Sat Jan 06 10:36:19 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Sat Jan 06 11:27:09 2001 +0100 @@ -300,7 +300,7 @@ Model checking \isa{EU} is again a least fixed point construction: \begin{isabelle}% -\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}% +\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}% \end{isabelle} \begin{exercise} diff -r ea69ee7e117b -r 2d4c058749a7 doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Sat Jan 06 10:36:19 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Sat Jan 06 11:27:09 2001 +0100 @@ -58,14 +58,14 @@ {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline {\isachardoublequote}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequote}\isanewline -{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}% +{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent Only the equation for \isa{EF} deserves some comments. Remember that the -postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the +postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}{\isacharbackquote}} are predefined and denote the converse of a relation and the application of a relation to a set. Thus -\isa{M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least -fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T} is the least set +\isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least +fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\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 @@ -73,7 +73,7 @@ First we prove monotonicity of the function inside \isa{lfp}% \end{isamarkuptext}% -\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline \isacommand{apply}\ blast\isanewline \isacommand{done}% @@ -85,7 +85,7 @@ a separate lemma:% \end{isamarkuptext}% \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline -\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% +\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent The equality is proved in the canonical fashion by proving that each set @@ -98,7 +98,7 @@ \noindent Simplification leaves us with the following first subgoal \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A% \end{isabelle} which is proved by \isa{lfp}-induction:% \end{isamarkuptxt}% @@ -127,7 +127,7 @@ \noindent After simplification and clarification we are left with \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% \end{isabelle} This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model checker works backwards (from \isa{t} to \isa{s}), we cannot use the @@ -148,14 +148,14 @@ \noindent The base case \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% \end{isabelle} is solved by unrolling \isa{lfp} once% \end{isamarkuptxt}% \ \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}% \end{isabelle} and disposing of the resulting trivial subgoal automatically:% \end{isamarkuptxt}% diff -r ea69ee7e117b -r 2d4c058749a7 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Sat Jan 06 10:36:19 2001 +0100 +++ b/doc-src/TutorialI/fp.tex Sat Jan 06 11:27:09 2001 +0100 @@ -160,8 +160,7 @@ \isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first element and the remainder of a list. (However, pattern-matching is usually preferable to \isa{hd} and \isa{tl}.) -Also available are the higher-order -functions \isa{map}, \isa{filter}, \isa{foldl} and \isa{foldr}. +Also available are higher-order functions like \isa{map} and \isa{filter}. Theory \isa{List} also contains more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we