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 ***
     1 (*<*)theory PDL = Base:(*>*)

     2

     3 subsection{*Propositional dynamic logic---PDL*}

     4

     5 text{*\index{PDL|(}

     6 The formulae of PDL are built up from atomic propositions via the customary

     7 propositional connectives of negation and conjunction and the two temporal

     8 connectives @{text AX} and @{text EF}. Since formulae are essentially

     9 (syntax) trees, they are naturally modelled as a datatype:

    10 *}

    11

    12 datatype formula = Atom atom

    13                   | Neg formula

    14                   | And formula formula

    15                   | AX formula

    16                   | EF formula

    17

    18 text{*\noindent

    19 This is almost the same as in the boolean expression case study in

    20 \S\ref{sec:boolex}, except that what used to be called @{text Var} is now

    21 called @{term Atom}.

    22

    23 The meaning of these formulae is given by saying which formula is true in

    24 which state:

    25 *}

    26

    27 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool"   ("(_ \<Turnstile> _)" [80,80] 80)

    28

    29 text{*\noindent

    30 The concrete syntax annotation allows us to write @{term"s \<Turnstile> f"} instead of

    31 @{text"valid s f"}.

    32

    33 The definition of @{text"\<Turnstile>"} is by recursion over the syntax:

    34 *}

    35

    36 primrec

    37 "s \<Turnstile> Atom a  = (a \<in> L s)"

    38 "s \<Turnstile> Neg f   = (\<not>(s \<Turnstile> f))"

    39 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"

    40 "s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"

    41 "s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)";

    42

    43 text{*\noindent

    44 The first three equations should be self-explanatory. The temporal formula

    45 @{term"AX f"} means that @{term f} is true in all next states whereas

    46 @{term"EF f"} means that there exists some future state in which @{term f} is

    47 true. The future is expressed via @{text"^*"}, the transitive reflexive

    48 closure. Because of reflexivity, the future includes the present.

    49

    50 Now we come to the model checker itself. It maps a formula into the set of

    51 states where the formula is true and is defined by recursion over the syntax,

    52 too:

    53 *}

    54

    55 consts mc :: "formula \<Rightarrow> state set";

    56 primrec

    57 "mc(Atom a)  = {s. a \<in> L s}"

    58 "mc(Neg f)   = -mc f"

    59 "mc(And f g) = mc f \<inter> mc g"

    60 "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"

    61 "mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"

    62

    63 text{*\noindent

    64 Only the equation for @{term EF} deserves some comments. Remember that the

    65 postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the

    66 converse of a relation and the application of a relation to a set. Thus

    67 @{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least

    68 fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set

    69 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you

    70 find it hard to see that @{term"mc(EF f)"} contains exactly those states from

    71 which there is a path to a state where @{term f} is true, do not worry---that

    72 will be proved in a moment.

    73

    74 First we prove monotonicity of the function inside @{term lfp}

    75 *}

    76

    77 lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)"

    78 apply(rule monoI)

    79 apply blast

    80 done

    81

    82 text{*\noindent

    83 in order to make sure it really has a least fixed point.

    84

    85 Now we can relate model checking and semantics. For the @{text EF} case we need

    86 a separate lemma:

    87 *}

    88

    89 lemma EF_lemma:

    90   "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"

    91

    92 txt{*\noindent

    93 The equality is proved in the canonical fashion by proving that each set

    94 contains the other; the containment is shown pointwise:

    95 *}

    96

    97 apply(rule equalityI);

    98  apply(rule subsetI);

    99  apply(simp)(*<*)apply(rename_tac s)(*>*)

   100

   101 txt{*\noindent

   102 Simplification leaves us with the following first subgoal

   103 @{subgoals[display,indent=0,goals_limit=1]}

   104 which is proved by @{term lfp}-induction:

   105 *}

   106

   107  apply(erule lfp_induct)

   108   apply(rule mono_ef)

   109  apply(simp)

   110 (*pr(latex xsymbols symbols);*)

   111 txt{*\noindent

   112 Having disposed of the monotonicity subgoal,

   113 simplification leaves us with the following main goal

   114 \begin{isabelle}

   115 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ A\ {\isasymor}\isanewline

   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

   117 \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A

   118 \end{isabelle}

   119 which is proved by @{text blast} with the help of transitivity of @{text"^*"}:

   120 *}

   121

   122  apply(blast intro: rtrancl_trans);

   123

   124 txt{*

   125 We now return to the second set containment subgoal, which is again proved

   126 pointwise:

   127 *}

   128

   129 apply(rule subsetI)

   130 apply(simp, clarify)

   131

   132 txt{*\noindent

   133 After simplification and clarification we are left with

   134 @{subgoals[display,indent=0,goals_limit=1]}

   135 This goal is proved by induction on @{term"(s,t)\<in>M^*"}. But since the model

   136 checker works backwards (from @{term t} to @{term s}), we cannot use the

   137 induction theorem @{thm[source]rtrancl_induct} because it works in the

   138 forward direction. Fortunately the converse induction theorem

   139 @{thm[source]converse_rtrancl_induct} already exists:

   140 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]}

   141 It says that if @{prop"(a,b):r^*"} and we know @{prop"P b"} then we can infer

   142 @{prop"P a"} provided each step backwards from a predecessor @{term z} of

   143 @{term b} preserves @{term P}.

   144 *}

   145

   146 apply(erule converse_rtrancl_induct)

   147

   148 txt{*\noindent

   149 The base case

   150 @{subgoals[display,indent=0,goals_limit=1]}

   151 is solved by unrolling @{term lfp} once

   152 *}

   153

   154  apply(rule ssubst[OF lfp_unfold[OF mono_ef]])

   155

   156 txt{*

   157 @{subgoals[display,indent=0,goals_limit=1]}

   158 and disposing of the resulting trivial subgoal automatically:

   159 *}

   160

   161  apply(blast)

   162

   163 txt{*\noindent

   164 The proof of the induction step is identical to the one for the base case:

   165 *}

   166

   167 apply(rule ssubst[OF lfp_unfold[OF mono_ef]])

   168 apply(blast)

   169 done

   170

   171 text{*

   172 The main theorem is proved in the familiar manner: induction followed by

   173 @{text auto} augmented with the lemma as a simplification rule.

   174 *}

   175

   176 theorem "mc f = {s. s \<Turnstile> f}";

   177 apply(induct_tac f);

   178 apply(auto simp add:EF_lemma);

   179 done;

   180

   181 text{*

   182 \begin{exercise}

   183 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}

   184 as that is the ASCII equivalent of @{text"\<exists>"}}

   185 (there exists a next state such that'') with the intended semantics

   186 @{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}

   187 Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?

   188

   189 Show that the semantics for @{term EF} satisfies the following recursion equation:

   190 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}

   191 \end{exercise}

   192 \index{PDL|)}

   193 *}

   194 (*<*)

   195 theorem main: "mc f = {s. s \<Turnstile> f}";

   196 apply(induct_tac f);

   197 apply(auto simp add:EF_lemma);

   198 done;

   199

   200 lemma aux: "s \<Turnstile> f = (s : mc f)";

   201 apply(simp add:main);

   202 done;

   203

   204 lemma "(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> Neg(AX(Neg(EF f))))";

   205 apply(simp only:aux);

   206 apply(simp);

   207 apply(rule ssubst[OF lfp_unfold[OF mono_ef]], fast);

   208 done

   209

   210 end

   211 (*>*)