Quelle  CTL.thy

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

subsection‹Computation Tree Logic --- CTL›

text‹\label{sec:CTL}
 index{CTL|(}%
  semantics of PDL only needs reflexive transitive closure.
  us be adventurous and introduce a more expressive temporal operator.
  extend the datatype
 ‹formula› by a new constructor
 ›
(*<*)
datatype formula = Atom "atom"
                  | Neg formula
                  | And formula formula
                  | AX formula
                  | EF formula(*>*)
                  | AF formula

text‹\noindent
  stands for ``\emph{A}lways in the \emph{F}uture'':
  all infinite paths, at some point the formula holds.
  the notion of an infinite path is easy
  HOL: it is simply a function from 🍋‹nat› to 🍋‹state›.
 ›

definition Paths :: "state ==> (nat ==> state)set" where
"Paths s ≡ {p. s = p 0 ∧ (∀i. (p i, p(i+1)) ∈ M)}"

text‹\noindent
  definition allows a succinct statement of the semantics of const‹AF›:
 footnote{Do not be misled: neither datatypes nor recursive functions can be
  by new constructors or equations. This is just a trick of the
  (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
  new datatype and a new function.}
 ›
(*<*)
primrec valid :: "state ==> formula ==> bool" ("(_ ⊨ _)" [80,80] 80) where
"s ⊨ Atom a = (a ∈ L s)" |
"s ⊨ Neg f = (~(s ⊨ f))" |
"s ⊨ And f g = (s ⊨ f ∧ s ⊨ g)" |
"s ⊨ AX f = (∀t. (s,t) ∈ M ⟶ t ⊨ f)" |
"s ⊨ EF f = (∃t. (s,t) ∈ M^* ∧ t ⊨ f)" |
(*>*)
"s ⊨ AF f = (∀p ∈ Paths s. ∃i. p i ⊨ f)"

text‹\noindent
  checking const‹AF› involves a function which
  just complicated enough to warrant a separate definition:
 ›

definition af :: "state set ==> state set ==> state set" where
"af A T ≡ A ∪ {s. ∀t. (s, t) ∈ M ⟶ t ∈ T}"

text‹\noindent
  we define term‹mc(AF f)› as the least set term‹T› that includes
 term‹mc f› and all states all of whose direct successors are in term‹T›:
 ›
(*<*)
primrec mc :: "formula ==> state set" where
"mc(Atom a) = {s. a ∈ L s}" |
"mc(Neg f) = -mc f" |
"mc(And f g) = mc f ∩ mc g" |
"mc(AX f) = {s. ∀t. (s,t) ∈ M ⟶ t ∈ mc f}" |
"mc(EF f) = lfp(λT. mc f ∪ M^-1 `` T)"|(*>*)
"mc(AF f) = lfp(af(mc f))"

text‹\noindent
  const‹af› is monotone in its second argument (and also its first, but
  is irrelevant), term‹af A› has a least fixed point:
 ›

lemma mono_af: "mono(af A)"
apply(simp add: mono_def af_def)
apply blast
done
(*<*)
lemma mono_ef: "mono(λT. A ∪ M^-1 `` T)"
apply(rule monoI)
by(blast)

lemma EF_lemma:
  "lfp(λT. A ∪ M^-1 `` T) = {s. ∃t. (s,t) ∈ M^* ∧ t ∈ A}"
apply(rule equalityI)
 apply(rule subsetI)
 apply(simp)
 apply(erule lfp_induct_set)
  apply(rule mono_ef)
 apply(simp)
 apply(blast intro: rtrancl_trans)
apply(rule subsetI)
apply(simp, clarify)
apply(erule converse_rtrancl_induct)
 apply(subst lfp_unfold[OF mono_ef])
 apply(blast)
apply(subst lfp_unfold[OF mono_ef])
by(blast)
(*>*)
text‹
  we need to prove now is prop‹mc(AF f) = {s. s ⊨ AF f}›, which states
  term‹mc› and ‹⊨› agree for const‹AF›\@.
  time we prove the two inclusions separately, starting
  the easy one:
 ›

theorem AF_lemma1: "lfp(af A) ⊆ {s. ∀p ∈ Paths s. ∃i. p i ∈ A}"

txt‹\noindent
  contrast to the analogous proof for const‹EF›, and just
  a change, we do not use fixed point induction. Park-induction,
  after David Park, is weaker but sufficient for this proof:
 begin{center}
 {thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
 end{center}
  instance of the premise prop‹f S ⊆ S› is proved pointwise,
  decision that \isa{auto} takes for us:
 ›
apply(rule lfp_lowerbound)
apply(auto simp add: af_def Paths_def)

txt‹
 {subgoals[display,indent=0,margin=70,goals_limit=1]}
  this remaining case, we set term‹t› to term‹p(1::nat)›.
  rest is automatic, which is surprising because it involves
  the instantiation term‹λi::nat. p(i+1)›
  ‹∀p›.
 ›

apply(erule_tac x = "p 1" in allE)
apply(auto)
done


text‹
  opposite inclusion is proved by contradiction: if some state
 term‹s› is not in term‹lfp(af A)›, then we can construct an
  term‹A›-avoiding path starting from~term‹s›. The reason is
  by unfolding const‹lfp› we find that if term‹s› is not in
 term‹lfp(af A)›, then term‹s› is not in term‹A› and there is a
  successor of term‹s› that is again not in \mbox{term‹lfp(af
 )›}. Iterating this argument yields the promised infinite
 term‹A›-avoiding path. Let us formalize this sketch.

  one-step argument in the sketch above
  proved by a variant of contraposition:
 ›

lemma not_in_lfp_afD:
 "s ∉ lfp(af A) ==> s ∉ A ∧ (∃ t. (s,t) ∈ M ∧ t ∉ lfp(af A))"
apply(erule contrapos_np)
apply(subst lfp_unfold[OF mono_af])
apply(simp add: af_def)
done

text‹\noindent
  assume the negation of the conclusion and prove term‹s ∈ lfp(af A)›.
  const‹lfp› once and
  with the definition of const‹af› finishes the proof.

  we iterate this process. The following construction of the desired
  is parameterized by a predicate term‹Q› that should hold along the path:
 ›

primrec path :: "state ==> (state ==> bool) ==> (nat ==> state)" where
"path s Q 0 = s" |
"path s Q (Suc n) = (SOME t. (path s Q n,t) ∈ M ∧ Q t)"

text‹\noindent
  term‹n+1::nat› on this path is some arbitrary successor
 term‹t› of element term‹n› such that term‹Q t› holds. Remember that ‹SOME t. R t›
  some arbitrary but fixed term‹t› such that prop‹R t› holds (see \S\ref{sec:SOME}). Of
 , such a term‹t› need not exist, but that is of no
  to us since we will only use const‹path› when a
  term‹t› does exist.

  us show that if each state term‹s› that satisfies term‹Q›
  a successor that again satisfies term‹Q›, then there exists an infinite term‹Q›-path:
 ›

lemma infinity_lemma:
  "[ Q s; ∀s. Q s ⟶ (∃ t. (s,t) ∈ M ∧ Q t) ] ==>
   ∃p∈Paths s. ∀i. Q(p i)"

txt‹\noindent
  we rephrase the conclusion slightly because we need to prove simultaneously
  the path property and the fact that term‹Q› holds:
 ›

apply(subgoal_tac
  "∃p. s = p 0 ∧ (∀i::nat. (p i, p(i+1)) ∈ M ∧ Q(p i))")

txt‹\noindent
  this proposition the original goal follows easily:
 ›

 apply(simp add: Paths_def, blast)

txt‹\noindent
  new subgoal is proved by providing the witness term‹path s Q› for term‹p›:
 ›

apply(rule_tac x = "path s Q" in exI)
apply(clarsimp)

txt‹\noindent
  simplification and clarification, the subgoal has the following form:
 {subgoals[display,indent=0,margin=70,goals_limit=1]}
  invites a proof by induction on term‹i›:
 ›

apply(induct_tac i)
 apply(simp)

txt‹\noindent
  simplification, the base case boils down to
 {subgoals[display,indent=0,margin=70,goals_limit=1]}
  conclusion looks exceedingly trivial: after all, term‹t› is chosen such that prop‹(s,t)∈M›
 . However, we first have to show that such a term‹t› actually exists! This reasoning
  embodied in the theorem @{thm[source]someI2_ex}:
 {thm[display,eta_contract=false]someI2_ex}
  we apply this theorem as an introduction rule, ‹?P x› becomes
 prop‹(s, x) ∈ M ∧ Q x› and ‹?Q x› becomes prop‹(s,x) ∈ M› and we have to prove
  subgoals: prop‹∃a. (s, a) ∈ M ∧ Q a›, which follows from the assumptions, and
 prop‹(s, x) ∈ M ∧ Q x ==> (s,x) ∈ M›, which is trivial. Thus it is not surprising that
 ‹fast› can prove the base case quickly:
 ›

 apply(fast intro: someI2_ex)

txt‹\noindent
  is worth noting here is that we have used \methdx{fast} rather than
 ‹blast›. The reason is that ‹blast› would fail because it cannot
  with @{thm[source]someI2_ex}: unifying its conclusion with the current
  is non-trivial because of the nested schematic variables. For
  reasons ‹blast› does not even attempt such unifications.
  ‹fast› can in principle cope with complicated unification
 , in practice the number of unifiers arising is often prohibitive and
  offending rule may need to be applied explicitly rather than
 . This is what happens in the step case.

  induction step is similar, but more involved, because now we face nested
  of ‹SOME›. As a result, ‹fast› is no longer able to
  the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely
  the proof commands but do not describe the details:
 ›

apply(simp)
apply(rule someI2_ex)
 apply(blast)
apply(rule someI2_ex)
 apply(blast)
apply(blast)
done

text‹
  const‹path› has fulfilled its purpose now and can be forgotten.
  was merely defined to provide the witness in the proof of the
 {thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
  we could have given the witness without having to define a new function:
  term
 {term[display]"rec_nat s (λn t. SOME u. (t,u)∈M ∧ Q u)"}
  extensionally equal to term‹path s Q›,
  term‹rec_nat› is the predefined primitive recursor on 🍋‹nat›.
 ›
(*<*)
lemma
"[ Q s; ∀ s. Q s ⟶ (∃ t. (s,t)∈M ∧ Q t) ] ==>
 ∃ p∈Paths s. ∀ i. Q(p i)"
apply(subgoal_tac
 "∃ p. s = p 0 ∧ (∀ i. (p i,p(Suc i))∈M ∧ Q(p i))")
 apply(simp add: Paths_def)
 apply(blast)
apply(rule_tac x = "rec_nat s (λn t. SOME u. (t,u)∈M ∧ Q u)" in exI)
apply(simp)
apply(intro strip)
apply(induct_tac i)
 apply(simp)
 apply(fast intro: someI2_ex)
apply(simp)
apply(rule someI2_ex)
 apply(blast)
apply(rule someI2_ex)
 apply(blast)
by(blast)
(*>*)

text‹
  last we can prove the opposite direction of @{thm[source]AF_lemma1}:
 ›

theorem AF_lemma2: "{s. ∀p ∈ Paths s. ∃i. p i ∈ A} ⊆ lfp(af A)"

txt‹\noindent
  proof is again pointwise and then by contraposition:
 ›

apply(rule subsetI)
apply(erule contrapos_pp)
apply simp

txt‹
 {subgoals[display,indent=0,goals_limit=1]}
  the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
  of @{thm[source]infinity_lemma} and the original subgoal:
 ›

apply(drule infinity_lemma)

txt‹
 {subgoals[display,indent=0,margin=65]}
  are solved automatically:
 ›

 apply(auto dest: not_in_lfp_afD)
done

text‹
  you find these proofs too complicated, we recommend that you read
 S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
  arguments.

  main theorem is proved as for PDL, except that we also derive the
  equality ‹lfp(af A) = ...› by combining
 {thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
 ›

theorem "mc f = {s. s ⊨ f}"
apply(induct_tac f)
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
done

text‹

  language defined above is not quite CTL\@. The latter also includes an
 -operator term‹EU f g› with semantics ``there \emph{E}xists a path
  term‹f› is true \emph{U}ntil term‹g› becomes true''. We need
  auxiliary function:
 ›

primrec
until:: "state set ==> state set ==> state ==> state list ==> bool" where
"until A B s [] = (s ∈ B)" |
"until A B s (t#p) = (s ∈ A ∧ (s,t) ∈ M ∧ until A B t p)"
(*<*)definition
 eusem :: "state set ==> state set ==> state set" where
"eusem A B ≡ {s. ∃p. until A B s p}"(*>*)

text‹\noindent
  the semantics of term‹EU› is now straightforward:
 {prop[display]"s ⊨ EU f g = (∃p. until {t. t ⊨ f} {t. t ⊨ g} s p)"}
  that term‹EU› is not definable in terms of the other operators!

  checking term‹EU› is again a least fixed point construction:
 {text[display]"mc(EU f g) = lfp(λT. mc g ∪ mc f ∩ (M^-1 `` T))"}

 begin{exercise}
  the datatype of formulae by the above until operator
  prove the equivalence between semantics and model checking, i.e.\ that
 {prop[display]"mc(EU f g) = {s. s ⊨ EU f g}"}
 For readability you may want to annotate {term EU} with its customary syntax
 {text[display]"| EU formula formula E[_ U _]"}
 which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
 end{exercise}
  more CTL exercises see, for example, Huth and Ryan cite‹"Huth-Ryan-book"›.
 ›

(*<*)
definition eufix :: "state set ==> state set ==> state set ==> state set" where
"eufix A B T ≡ B ∪ A ∩ (M^-1 `` T)"

lemma "lfp(eufix A B) ⊆ eusem A B"
apply(rule lfp_lowerbound)
apply(auto simp add: eusem_def eufix_def)
 apply(rule_tac x = "[]" in exI)
 apply simp
apply(rule_tac x = "xa#xb" in exI)
apply simp
done

lemma mono_eufix: "mono(eufix A B)"
apply(simp add: mono_def eufix_def)
apply blast
done

lemma "eusem A B ⊆ lfp(eufix A B)"
apply(clarsimp simp add: eusem_def)
apply(erule rev_mp)
apply(rule_tac x = x in spec)
apply(induct_tac p)
 apply(subst lfp_unfold[OF mono_eufix])
 apply(simp add: eufix_def)
apply(clarsimp)
apply(subst lfp_unfold[OF mono_eufix])
apply(simp add: eufix_def)
apply blast
done

(*
definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
"eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"

axiomatization where
M_total: "\<exists>t. (s,t) \<in> M"

consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)"
primrec
"apath s 0 = s"
"apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"

lemma [iff]: "apath s \<in> Paths s";
apply(simp add: Paths_def);
apply(blast intro: M_total[THEN someI_ex])
done

definition pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)" where
"pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"

lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
by(simp add: Paths_def pcons_def split: nat.split);

lemma "lfp(eufix A B) \<subseteq> eusem A B"
apply(rule lfp_lowerbound)
apply(clarsimp simp add: eusem_def eufix_def);
apply(erule disjE);
 apply(rule_tac x = "apath x" in bexI);
  apply(rule_tac x = 0 in exI);
  apply simp;
 apply simp;
apply(clarify);
apply(rule_tac x = "pcons xb p" in bexI);
 apply(rule_tac x = "j+1" in exI);
 apply (simp add: pcons_def split: nat.split);
apply (simp add: pcons_PathI)
done
*)
(*>*)

text‹Let us close this section with a few words about the executability of
  model checkers. It is clear that if all sets are finite, they can be
  as lists and the usual set operations are easily
 . Only const‹lfp› requires a little thought. Fortunately, theory
 ‹While_Combinator› in the Library~cite‹"HOL-Library"› provides a
  stating that in the case of finite sets and a monotone
 ~term‹F›, the value of \mbox{term‹lfp F›} can be computed by
  application of term‹F› to~term‹{}› until a fixed point is
 . It is actually possible to generate executable functional programs
  HOL definitions, but that is beyond the scope of the tutorial.%
 index{CTL|)}›
(*<*)end(*>*)