doc-src/TutorialI/CTL/CTL.thy
author nipkow
Thu Oct 12 18:38:23 2000 +0200 (2000-10-12)
changeset 10212 33fe2d701ddd
parent 10210 e8aa81362f41
child 10217 e61e7e1eacaf
permissions -rw-r--r--
*** empty log message ***
nipkow@10159
     1
(*<*)theory CTL = Base:;(*>*)
nipkow@9958
     2
nipkow@10159
     3
subsection{*Computation tree logic---CTL*};
nipkow@9958
     4
nipkow@10212
     5
text{*\label{sec:CTL}
nipkow@10149
     6
The semantics of PDL only needs transitive reflexive closure.
nipkow@10149
     7
Let us now be a bit more adventurous and introduce a new temporal operator
nipkow@10149
     8
that goes beyond transitive reflexive closure. We extend the datatype
nipkow@10149
     9
@{text formula} by a new constructor
nipkow@10159
    10
*};
nipkow@10149
    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@10159
    17
                  | AF formula;
nipkow@9958
    18
nipkow@10149
    19
text{*\noindent
nipkow@10149
    20
which stands for "always in the future":
nipkow@10159
    21
on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
nipkow@10159
    22
in HOL: it is simply a function from @{typ nat} to @{typ state}.
nipkow@10159
    23
*};
nipkow@9958
    24
nipkow@9958
    25
constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set"
nipkow@10149
    26
         "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
nipkow@10149
    27
nipkow@10149
    28
text{*\noindent
nipkow@10159
    29
This definition allows a very succinct statement of the semantics of @{term AF}:
nipkow@10149
    30
\footnote{Do not be mislead: neither datatypes nor recursive functions can be
nipkow@10149
    31
extended by new constructors or equations. This is just a trick of the
nipkow@10149
    32
presentation. In reality one has to define a new datatype and a new function.}
nipkow@10159
    33
*};
nipkow@10149
    34
(*<*)
nipkow@10159
    35
consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
nipkow@9958
    36
nipkow@9958
    37
primrec
nipkow@10133
    38
"s \<Turnstile> Atom a  =  (a \<in> L s)"
nipkow@10149
    39
"s \<Turnstile> Neg f   = (~(s \<Turnstile> f))"
nipkow@9958
    40
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
nipkow@9958
    41
"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
nipkow@9958
    42
"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
nipkow@10149
    43
(*>*)
nipkow@9958
    44
"s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
nipkow@9958
    45
nipkow@10149
    46
text{*\noindent
nipkow@10149
    47
Model checking @{term AF} involves a function which
nipkow@10159
    48
is just complicated enough to warrant a separate definition:
nipkow@10159
    49
*};
nipkow@10149
    50
nipkow@9958
    51
constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set"
nipkow@10149
    52
         "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
nipkow@10149
    53
nipkow@10149
    54
text{*\noindent
nipkow@10159
    55
Now we define @{term "mc(AF f)"} as the least set @{term T} that contains
nipkow@10149
    56
@{term"mc f"} and all states all of whose direct successors are in @{term T}:
nipkow@10159
    57
*};
nipkow@10149
    58
(*<*)
nipkow@10149
    59
consts mc :: "formula \<Rightarrow> state set";
nipkow@9958
    60
primrec
nipkow@10133
    61
"mc(Atom a)  = {s. a \<in> L s}"
nipkow@10149
    62
"mc(Neg f)   = -mc f"
nipkow@9958
    63
"mc(And f g) = mc f \<inter> mc g"
nipkow@9958
    64
"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
nipkow@10149
    65
"mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"(*>*)
nipkow@9958
    66
"mc(AF f)    = lfp(af(mc f))";
nipkow@10159
    67
nipkow@10159
    68
text{*\noindent
nipkow@10159
    69
Because @{term af} is monotone in its second argument (and also its first, but
nipkow@10159
    70
that is irrelevant) @{term"af A"} has a least fixpoint:
nipkow@10159
    71
*};
nipkow@10159
    72
nipkow@10159
    73
lemma mono_af: "mono(af A)";
nipkow@10159
    74
apply(simp add: mono_def af_def);
nipkow@10159
    75
apply blast;
nipkow@10159
    76
done
nipkow@10149
    77
(*<*)
nipkow@10159
    78
lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)";
nipkow@10159
    79
apply(rule monoI);
nipkow@10159
    80
by(blast);
nipkow@9958
    81
