7 propositional connectives of negation and conjunction and the two temporal |
7 propositional connectives of negation and conjunction and the two temporal |
8 connectives @{text AX} and @{text EF}. Since formulae are essentially |
8 connectives @{text AX} and @{text EF}. Since formulae are essentially |
9 (syntax) trees, they are naturally modelled as a datatype: |
9 (syntax) trees, they are naturally modelled as a datatype: |
10 *} |
10 *} |
11 |
11 |
12 datatype pdl_form = Atom atom |
12 datatype formula = Atom atom |
13 | NOT pdl_form |
13 | Neg formula |
14 | And pdl_form pdl_form |
14 | And formula formula |
15 | AX pdl_form |
15 | AX formula |
16 | EF pdl_form; |
16 | EF formula |
17 |
17 |
18 text{*\noindent |
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 |
19 The meaning of these formulae is given by saying which formula is true in |
23 The meaning of these formulae is given by saying which formula is true in |
20 which state: |
24 which state: |
21 *} |
25 *} |
22 |
26 |
23 consts valid :: "state \<Rightarrow> pdl_form \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) |
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 *} |
24 |
35 |
25 primrec |
36 primrec |
26 "s \<Turnstile> Atom a = (a \<in> L s)" |
37 "s \<Turnstile> Atom a = (a \<in> L s)" |
27 "s \<Turnstile> NOT f = (\<not>(s \<Turnstile> f))" |
38 "s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))" |
28 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
39 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
29 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" |
40 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" |
30 "s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"; |
41 "s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"; |
31 |
42 |
32 text{* |
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 |
33 Now we come to the model checker itself. It maps a formula into the set of |
50 Now we come to the model checker itself. It maps a formula into the set of |
34 states where the formula is true and is defined by recursion over the syntax: |
51 states where the formula is true and is defined by recursion over the syntax, |
|
52 too: |
35 *} |
53 *} |
36 |
54 |
37 consts mc :: "pdl_form \<Rightarrow> state set"; |
55 consts mc :: "formula \<Rightarrow> state set"; |
38 primrec |
56 primrec |
39 "mc(Atom a) = {s. a \<in> L s}" |
57 "mc(Atom a) = {s. a \<in> L s}" |
40 "mc(NOT f) = -mc f" |
58 "mc(Neg f) = -mc f" |
41 "mc(And f g) = mc f \<inter> mc g" |
59 "mc(And f g) = mc f \<inter> mc g" |
42 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
60 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" |
43 "mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)" |
61 "mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)" |
44 |
62 |
45 |
63 |
46 text{* |
64 text{*\noindent |
47 Only the equation for @{term EF} deserves a comment: the postfix @{text"^-1"} |
65 Only the equation for @{term EF} deserves some comments. Remember that the |
48 and the infix @{text"^^"} are predefined and denote the converse of a |
66 postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the |
49 relation and the application of a relation to a set. Thus @{term "M^-1 ^^ T"} |
67 converse of a relation and the application of a relation to a set. Thus |
50 is the set of all predecessors of @{term T} and @{term"mc(EF f)"} is the least |
68 @{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least |
51 set @{term T} containing @{term"mc f"} and all predecessors of @{term T}. |
69 fixpoint (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set |
|
70 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you |
|
71 find it hard to see that @{term"mc(EF f)"} contains exactly those states from |
|
72 which there is a path to a state where @{term f} is true, do not worry---that |
|
73 will be proved in a moment. |
|
74 |
|
75 First we prove monotonicity of the function inside @{term lfp} |
52 *} |
76 *} |
53 |
77 |
54 lemma mono_lemma: "mono(\<lambda>T. A \<union> M^-1 ^^ T)" |
78 lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)" |
55 apply(rule monoI); |
79 apply(rule monoI) |
56 by(blast); |
80 by(blast) |
57 |
81 |
58 lemma lfp_conv_EF: |
82 text{*\noindent |
59 "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"; |
83 in order to make sure it really has a least fixpoint. |
|
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 |
60 apply(rule equalityI); |
97 apply(rule equalityI); |
61 apply(rule subsetI); |
98 apply(rule subsetI); |
62 apply(simp); |
99 apply(simp) |
63 apply(erule Lfp.induct); |
100 (*pr(latex xsymbols symbols);*) |
64 apply(rule mono_lemma); |
101 txt{*\noindent |
65 apply(simp); |
102 Simplification leaves us with the following first subgoal |
|
103 \begin{isabelle} |
|
104 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
|
105 \end{isabelle} |
|
106 which is proved by @{term lfp}-induction: |
|
107 *} |
|
108 |
|
109 apply(erule Lfp.induct) |
|
110 apply(rule mono_ef) |
|
111 apply(simp) |
|
112 (*pr(latex xsymbols symbols);*) |
|
113 txt{*\noindent |
|
114 Having disposed of the monotonicity subgoal, |
|
115 simplification leaves us with the following main goal |
|
116 \begin{isabelle} |
|
117 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ A\ {\isasymor}\isanewline |
|
118 \ \ \ \ \ \ \ \ \ 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 |
|
119 \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A |
|
120 \end{isabelle} |
|
121 which is proved by @{text blast} with the help of a few lemmas about |
|
122 @{text"^*"}: |
|
123 *} |
|
124 |
66 apply(blast intro: r_into_rtrancl rtrancl_trans); |
125 apply(blast intro: r_into_rtrancl rtrancl_trans); |
67 apply(rule subsetI); |
126 |
68 apply(simp); |
127 txt{* |
69 apply(erule exE); |
128 We now return to the second set containment subgoal, which is again proved |
70 apply(erule conjE); |
129 pointwise: |
71 apply(erule_tac P = "t\<in>A" in rev_mp); |
130 *} |
72 apply(erule converse_rtrancl_induct); |
131 |
73 apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]); |
132 apply(rule subsetI) |
74 apply(blast); |
133 apply(simp, clarify) |
75 apply(rule ssubst[OF lfp_Tarski[OF mono_lemma]]); |
134 (*pr(latex xsymbols symbols);*) |
76 by(blast); |
135 txt{*\noindent |
|
136 After simplification and clarification we are left with |
|
137 \begin{isabelle} |
|
138 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright} |
|
139 \end{isabelle} |
|
140 This goal is proved by induction on @{term"(s,t)\<in>M^*"}. But since the model |
|
141 checker works backwards (from @{term t} to @{term s}), we cannot use the |
|
142 induction theorem @{thm[source]rtrancl_induct} because it works in the |
|
143 forward direction. Fortunately the converse induction theorem |
|
144 @{thm[source]converse_rtrancl_induct} already exists: |
|
145 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]} |
|
146 It says that if @{prop"(a,b):r^*"} and we know @{prop"P b"} then we can infer |
|
147 @{prop"P a"} provided each step backwards from a predecessor @{term z} of |
|
148 @{term b} preserves @{term P}. |
|
149 *} |
|
150 |
|
151 apply(erule converse_rtrancl_induct) |
|
152 (*pr(latex xsymbols symbols);*) |
|
153 txt{*\noindent |
|
154 The base case |
|
155 \begin{isabelle} |
|
156 \ \isadigit{1}{\isachardot}\ {\isasymAnd}t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright} |
|
157 \end{isabelle} |
|
158 is solved by unrolling @{term lfp} once |
|
159 *} |
|
160 |
|
161 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) |
|
162 (*pr(latex xsymbols symbols);*) |
|
163 txt{* |
|
164 \begin{isabelle} |
|
165 \ \isadigit{1}{\isachardot}\ {\isasymAnd}t{\isachardot}\ t\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright} |
|
166 \end{isabelle} |
|
167 and disposing of the resulting trivial subgoal automatically: |
|
168 *} |
|
169 |
|
170 apply(blast) |
|
171 |
|
172 txt{*\noindent |
|
173 The proof of the induction step is identical to the one for the base case: |
|
174 *} |
|
175 |
|
176 apply(rule ssubst[OF lfp_Tarski[OF mono_ef]]) |
|
177 by(blast) |
|
178 |
|
179 text{* |
|
180 The main theorem is proved in the familiar manner: induction followed by |
|
181 @{text auto} augmented with the lemma as a simplification rule. |
|
182 *} |
77 |
183 |
78 theorem "mc f = {s. s \<Turnstile> f}"; |
184 theorem "mc f = {s. s \<Turnstile> f}"; |
79 apply(induct_tac f); |
185 apply(induct_tac f); |
80 by(auto simp add:lfp_conv_EF); |
186 by(auto simp add:EF_lemma); |
81 (*<*)end(*>*) |
187 (*<*)end(*>*) |