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 \ 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 \ state set \ state set";  nipkow@10218  27 inductive "Avoid s A"  nipkow@10218  28 intros "s \ Avoid s A"  nipkow@10218  29  "\ t \ Avoid s A; t \ A; (t,u) \ M \ \ u \ 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 \ 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 \ 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 \ Avoid s A \  nipkow@10218  44  \f\Paths t. (\i. f i \ A) \ (\p\Paths s. \i. p i \ 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 = "\i. case i of 0 \ t | Suc i \ 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"\f\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 \ 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  "\p\Paths s. \i. p i \ A \ t \ Avoid s A \ t \ lfp(af A)";  nipkow@10218  70 txt{*\noindent  nipkow@10218  71 The trick is not to induct on @{prop"t \ 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 \ 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) \ M \ x \ Avoid s A \ y \ Avoid s A \ x \ 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)\M \ x \ Avoid s A \ y \ Avoid s A \ x \ 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 \ 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 \ 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"\p"} is turned  nipkow@10218  126 into a @{text"\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 \ 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. \p \ Paths s. \ i. p i \ A} \ 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(*>*)