nipkow@10149
    82
lemma EF_lemma:
nipkow@10159
    83
  "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
nipkow@9958
    84
apply(rule equalityI);
nipkow@9958
    85
 apply(rule subsetI);
nipkow@10159
    86
 apply(simp);
wenzelm@10210
    87
 apply(erule lfp_induct);
nipkow@10159
    88
  apply(rule mono_ef);
nipkow@10159
    89
 apply(simp);
nipkow@9958
    90
 apply(blast intro: r_into_rtrancl rtrancl_trans);
nipkow@10159
    91
apply(rule subsetI);
nipkow@10159
    92
apply(simp, clarify);
nipkow@10159
    93
apply(erule converse_rtrancl_induct);
nipkow@10186
    94
 apply(rule ssubst[OF lfp_unfold[OF mono_ef]]);
nipkow@10159
    95
 apply(blast);
nipkow@10186
    96
apply(rule ssubst[OF lfp_unfold[OF mono_ef]]);
nipkow@10159
    97
by(blast);
nipkow@10149
    98
(*>*)
nipkow@10159
    99
text{*
nipkow@10159
   100
All we need to prove now is that @{term mc} and @{text"\<Turnstile>"}
nipkow@10159
   101
agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \<Turnstile>
nipkow@10159
   102
AF f}"}. This time we prove the two containments separately, starting
nipkow@10159
   103
with the easy one:
nipkow@10159
   104
*};
nipkow@9958
   105
nipkow@10159
   106
theorem AF_lemma1:
nipkow@10159
   107
  "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
nipkow@10159
   108
nipkow@10159
   109
txt{*\noindent
nipkow@10159
   110
The proof is again pointwise. Fixpoint induction on the premise @{prop"s \<in> lfp(af A)"} followed
nipkow@10159
   111
by simplification and clarification
nipkow@10159
   112
*};
nipkow@10159
   113
nipkow@9958
   114
apply(rule subsetI);
wenzelm@10210
   115
apply(erule lfp_induct[OF _ mono_af]);
nipkow@10159
   116
apply(clarsimp simp add: af_def Paths_def);
nipkow@10159
   117
(*ML"Pretty.setmargin 70";
nipkow@10159
   118
pr(latex xsymbols symbols);*)
nipkow@10159
   119
txt{*\noindent
nipkow@10159
   120
leads to the following somewhat involved proof state
nipkow@10159
   121
\begin{isabelle}
nipkow@10159
   122
\ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
nipkow@10159
   123
\ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
nipkow@10159
   124
\ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
nipkow@10159
   125
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\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
nipkow@10159
   126
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
nipkow@10159
   127
\ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
nipkow@10159
   128
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
nipkow@10159
   129
\end{isabelle}
nipkow@10159
   130
Now we eliminate the disjunction. The case @{prop"p 0 \<in> A"} is trivial:
nipkow@10159
   131
*};
nipkow@10159
   132
nipkow@9958
   133
apply(erule disjE);
nipkow@9958
   134
 apply(blast);
nipkow@10159
   135
nipkow@10159
   136
txt{*\noindent
nipkow@10159
   137
In the other case we set @{term t} to @{term"p 1"} and simplify matters:
nipkow@10159
   138
*};
nipkow@10159
   139
nipkow@9958
   140
apply(erule_tac x = "p 1" in allE);
nipkow@9958
   141
apply(clarsimp);
nipkow@10159
   142
(*ML"Pretty.setmargin 70";
nipkow@10159
   143
pr(latex xsymbols symbols);*)
nipkow@10159
   144
nipkow@10159
   145
txt{*
nipkow@10159
   146
\begin{isabelle}
nipkow@10159
   147
\ \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
nipkow@10159
   148
\ \ \ \ \ \ \ \ \ \ \ {\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
nipkow@10159
   149
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
nipkow@10159
   150
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
nipkow@10159
   151
\end{isabelle}
nipkow@10159
   152
It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1)"}, i.e.\ @{term p} without its
nipkow@10159
   153
first element. The rest is practically automatic:
nipkow@10159
   154
*};
nipkow@10159
   155
nipkow@9958
   156
apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
nipkow@10159
   157
apply simp;
nipkow@10159
   158
apply blast;
nipkow@10159
   159
done;
nipkow@9958
   160
nipkow@9958
   161
