wenzelm@17914: (*<*)theory CTLind imports CTL begin(*>*) nipkow@10218: paulson@10885: subsection{*CTL Revisited*} nipkow@10218: nipkow@10218: text{*\label{sec:CTL-revisited} paulson@11494: \index{CTL|(}% paulson@11494: The purpose of this section is twofold: to demonstrate paulson@11494: some of the induction principles and heuristics discussed above and to nipkow@10281: show how inductive definitions can simplify proofs. nipkow@10218: In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a paulson@10795: model checker for CTL\@. In particular the proof of the nipkow@10218: @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as paulson@11494: simple as one might expect, due to the @{text SOME} operator nipkow@10281: involved. Below we give a simpler proof of @{thm[source]AF_lemma2} nipkow@10281: based on an auxiliary inductive definition. nipkow@10218: nipkow@10218: Let us call a (finite or infinite) path \emph{@{term A}-avoiding} if it does nipkow@10218: not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says nipkow@10218: that if no infinite path from some state @{term s} is @{term A}-avoiding, nipkow@10218: then @{prop"s \ lfp(af A)"}. We prove this by inductively defining the set nipkow@10218: @{term"Avoid s A"} of states reachable from @{term s} by a finite @{term nipkow@10218: A}-avoiding path: paulson@10241: % Second proof of opposite direction, directly by well-founded induction nipkow@10218: % on the initial segment of M that avoids A. nipkow@10218: *} nipkow@10218: berghofe@23733: inductive_set berghofe@23733: Avoid :: "state \ state set \ state set" berghofe@23733: for s :: state and A :: "state set" berghofe@23733: where berghofe@23733: "s \ Avoid s A" berghofe@23733: | "\ t \ Avoid s A; t \ A; (t,u) \ M \ \ u \ Avoid s A"; nipkow@10218: nipkow@10218: text{* nipkow@10218: It is easy to see that for any infinite @{term A}-avoiding path @{term f} nipkow@12492: with @{prop"f(0::nat) \ Avoid s A"} there is an infinite @{term A}-avoiding path haftmann@15904: starting with @{term s} because (by definition of @{const Avoid}) there is a nipkow@12492: finite @{term A}-avoiding path from @{term s} to @{term"f(0::nat)"}. nipkow@12492: The proof is by induction on @{prop"f(0::nat) \ Avoid s A"}. However, nipkow@10218: this requires the following nipkow@10218: reformulation, as explained in \S\ref{sec:ind-var-in-prems} above; nipkow@10218: the @{text rule_format} directive undoes the reformulation after the proof. nipkow@10218: *} nipkow@10218: nipkow@10218: lemma ex_infinite_path[rule_format]: nipkow@10218: "t \ Avoid s A \ nipkow@10218: \f\Paths t. (\i. f i \ A) \ (\p\Paths s. \i. p i \ A)"; nipkow@10218: apply(erule Avoid.induct); nipkow@10218: apply(blast); nipkow@10218: apply(clarify); nipkow@10218: apply(drule_tac x = "\i. case i of 0 \ t | Suc i \ f i" in bspec); wenzelm@12815: apply(simp_all add: Paths_def split: nat.split); nipkow@10218: done nipkow@10218: nipkow@10218: text{*\noindent paulson@11494: The base case (@{prop"t = s"}) is trivial and proved by @{text blast}. nipkow@10218: In the induction step, we have an infinite @{term A}-avoiding path @{term f} nipkow@10218: starting from @{term u}, a successor of @{term t}. Now we simply instantiate nipkow@10218: the @{text"\f\Paths t"} in the induction hypothesis by the path starting with nipkow@10218: @{term t} and continuing with @{term f}. That is what the above $\lambda$-term paulson@10885: expresses. Simplification shows that this is a path starting with @{term t} paulson@10885: and that the instantiated induction hypothesis implies the conclusion. nipkow@10218: nipkow@11196: Now we come to the key lemma. Assuming that no infinite @{term A}-avoiding nipkow@11277: path starts from @{term s}, we want to show @{prop"s \ lfp(af A)"}. For the nipkow@11277: inductive proof this must be generalized to the statement that every point @{term t} paulson@11494: ``between'' @{term s} and @{term A}, in other words all of @{term"Avoid s A"}, nipkow@11196: is contained in @{term"lfp(af A)"}: nipkow@10218: *} nipkow@10218: nipkow@10218: lemma Avoid_in_lfp[rule_format(no_asm)]: nipkow@10218: "\p\Paths s. \i. p i \ A \ t \ Avoid s A \ t \ lfp(af A)"; nipkow@11196: nipkow@10218: txt{*\noindent nipkow@11196: The proof is by induction on the ``distance'' between @{term t} and @{term nipkow@11196: A}. Remember that @{prop"lfp(af A) = A \ M\ `` lfp(af A)"}. nipkow@11196: If @{term t} is already in @{term A}, then @{prop"t \ lfp(af A)"} is nipkow@11196: trivial. If @{term t} is not in @{term A} but all successors are in nipkow@11196: @{term"lfp(af A)"} (induction hypothesis), then @{prop"t \ lfp(af A)"} is nipkow@11196: again trivial. nipkow@11196: nipkow@11196: The formal counterpart of this proof sketch is a well-founded induction paulson@11494: on~@{term M} restricted to @{term"Avoid s A - A"}, roughly speaking: nipkow@11196: @{term[display]"{(y,x). (x,y) \ M \ x \ Avoid s A \ x \ A}"} nipkow@11277: As we shall see presently, the absence of infinite @{term A}-avoiding paths paulson@10241: starting from @{term s} implies well-foundedness of this relation. For the nipkow@10218: moment we assume this and proceed with the induction: nipkow@10218: *} nipkow@10218: nipkow@11196: apply(subgoal_tac "wf{(y,x). (x,y) \ M \ x \ Avoid s A \ x \ A}"); nipkow@10218: apply(erule_tac a = t in wf_induct); nipkow@10218: apply(clarsimp); nipkow@11196: (*<*)apply(rename_tac t)(*>*) nipkow@10218: nipkow@10218: txt{*\noindent paulson@10885: @{subgoals[display,indent=0,margin=65]} paulson@10885: Now the induction hypothesis states that if @{prop"t \ A"} nipkow@10218: then all successors of @{term t} that are in @{term"Avoid s A"} are in nipkow@11196: @{term"lfp (af A)"}. Unfolding @{term lfp} in the conclusion of the first nipkow@11196: subgoal once, we have to prove that @{term t} is in @{term A} or all successors paulson@11494: of @{term t} are in @{term"lfp (af A)"}. But if @{term t} is not in @{term A}, nipkow@11196: the second haftmann@15904: @{const Avoid}-rule implies that all successors of @{term t} are in paulson@11494: @{term"Avoid s A"}, because we also assume @{prop"t \ Avoid s A"}. paulson@11494: Hence, by the induction hypothesis, all successors of @{term t} are indeed in nipkow@10218: @{term"lfp(af A)"}. Mechanically: nipkow@10218: *} nipkow@10218: nipkow@11196: apply(subst lfp_unfold[OF mono_af]); nipkow@11196: apply(simp (no_asm) add: af_def); wenzelm@12815: apply(blast intro: Avoid.intros); nipkow@10218: nipkow@10218: txt{* paulson@11494: Having proved the main goal, we return to the proof obligation that the paulson@11494: relation used above is indeed well-founded. This is proved by contradiction: if paulson@10885: the relation is not well-founded then there exists an infinite @{term nipkow@10218: A}-avoiding path all in @{term"Avoid s A"}, by theorem nipkow@10218: @{thm[source]wf_iff_no_infinite_down_chain}: nipkow@10218: @{thm[display]wf_iff_no_infinite_down_chain[no_vars]} nipkow@10218: From lemma @{thm[source]ex_infinite_path} the existence of an infinite paulson@10885: @{term A}-avoiding path starting in @{term s} follows, contradiction. nipkow@10218: *} nipkow@10218: paulson@10235: apply(erule contrapos_pp); wenzelm@12815: apply(simp add: wf_iff_no_infinite_down_chain); nipkow@10218: apply(erule exE); nipkow@10218: apply(rule ex_infinite_path); wenzelm@12815: apply(auto simp add: Paths_def); nipkow@10218: done nipkow@10218: nipkow@10218: text{* nipkow@11196: The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive in the nipkow@11196: statement of the lemma means paulson@11494: that the assumption is left unchanged; otherwise the @{text"\p"} paulson@11494: would be turned nipkow@10218: into a @{text"\p"}, which would complicate matters below. As it is, nipkow@10218: @{thm[source]Avoid_in_lfp} is now nipkow@10218: @{thm[display]Avoid_in_lfp[no_vars]} nipkow@10218: The main theorem is simply the corollary where @{prop"t = s"}, paulson@11494: when the assumption @{prop"t \ Avoid s A"} is trivially true haftmann@15904: by the first @{const Avoid}-rule. Isabelle confirms this:% paulson@11494: \index{CTL|)}*} nipkow@10218: nipkow@10855: theorem AF_lemma2: "{s. \p \ Paths s. \ i. p i \ A} \ lfp(af A)"; wenzelm@12815: by(auto elim: Avoid_in_lfp intro: Avoid.intros); nipkow@10218: nipkow@10218: nipkow@10218: (*<*)end(*>*)