
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 \<in> 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 \<Rightarrow> state set \<Rightarrow> state set"
berghofe@23733:   for s :: state and A :: "state set"
berghofe@23733: where
berghofe@23733:     "s \<in> Avoid s A"
berghofe@23733:   | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> 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) \<in> 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) \<in> 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 \<in> Avoid s A  \<Longrightarrow>
nipkow@10218:    \<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: apply(erule Avoid.induct);
nipkow@10218:  apply(blast);
nipkow@10218: apply(clarify);
nipkow@10218: apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> 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"\<forall>f\<in>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 \<in> 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:   "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> 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 \<union> M\<inverse> `` lfp(af A)"}.
nipkow@11196: If @{term t} is already in @{term A}, then @{prop"t \<in> 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 \<in> 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) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> 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) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> 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 \<notin> 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 \<in> 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"\<forall>p"} 
paulson@11494: would be turned
nipkow@10218: into a @{text"\<And>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 \<in> 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. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
wenzelm@12815: by(auto elim: Avoid_in_lfp intro: Avoid.intros);
nipkow@10218: 
nipkow@10218: 
nipkow@10218: (*<*)end(*>*)