text{*
nipkow@10159
   162
The opposite containment is proved by contradiction: if some state
nipkow@10159
   163
@{term s} is not in @{term"lfp(af A)"}, then we can construct an
nipkow@9958
   164
infinite @{term A}-avoiding path starting from @{term s}. The reason is
nipkow@10159
   165
that by unfolding @{term lfp} we find that if @{term s} is not in
nipkow@9958
   166
@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
nipkow@9958
   167
direct successor of @{term s} that is again not in @{term"lfp(af
nipkow@9958
   168
A)"}. Iterating this argument yields the promised infinite
nipkow@9958
   169
@{term A}-avoiding path. Let us formalize this sketch.
nipkow@9958
   170
nipkow@9958
   171
The one-step argument in the above sketch
nipkow@9958
   172
*};
nipkow@9958
   173
nipkow@9958
   174
lemma not_in_lfp_afD:
nipkow@9958
   175
 "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
nipkow@9958
   176
apply(erule swap);
nipkow@10186
   177
apply(rule ssubst[OF lfp_unfold[OF mono_af]]);
nipkow@10159
   178
apply(simp add:af_def);
nipkow@10159
   179
done;
nipkow@9958
   180
nipkow@9958
   181
text{*\noindent
nipkow@9958
   182
is proved by a variant of contraposition (@{thm[source]swap}:
nipkow@9958
   183
@{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion
nipkow@9958
   184
and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
nipkow@9958
   185
simplifying with the definition of @{term af} finishes the proof.
nipkow@9958
   186
nipkow@9958
   187
Now we iterate this process. The following construction of the desired
nipkow@9958
   188
path is parameterized by a predicate @{term P} that should hold along the path:
nipkow@9958
   189
*};
nipkow@9958
   190
nipkow@9958
   191
consts path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)";
nipkow@9958
   192
primrec
nipkow@9958
   193
"path s P 0 = s"
nipkow@9958
   194
"path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)";
nipkow@9958
   195
nipkow@9958
   196
text{*\noindent
nipkow@9958
   197
Element @{term"n+1"} on this path is some arbitrary successor
nipkow@10159
   198
@{term t} of element @{term n} such that @{term"P t"} holds.  Remember that @{text"SOME t. R t"}
nipkow@10159
   199
is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of
nipkow@10159
   200
course, such a @{term t} may in general not exist, but that is of no
nipkow@9958
   201
concern to us since we will only use @{term path} in such cases where a
nipkow@10159
   202
suitable @{term t} does exist.
nipkow@9958
   203
nipkow@10159
   204
Let us show that if each state @{term s} that satisfies @{term P}
nipkow@10159
   205
has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path:
nipkow@9958
   206
*};
nipkow@9958
   207
nipkow@10159
   208
lemma infinity_lemma:
nipkow@10159
   209
  "\<lbrakk> P s; \<forall>s. P s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> P t) \<rbrakk> \<Longrightarrow>
nipkow@10159
   210
   \<exists>p\<in>Paths s. \<forall>i. P(p i)";
nipkow@9958
   211
nipkow@9958
   212
txt{*\noindent
nipkow@9958
   213
First we rephrase the conclusion slightly because we need to prove both the path property
nipkow@10159
   214
and the fact that @{term P} holds simultaneously:
nipkow@9958
   215
*};
nipkow@9958
   216
nipkow@10159
   217
apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> P(p i))");
nipkow@9958
   218
nipkow@9958
   219
txt{*\noindent
nipkow@10159
   220
From this proposition the original goal follows easily:
nipkow@9958
   221
*};
nipkow@9958
   222
nipkow@9958
   223
 apply(simp add:Paths_def, blast);
nipkow@10159
   224
nipkow@10159
   225
txt{*\noindent
nipkow@10159
   226
The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}:
nipkow@10159
   227
*};
nipkow@10159
   228
nipkow@9958
   229
apply(rule_tac x = "path s P" in exI);
nipkow@10159
   230
apply(clarsimp);
nipkow@10159
   231
(*ML"Pretty.setmargin 70";
nipkow@10159
   232
pr(latex xsymbols symbols);*)
nipkow@10159
   233
nipkow@10159
   234
