# HG changeset patch # User nipkow # Date 970828313 -7200 # Node ID a72ddfdbfca09c0d8b74a4afa713b42be5967f6e # Parent 00fdd5c330eac2cd7144e27c2c30d0e25ba32007 *** empty log message *** diff -r 00fdd5c330ea -r a72ddfdbfca0 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Fri Oct 06 01:21:17 2000 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Oct 06 12:31:53 2000 +0200 @@ -1,38 +1,38 @@ -(*<*)theory CTL = Base:(*>*) +(*<*)theory CTL = Base:;(*>*) -subsection{*Computation tree logic---CTL*} +subsection{*Computation tree logic---CTL*}; text{* The semantics of PDL only needs transitive reflexive closure. Let us now be a bit more adventurous and introduce a new temporal operator that goes beyond transitive reflexive closure. We extend the datatype @{text formula} by a new constructor -*} +*}; (*<*) datatype formula = Atom atom | Neg formula | And formula formula | AX formula | EF formula(*>*) - | AF formula + | AF formula; text{*\noindent which stands for "always in the future": -on all paths, at some point the formula holds. -Introducing the notion of paths (in @{term M}) -*} +on all 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}. +*}; constdefs Paths :: "state \ (nat \ state)set" "Paths s \ {p. s = p 0 \ (\i. (p i, p(i+1)) \ M)}"; text{*\noindent -allows a very succinct definition of the semantics of @{term AF}: +This definition allows a very succinct statement of the semantics of @{term AF}: \footnote{Do not be mislead: neither datatypes nor recursive functions can be extended by new constructors or equations. This is just a trick of the presentation. In reality one has to define a new datatype and a new function.} -*} +*}; (*<*) -consts valid :: "state \ formula \ bool" ("(_ \ _)" [80,80] 80) +consts valid :: "state \ formula \ bool" ("(_ \ _)" [80,80] 80); primrec "s \ Atom a = (a \ L s)" @@ -45,25 +45,16 @@ text{*\noindent Model checking @{term AF} involves a function which -is just large enough to warrant a separate definition: -*} +is just complicated enough to warrant a separate definition: +*}; constdefs af :: "state set \ state set \ state set" "af A T \ A \ {s. \t. (s, t) \ M \ t \ T}"; text{*\noindent -This function is monotone in its second argument (and also its first, but -that is irrelevant), and hence @{term"af A"} has a least fixpoint. -*} - -lemma mono_af: "mono(af A)"; -apply(simp add: mono_def af_def) -by(blast); - -text{*\noindent -Now we can define @{term "mc(AF f)"} as the least set @{term T} that contains +Now we define @{term "mc(AF f)"} as the least set @{term T} that contains @{term"mc f"} and all states all of whose direct successors are in @{term T}: -*} +*}; (*<*) consts mc :: "formula \ state set"; primrec @@ -73,48 +64,107 @@ "mc(AX f) = {s. \t. (s,t) \ M \ t \ mc f}" "mc(EF f) = lfp(\T. mc f \ M^-1 ^^ T)"(*>*) "mc(AF f) = lfp(af(mc f))"; + +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 fixpoint: +*}; + +lemma mono_af: "mono(af A)"; +apply(simp add: mono_def af_def); +apply blast; +done (*<*) -lemma mono_ef: "mono(\T. A \ M^-1 ^^ T)" -apply(rule monoI) -by(blast) +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) - apply(erule Lfp.induct) - apply(rule mono_ef) - apply(simp) + apply(simp); + apply(erule Lfp.induct); + apply(rule mono_ef); + apply(simp); apply(blast intro: r_into_rtrancl rtrancl_trans); -apply(rule subsetI) -apply(simp, clarify) -apply(erule converse_rtrancl_induct) - apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) - apply(blast) -apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) -by(blast) +apply(rule subsetI); +apply(simp, clarify); +apply(erule converse_rtrancl_induct); + apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]); + apply(blast); +apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]); +by(blast); (*>*) +text{* +All we need to prove now is that @{term mc} and @{text"\"} +agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \ +AF f}"}. This time we prove the two containments separately, starting +with the easy one: +*}; -theorem lfp_subset_AF: -"lfp(af A) \ {s. \ p \ Paths s. \ i. p i \ A}"; +theorem AF_lemma1: + "lfp(af A) \ {s. \ p \ Paths s. \ i. p i \ A}"; + +txt{*\noindent +The proof is again pointwise. Fixpoint induction on the premise @{prop"s \ lfp(af A)"} followed +by simplification and clarification +*}; + apply(rule subsetI); apply(erule Lfp.induct[OF _ mono_af]); -apply(simp add: af_def Paths_def); +apply(clarsimp simp add: af_def Paths_def); +(*ML"Pretty.setmargin 70"; +pr(latex xsymbols symbols);*) +txt{*\noindent +FIXME OF/of with undescore? + +leads to the following somewhat involved proof state +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline +\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A +\end{isabelle} +Now we eliminate the disjunction. The case @{prop"p 0 \ A"} is trivial: +*}; + apply(erule disjE); apply(blast); -apply(clarify); + +txt{*\noindent +In the other case we set @{term t} to @{term"p 1"} and simplify matters: +*}; + apply(erule_tac x = "p 1" in allE); apply(clarsimp); +(*ML"Pretty.setmargin 70"; +pr(latex xsymbols symbols);*) + +txt{* +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A +\end{isabelle} +It merely remains to set @{term pa} to @{term"\i. p(i+1)"}, i.e.\ @{term p} without its +first element. The rest is practically automatic: +*}; + apply(erule_tac x = "\i. p(i+1)" in allE); -apply(simp); -by(blast); +apply simp; +apply blast; +done; text{* -The opposite direction is proved by contradiction: if some state -{term s} is not in @{term"lfp(af A)"}, then we can construct an +The opposite containment is proved by contradiction: if some state +@{term s} is not in @{term"lfp(af A)"}, then we can construct an 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 +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 @@ -127,7 +177,8 @@ "s \ lfp(af A) \ s \ A \ (\ t. (s,t)\M \ t \ lfp(af A))"; apply(erule swap); apply(rule ssubst[OF lfp_Tarski[OF mono_af]]); -by(simp add:af_def); +apply(simp add:af_def); +done; text{*\noindent is proved by a variant of contraposition (@{thm[source]swap}: @@ -146,44 +197,109 @@ text{*\noindent Element @{term"n+1"} on this path is some arbitrary successor -@{term"t"} of element @{term"n"} such that @{term"P t"} holds. Of -course, such a @{term"t"} may in general not exist, but that is of no +@{term t} of element @{term n} such that @{term"P t"} holds. Remember that @{text"SOME t. R t"} +is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of +course, such a @{term t} may in general not exist, but that is of no concern to us since we will only use @{term path} in such cases where a -suitable @{term"t"} does exist. +suitable @{term t} does exist. -Now we prove that if each state @{term"s"} that satisfies @{term"P"} -has a successor that again satisfies @{term"P"}, then there exists an infinite @{term"P"}-path. +Let us show that if each state @{term s} that satisfies @{term P} +has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path: *}; -lemma seq_lemma: -"\ P s; \s. P s \ (\ t. (s,t)\M \ P t) \ \ \p\Paths s. \i. P(p i)"; +lemma infinity_lemma: + "\ P s; \s. P s \ (\ t. (s,t) \ M \ P t) \ \ + \p\Paths s. \i. P(p i)"; txt{*\noindent First we rephrase the conclusion slightly because we need to prove both the path property -and the fact that @{term"P"} holds simultaneously: +and the fact that @{term P} holds simultaneously: *}; -apply(subgoal_tac "\ p. s = p 0 \ (\ i. (p i,p(i+1)) \ M \ P(p i))"); +apply(subgoal_tac "\p. s = p 0 \ (\i. (p i,p(i+1)) \ M \ P(p i))"); txt{*\noindent -From this proposition the original goal follows easily +From this proposition the original goal follows easily: *}; apply(simp add:Paths_def, blast); + +txt{*\noindent +The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}: +*}; + apply(rule_tac x = "path s P" in exI); -apply(simp); -apply(intro strip); +apply(clarsimp); +(*ML"Pretty.setmargin 70"; +pr(latex xsymbols symbols);*) + +txt{*\noindent +After simplification and clarification the subgoal has the following compact form +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright} +\end{isabelle} +and invites a proof by induction on @{term i}: +*}; + apply(induct_tac i); apply(simp); +(*ML"Pretty.setmargin 70"; +pr(latex xsymbols symbols);*) + +txt{*\noindent +After simplification the base case boils down to +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M +\end{isabelle} +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 +is embodied in the theorem @{thm[source]someI2_ex}: +@{thm[display,eta_contract=false]someI2_ex} +When we apply this theorem as an introduction rule, @{text"?P x"} becomes +@{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove +two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and +@{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that +@{text fast} can prove the base case quickly: +*}; + apply(fast intro:someI2_ex); + +txt{*\noindent +What is worth noting here is that we have used @{text fast} rather than @{text blast}. +The reason is that @{text blast} would fail because it cannot cope with @{thm[source]someI2_ex}: +unifying its conclusion with the current subgoal is nontrivial because of the nested schematic +variables. For efficiency reasons @{text blast} does not even attempt such unifications. +Although @{text fast} can in principle cope with complicated unification problems, in practice +the number of unifiers arising is often prohibitive and the offending rule may need to be applied +explicitly rather than automatically. + +The induction step is similar, but more involved, because now we face nested occurrences of +@{text SOME}. We merely show the proof commands but do not describe th details: +*}; + apply(simp); apply(rule someI2_ex); apply(blast); apply(rule someI2_ex); apply(blast); -by(blast); +apply(blast); +done; -lemma seq_lemma: +text{* +Function @{term path} has fulfilled its purpose now and can be forgotten +about. It was merely defined to provide the witness in the proof of the +@{thm[source]infinity_lemma}. Afficionados of minimal proofs might like to know +that we could have given the witness without having to define a new function: +the term +@{term[display]"nat_rec s (\n t. SOME u. (t,u)\M \ P u)"} +where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining +equations we omit, is extensionally equal to @{term"path s P"}. +*}; +(*<*) +lemma infinity_lemma: "\ P s; \ s. P s \ (\ t. (s,t)\M \ P t) \ \ \ p\Paths s. \ i. P(p i)"; apply(subgoal_tac @@ -202,16 +318,70 @@ apply(rule someI2_ex); apply(blast); by(blast); +(*>*) -theorem AF_subset_lfp: +text{* +At last we can prove the opposite direction of @{thm[source]AF_lemma1}: +*}; + +theorem AF_lemma2: "{s. \ p \ Paths s. \ i. p i \ A} \ lfp(af A)"; + +txt{*\noindent +The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule +@{thm contrapos2}): +*}; + apply(rule subsetI); apply(erule contrapos2); apply simp; -apply(drule seq_lemma); -by(auto dest:not_in_lfp_afD); +(*pr(latex xsymbols symbols);*) + +txt{* +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A +\end{isabelle} +Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second +premise of @{thm[source]infinity_lemma} and the original subgoal: +*}; + +apply(drule infinity_lemma); +(*pr(latex xsymbols symbols);*) + +txt{* +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymforall}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}\isanewline +\ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline +\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A +\end{isabelle} +Both are solved automatically: +*}; + apply(auto dest:not_in_lfp_afD); +done; +text{* +The main theorem is proved as for PDL, except that we also derive the necessary equality +@{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} +on the spot: +*} + +theorem "mc f = {s. s \ f}"; +apply(induct_tac f); +apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]); +done + +text{* +Let us close this section with a few words about the executability of @{term mc}. +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 proves that in the case of finite sets and a monotone @{term F}, +@{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until +a fixpoint is reached. It is possible to generate executable functional programs +from HOL definitions, but that is beyond the scope of the tutorial. +*} + +(*<*) (* Second proof of opposite direction, directly by wellfounded induction on the initial segment of M that avoids A. @@ -252,16 +422,11 @@ apply(rule ex_infinite_path); by(auto); -theorem AF_subset_lfp: +theorem AF_lemma2: "{s. \p \ Paths s. \ i. p i \ A} \ lfp(af A)"; apply(rule subsetI); apply(simp); apply(erule Avoid_in_lfp); by(rule Avoid.intros); - -theorem "mc f = {s. s \ f}"; -apply(induct_tac f); -by(auto simp add: EF_lemma equalityI[OF lfp_subset_AF AF_subset_lfp]); - -(*<*)end(*>*) +end(*>*) diff -r 00fdd5c330ea -r a72ddfdbfca0 doc-src/TutorialI/CTL/PDL.thy --- a/doc-src/TutorialI/CTL/PDL.thy Fri Oct 06 01:21:17 2000 +0200 +++ b/doc-src/TutorialI/CTL/PDL.thy Fri Oct 06 12:31:53 2000 +0200 @@ -77,7 +77,8 @@ lemma mono_ef: "mono(\T. A \ M^-1 ^^ T)" apply(rule monoI) -by(blast) +apply blast +done text{*\noindent in order to make sure it really has a least fixpoint. @@ -174,7 +175,8 @@ *} apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) -by(blast) +apply(blast) +done text{* The main theorem is proved in the familiar manner: induction followed by @@ -183,5 +185,6 @@ theorem "mc f = {s. s \ f}"; apply(induct_tac f); -by(auto simp add:EF_lemma); +apply(auto simp add:EF_lemma); +done; (*<*)end(*>*) diff -r 00fdd5c330ea -r a72ddfdbfca0 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Oct 06 01:21:17 2000 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Oct 06 12:31:53 2000 +0200 @@ -14,14 +14,14 @@ \begin{isamarkuptext}% \noindent which stands for "always in the future": -on all paths, at some point the formula holds. -Introducing the notion of paths (in \isa{M})% +on all 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 \ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}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{\isacharparenright}{\isacharbraceright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -allows a very succinct definition of the semantics of \isa{AF}: +This definition allows a very succinct statement of the semantics of \isa{AF}: \footnote{Do not be mislead: neither datatypes nor recursive functions can be extended by new constructors or equations. This is just a trick of the presentation. In reality one has to define a new datatype and a new function.}% @@ -30,40 +30,81 @@ \begin{isamarkuptext}% \noindent Model checking \isa{AF} involves a function which -is just large enough to warrant a separate definition:% +is just complicated enough to warrant a separate definition:% \end{isamarkuptext}% \isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline \ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -This function is monotone in its second argument (and also its first, but -that is irrelevant), and hence \isa{af\ A} has a least fixpoint.% +Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains +\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:% +\end{isamarkuptext}% +{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}% +\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 fixpoint:% \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 -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}% +\isacommand{apply}\ blast\isanewline +\isacommand{done}% \begin{isamarkuptext}% +All we need to prove now is that \isa{mc} and \isa{{\isasymTurnstile}} +agree for \isa{AF}, i.e.\ that \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}. This time we prove the two containments separately, starting +with the easy one:% +\end{isamarkuptext}% +\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{1}{\isacharcolon}\isanewline +\ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}% +\begin{isamarkuptxt}% \noindent -Now we can define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that contains -\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:% -\end{isamarkuptext}% -{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{theorem}\ lfp{\isacharunderscore}subset{\isacharunderscore}AF{\isacharcolon}\isanewline -{\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isanewline +The proof is again pointwise. Fixpoint induction on the premise \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} followed +by simplification and clarification% +\end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}erule\ Lfp{\isachardot}induct{\isacharbrackleft}OF\ {\isacharunderscore}\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +FIXME OF/of with undescore? + +leads to the following somewhat involved proof state +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline +\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A +\end{isabelle} +Now we eliminate the disjunction. The case \isa{p\ \isadigit{0}\ {\isasymin}\ A} is trivial:% +\end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +In the other case we set \isa{t} to \isa{p\ \isadigit{1}} and simplify matters:% +\end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ \isadigit{1}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline +\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A +\end{isabelle} +It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ \isadigit{1}{\isacharparenright}}, i.e.\ \isa{p} without its +first element. The rest is practically automatic:% +\end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}\isadigit{1}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}% +\isacommand{apply}\ simp\isanewline +\isacommand{apply}\ blast\isanewline +\isacommand{done}% \begin{isamarkuptext}% -The opposite direction is proved by contradiction: if some state -{term s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an +The opposite containment is proved by contradiction: if some state +\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an 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 @@ -76,7 +117,8 @@ \ {\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\ swap{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}% +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline +\isacommand{done}% \begin{isamarkuptext}% \noindent is proved by a variant of contraposition (\isa{swap}: @@ -94,113 +136,149 @@ \begin{isamarkuptext}% \noindent Element \isa{n\ {\isacharplus}\ \isadigit{1}} on this path is some arbitrary successor -\isa{t} of element \isa{n} such that \isa{P\ t} holds. Of +\isa{t} of element \isa{n} such that \isa{P\ t} holds. Remember that \isa{SOME\ t{\isachardot}\ R\ t} +is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec-SOME}). Of course, such a \isa{t} may in general not exist, but that is of no concern to us since we will only use \isa{path} in such cases where a suitable \isa{t} does exist. -Now we prove that if each state \isa{s} that satisfies \isa{P} -has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path.% +Let us show that if each state \isa{s} that satisfies \isa{P} +has a successor that again satisfies \isa{P}, then there exists an infinite \isa{P}-path:% \end{isamarkuptext}% -\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline -{\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}% +\isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline +\ \ {\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline +\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ P{\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{P} holds simultaneously:% \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}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}% +\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}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +From this proposition the original goal follows easily:% +\end{isamarkuptxt}% +\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +The new subgoal is proved by providing the witness \isa{path\ s\ P} for \isa{p}:% +\end{isamarkuptxt}% +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +After simplification and clarification the subgoal has the following compact form +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright} +\end{isabelle} +and invites a proof by induction on \isa{i}:% +\end{isamarkuptxt}% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}% \begin{isamarkuptxt}% \noindent -From this proposition the original goal follows easily% +After simplification the base case boils down to +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline +\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M +\end{isabelle} +The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M} +holds. However, we first have to show that such a \isa{t} actually exists! This reasoning +is embodied in the theorem \isa{someI\isadigit{2}{\isacharunderscore}ex}: +\begin{isabelle}% +\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}Eps\ {\isacharquery}P{\isacharparenright}% +\end{isabelle} +When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes +\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove +two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ a}, which follows from the assumptions, and +\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that +\isa{fast} can prove the base case quickly:% \end{isamarkuptxt}% -\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ P{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isanewline -\isacommand{lemma}\ seq{\isacharunderscore}lemma{\isacharcolon}\isanewline -{\isachardoublequote}{\isasymlbrakk}\ P\ s{\isacharsemicolon}\ {\isasymforall}\ s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline -\ {\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}\ i{\isachardot}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline -\ {\isachardoublequote}{\isasymexists}\ p{\isachardot}\ s\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}\ i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}{\isasymin}M\ {\isasymand}\ P{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}{\isasymin}M\ {\isasymand}\ P\ u{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}intro\ strip{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}% +\begin{isamarkuptxt}% +\noindent +What is worth noting here is that we have used \isa{fast} rather than \isa{blast}. +The reason is that \isa{blast} would fail because it cannot cope with \isa{someI\isadigit{2}{\isacharunderscore}ex}: +unifying its conclusion with the current subgoal is nontrivial because of the nested schematic +variables. For efficiency reasons \isa{blast} does not even attempt such unifications. +Although \isa{fast} can in principle cope with complicated unification problems, in practice +the number of unifiers arising is often prohibitive and the offending rule may need to be applied +explicitly rather than automatically. + +The induction step is similar, but more involved, because now we face nested occurrences of +\isa{SOME}. We merely show the proof commands but do not describe th details:% +\end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}rule\ someI\isadigit{2}{\isacharunderscore}ex{\isacharparenright}\isanewline \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isanewline -\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline -{\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +Function \isa{path} has fulfilled its purpose now and can be forgotten +about. It was merely defined to provide the witness in the proof of the +\isa{infinity{\isacharunderscore}lemma}. Afficionados of minimal proofs might like to know +that we could have given the witness without having to define a new function: +the term +\begin{isabelle}% +\ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ u{\isacharparenright}% +\end{isabelle} +where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}, whose defining +equations we omit, is extensionally equal to \isa{path\ s\ P}.% +\end{isamarkuptext}% +% +\begin{isamarkuptext}% +At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma\isadigit{1}}:% +\end{isamarkuptext}% +\isacommand{theorem}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharcolon}\isanewline +{\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}% +\begin{isamarkuptxt}% +\noindent +The proof is again pointwise and then by contraposition (\isa{contrapos\isadigit{2}} is the rule +\isa{{\isasymlbrakk}{\isacharquery}Q{\isacharsemicolon}\ {\isasymnot}\ {\isacharquery}P\ {\isasymLongrightarrow}\ {\isasymnot}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}):% +\end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline \isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline -\isacommand{apply}\ simp\isanewline -\isacommand{apply}{\isacharparenleft}drule\ seq{\isacharunderscore}lemma{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline -\isanewline -\isanewline -\isanewline -\isanewline -\isacommand{consts}\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline -\isacommand{inductive}\ {\isachardoublequote}Avoid\ s\ A{\isachardoublequote}\isanewline -\isakeyword{intros}\ {\isachardoublequote}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline -\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequote}\isanewline -\isanewline -\isanewline -\isacommand{lemma}\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline -{\isachardoublequote}t\ {\isasymin}\ Avoid\ s\ A\ \ {\isasymLongrightarrow}\isanewline -\ {\isasymforall}f{\isachardot}\ t\ {\isacharequal}\ f\ \isadigit{0}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}f\ i{\isacharcomma}\ f\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ f\ i\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ f\ i\ {\isasymnotin}\ A{\isacharparenright}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isachardot}induct{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ allI{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ \isadigit{0}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}force\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline -\isanewline -\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline -{\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}unfold\ af{\isacharunderscore}def{\isacharparenright}\isanewline -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ contrapos\isadigit{2}{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline -\isanewline -\isacommand{theorem}\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharcolon}\isanewline -{\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline -\isacommand{apply}{\isacharparenleft}erule\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}rule\ Avoid{\isachardot}intros{\isacharparenright}\isanewline -\isanewline -\isanewline +\isacommand{apply}\ simp% +\begin{isamarkuptxt}% +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A +\end{isabelle} +Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second +premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:% +\end{isamarkuptxt}% +\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}% +\begin{isamarkuptxt}% +\begin{isabelle} +\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymforall}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}\isanewline +\ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline +\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A +\end{isabelle} +Both are solved automatically:% +\end{isamarkuptxt}% +\ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +The main theorem is proved as for PDL, except that we also derive the necessary equality +\isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma\isadigit{1}} and \isa{AF{\isacharunderscore}lemma\isadigit{2}} +on the spot:% +\end{isamarkuptext}% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ lfp{\isacharunderscore}subset{\isacharunderscore}AF\ AF{\isacharunderscore}subset{\isacharunderscore}lfp{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma\isadigit{1}\ AF{\isacharunderscore}lemma\isadigit{2}{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{done}% +\begin{isamarkuptext}% +Let us close this section with a few words about the executability of \isa{mc}. +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 proves that in the case of finite sets and a monotone \isa{F}, +\isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until +a fixpoint is reached. It is possible to generate executable functional programs +from HOL definitions, but that is beyond the scope of the tutorial.% +\end{isamarkuptext}% \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 00fdd5c330ea -r a72ddfdbfca0 doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Fri Oct 06 01:21:17 2000 +0200 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Fri Oct 06 12:31:53 2000 +0200 @@ -73,7 +73,8 @@ \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{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}% +\isacommand{apply}\ blast\isanewline +\isacommand{done}% \begin{isamarkuptext}% \noindent in order to make sure it really has a least fixpoint. @@ -163,14 +164,16 @@ The proof of the induction step is identical to the one for the base case:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}Tarski{\isacharbrackleft}OF\ mono{\isacharunderscore}ef{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}blast{\isacharparenright}% +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline +\isacommand{done}% \begin{isamarkuptext}% The main theorem is proved in the familiar manner: induction followed by \isa{auto} augmented with the lemma as a simplification rule.% \end{isamarkuptext}% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline -\isacommand{by}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\end{isabellebody}% +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline +\isacommand{done}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root"