Quelle  CTLind.thy

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

subsection‹CTL Revisited›

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

  us call a (finite or infinite) path \emph{term‹A›-avoiding} if it does
  touch any node in the set term‹A›. Then @{thm[source]AF_lemma2} says
  if no infinite path from some state term‹s› is term‹A›-avoiding,
  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‹
  is easy to see that for any infinite term‹A›-avoiding path term‹f›
  prop‹f(0::nat) ∈ Avoid s A› there is an infinite term‹A›-avoiding path
  with term‹s› because (by definition of const‹Avoid›) there is a
  term‹A›-avoiding path from term‹s› to term‹f(0::nat)›.
  proof is by induction on prop‹f(0::nat) ∈ Avoid s A›. However,
  requires the following
 , as explained in \S\ref{sec:ind-var-in-prems} above;
  ‹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
  base case (prop‹t = s›) is trivial and proved by ‹blast›.
  the induction step, we have an infinite term‹A›-avoiding path term‹f›
  from term‹u›, a successor of term‹t›. Now we simply instantiate
  ‹∀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
 . Simplification shows that this is a path starting with term‹t›
  that the instantiated induction hypothesis implies the conclusion.

  we come to the key lemma. Assuming that no infinite term‹A›-avoiding
  starts from term‹s›, we want to show prop‹s ∈ lfp(af A)›. For the
  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›,
  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
  proof is by induction on the ``distance'' between term‹t› and term‹A›. Remember that prop‹lfp(af A) = A ∪ M<sup>-1</sup> `` lfp(af A)›.
  term‹t› is already in term‹A›, then prop‹t ∈ lfp(af A)› is
 . 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
  trivial.

  formal counterpart of this proof sketch is a well-founded induction
 ~term‹M› restricted to term‹Avoid s A - A›, roughly speaking:
 {term[display]"{(y,x). (x,y) ∈ M ∧ x ∈ Avoid s A ∧ x ∉ A}"}
  we shall see presently, the absence of infinite term‹A›-avoiding paths
  from term‹s› implies well-foundedness of this relation. For the
  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]}
  the induction hypothesis states that if prop‹t ∉ A›
  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
  once, we have to prove that term‹t› is in term‹A› or all successors
  term‹t› are in term‹lfp (af A)›. But if term‹t› is not in term‹A›,
  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›.
 , 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‹
  proved the main goal, we return to the proof obligation that the
  used above is indeed well-founded. This is proved by contradiction: if
  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]}
  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‹
  ‹(no_asm)› modifier of the ‹rule_format› directive in the
  of the lemma means
  the assumption is left unchanged; otherwise the ‹∀p›
  be turned
  a ‹∧p›, which would complicate matters below. As it is,
 {thm[source]Avoid_in_lfp} is now
 {thm[display]Avoid_in_lfp[no_vars]}
  main theorem is simply the corollary where prop‹t = s›,
  the assumption prop‹t ∈ Avoid s A› is trivially true
  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(*>*)