txt{*\noindent
nipkow@10159
   235
After simplification and clarification the subgoal has the following compact form
nipkow@10159
   236
\begin{isabelle}
nipkow@10159
   237
\ \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
nipkow@10159
   238
\ \ \ \ \ \ \ \ {\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
nipkow@10159
   239
\ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
nipkow@10159
   240
\end{isabelle}
nipkow@10159
   241
and invites a proof by induction on @{term i}:
nipkow@10159
   242
*};
nipkow@10159
   243
nipkow@9958
   244
apply(induct_tac i);
nipkow@9958
   245
 apply(simp);
nipkow@10159
   246
(*ML"Pretty.setmargin 70";
nipkow@10159
   247
pr(latex xsymbols symbols);*)
nipkow@10159
   248
nipkow@10159
   249
txt{*\noindent
nipkow@10159
   250
After simplification the base case boils down to
nipkow@10159
   251
\begin{isabelle}
nipkow@10159
   252
\ \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
nipkow@10159
   253
\ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
nipkow@10159
   254
\end{isabelle}
nipkow@10159
   255
The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
nipkow@10159
   256
holds. However, we first have to show that such a @{term t} actually exists! This reasoning
nipkow@10159
   257
is embodied in the theorem @{thm[source]someI2_ex}:
nipkow@10159
   258
@{thm[display,eta_contract=false]someI2_ex}
nipkow@10159
   259
When we apply this theorem as an introduction rule, @{text"?P x"} becomes
nipkow@10159
   260
@{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove
nipkow@10159
   261
two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and
nipkow@10159
   262
@{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
nipkow@10159
   263
@{text fast} can prove the base case quickly:
nipkow@10159
   264
*};
nipkow@10159
   265
wenzelm@10000
   266
 apply(fast intro:someI2_ex);
nipkow@10159
   267
nipkow@10159
   268
txt{*\noindent
nipkow@10212
   269
What is worth noting here is that we have used @{text fast} rather than
nipkow@10212
   270
@{text blast}.  The reason is that @{text blast} would fail because it cannot
nipkow@10212
   271
cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
nipkow@10212
   272
subgoal is nontrivial because of the nested schematic variables. For
nipkow@10212
   273
efficiency reasons @{text blast} does not even attempt such unifications.
nipkow@10212
   274
Although @{text fast} can in principle cope with complicated unification
nipkow@10212
   275
problems, in practice the number of unifiers arising is often prohibitive and
nipkow@10212
   276
the offending rule may need to be applied explicitly rather than
nipkow@10212
   277
automatically. This is what happens in the step case.
nipkow@10159
   278
nipkow@10212
   279
The induction step is similar, but more involved, because now we face nested
nipkow@10212
   280
occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
nipkow@10212
   281
solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
nipkow@10212
   282
show the proof commands but do not describe the details:
nipkow@10159
   283
*};
nipkow@10159
   284
nipkow@9958
   285
apply(simp);
wenzelm@10000
   286
apply(rule someI2_ex);
nipkow@9958
   287
 apply(blast);
wenzelm@10000
   288
apply(rule someI2_ex);
nipkow@9958
   289
 apply(blast);
nipkow@10159
   290
apply(blast);
nipkow@10159
   291
done;
nipkow@9958
   292
nipkow@10159
   293
text{*
nipkow@10159
   294
Function @{term path} has fulfilled its purpose now and can be forgotten
nipkow@10159
   295
about. It was merely defined to provide the witness in the proof of the
nipkow@10171
   296
@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
nipkow@10159
   297
that we could have given the witness without having to define a new function:
nipkow@10159
   298
the term
nipkow@10159
   299
@{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
nipkow@10171
   300
is extensionally equal to @{term"path s P"},
nipkow@10159
   301
where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
nipkow@10171
   302
equations we omit.
nipkow@10159
   303
*};
nipkow@10159
   304
(*<*)
nipkow@10159
   305
lemma infinity_lemma:
nipkow@9958
   306
"\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow>
nipkow@9958
   307
 \<exists> p\<in>Paths s. \<forall> i. P(p i)";
nipkow@9958
   308
apply(subgoal_tac
nipkow@9958
   309
 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))");
nipkow@9958
   310
 apply(simp add:Paths_def);
nipkow@9958
   311
 apply(blast);
nipkow@9958
   312
apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)" in exI);
nipkow@9958
   313
apply(simp);
nipkow@9958
   314
apply(intro strip);
nipkow@9958
   315
apply(induct_tac i);
nipkow@9958
   316
 apply(simp);
wenzelm@10000
   317
 apply(fast intro:someI2_ex);
nipkow@9958
   318
apply(simp);
wenzelm@10000
   319
apply(rule someI2_ex);
nipkow@9958
   320
 apply(blast);
wenzelm@10000
   321
apply(rule someI2_ex);
nipkow@9958
   322
 apply(blast);
nipkow@9958
   323
by(blast);
nipkow@10159
   324
(*>*)
nipkow@9958
   325
nipkow@10159
   326
text{*
nipkow@10159
   327
At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
nipkow@10159
   328
*};
nipkow@10159
   329
nipkow@10159
   330
theorem AF_lemma2:
nipkow@9958
   331
"{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
nipkow@10159
   332
nipkow@10159
   333
txt{*\noindent
nipkow@10159
   334
The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule
nipkow@10159
   335
@{thm contrapos2}):
nipkow@10159
   336
*};
nipkow@10159
   337
nipkow@9958
   338
apply(rule subsetI);
nipkow@9958
   339
apply(erule contrapos2);
nipkow@9958
   340
apply simp;
nipkow@10159
   341
(*pr(latex xsymbols symbols);*)
nipkow@10159
   342
nipkow@10159
   343
txt{*
nipkow@10159
   344
\begin{isabelle}
nipkow@10159
   345
\ \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
nipkow@10159
   346
\end{isabelle}
nipkow@10159
   347
Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
nipkow@10159
   348
premise of @{thm[source]infinity_lemma} and the original subgoal:
nipkow@10159
   349
*};
nipkow@10159
   350
nipkow@10159
   351
apply(drule infinity_lemma);
nipkow@10159
   352
(*pr(latex xsymbols symbols);*)
nipkow@10159
   353
nipkow@10159
   354
txt{*
nipkow@10159
   355
\begin{isabelle}
nipkow@10159
   356
\ \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
nipkow@10159
   357
\ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
nipkow@10159
   358
\ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
nipkow@10159
   359
\end{isabelle}
nipkow@10159
   360
Both are solved automatically:
nipkow@10159
   361
*};
nipkow@9958
   362
nipkow@10159
   363
 apply(auto dest:not_in_lfp_afD);
nipkow@10159
   364
done;
nipkow@9958
   365
nipkow@10159
   366
text{*
nipkow@10159
   367
The main theorem is proved as for PDL, except that we also derive the necessary equality
nipkow@10159
   368
@{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2}
nipkow@10159
   369
on the spot:
nipkow@10159
   370
*}
nipkow@10159
   371
nipkow@10159
   372
theorem "mc f = {s. s \<Turnstile> f}";
nipkow@10159
   373
apply(induct_tac f);
nipkow@10159
   374
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
nipkow@10159
   375
done
nipkow@10159
   376
nipkow@10159
   377
text{*
nipkow@10171
   378
The above language is not quite CTL. The latter also includes an
nipkow@10178
   379
until-operator, which is the subject of the following exercise.
nipkow@10171
   380
It is not definable in terms of the other operators!
nipkow@10171
   381
\begin{exercise}
nipkow@10178
   382
Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics
nipkow@10178
   383
``there exist a path where @{term f} is true until @{term g} becomes true''
nipkow@10178
   384
@{text[display]"s \<Turnstile> EU f g = (\<exists>p\<in>Paths s. \<exists>j. p j \<Turnstile> g \<and> (\<exists>i < j. p i \<Turnstile> f))"}
nipkow@10171
   385
and model checking algorithm
nipkow@10178
   386
@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
nipkow@10186
   387
Prove the equivalence between semantics and model checking, i.e.\ that
nipkow@10186
   388
@{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}
nipkow@10186
   389
%For readability you may want to annotate {term EU} with its customary syntax
nipkow@10186
   390
%{text[display]"| EU formula formula    E[_ U _]"}
nipkow@10186
   391
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
nipkow@10186
   392
\end{exercise}
nipkow@10192
   393
For more CTL exercises see, for example \cite{Huth-Ryan-book}.
nipkow@10186
   394
\bigskip
nipkow@10178
   395
nipkow@10186
   396
Let us close this section with a few words about the executability of our model checkers.
nipkow@10159
   397
It is clear that if all sets are finite, they can be represented as lists and the usual
nipkow@10159
   398
set operations are easily implemented. Only @{term lfp} requires a little thought.
nipkow@10159
   399
Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
nipkow@10159
   400
@{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
nipkow@10186
   401
a fixpoint is reached. It is actually possible to generate executable functional programs
nipkow@10159
   402
from HOL definitions, but that is beyond the scope of the tutorial.
nipkow@10159
   403
*}
nipkow@10212
   404
(*<*)end(*>*)