src/HOL/ex/CTL.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 46685 866a798d051c
child 58622 aa99568f56de
permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/ex/CTL.thy
     2     Author:     Gertrud Bauer
     3 *)
     4 
     5 header {* CTL formulae *}
     6 
     7 theory CTL
     8 imports Main
     9 begin
    10 
    11 text {*
    12   We formalize basic concepts of Computational Tree Logic (CTL)
    13   \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
    14   simply-typed set theory of HOL.
    15 
    16   By using the common technique of ``shallow embedding'', a CTL
    17   formula is identified with the corresponding set of states where it
    18   holds.  Consequently, CTL operations such as negation, conjunction,
    19   disjunction simply become complement, intersection, union of sets.
    20   We only require a separate operation for implication, as point-wise
    21   inclusion is usually not encountered in plain set-theory.
    22 *}
    23 
    24 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
    25 
    26 type_synonym 'a ctl = "'a set"
    27 
    28 definition
    29   imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where
    30   "p \<rightarrow> q = - p \<union> q"
    31 
    32 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
    33 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by rule
    34 
    35 
    36 text {*
    37   \smallskip The CTL path operators are more interesting; they are
    38   based on an arbitrary, but fixed model @{text \<M>}, which is simply
    39   a transition relation over states @{typ "'a"}.
    40 *}
    41 
    42 axiomatization \<M> :: "('a \<times> 'a) set"
    43 
    44 text {*
    45   The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
    46   as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
    47   defined as derived ones.  The formula @{text "\<EX> p"} holds in a
    48   state @{term s}, iff there is a successor state @{term s'} (with
    49   respect to the model @{term \<M>}), such that @{term p} holds in
    50   @{term s'}.  The formula @{text "\<EF> p"} holds in a state @{term
    51   s}, iff there is a path in @{text \<M>}, starting from @{term s},
    52   such that there exists a state @{term s'} on the path, such that
    53   @{term p} holds in @{term s'}.  The formula @{text "\<EG> p"} holds
    54   in a state @{term s}, iff there is a path, starting from @{term s},
    55   such that for all states @{term s'} on the path, @{term p} holds in
    56   @{term s'}.  It is easy to see that @{text "\<EF> p"} and @{text
    57   "\<EG> p"} may be expressed using least and greatest fixed points
    58   \cite{McMillan-PhDThesis}.
    59 *}
    60 
    61 definition
    62   EX  ("\<EX> _" [80] 90) where "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    63 definition
    64   EF ("\<EF> _" [80] 90)  where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
    65 definition
    66   EG ("\<EG> _" [80] 90)  where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
    67 
    68 text {*
    69   @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
    70   dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
    71   "\<EG>"}.
    72 *}
    73 
    74 definition
    75   AX  ("\<AX> _" [80] 90) where "\<AX> p = - \<EX> - p"
    76 definition
    77   AF  ("\<AF> _" [80] 90) where "\<AF> p = - \<EG> - p"
    78 definition
    79   AG  ("\<AG> _" [80] 90) where "\<AG> p = - \<EF> - p"
    80 
    81 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
    82 
    83 
    84 subsection {* Basic fixed point properties *}
    85 
    86 text {*
    87   First of all, we use the de-Morgan property of fixed points
    88 *}
    89 
    90 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
    91 proof
    92   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
    93   proof
    94     fix x assume l: "x \<in> lfp f"
    95     show "x \<in> - gfp (\<lambda>s. - f (- s))"
    96     proof
    97       assume "x \<in> gfp (\<lambda>s. - f (- s))"
    98       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
    99         by (auto simp add: gfp_def)
   100       then have "f (- u) \<subseteq> - u" by auto
   101       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
   102       from l and this have "x \<notin> u" by auto
   103       with `x \<in> u` show False by contradiction
   104     qed
   105   qed
   106   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
   107   proof (rule lfp_greatest)
   108     fix u assume "f u \<subseteq> u"
   109     then have "- u \<subseteq> - f u" by auto
   110     then have "- u \<subseteq> - f (- (- u))" by simp
   111     then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
   112     then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
   113   qed
   114 qed
   115 
   116 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
   117   by (simp add: lfp_gfp)
   118 
   119 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
   120   by (simp add: lfp_gfp)
   121 
   122 text {*
   123   in order to give dual fixed point representations of @{term "AF p"}
   124   and @{term "AG p"}:
   125 *}
   126 
   127 lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
   128 lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
   129 
   130 lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
   131 proof -
   132   have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
   133   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
   134 qed
   135 
   136 lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
   137 proof -
   138   have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
   139   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
   140 qed
   141 
   142 lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
   143 proof -
   144   have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
   145   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
   146 qed
   147 
   148 text {*
   149   From the greatest fixed point definition of @{term "\<AG> p"}, we
   150   derive as a consequence of the Knaster-Tarski theorem on the one
   151   hand that @{term "\<AG> p"} is a fixed point of the monotonic
   152   function @{term "\<lambda>s. p \<inter> \<AX> s"}.
   153 *}
   154 
   155 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
   156 proof -
   157   have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
   158   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
   159 qed
   160 
   161 text {*
   162   This fact may be split up into two inequalities (merely using
   163   transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
   164   @{text "\<le>"} in Isabelle/HOL).
   165 *}
   166 
   167 lemma AG_fp_1: "\<AG> p \<subseteq> p"
   168 proof -
   169   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
   170   finally show ?thesis .
   171 qed
   172 
   173 lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
   174 proof -
   175   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
   176   finally show ?thesis .
   177 qed
   178 
   179 text {*
   180   On the other hand, we have from the Knaster-Tarski fixed point
   181   theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
   182   smaller than @{term "AG p"}.  A post-fixed point is a set of states
   183   @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}.  This leads to the
   184   following co-induction principle for @{term "AG p"}.
   185 *}
   186 
   187 lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
   188   by (simp only: AG_gfp) (rule gfp_upperbound)
   189 
   190 
   191 subsection {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
   192 
   193 text {*
   194   With the most basic facts available, we are now able to establish a
   195   few more interesting results, leading to the \emph{tree induction}
   196   principle for @{text AG} (see below).  We will use some elementary
   197   monotonicity and distributivity rules.
   198 *}
   199 
   200 lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
   201 lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
   202 lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
   203   by (simp only: AG_gfp, rule gfp_mono) auto 
   204 
   205 text {*
   206   The formula @{term "AG p"} implies @{term "AX p"} (we use
   207   substitution of @{text "\<subseteq>"} with monotonicity).
   208 *}
   209 
   210 lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
   211 proof -
   212   have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
   213   also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
   214   finally show ?thesis .
   215 qed
   216 
   217 text {*
   218   Furthermore we show idempotency of the @{text "\<AG>"} operator.
   219   The proof is a good example of how accumulated facts may get
   220   used to feed a single rule step.
   221 *}
   222 
   223 lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
   224 proof
   225   show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
   226 next
   227   show "\<AG> p \<subseteq> \<AG> \<AG> p"
   228   proof (rule AG_I)
   229     have "\<AG> p \<subseteq> \<AG> p" ..
   230     moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
   231     ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
   232   qed
   233 qed
   234 
   235 text {*
   236   \smallskip We now give an alternative characterization of the @{text
   237   "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
   238   an ``operational'' way by tree induction: In a state holds @{term
   239   "AG p"} iff in that state holds @{term p}, and in all reachable
   240   states @{term s} follows from the fact that @{term p} holds in
   241   @{term s}, that @{term p} also holds in all successor states of
   242   @{term s}.  We use the co-induction principle @{thm [source] AG_I}
   243   to establish this in a purely algebraic manner.
   244 *}
   245 
   246 theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
   247 proof
   248   show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")
   249   proof (rule AG_I)
   250     show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
   251     proof
   252       show "?lhs \<subseteq> p" ..
   253       show "?lhs \<subseteq> \<AX> ?lhs"
   254       proof -
   255         {
   256           have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
   257           also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
   258           finally have "?lhs \<subseteq> \<AX> p" by auto
   259         }  
   260         moreover
   261         {
   262           have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
   263           also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
   264           finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
   265         }  
   266         ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
   267         also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
   268         finally show ?thesis .
   269       qed
   270     qed
   271   qed
   272 next
   273   show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
   274   proof
   275     show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   276     show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
   277     proof -
   278       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   279       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
   280       also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
   281       finally show ?thesis .
   282     qed
   283   qed
   284 qed
   285 
   286 
   287 subsection {* An application of tree induction \label{sec:calc-ctl-commute} *}
   288 
   289 text {*
   290   Further interesting properties of CTL expressions may be
   291   demonstrated with the help of tree induction; here we show that
   292   @{text \<AX>} and @{text \<AG>} commute.
   293 *}
   294 
   295 theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
   296 proof -
   297   have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
   298   also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
   299   also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")
   300   proof  
   301     have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
   302     also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
   303     also note Int_mono AG_mono
   304     ultimately show "?lhs \<subseteq> \<AG> p" by fast
   305   next  
   306     have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   307     moreover 
   308     {
   309       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   310       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
   311       also note AG_mono
   312       ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
   313     } 
   314     ultimately show "\<AG> p \<subseteq> ?lhs" ..
   315   qed  
   316   finally show ?thesis .
   317 qed
   318 
   319 end