src/Doc/Tutorial/CTL/CTL.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 48994 c84278efa9d5
child 55415 05f5fdb8d093
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17914
99ead7a7eb42 fix headers;
wenzelm
parents: 16069
diff changeset
     1
(*<*)theory CTL imports Base begin(*>*)
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
     2
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10895
diff changeset
     3
subsection{*Computation Tree Logic --- CTL*};
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
     4
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
     5
text{*\label{sec:CTL}
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
     6
\index{CTL|(}%
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
     7
The semantics of PDL only needs reflexive transitive closure.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
     8
Let us be adventurous and introduce a more expressive temporal operator.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
     9
We extend the datatype
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    10
@{text formula} by a new constructor
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    11
*};
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    12
(*<*)
18724
cb6e0064c88c quote "atom";
wenzelm
parents: 17914
diff changeset
    13
datatype formula = Atom "atom"
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    14
                  | Neg formula
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    15
                  | And formula formula
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    16
                  | AX formula
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    17
                  | EF formula(*>*)
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    18
                  | AF formula;
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    19
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    20
text{*\noindent
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    21
which stands for ``\emph{A}lways in the \emph{F}uture'':
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    22
on all infinite paths, at some point the formula holds.
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    23
Formalizing the notion of an infinite path is easy
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    24
in HOL: it is simply a function from @{typ nat} to @{typ state}.
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    25
*};
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    26
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    27
definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    28
"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    29
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    30
text{*\noindent
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
    31
This definition allows a succinct statement of the semantics of @{const AF}:
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    32
\footnote{Do not be misled: neither datatypes nor recursive functions can be
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    33
extended by new constructors or equations. This is just a trick of the
12815
wenzelm
parents: 12699
diff changeset
    34
presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
wenzelm
parents: 12699
diff changeset
    35
a new datatype and a new function.}
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    36
*};
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    37
(*<*)
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    38
primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    39
"s \<Turnstile> Atom a  =  (a \<in> L s)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    40
"s \<Turnstile> Neg f   = (~(s \<Turnstile> f))" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    41
"s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    42
"s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    43
"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" |
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    44
(*>*)
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    45
"s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)"
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    46
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    47
text{*\noindent
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
    48
Model checking @{const AF} involves a function which
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    49
is just complicated enough to warrant a separate definition:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    50
*};
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    51
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    52
definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    53
"af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    54
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    55
text{*\noindent
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
    56
Now we define @{term "mc(AF f)"} as the least set @{term T} that includes
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    57
@{term"mc f"} and all states all of whose direct successors are in @{term T}:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    58
*};
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    59
(*<*)
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    60
primrec mc :: "formula \<Rightarrow> state set" where
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    61
"mc(Atom a)  = {s. a \<in> L s}" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    62
"mc(Neg f)   = -mc f" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    63
"mc(And f g) = mc f \<inter> mc g" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    64
"mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
    65
"mc(EF f)    = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"|(*>*)
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    66
"mc(AF f)    = lfp(af(mc f))";
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    67
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    68
text{*\noindent
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
    69
Because @{const af} is monotone in its second argument (and also its first, but
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
    70
that is irrelevant), @{term"af A"} has a least fixed point:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    71
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    72
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    73
lemma mono_af: "mono(af A)";
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    74
apply(simp add: mono_def af_def);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    75
apply blast;
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    76
done
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    77
(*<*)
10839
1f93f5a27de6 *** empty log message ***
nipkow
parents: 10801
diff changeset
    78
lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)";
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    79
apply(rule monoI);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    80
by(blast);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    81
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    82
lemma EF_lemma:
10839
1f93f5a27de6 *** empty log message ***
nipkow
parents: 10801
diff changeset
    83
  "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}";
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    84
apply(rule equalityI);
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
    85
 apply(rule subsetI);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    86
 apply(simp);
21260
11ba04d15f36 lfp_induct_set;
wenzelm
parents: 18724
diff changeset
    87
 apply(erule lfp_induct_set);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    88
  apply(rule mono_ef);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    89
 apply(simp);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
    90
 apply(blast intro: rtrancl_trans);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    91
apply(rule subsetI);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    92
apply(simp, clarify);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    93
apply(erule converse_rtrancl_induct);
11231
30d96882f915 *** empty log message ***
nipkow
parents: 11149
diff changeset
    94
 apply(subst lfp_unfold[OF mono_ef]);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    95
 apply(blast);
11231
30d96882f915 *** empty log message ***
nipkow
parents: 11149
diff changeset
    96
apply(subst lfp_unfold[OF mono_ef]);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    97
by(blast);
10149
7cfdf6a330a0 *** empty log message ***
nipkow
parents: 10133
diff changeset
    98
(*>*)
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
    99
text{*
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   100
All we need to prove now is  @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   101
that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   102
This time we prove the two inclusions separately, starting
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   103
with the easy one:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   104
*};
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   105
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
   106
theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}"
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   107
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   108
txt{*\noindent
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   109
In contrast to the analogous proof for @{const EF}, and just
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   110
for a change, we do not use fixed point induction.  Park-induction,
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   111
named after David Park, is weaker but sufficient for this proof:
10995
ef0b521698b7 *** empty log message ***
nipkow
parents: 10983
diff changeset
   112
\begin{center}
ef0b521698b7 *** empty log message ***
nipkow
parents: 10983
diff changeset
   113
@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
ef0b521698b7 *** empty log message ***
nipkow
parents: 10983
diff changeset
   114
\end{center}
10225
b9fd52525b69 *** empty log message ***
nipkow
parents: 10217
diff changeset
   115
The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13552
diff changeset
   116
a decision that \isa{auto} takes for us:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   117
*};
10225
b9fd52525b69 *** empty log message ***
nipkow
parents: 10217
diff changeset
   118
