doc-src/TutorialI/CTL/CTLind.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10281 9554ce1c2e54
child 10795 9e888d60d3e5
permissions -rw-r--r--
*** empty log message ***
nipkow@10218
     1
(*<*)theory CTLind = CTL:(*>*)
nipkow@10218
     2
nipkow@10218
     3
subsection{*CTL revisited*}
nipkow@10218
     4
nipkow@10218
     5
text{*\label{sec:CTL-revisited}
nipkow@10281
     6
The purpose of this section is twofold: we want to demonstrate
nipkow@10281
     7
some of the induction principles and heuristics discussed above and we want to
nipkow@10281
     8
show how inductive definitions can simplify proofs.
nipkow@10218
     9
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
nipkow@10218
    10
model checker for CTL. In particular the proof of the
nipkow@10218
    11
@{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
nipkow@10218
    12
simple as one might intuitively expect, due to the @{text SOME} operator
nipkow@10281
    13
involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
nipkow@10281
    14
based on an auxiliary inductive definition.
nipkow@10218
    15
nipkow@10218
    16
Let us call a (finite or infinite) path \emph{@{term A}-avoiding} if it does
nipkow@10218
    17
not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says
nipkow@10218
    18
that if no infinite path from some state @{term s} is @{term A}-avoiding,
nipkow@10218
    19
then @{prop"s \<in> lfp(af A)"}. We prove this by inductively defining the set
nipkow@10218
    20
@{term"Avoid s A"} of states reachable from @{term s} by a finite @{term
nipkow@10218
    21
A}-avoiding path:
paulson@10241
    22
% Second proof of opposite direction, directly by well-founded induction
nipkow@10218
    23
% on the initial segment of M that avoids A.
nipkow@10218
    24
*}
nipkow@10218
    25
nipkow@10218
    26
consts Avoid :: "state \<Rightarrow> state set \<Rightarrow> state set";
nipkow@10218
    27
inductive "Avoid s A"
nipkow@10218
    28
intros "s \<in> Avoid s A"
nipkow@10218
    29
       "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
nipkow@10218
    30
nipkow@10218
    31
text{*
nipkow@10218
    32
It is easy to see that for any infinite @{term A}-avoiding path @{term f}
nipkow@10218
    33
with @{prop"f 0 \<in> Avoid s A"} there is an infinite @{term A}-avoiding path
nipkow@10218
    34
starting with @{term s} because (by definition of @{term Avoid}) there is a
nipkow@10218
    35
finite @{term A}-avoiding path from @{term s} to @{term"f 0"}.
nipkow@10218
    36
The proof is by induction on @{prop"f 0 \<in> Avoid s A"}. However,
nipkow@10218
    37
this requires the following
nipkow@10218
    38
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
nipkow@10218
    39
the @{text rule_format} directive undoes the reformulation after the proof.
nipkow@10218
    40
*}
nipkow@10218
    41
nipkow@10218
    42
lemma ex_infinite_path[rule_format]:
nipkow@10218
    43
  "t \<in> Avoid s A  \<Longrightarrow>
nipkow@10218
    44
   \<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)";
nipkow@10218
    45
apply(erule Avoid.induct);
nipkow@10218
    46
 apply(blast);
nipkow@10218
    47
apply(clarify);
nipkow@10218
    48
apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec);
nipkow@10218
    49
apply(simp_all add:Paths_def split:nat.split);
nipkow@10218
    50
done
nipkow@10218
    51
nipkow@10218
    52
text{*\noindent
nipkow@10218
    53
The base case (@{prop"t = s"}) is trivial (@{text blast}).
nipkow@10218
    54
In the induction step, we have an infinite @{term A}-avoiding path @{term f}
nipkow@10218
    55
starting from @{term u}, a successor of @{term t}. Now we simply instantiate
nipkow@10218
    56
the @{text"\<forall>f\<in>Paths t"} in the induction hypothesis by the path starting with
nipkow@10218
    57
@{term t} and continuing with @{term f}. That is what the above $\lambda$-term
nipkow@10218
    58
expresses. That fact that this is a path starting with @{term t} and that
nipkow@10218
    59
the instantiated induction hypothesis implies the conclusion is shown by
nipkow@10218
    60
simplification.
nipkow@10218
    61
nipkow@10218
    62
Now we come to the key lemma. It says that if @{term t} can be reached by a
nipkow@10218
    63
finite @{term A}-avoiding path from @{term s}, then @{prop"t \<in> lfp(af A)"},
nipkow@10218
    64
provided there is no infinite @{term A}-avoiding path starting from @{term
nipkow@10218
    65
s}.
nipkow@10218
    66
*}
nipkow@10218
    67
nipkow@10218
    68
lemma Avoid_in_lfp[rule_format(no_asm)]:
nipkow@10218
    69
  "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
nipkow@10218
    70
