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