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{termA-avoiding} if it does
not touch any node in the set termA. Then @{thm[source]AF_lemma2} says
that if no infinite path from some state terms is termA-avoiding,
then props  lfp(af A). We prove this by inductively defining the set
termAvoid s A of states reachable from terms by a finite termA-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 termA-avoiding path termf
with propf(0::nat)  Avoid s A there is an infinite termA-avoiding path
starting with terms because (by definition of constAvoid) there is a
finite termA-avoiding path from terms to termf(0::nat).
The proof is by induction on propf(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  
   fPaths t. (i. f i  A)  (pPaths 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 (propt = s) is trivial and proved by blast›.
In the induction step, we have an infinite termA-avoiding path termf
starting from termu, a successor of termt. Now we simply instantiate
the ∀f∈Paths t› in the induction hypothesis by the path starting with
termt and continuing with termf. That is what the above $\lambda$-term
expresses.  Simplification shows that this is a path starting with termt 
and that the instantiated induction hypothesis implies the conclusion.

Now we come to the key lemma. Assuming that no infinite termA-avoiding
path starts from terms, we want to show props  lfp(af A). For the
inductive proof this must be generalized to the statement that every point termt
``between'' terms and termA, in other words all of termAvoid s A,
is contained in termlfp(af A):
›

lemma Avoid_in_lfp[rule_format(no_asm)]:
  "pPaths s. i. p i  A  t  Avoid s A  t  lfp(af A)"

txt‹\noindent
The proof is by induction on the ``distance'' between termt and termA. Remember that proplfp(af A) = A  M¯ `` lfp(af A).
If termt is already in termA, then propt  lfp(af A) is
trivial. If termt is not in termA but all successors are in
termlfp(af A) (induction hypothesis), then propt  lfp(af A) is
again trivial.

The formal counterpart of this proof sketch is a well-founded induction
on~termM restricted to termAvoid 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 termA-avoiding paths
starting from terms 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 propt  A
then all successors of termt that are in termAvoid s A are in
termlfp (af A). Unfolding termlfp in the conclusion of the first
subgoal once, we have to prove that termt is in termA or all successors
of termt are in termlfp (af A).  But if termt is not in termA,
the second 
constAvoid-rule implies that all successors of termt are in
termAvoid s A, because we also assume propt  Avoid s A.
Hence, by the induction hypothesis, all successors of termt are indeed in
termlfp(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 termA-avoiding path all in termAvoid 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
termA-avoiding path starting in terms 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 propt = s,
when the assumption propt  Avoid s A is trivially true
by the first constAvoid-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(*>*)