doc-src/TutorialI/CTL/PDL.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10524 270b285d48ee child 10800 2d4c058749a7 permissions -rw-r--r--
*** empty log message ***
 nipkow@10122  1 (*<*)theory PDL = Base:(*>*)  nipkow@9958  2 nipkow@10178  3 subsection{*Propositional dynamic logic---PDL*}  nipkow@9958  4 nipkow@10178  5 text{*\index{PDL|(}  nipkow@10133  6 The formulae of PDL are built up from atomic propositions via the customary  nipkow@10133  7 propositional connectives of negation and conjunction and the two temporal  nipkow@10133  8 connectives @{text AX} and @{text EF}. Since formulae are essentially  nipkow@10133  9 (syntax) trees, they are naturally modelled as a datatype:  nipkow@10133  10 *}  nipkow@9958  11 nipkow@10149  12 datatype formula = Atom atom  nipkow@10149  13  | Neg formula  nipkow@10149  14  | And formula formula  nipkow@10149  15  | AX formula  nipkow@10149  16  | EF formula  nipkow@10133  17 nipkow@10133  18 text{*\noindent  nipkow@10149  19 This is almost the same as in the boolean expression case study in  nipkow@10149  20 \S\ref{sec:boolex}, except that what used to be called @{text Var} is now  nipkow@10149  21 called @{term Atom}.  nipkow@10149  22 nipkow@10133  23 The meaning of these formulae is given by saying which formula is true in  nipkow@10133  24 which state:  nipkow@10133  25 *}  nipkow@10133  26 nipkow@10149  27 consts valid :: "state \ formula \ bool" ("(_ \ _)" [80,80] 80)  nipkow@10149  28 nipkow@10149  29 text{*\noindent  nipkow@10149  30 The concrete syntax annotation allows us to write @{term"s \ f"} instead of  nipkow@10149  31 @{text"valid s f"}.  nipkow@10149  32 nipkow@10149  33 The definition of @{text"\"} is by recursion over the syntax:  nipkow@10149  34 *}  nipkow@9958  35 nipkow@9958  36 primrec  nipkow@10133  37 "s \ Atom a = (a \ L s)"  nipkow@10149  38 "s \ Neg f = (\(s \ f))"  nipkow@9958  39 "s \ And f g = (s \ f \ s \ g)"  nipkow@9958  40 "s \ AX f = (\t. (s,t) \ M \ t \ f)"  nipkow@9958  41 "s \ EF f = (\t. (s,t) \ M^* \ t \ f)";  nipkow@9958  42 nipkow@10149  43 text{*\noindent  nipkow@10149  44 The first three equations should be self-explanatory. The temporal formula  nipkow@10149  45 @{term"AX f"} means that @{term f} is true in all next states whereas  nipkow@10149  46 @{term"EF f"} means that there exists some future state in which @{term f} is  nipkow@10149  47 true. The future is expressed via @{text"^*"}, the transitive reflexive  nipkow@10149  48 closure. Because of reflexivity, the future includes the present.  nipkow@10149  49 nipkow@10133  50 Now we come to the model checker itself. It maps a formula into the set of  nipkow@10149  51 states where the formula is true and is defined by recursion over the syntax,  nipkow@10149  52 too:  nipkow@10133  53 *}  nipkow@10133  54 nipkow@10149  55 consts mc :: "formula \ state set";  nipkow@9958  56 primrec  nipkow@10133  57 "mc(Atom a) = {s. a \ L s}"  nipkow@10149  58 "mc(Neg f) = -mc f"  nipkow@10133  59 "mc(And f g) = mc f \ mc g"  nipkow@9958  60 "mc(AX f) = {s. \t. (s,t) \ M \ t \ mc f}"  nipkow@10133  61 "mc(EF f) = lfp(\T. mc f \ M^-1 ^^ T)"  nipkow@10133  62 nipkow@10149  63 text{*\noindent  nipkow@10149  64 Only the equation for @{term EF} deserves some comments. Remember that the  nipkow@10149  65 postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the  nipkow@10149  66 converse of a relation and the application of a relation to a set. Thus  nipkow@10149  67 @{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least  nipkow@10242  68 fixed point (@{term lfp}) of @{term"\T. mc f \ M^-1 ^^ T"} is the least set  nipkow@10149  69 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you  nipkow@10149  70 find it hard to see that @{term"mc(EF f)"} contains exactly those states from  nipkow@10149  71 which there is a path to a state where @{term f} is true, do not worry---that  nipkow@10149  72 will be proved in a moment.  nipkow@10149  73 nipkow@10149  74 First we prove monotonicity of the function inside @{term lfp}  nipkow@10133  75 *}  nipkow@10133  76 nipkow@10149  77 lemma mono_ef: "mono(\T. A \ M^-1 ^^ T)"  nipkow@10149  78 apply(rule monoI)  nipkow@10159  79 apply blast  nipkow@10159  80 done  nipkow@10149  81 nipkow@10149  82 text{*\noindent  nipkow@10242  83 in order to make sure it really has a least fixed point.  nipkow@9958  84 nipkow@10149  85 Now we can relate model checking and semantics. For the @{text EF} case we need  nipkow@10149  86 a separate lemma:  nipkow@10149  87 *}  nipkow@10149  88 nipkow@10149  89 lemma EF_lemma:  nipkow@10149  90  "lfp(\T. A \ M^-1 ^^ T) = {s. \t. (s,t) \ M^* \ t \ A}"  nipkow@10149  91 nipkow@10149  92 txt{*\noindent  nipkow@10149  93 The equality is proved in the canonical fashion by proving that each set  nipkow@10149  94 contains the other; the containment is shown pointwise:  nipkow@10149  95 *}  nipkow@10149  96 nipkow@9958  97 apply(rule equalityI);  nipkow@9958  98  apply(rule subsetI);  nipkow@10524  99  apply(simp)(*<*)apply(rename_tac s)(*>*)  nipkow@10363  100 nipkow@10149  101 txt{*\noindent  nipkow@10149  102 Simplification leaves us with the following first subgoal  nipkow@10363  103 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@10149  104 which is proved by @{term lfp}-induction:  nipkow@10149  105 *}  nipkow@10149  106 wenzelm@10210  107  apply(erule lfp_induct)  nipkow@10149  108  apply(rule mono_ef)  nipkow@10149  109  apply(simp)  nipkow@10149  110 (*pr(latex xsymbols symbols);*)  nipkow@10149  111 txt{*\noindent  nipkow@10149  112 Having disposed of the monotonicity subgoal,  nipkow@10149  113 simplification leaves us with the following main goal  nipkow@10149  114 \begin{isabelle}  nipkow@10149  115 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ A\ {\isasymor}\isanewline  nipkow@10149  116 \ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline  nipkow@10149  117 \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A  nipkow@10149  118 \end{isabelle}  nipkow@10212  119 which is proved by @{text blast} with the help of transitivity of @{text"^*"}:  nipkow@10149  120 *}  nipkow@10149  121 nipkow@10212  122  apply(blast intro: rtrancl_trans);  nipkow@10149  123 nipkow@10149  124 txt{*  nipkow@10149  125 We now return to the second set containment subgoal, which is again proved  nipkow@10149  126 pointwise:  nipkow@10149  127 *}  nipkow@10149  128 nipkow@10149  129 apply(rule subsetI)  nipkow@10149  130 apply(simp, clarify)  nipkow@10363  131 nipkow@10149  132 txt{*\noindent  nipkow@10149  133 After simplification and clarification we are left with  nipkow@10363  134 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@10149  135 This goal is proved by induction on @{term"(s,t)\M^*"}. But since the model  nipkow@10149  136 checker works backwards (from @{term t} to @{term s}), we cannot use the  nipkow@10149  137 induction theorem @{thm[source]rtrancl_induct} because it works in the  nipkow@10149  138 forward direction. Fortunately the converse induction theorem  nipkow@10149  139 @{thm[source]converse_rtrancl_induct} already exists:  nipkow@10149  140 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]}  nipkow@10149  141 It says that if @{prop"(a,b):r^*"} and we know @{prop"P b"} then we can infer  nipkow@10149  142 @{prop"P a"} provided each step backwards from a predecessor @{term z} of  nipkow@10149  143 @{term b} preserves @{term P}.  nipkow@10149  144 *}  nipkow@10149  145 nipkow@10149  146 apply(erule converse_rtrancl_induct)  nipkow@10363  147 nipkow@10149  148 txt{*\noindent  nipkow@10149  149 The base case  nipkow@10363  150 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@10149  151 is solved by unrolling @{term lfp} once  nipkow@10149  152 *}  nipkow@10149  153 nipkow@10186  154  apply(rule ssubst[OF lfp_unfold[OF mono_ef]])  nipkow@10363  155 nipkow@10149  156 txt{*  nipkow@10363  157 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@10149  158 and disposing of the resulting trivial subgoal automatically:  nipkow@10149  159 *}  nipkow@10149  160 nipkow@10149  161  apply(blast)  nipkow@10149  162 nipkow@10149  163 txt{*\noindent  nipkow@10149  164 The proof of the induction step is identical to the one for the base case:  nipkow@10149  165 *}  nipkow@10149  166 nipkow@10186  167 apply(rule ssubst[OF lfp_unfold[OF mono_ef]])  nipkow@10159  168 apply(blast)  nipkow@10159  169 done  nipkow@10149  170 nipkow@10149  171 text{*  nipkow@10149  172 The main theorem is proved in the familiar manner: induction followed by  nipkow@10149  173 @{text auto} augmented with the lemma as a simplification rule.  nipkow@10149  174 *}  nipkow@9958  175 nipkow@9958  176 theorem "mc f = {s. s \ f}";  nipkow@9958  177 apply(induct_tac f);  nipkow@10159  178 apply(auto simp add:EF_lemma);  nipkow@10159  179 done;  nipkow@10171  180 nipkow@10171  181 text{*  nipkow@10171  182 \begin{exercise}  nipkow@10171  183 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}  nipkow@10171  184 as that is the ASCII equivalent of @{text"\"}}  nipkow@10171  185 (there exists a next state such that'') with the intended semantics  nipkow@10171  186 @{prop[display]"(s \ EN f) = (EX t. (s,t) : M & t \ f)"}  nipkow@10171  187 Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?  nipkow@10171  188 nipkow@10171  189 Show that the semantics for @{term EF} satisfies the following recursion equation:  nipkow@10171  190 @{prop[display]"(s \ EF f) = (s \ f | s \ EN(EF f))"}  nipkow@10171  191 \end{exercise}  nipkow@10178  192 \index{PDL|)}  nipkow@10171  193 *}  nipkow@10171  194 (*<*)  nipkow@10171  195 theorem main: "mc f = {s. s \ f}";  nipkow@10171  196 apply(induct_tac f);  nipkow@10171  197 apply(auto simp add:EF_lemma);  nipkow@10171  198 done;  nipkow@10171  199 nipkow@10171  200 lemma aux: "s \ f = (s : mc f)";  nipkow@10171  201 apply(simp add:main);  nipkow@10171  202 done;  nipkow@10171  203 nipkow@10171  204 lemma "(s \ EF f) = (s \ f | s \ Neg(AX(Neg(EF f))))";  nipkow@10171  205 apply(simp only:aux);  nipkow@10171  206 apply(simp);  nipkow@10186  207 apply(rule ssubst[OF lfp_unfold[OF mono_ef]], fast);  nipkow@10171  208 done  nipkow@10171  209 nipkow@10171  210 end  nipkow@10171  211 (*>*)