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