# Theory CTL

Up to index of Isabelle/HOL/ex

theory CTL
imports Main
begin

    (*  Title:      HOL/ex/CTL.thy
        ID:         $Id: CTL.thy,v 1.3 2005/09/14 20:08:08 wenzelm Exp $
        Author:     Gertrud Bauer
    *)

    header {* CTL formulae *}

    theory CTL imports Main begin

    text {*
      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_lower2

    types 'a ctl = "'a set"
    constdefs
      imp :: "'a ctl => 'a ctl => 'a ctl"    (infixr "->" 75)
      "p -> q ≡ - p ∪ q"

    lemma [intro!]: "p ∩ p -> q ⊆ q" by (unfold imp_def) auto
    lemma [intro!]: "p ⊆ (q -> p)" by (unfold imp_def) rule

    text {*
      \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"}.
    *}

    consts model :: "('a × 'a) set"    ("\<M>")

    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}.
    *}

    constdefs
      EX :: "'a ctl => 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p ≡ {s. ∃s'. (s, s') ∈ \<M> ∧ s' ∈ p}"
      EF :: "'a ctl => 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p ≡ lfp (λs. p ∪ \<EX> s)"
      EG :: "'a ctl => 'a ctl"    ("\<EG> _" [80] 90)    "\<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>"}.
    *}

    constdefs
      AX :: "'a ctl => 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p ≡ - \<EX> - p"
      AF :: "'a ctl => 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p ≡ - \<EG> - p"
      AG :: "'a ctl => 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p ≡ - \<EF> - p"

    lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def

    section {* Basic fixed point properties *}

    text {*
      First of all, we use the de-Morgan property of fixed points
    *}

    lemma lfp_gfp: "lfp f = - gfp (λs . - (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 (unfold gfp_def) auto
          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
          then 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
      qed
    qed

    lemma lfp_gfp': "- lfp f = gfp (λs. - (f (- s)))"
      by (simp add: lfp_gfp)

    lemma gfp_lfp': "- gfp f = lfp (λs. - (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 simp add: EX_def)
      then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
    qed

    lemma AF_fp: "\<AF> p = p ∪ \<AX> \<AF> p"
    proof -
      have "mono (λs. p ∪ \<AX> s)" by rule (auto simp add: AX_def EX_def)
      then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
    qed

    lemma EG_fp: "\<EG> p = p ∩ \<EX> \<EG> p"
    proof -
      have "mono (λs. p ∩ \<EX> s)" by rule (auto simp add: EX_def)
      then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
    qed

    text {*
      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 simp add: AX_def EX_def)
      then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
    qed

    text {*
      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 .
    qed

    text {**}

    lemma 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 .
    qed

    text {*
      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)

    section {* 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 auto
    lemma 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 .
    qed

    text {*
      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" ..
      qed
    qed

    text {*
      \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
      qed
    next
      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
      qed
    qed

    section {* 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 .
    qed

    end

lemmas

      [| C ⊆ A; C ⊆ B |] ==> C ⊆ A ∩ B

      B ⊆ A ∪ B

      A ⊆ A ∪ B

      A ∩ B ⊆ A

      A ∩ B ⊆ B

lemmas

      [| C ⊆ A; C ⊆ B |] ==> C ⊆ A ∩ B

      B ⊆ A ∪ B

      A ⊆ A ∪ B

      A ∩ B ⊆ A

      A ∩ B ⊆ B

lemma

      p ∩ p -> q ⊆ q

lemma

      p ⊆ q -> p

lemmas

      \<EX> p == {s. ∃s'. (s, s') ∈ \<M> ∧ s' ∈ p}

      \<EG> p == gfp (%s. p ∩ \<EX> s)

      \<AX> p == - \<EX> - p

      \<EF> p == lfp (%s. p ∪ \<EX> s)

      \<AF> p == - \<EG> - p

      \<AG> p == - \<EF> - p

lemmas

      \<EX> p == {s. ∃s'. (s, s') ∈ \<M> ∧ s' ∈ p}

      \<EG> p == gfp (%s. p ∩ \<EX> s)

      \<AX> p == - \<EX> - p

      \<EF> p == lfp (%s. p ∪ \<EX> s)

      \<AF> p == - \<EG> - p

      \<AG> p == - \<EF> - p

## Basic fixed point properties

lemma lfp_gfp:

      lfp f = - gfp (%s. - f (- s))

lemma lfp_gfp':

      - lfp f = gfp (%s. - f (- s))

lemma gfp_lfp':

      - gfp f = lfp (%s. - f (- s))

lemma AF_lfp:

      \<AF> p = lfp (%s. p ∪ \<AX> s)

lemma AG_gfp:

      \<AG> p = gfp (%s. p ∩ \<AX> s)

lemma EF_fp:

      \<EF> p = p ∪ \<EX> \<EF> p

lemma AF_fp:

      \<AF> p = p ∪ \<AX> \<AF> p

lemma EG_fp:

      \<EG> p = p ∩ \<EX> \<EG> p

lemma AG_fp:

      \<AG> p = p ∩ \<AX> \<AG> p

lemma AG_fp_1:

      \<AG> p ⊆ p

lemma AG_fp_2:

      \<AG> p ⊆ \<AX> \<AG> p

lemma AG_I:

      q ⊆ p ∩ \<AX> q ==> q ⊆ \<AG> p

## The tree induction principle \label{sec:calc-ctl-tree-induct}

lemma AX_int:

      \<AX> (p ∩ q) = \<AX> p ∩ \<AX> q

lemma AX_mono:

      p ⊆ q ==> \<AX> p ⊆ \<AX> q

lemma AG_mono:

      p ⊆ q ==> \<AG> p ⊆ \<AG> q

lemma AG_AX:

      \<AG> p ⊆ \<AX> p

lemma AG_AG:

      \<AG> \<AG> p = \<AG> p

theorem AG_induct:

      p ∩ \<AG> (p -> \<AX> p) = \<AG> p

## An application of tree induction \label{sec:calc-ctl-commute}

theorem AG_AX_commute:

      \<AG> \<AX> p = \<AX> \<AG> p