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