# Theory CTL

theory CTL
imports Main
(*  Title:      HOL/ex/CTL.thy    Author:     Gertrud Bauer*)header {* CTL formulae *}theory CTLimports Mainbegintext {*  We formalize basic concepts of Computational Tree Logic (CTL)  \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the  simply-typed set theory of HOL.  By using the common technique of shallow embedding'', a CTL  formula is identified with the corresponding set of states where it  holds.  Consequently, CTL operations such as negation, conjunction,  disjunction simply become complement, intersection, union of sets.  We only require a separate operation for implication, as point-wise  inclusion is usually not encountered in plain set-theory.*}lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2type_synonym 'a ctl = "'a set"definition  imp :: "'a ctl => 'a ctl => 'a ctl"    (infixr "->" 75) where  "p -> q = - p ∪ q"lemma [intro!]: "p ∩ p -> q ⊆ q" unfolding imp_def by autolemma [intro!]: "p ⊆ (q -> p)" unfolding imp_def by ruletext {*  \smallskip The CTL path operators are more interesting; they are  based on an arbitrary, but fixed model @{text \<M>}, which is simply  a transition relation over states @{typ "'a"}.*}axiomatization \<M> :: "('a × 'a) set"text {*  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken  as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are  defined as derived ones.  The formula @{text "\<EX> p"} holds in a  state @{term s}, iff there is a successor state @{term s'} (with  respect to the model @{term \<M>}), such that @{term p} holds in  @{term s'}.  The formula @{text "\<EF> p"} holds in a state @{term  s}, iff there is a path in @{text \<M>}, starting from @{term s},  such that there exists a state @{term s'} on the path, such that  @{term p} holds in @{term s'}.  The formula @{text "\<EG> p"} holds  in a state @{term s}, iff there is a path, starting from @{term s},  such that for all states @{term s'} on the path, @{term p} holds in  @{term s'}.  It is easy to see that @{text "\<EF> p"} and @{text  "\<EG> p"} may be expressed using least and greatest fixed points  \cite{McMillan-PhDThesis}.*}definition  EX  ("\<EX> _" [80] 90) where "\<EX> p = {s. ∃s'. (s, s') ∈ \<M> ∧ s' ∈ p}"definition  EF ("\<EF> _" [80] 90)  where "\<EF> p = lfp (λs. p ∪ \<EX> s)"definition  EG ("\<EG> _" [80] 90)  where "\<EG> p = gfp (λs. p ∩ \<EX> s)"text {*  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text  "\<EG>"}.*}definition  AX  ("\<AX> _" [80] 90) where "\<AX> p = - \<EX> - p"definition  AF  ("\<AF> _" [80] 90) where "\<AF> p = - \<EG> - p"definition  AG  ("\<AG> _" [80] 90) where "\<AG> p = - \<EF> - p"lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_defsubsection {* Basic fixed point properties *}text {*  First of all, we use the de-Morgan property of fixed points*}lemma lfp_gfp: "lfp f = - gfp (λs::'a set. - (f (- s)))"proof  show "lfp f ⊆ - gfp (λs. - f (- s))"  proof    fix x assume l: "x ∈ lfp f"    show "x ∈ - gfp (λs. - f (- s))"    proof      assume "x ∈ gfp (λs. - f (- s))"      then obtain u where "x ∈ u" and "u ⊆ - f (- u)"        by (auto simp add: gfp_def)      then have "f (- u) ⊆ - u" by auto      then have "lfp f ⊆ - u" by (rule lfp_lowerbound)      from l and this have "x ∉ u" by auto      with x ∈ u show False by contradiction    qed  qed  show "- gfp (λs. - f (- s)) ⊆ lfp f"  proof (rule lfp_greatest)    fix u assume "f u ⊆ u"    then have "- u ⊆ - f u" by auto    then have "- u ⊆ - f (- (- u))" by simp    then have "- u ⊆ gfp (λs. - f (- s))" by (rule gfp_upperbound)    then show "- gfp (λs. - f (- s)) ⊆ u" by auto  qedqedlemma lfp_gfp': "- lfp f = gfp (λs::'a set. - (f (- s)))"  by (simp add: lfp_gfp)lemma gfp_lfp': "- gfp f = lfp (λs::'a set. - (f (- s)))"  by (simp add: lfp_gfp)text {*  in order to give dual fixed point representations of @{term "AF p"}  and @{term "AG p"}:*}lemma AF_lfp: "\<AF> p = lfp (λs. p ∪ \<AX> s)" by (simp add: lfp_gfp)lemma AG_gfp: "\<AG> p = gfp (λs. p ∩ \<AX> s)" by (simp add: lfp_gfp)lemma EF_fp: "\<EF> p = p ∪ \<EX> \<EF> p"proof -  have "mono (λs. p ∪ \<EX> s)" by rule auto  then show ?thesis by (simp only: EF_def) (rule lfp_unfold)qedlemma AF_fp: "\<AF> p = p ∪ \<AX> \<AF> p"proof -  have "mono (λs. p ∪ \<AX> s)" by rule auto  then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)qedlemma EG_fp: "\<EG> p = p ∩ \<EX> \<EG> p"proof -  have "mono (λs. p ∩ \<EX> s)" by rule auto  then show ?thesis by (simp only: EG_def) (rule gfp_unfold)qedtext {*  From the greatest fixed point definition of @{term "\<AG> p"}, we  derive as a consequence of the Knaster-Tarski theorem on the one  hand that @{term "\<AG> p"} is a fixed point of the monotonic  function @{term "λs. p ∩ \<AX> s"}.*}lemma AG_fp: "\<AG> p = p ∩ \<AX> \<AG> p"proof -  have "mono (λs. p ∩ \<AX> s)" by rule auto  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)qedtext {*  This fact may be split up into two inequalities (merely using  transitivity of @{text "⊆" }, which is an instance of the overloaded  @{text "≤"} in Isabelle/HOL).*}lemma AG_fp_1: "\<AG> p ⊆ p"proof -  note AG_fp also have "p ∩ \<AX> \<AG> p ⊆ p" by auto  finally show ?thesis .qedlemma AG_fp_2: "\<AG> p ⊆ \<AX> \<AG> p"proof -  note AG_fp also have "p ∩ \<AX> \<AG> p ⊆ \<AX> \<AG> p" by auto  finally show ?thesis .qedtext {*  On the other hand, we have from the Knaster-Tarski fixed point  theorem that any other post-fixed point of @{term "λs. p ∩ AX s"} is  smaller than @{term "AG p"}.  A post-fixed point is a set of states  @{term q} such that @{term "q ⊆ p ∩ AX q"}.  This leads to the  following co-induction principle for @{term "AG p"}.*}lemma AG_I: "q ⊆ p ∩ \<AX> q ==> q ⊆ \<AG> p"  by (simp only: AG_gfp) (rule gfp_upperbound)subsection {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}text {*  With the most basic facts available, we are now able to establish a  few more interesting results, leading to the \emph{tree induction}  principle for @{text AG} (see below).  We will use some elementary  monotonicity and distributivity rules.*}lemma AX_int: "\<AX> (p ∩ q) = \<AX> p ∩ \<AX> q" by auto lemma AX_mono: "p ⊆ q ==> \<AX> p ⊆ \<AX> q" by autolemma AG_mono: "p ⊆ q ==> \<AG> p ⊆ \<AG> q"  by (simp only: AG_gfp, rule gfp_mono) auto text {*  The formula @{term "AG p"} implies @{term "AX p"} (we use  substitution of @{text "⊆"} with monotonicity).*}lemma AG_AX: "\<AG> p ⊆ \<AX> p"proof -  have "\<AG> p ⊆ \<AX> \<AG> p" by (rule AG_fp_2)  also have "\<AG> p ⊆ p" by (rule AG_fp_1) moreover note AX_mono  finally show ?thesis .qedtext {*  Furthermore we show idempotency of the @{text "\<AG>"} operator.  The proof is a good example of how accumulated facts may get  used to feed a single rule step.*}lemma AG_AG: "\<AG> \<AG> p = \<AG> p"proof  show "\<AG> \<AG> p ⊆ \<AG> p" by (rule AG_fp_1)next  show "\<AG> p ⊆ \<AG> \<AG> p"  proof (rule AG_I)    have "\<AG> p ⊆ \<AG> p" ..    moreover have "\<AG> p ⊆ \<AX> \<AG> p" by (rule AG_fp_2)    ultimately show "\<AG> p ⊆ \<AG> p ∩ \<AX> \<AG> p" ..  qedqedtext {*  \smallskip We now give an alternative characterization of the @{text  "\<AG>"} operator, which describes the @{text "\<AG>"} operator in  an operational'' way by tree induction: In a state holds @{term  "AG p"} iff in that state holds @{term p}, and in all reachable  states @{term s} follows from the fact that @{term p} holds in  @{term s}, that @{term p} also holds in all successor states of  @{term s}.  We use the co-induction principle @{thm [source] AG_I}  to establish this in a purely algebraic manner.*}theorem AG_induct: "p ∩ \<AG> (p -> \<AX> p) = \<AG> p"proof  show "p ∩ \<AG> (p -> \<AX> p) ⊆ \<AG> p"  (is "?lhs ⊆ _")  proof (rule AG_I)    show "?lhs ⊆ p ∩ \<AX> ?lhs"    proof      show "?lhs ⊆ p" ..      show "?lhs ⊆ \<AX> ?lhs"      proof -        {          have "\<AG> (p -> \<AX> p) ⊆ p -> \<AX> p" by (rule AG_fp_1)          also have "p ∩ p -> \<AX> p ⊆ \<AX> p" ..          finally have "?lhs ⊆ \<AX> p" by auto        }          moreover        {          have "p ∩ \<AG> (p -> \<AX> p) ⊆ \<AG> (p -> \<AX> p)" ..          also have "… ⊆ \<AX> …" by (rule AG_fp_2)          finally have "?lhs ⊆ \<AX> \<AG> (p -> \<AX> p)" .        }          ultimately have "?lhs ⊆ \<AX> p ∩ \<AX> \<AG> (p -> \<AX> p)" ..        also have "… = \<AX> ?lhs" by (simp only: AX_int)        finally show ?thesis .      qed    qed  qednext  show "\<AG> p ⊆ p ∩ \<AG> (p -> \<AX> p)"  proof    show "\<AG> p ⊆ p" by (rule AG_fp_1)    show "\<AG> p ⊆ \<AG> (p -> \<AX> p)"    proof -      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)      also have "\<AG> p ⊆ \<AX> p" by (rule AG_AX) moreover note AG_mono      also have "\<AX> p ⊆ (p -> \<AX> p)" .. moreover note AG_mono      finally show ?thesis .    qed  qedqedsubsection {* An application of tree induction \label{sec:calc-ctl-commute} *}text {*  Further interesting properties of CTL expressions may be  demonstrated with the help of tree induction; here we show that  @{text \<AX>} and @{text \<AG>} commute.*}theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"proof -  have "\<AG> \<AX> p = \<AX> p ∩ \<AX> \<AG> \<AX> p" by (rule AG_fp)  also have "… = \<AX> (p ∩ \<AG> \<AX> p)" by (simp only: AX_int)  also have "p ∩ \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")  proof      have "\<AX> p ⊆ p -> \<AX> p" ..    also have "p ∩ \<AG> (p -> \<AX> p) = \<AG> p" by (rule AG_induct)    also note Int_mono AG_mono    ultimately show "?lhs ⊆ \<AG> p" by fast  next      have "\<AG> p ⊆ p" by (rule AG_fp_1)    moreover     {      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)      also have "\<AG> p ⊆ \<AX> p" by (rule AG_AX)      also note AG_mono      ultimately have "\<AG> p ⊆ \<AG> \<AX> p" .    }     ultimately show "\<AG> p ⊆ ?lhs" ..  qed    finally show ?thesis .qedend