apply(rule lfp_lowerbound);
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13552
diff changeset
   119
apply(auto simp add: af_def Paths_def);
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10281
diff changeset
   120
10225
b9fd52525b69 *** empty log message ***
nipkow
parents: 10217
diff changeset
   121
txt{*
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10281
diff changeset
   122
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13552
diff changeset
   123
In this remaining case, we set @{term t} to @{term"p(1::nat)"}.
15106
e8cef6993701 aded comment
nipkow
parents: 15102
diff changeset
   124
The rest is automatic, which is surprising because it involves
e8cef6993701 aded comment
nipkow
parents: 15102
diff changeset
   125
finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
e8cef6993701 aded comment
nipkow
parents: 15102
diff changeset
   126
for @{text"\<forall>p"}.
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   127
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   128
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   129
apply(erule_tac x = "p 1" in allE);
15102
04b0e943fcc9 new simprules Int_subset_iff and Un_subset_iff
paulson
parents: 13552
diff changeset
   130
apply(auto);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   131
done;
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   132
10225
b9fd52525b69 *** empty log message ***
nipkow
parents: 10217
diff changeset
   133
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   134
text{*
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   135
The opposite inclusion is proved by contradiction: if some state
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   136
@{term s} is not in @{term"lfp(af A)"}, then we can construct an
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   137
infinite @{term A}-avoiding path starting from~@{term s}. The reason is
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   138
that by unfolding @{const lfp} we find that if @{term s} is not in
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   139
@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   140
direct successor of @{term s} that is again not in \mbox{@{term"lfp(af
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   141
A)"}}. Iterating this argument yields the promised infinite
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   142
@{term A}-avoiding path. Let us formalize this sketch.
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   143
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   144
The one-step argument in the sketch above
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   145
is proved by a variant of contraposition:
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   146
*};
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   147
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   148
lemma not_in_lfp_afD:
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   149
 "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
10235
20cf817f3b4a renaming of contrapos rules
paulson
parents: 10225
diff changeset
   150
apply(erule contrapos_np);
11231
30d96882f915 *** empty log message ***
nipkow
parents: 11149
diff changeset
   151
apply(subst lfp_unfold[OF mono_af]);
12815
wenzelm
parents: 12699
diff changeset
   152
apply(simp add: af_def);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   153
done;
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   154
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   155
text{*\noindent
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   156
We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   157
Unfolding @{const lfp} once and
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   158
simplifying with the definition of @{const af} finishes the proof.
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   159
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   160
Now we iterate this process. The following construction of the desired
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   161
path is parameterized by a predicate @{term Q} that should hold along the path:
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   162
*};
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   163
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
   164
primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
   165
"path s Q 0 = s" |
f8537d69f514 *** empty log message ***
nipkow
parents: 21260
diff changeset
   166
"path s Q (Suc n) = (SOME t. (path s Q n,t) \<in> M \<and> Q t)"
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   167
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   168
text{*\noindent
12699
deae80045527 *** empty log message ***
nipkow
parents: 12489
diff changeset
   169
Element @{term"n+1::nat"} on this path is some arbitrary successor
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   170
@{term t} of element @{term n} such that @{term"Q t"} holds.  Remember that @{text"SOME t. R t"}
10654
458068404143 *** empty log message ***
nipkow
parents: 10363
diff changeset
   171
is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   172
course, such a @{term t} need not exist, but that is of no
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   173
concern to us since we will only use @{const path} when a
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   174
suitable @{term t} does exist.
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   175
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   176
Let us show that if each state @{term s} that satisfies @{term Q}
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   177
has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path:
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   178
*};
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   179
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   180
lemma infinity_lemma:
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   181
  "\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow>
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   182
   \<exists>p\<in>Paths s. \<forall>i. Q(p i)";
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   183
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   184
txt{*\noindent
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   185
First we rephrase the conclusion slightly because we need to prove simultaneously
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   186
both the path property and the fact that @{term Q} holds:
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   187
*};
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   188
12489
c92e38c3cbaa *** empty log message ***
nipkow
parents: 12473
diff changeset
   189
apply(subgoal_tac
c92e38c3cbaa *** empty log message ***
nipkow
parents: 12473
diff changeset
   190
  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))");
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   191
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   192
txt{*\noindent
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   193
From this proposition the original goal follows easily:
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   194
*};
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   195
12815
wenzelm
parents: 12699
diff changeset
   196
 apply(simp add: Paths_def, blast);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   197
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   198
txt{*\noindent
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   199
The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   200
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   201
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   202
apply(rule_tac x = "path s Q" in exI);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   203
apply(clarsimp);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   204
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   205
txt{*\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   206
After simplification and clarification, the subgoal has the following form:
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10281
diff changeset
   207
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   208
It invites a proof by induction on @{term i}:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   209
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   210
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   211
apply(induct_tac i);
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   212
 apply(simp);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   213
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   214
txt{*\noindent
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   215
After simplification, the base case boils down to
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10281
diff changeset
   216
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   217
The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   218
holds. However, we first have to show that such a @{term t} actually exists! This reasoning
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   219
is embodied in the theorem @{thm[source]someI2_ex}:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   220
@{thm[display,eta_contract=false]someI2_ex}
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   221
When we apply this theorem as an introduction rule, @{text"?P x"} becomes
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   222
@{prop"(s, x) : M & Q x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   223
two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   224
@{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   225
@{text fast} can prove the base case quickly:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   226
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   227
12815
wenzelm
parents: 12699
diff changeset
   228
 apply(fast intro: someI2_ex);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   229
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   230
txt{*\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   231
What is worth noting here is that we have used \methdx{fast} rather than
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   232
@{text blast}.  The reason is that @{text blast} would fail because it cannot
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   233
cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
11149
e258b536a137 *** empty log message ***
nipkow
parents: 10995
diff changeset
   234
subgoal is non-trivial because of the nested schematic variables. For
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   235
efficiency reasons @{text blast} does not even attempt such unifications.
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   236
Although @{text fast} can in principle cope with complicated unification
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   237
problems, in practice the number of unifiers arising is often prohibitive and
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   238
the offending rule may need to be applied explicitly rather than
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   239
automatically. This is what happens in the step case.
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   240
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   241
The induction step is similar, but more involved, because now we face nested
16069
3f2a9f400168 *** empty log message ***
nipkow
parents: 15904
diff changeset
   242
occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   243
solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   244
show the proof commands but do not describe the details:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   245
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   246
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   247
apply(simp);
10000
fe6ffa46266f someI2_ex;
wenzelm
parents: 9992
diff changeset
   248
apply(rule someI2_ex);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   249
 apply(blast);
10000
fe6ffa46266f someI2_ex;
wenzelm
parents: 9992
diff changeset
   250
apply(rule someI2_ex);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   251
 apply(blast);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   252
apply(blast);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   253
done;
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   254
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   255
text{*
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   256
Function @{const path} has fulfilled its purpose now and can be forgotten.
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   257
It was merely defined to provide the witness in the proof of the
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   258
@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   259
that we could have given the witness without having to define a new function:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   260
the term
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   261
@{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   262
is extensionally equal to @{term"path s Q"},
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   263
where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   264
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   265
(*<*)
13552
83d674e8cd2a *** empty log message ***
nipkow
parents: 12815
diff changeset
   266
lemma
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   267
"\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   268
 \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   269
apply(subgoal_tac
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   270
 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
12815
wenzelm
parents: 12699
diff changeset
   271
 apply(simp add: Paths_def);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   272
 apply(blast);
10895
79194f07d356 *** empty log message ***
nipkow
parents: 10885
diff changeset
   273
apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   274
apply(simp);
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   275
apply(intro strip);
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   276
apply(induct_tac i);
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   277
 apply(simp);
12815
wenzelm
parents: 12699
diff changeset
   278
 apply(fast intro: someI2_ex);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   279
apply(simp);
10000
fe6ffa46266f someI2_ex;
wenzelm
parents: 9992
diff changeset
   280
apply(rule someI2_ex);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   281
 apply(blast);
10000
fe6ffa46266f someI2_ex;
wenzelm
parents: 9992
diff changeset
   282
apply(rule someI2_ex);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   283
 apply(blast);
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   284
by(blast);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   285
(*>*)
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   286
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   287
text{*
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   288
At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   289
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   290
12328
7c4ec77a8715 *** empty log message ***
nipkow
parents: 11705
diff changeset
   291
theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)";
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   292
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   293
txt{*\noindent
10237
875bf54b5d74 *** empty log message ***
nipkow
parents: 10235
diff changeset
   294
The proof is again pointwise and then by contraposition:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   295
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   296
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   297
apply(rule subsetI);
10235
20cf817f3b4a renaming of contrapos rules
paulson
parents: 10225
diff changeset
   298
apply(erule contrapos_pp);
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   299
apply simp;
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   300
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   301
txt{*
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10281
diff changeset
   302
@{subgoals[display,indent=0,goals_limit=1]}
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   303
Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   304
premise of @{thm[source]infinity_lemma} and the original subgoal:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   305
*};
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   306
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   307
apply(drule infinity_lemma);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   308
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   309
txt{*
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10281
diff changeset
   310
@{subgoals[display,indent=0,margin=65]}
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   311
Both are solved automatically:
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   312
*};
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   313
12815
wenzelm
parents: 12699
diff changeset
   314
 apply(auto dest: not_in_lfp_afD);
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   315
done;
9958
67f2920862c7 *** empty log message ***
nipkow
parents:
diff changeset
   316
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   317
text{*
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   318
If you find these proofs too complicated, we recommend that you read
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   319
\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
10217
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   320
simpler arguments.
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   321
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   322
The main theorem is proved as for PDL, except that we also derive the
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   323
necessary equality @{text"lfp(af A) = ..."} by combining
e61e7e1eacaf *** empty log message ***
nipkow
parents: 10212
diff changeset
   324
@{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
10159
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   325
*}
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   326
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   327
theorem "mc f = {s. s \<Turnstile> f}";
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   328
apply(induct_tac f);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   329
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   330
done
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   331
a72ddfdbfca0 *** empty log message ***
nipkow
parents: 10149
diff changeset
   332
text{*
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   333
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   334
The language defined above is not quite CTL\@. The latter also includes an
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   335
until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   336
where @{term f} is true \emph{U}ntil @{term g} becomes true''.  We need
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   337
an auxiliary function:
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   338
*}
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   339
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   340
primrec
27027
63f0b638355c *** empty log message ***
nipkow
parents: 27015
diff changeset
   341
until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool" where
63f0b638355c *** empty log message ***
nipkow
parents: 27015
diff changeset
   342
"until A B s []    = (s \<in> B)" |
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   343
"until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)"
27027
63f0b638355c *** empty log message ***
nipkow
parents: 27015
diff changeset
   344
(*<*)definition
63f0b638355c *** empty log message ***
nipkow
parents: 27015
diff changeset
   345
 eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   346
"eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*)
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   347
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   348
text{*\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   349
Expressing the semantics of @{term EU} is now straightforward:
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10971
diff changeset
   350
@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"}
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   351
Note that @{term EU} is not definable in terms of the other operators!
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   352
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   353
Model checking @{term EU} is again a least fixed point construction:
10839
1f93f5a27de6 *** empty log message ***
nipkow
parents: 10801
diff changeset
   354
@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M\<inverse> `` T))"}
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   355
10171
59d6633835fa *** empty log message ***
nipkow
parents: 10159
diff changeset
   356
\begin{exercise}
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   357
Extend the datatype of formulae by the above until operator
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   358
and prove the equivalence between semantics and model checking, i.e.\ that
10186
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   359
@{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   360
%For readability you may want to annotate {term EU} with its customary syntax
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   361
%{text[display]"| EU formula formula    E[_ U _]"}
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   362
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
499637e8f2c6 *** empty log message ***
nipkow
parents: 10178
diff changeset
   363
\end{exercise}
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10866
diff changeset
   364
For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   365
*}
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   366
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   367
(*<*)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 27027
diff changeset
   368
definition eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set" where
10839
1f93f5a27de6 *** empty log message ***
nipkow
parents: 10801
diff changeset
   369
"eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse> `` T)"
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   370
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   371
lemma "lfp(eufix A B) \<subseteq> eusem A B"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   372
apply(rule lfp_lowerbound)
46932
53d06963d83d corrected fragile proof; tuned semicolons
haftmann
parents: 35416
diff changeset
   373
apply(auto simp add: eusem_def eufix_def)
53d06963d83d corrected fragile proof; tuned semicolons
haftmann
parents: 35416
diff changeset
   374
 apply(rule_tac x = "[]" in exI)
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   375
 apply simp
46932
53d06963d83d corrected fragile proof; tuned semicolons
haftmann
parents: 35416
diff changeset
   376
apply(rule_tac x = "xa#xb" in exI)
53d06963d83d corrected fragile proof; tuned semicolons
haftmann
parents: 35416
diff changeset
   377
apply simp
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   378
done
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   379
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   380
lemma mono_eufix: "mono(eufix A B)";
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   381
apply(simp add: mono_def eufix_def);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   382
apply blast;
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   383
done
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   384
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   385
lemma "eusem A B \<subseteq> lfp(eufix A B)";
12815
wenzelm
parents: 12699
diff changeset
   386
apply(clarsimp simp add: eusem_def);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   387
apply(erule rev_mp);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   388
apply(rule_tac x = x in spec);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   389
apply(induct_tac p);
11231
30d96882f915 *** empty log message ***
nipkow
parents: 11149
diff changeset
   390
 apply(subst lfp_unfold[OF mono_eufix])
12815
wenzelm
parents: 12699
diff changeset
   391
 apply(simp add: eufix_def);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   392
apply(clarsimp);
11231
30d96882f915 *** empty log message ***
nipkow
parents: 11149
diff changeset
   393
apply(subst lfp_unfold[OF mono_eufix])
12815
wenzelm
parents: 12699
diff changeset
   394
apply(simp add: eufix_def);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   395
apply blast;
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   396
done
10178
aecb5bf6f76f *** empty log message ***
nipkow
parents: 10171
diff changeset
   397
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   398
(*
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 27027
diff changeset
   399
definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   400
"eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   401
48994
c84278efa9d5 modernized specifications;
wenzelm
parents: 48985
diff changeset
   402
axiomatization where
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   403
M_total: "\<exists>t. (s,t) \<in> M"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   404
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   405
consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   406
primrec
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   407
"apath s 0 = s"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   408
"apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   409
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   410
lemma [iff]: "apath s \<in> Paths s";
12815
wenzelm
parents: 12699
diff changeset
   411
apply(simp add: Paths_def);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   412
apply(blast intro: M_total[THEN someI_ex])
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   413
done
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   414
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 27027
diff changeset
   415
definition pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)" where
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   416
"pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   417
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   418
lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
12815
wenzelm
parents: 12699
diff changeset
   419
by(simp add: Paths_def pcons_def split: nat.split);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   420
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   421
lemma "lfp(eufix A B) \<subseteq> eusem A B"
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   422
apply(rule lfp_lowerbound)
12815
wenzelm
parents: 12699
diff changeset
   423
apply(clarsimp simp add: eusem_def eufix_def);
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   424
apply(erule disjE);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   425
 apply(rule_tac x = "apath x" in bexI);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   426
  apply(rule_tac x = 0 in exI);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   427
  apply simp;
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   428
 apply simp;
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   429
apply(clarify);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   430
apply(rule_tac x = "pcons xb p" in bexI);
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   431
 apply(rule_tac x = "j+1" in exI);
12815
wenzelm
parents: 12699
diff changeset
   432
 apply (simp add: pcons_def split: nat.split);
wenzelm
parents: 12699
diff changeset
   433
apply (simp add: pcons_PathI)
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   434
done
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   435
*)
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10242
diff changeset
   436
(*>*)
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   437
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   438
text{* Let us close this section with a few words about the executability of
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   439
our model checkers.  It is clear that if all sets are finite, they can be
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   440
represented as lists and the usual set operations are easily
15904
a6fb4ddc05c7 introduced @{const ...} antiquotation
haftmann
parents: 15106
diff changeset
   441
implemented. Only @{const lfp} requires a little thought.  Fortunately, theory
12473
f41e477576b9 *** empty log message ***
nipkow
parents: 12334
diff changeset
   442
@{text While_Combinator} in the Library~\cite{HOL-Library} provides a
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   443
theorem stating that in the case of finite sets and a monotone
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   444
function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   445
iterated application of @{term F} to~@{term"{}"} until a fixed point is
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   446
reached. It is actually possible to generate executable functional programs
11494
23a118849801 revisions and indexing
paulson
parents: 11231
diff changeset
   447
from HOL definitions, but that is beyond the scope of the tutorial.%
12334
60bf75e157e4 *** empty log message ***
nipkow
parents: 12332
diff changeset
   448
\index{CTL|)} *}
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 10210
diff changeset
   449
(*<*)end(*>*)