txt{*\noindent
nipkow@10218
    71
The trick is not to induct on @{prop"t \<in> Avoid s A"}, as already the base
paulson@10241
    72
case would be a problem, but to proceed by well-founded induction @{term
nipkow@10218
    73
t}. Hence @{prop"t \<in> Avoid s A"} needs to be brought into the conclusion as
nipkow@10218
    74
well, which the directive @{text rule_format} undoes at the end (see below).
paulson@10241
    75
But induction with respect to which well-founded relation? The restriction
nipkow@10218
    76
of @{term M} to @{term"Avoid s A"}:
nipkow@10218
    77
@{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}"}
nipkow@10218
    78
As we shall see in a moment, the absence of infinite @{term A}-avoiding paths
paulson@10241
    79
starting from @{term s} implies well-foundedness of this relation. For the
nipkow@10218
    80
moment we assume this and proceed with the induction:
nipkow@10218
    81
*}
nipkow@10218
    82
nipkow@10218
    83
apply(subgoal_tac
nipkow@10218
    84
  "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}");
nipkow@10218
    85
 apply(erule_tac a = t in wf_induct);
nipkow@10218
    86
 apply(clarsimp);
nipkow@10218
    87
nipkow@10218
    88
txt{*\noindent
nipkow@10218
    89
Now can assume additionally (induction hypothesis) that if @{prop"t \<notin> A"}
nipkow@10218
    90
then all successors of @{term t} that are in @{term"Avoid s A"} are in
nipkow@10218
    91
@{term"lfp (af A)"}. To prove the actual goal we unfold @{term lfp} once. Now
nipkow@10218
    92
we have to prove that @{term t} is in @{term A} or all successors of @{term
nipkow@10218
    93
t} are in @{term"lfp (af A)"}. If @{term t} is not in @{term A}, the second
nipkow@10218
    94
@{term Avoid}-rule implies that all successors of @{term t} are in
nipkow@10218
    95
@{term"Avoid s A"} (because we also assume @{prop"t \<in> Avoid s A"}), and
nipkow@10218
    96
hence, by the induction hypothesis, all successors of @{term t} are indeed in
nipkow@10218
    97
@{term"lfp(af A)"}. Mechanically:
nipkow@10218
    98
*}
nipkow@10218
    99
nipkow@10218
   100
 apply(rule ssubst [OF lfp_unfold[OF mono_af]]);
nipkow@10218
   101
 apply(simp only: af_def);
nipkow@10218
   102
 apply(blast intro:Avoid.intros);
nipkow@10218
   103
nipkow@10218
   104
txt{*
nipkow@10218
   105
Having proved the main goal we return to the proof obligation that the above
paulson@10241
   106
relation is indeed well-founded. This is proved by contraposition: we assume
paulson@10241
   107
the relation is not well-founded. Thus there exists an infinite @{term
nipkow@10218
   108
A}-avoiding path all in @{term"Avoid s A"}, by theorem
nipkow@10218
   109
@{thm[source]wf_iff_no_infinite_down_chain}:
nipkow@10218
   110
@{thm[display]wf_iff_no_infinite_down_chain[no_vars]}
nipkow@10218
   111
From lemma @{thm[source]ex_infinite_path} the existence of an infinite
nipkow@10218
   112
@{term A}-avoiding path starting in @{term s} follows, just as required for
nipkow@10218
   113
the contraposition.
nipkow@10218
   114
*}
nipkow@10218
   115
paulson@10235
   116
apply(erule contrapos_pp);
nipkow@10218
   117
apply(simp add:wf_iff_no_infinite_down_chain);
nipkow@10218
   118
apply(erule exE);
nipkow@10218
   119
apply(rule ex_infinite_path);
nipkow@10218
   120
apply(auto simp add:Paths_def);
nipkow@10218
   121
done
nipkow@10218
   122
nipkow@10218
   123
text{*
nipkow@10218
   124
The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive means
nipkow@10218
   125
that the assumption is left unchanged---otherwise the @{text"\<forall>p"} is turned
nipkow@10218
   126
into a @{text"\<And>p"}, which would complicate matters below. As it is,
nipkow@10218
   127
@{thm[source]Avoid_in_lfp} is now
nipkow@10218
   128
@{thm[display]Avoid_in_lfp[no_vars]}
nipkow@10218
   129
The main theorem is simply the corollary where @{prop"t = s"},
nipkow@10218
   130
in which case the assumption @{prop"t \<in> Avoid s A"} is trivially true
nipkow@10218
   131
by the first @{term Avoid}-rule). Isabelle confirms this:
nipkow@10218
   132
*}
nipkow@10218
   133
nipkow@10218
   134
theorem AF_lemma2:
nipkow@10218
   135
  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
nipkow@10218
   136
by(auto elim:Avoid_in_lfp intro:Avoid.intros);
nipkow@10218
   137
nipkow@10218
   138
nipkow@10218
   139
(*<*)end(*>*)