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