Theory CTLind

(*<*)theory CTLind imports CTL begin(*>*)

subsection‹CTL Revisited›

text‹\label{sec:CTL-revisited}
\index{CTL|(}%
The purpose of this section is twofold: to demonstrate
some of the induction principles and heuristics discussed above and to
show how inductive definitions can simplify proofs.
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
model checker for CTL\@. In particular the proof of the
@{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
simple as one might expect, due to the ‹SOME› operator
involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
based on an auxiliary inductive definition.

Let us call a (finite or infinite) path \emph{\<^term>‹A›-avoiding} if it does
not touch any node in the set \<^term>‹A›. Then @{thm[source]AF_lemma2} says
that if no infinite path from some state \<^term>‹s› is \<^term>‹A›-avoiding,
then \<^prop>‹s ∈ lfp(af A)›. We prove this by inductively defining the set
\<^term>‹Avoid s A› of states reachable from \<^term>‹s› by a finite \<^term>‹A›-avoiding path:
% Second proof of opposite direction, directly by well-founded induction
% on the initial segment of M that avoids A.
›

inductive_set
  Avoid :: "state ⇒ state set ⇒ state set"
  for s :: state and A :: "state set"
where
    "s ∈ Avoid s A"
  | "⟦ t ∈ Avoid s A; t ∉ A; (t,u) ∈ M ⟧ ⟹ u ∈ Avoid s A"

text‹
It is easy to see that for any infinite \<^term>‹A›-avoiding path \<^term>‹f›
with \<^prop>‹f(0::nat) ∈ Avoid s A› there is an infinite \<^term>‹A›-avoiding path
starting with \<^term>‹s› because (by definition of \<^const>‹Avoid›) there is a
finite \<^term>‹A›-avoiding path from \<^term>‹s› to \<^term>‹f(0::nat)›.
The proof is by induction on \<^prop>‹f(0::nat) ∈ Avoid s A›. However,
this requires the following
reformulation, as explained in \S\ref{sec:ind-var-in-prems} above;
the ‹rule_format› directive undoes the reformulation after the proof.
›

lemma ex_infinite_path[rule_format]:
  "t ∈ Avoid s A  ⟹
   ∀f∈Paths t. (∀i. f i ∉ A) ⟶ (∃p∈Paths s. ∀i. p i ∉ A)"
apply(erule Avoid.induct)
 apply(blast)
apply(clarify)
apply(drule_tac x = "λi. case i of 0 ⇒ t | Suc i ⇒ f i" in bspec)
apply(simp_all add: Paths_def split: nat.split)
done

text‹\noindent
The base case (\<^prop>‹t = s›) is trivial and proved by ‹blast›.
In the induction step, we have an infinite \<^term>‹A›-avoiding path \<^term>‹f›
starting from \<^term>‹u›, a successor of \<^term>‹t›. Now we simply instantiate
the ‹∀f∈Paths t› in the induction hypothesis by the path starting with
\<^term>‹t› and continuing with \<^term>‹f›. That is what the above $\lambda$-term
expresses.  Simplification shows that this is a path starting with \<^term>‹t› 
and that the instantiated induction hypothesis implies the conclusion.

Now we come to the key lemma. Assuming that no infinite \<^term>‹A›-avoiding
path starts from \<^term>‹s›, we want to show \<^prop>‹s ∈ lfp(af A)›. For the
inductive proof this must be generalized to the statement that every point \<^term>‹t›
``between'' \<^term>‹s› and \<^term>‹A›, in other words all of \<^term>‹Avoid s A›,
is contained in \<^term>‹lfp(af A)›:
›

lemma Avoid_in_lfp[rule_format(no_asm)]:
  "∀p∈Paths s. ∃i. p i ∈ A ⟹ t ∈ Avoid s A ⟶ t ∈ lfp(af A)"

txt‹\noindent
The proof is by induction on the ``distance'' between \<^term>‹t› and \<^term>‹A›. Remember that \<^prop>‹lfp(af A) = A ∪ M¯ `` lfp(af A)›.
If \<^term>‹t› is already in \<^term>‹A›, then \<^prop>‹t ∈ lfp(af A)› is
trivial. If \<^term>‹t› is not in \<^term>‹A› but all successors are in
\<^term>‹lfp(af A)› (induction hypothesis), then \<^prop>‹t ∈ lfp(af A)› is
again trivial.

The formal counterpart of this proof sketch is a well-founded induction
on~\<^term>‹M› restricted to \<^term>‹Avoid s A - A›, roughly speaking:
@{term[display]"{(y,x). (x,y) ∈ M ∧ x ∈ Avoid s A ∧ x ∉ A}"}
As we shall see presently, the absence of infinite \<^term>‹A›-avoiding paths
starting from \<^term>‹s› implies well-foundedness of this relation. For the
moment we assume this and proceed with the induction:
›

apply(subgoal_tac "wf{(y,x). (x,y) ∈ M ∧ x ∈ Avoid s A ∧ x ∉ A}")
 apply(erule_tac a = t in wf_induct)
 apply(clarsimp)
(*<*)apply(rename_tac t)(*>*)

txt‹\noindent
@{subgoals[display,indent=0,margin=65]}
Now the induction hypothesis states that if \<^prop>‹t ∉ A›
then all successors of \<^term>‹t› that are in \<^term>‹Avoid s A› are in
\<^term>‹lfp (af A)›. Unfolding \<^term>‹lfp› in the conclusion of the first
subgoal once, we have to prove that \<^term>‹t› is in \<^term>‹A› or all successors
of \<^term>‹t› are in \<^term>‹lfp (af A)›.  But if \<^term>‹t› is not in \<^term>‹A›,
the second 
\<^const>‹Avoid›-rule implies that all successors of \<^term>‹t› are in
\<^term>‹Avoid s A›, because we also assume \<^prop>‹t ∈ Avoid s A›.
Hence, by the induction hypothesis, all successors of \<^term>‹t› are indeed in
\<^term>‹lfp(af A)›. Mechanically:
›

 apply(subst lfp_unfold[OF mono_af])
 apply(simp (no_asm) add: af_def)
 apply(blast intro: Avoid.intros)

txt‹
Having proved the main goal, we return to the proof obligation that the 
relation used above is indeed well-founded. This is proved by contradiction: if
the relation is not well-founded then there exists an infinite \<^term>‹A›-avoiding path all in \<^term>‹Avoid s A›, by theorem
@{thm[source]wf_iff_no_infinite_down_chain}:
@{thm[display]wf_iff_no_infinite_down_chain[no_vars]}
From lemma @{thm[source]ex_infinite_path} the existence of an infinite
\<^term>‹A›-avoiding path starting in \<^term>‹s› follows, contradiction.
›

apply(erule contrapos_pp)
apply(simp add: wf_iff_no_infinite_down_chain)
apply(erule exE)
apply(rule ex_infinite_path)
apply(auto simp add: Paths_def)
done

text‹
The ‹(no_asm)› modifier of the ‹rule_format› directive in the
statement of the lemma means
that the assumption is left unchanged; otherwise the ‹∀p› 
would be turned
into a ‹⋀p›, which would complicate matters below. As it is,
@{thm[source]Avoid_in_lfp} is now
@{thm[display]Avoid_in_lfp[no_vars]}
The main theorem is simply the corollary where \<^prop>‹t = s›,
when the assumption \<^prop>‹t ∈ Avoid s A› is trivially true
by the first \<^const>‹Avoid›-rule. Isabelle confirms this:%
\index{CTL|)}›

theorem AF_lemma2:  "{s. ∀p ∈ Paths s. ∃ i. p i ∈ A} ⊆ lfp(af A)"
by(auto elim: Avoid_in_lfp intro: Avoid.intros)


(*<*)end(*>*)