src/HOL/ex/CTL.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 42463 f270e3e18be5
child 46008 c296c75f4cf4
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/CTL.thy
     2     Author:     Gertrud Bauer
     3 *)
     4 
     5 header {* CTL formulae *}
     6 
     7 theory CTL imports Main begin
     8 
     9 text {*
    10   We formalize basic concepts of Computational Tree Logic (CTL)
    11   \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
    12   simply-typed set theory of HOL.
    13 
    14   By using the common technique of ``shallow embedding'', a CTL
    15   formula is identified with the corresponding set of states where it
    16   holds.  Consequently, CTL operations such as negation, conjunction,
    17   disjunction simply become complement, intersection, union of sets.
    18   We only require a separate operation for implication, as point-wise
    19   inclusion is usually not encountered in plain set-theory.
    20 *}
    21 
    22 lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
    23 
    24 type_synonym 'a ctl = "'a set"
    25 
    26 definition
    27   imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75) where
    28   "p \<rightarrow> q = - p \<union> q"
    29 
    30 lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" unfolding imp_def by auto
    31 lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" unfolding imp_def by 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 axiomatization \<M> :: "('a \<times> 'a) set"
    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 definition
    60   EX  ("\<EX> _" [80] 90) where "\<EX> p = {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    61 definition
    62   EF ("\<EF> _" [80] 90)  where "\<EF> p = lfp (\<lambda>s. p \<union> \<EX> s)"
    63 definition
    64   EG ("\<EG> _" [80] 90)  where "\<EG> p = gfp (\<lambda>s. p \<inter> \<EX> s)"
    65 
    66 text {*
    67   @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
    68   dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
    69   "\<EG>"}.
    70 *}
    71 
    72 definition
    73   AX  ("\<AX> _" [80] 90) where "\<AX> p = - \<EX> - p"
    74 definition
    75   AF  ("\<AF> _" [80] 90) where "\<AF> p = - \<EG> - p"
    76 definition
    77   AG  ("\<AG> _" [80] 90) where "\<AG> p = - \<EF> - p"
    78 
    79 lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
    80 
    81 
    82 subsection {* Basic fixed point properties *}
    83 
    84 text {*
    85   First of all, we use the de-Morgan property of fixed points
    86 *}
    87 
    88 lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
    89 proof
    90   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
    91   proof
    92     fix x assume l: "x \<in> lfp f"
    93     show "x \<in> - gfp (\<lambda>s. - f (- s))"
    94     proof
    95       assume "x \<in> gfp (\<lambda>s. - f (- s))"
    96       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
    97         by (auto simp add: gfp_def)
    98       then have "f (- u) \<subseteq> - u" by auto
    99       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
   100       from l and this have "x \<notin> u" by auto
   101       with `x \<in> u` show False by contradiction
   102     qed
   103   qed
   104   show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
   105   proof (rule lfp_greatest)
   106     fix u assume "f u \<subseteq> u"
   107     then have "- u \<subseteq> - f u" by auto
   108     then have "- u \<subseteq> - f (- (- u))" by simp
   109     then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
   110     then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
   111   qed
   112 qed
   113 
   114 lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
   115   by (simp add: lfp_gfp)
   116 
   117 lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
   118   by (simp add: lfp_gfp)
   119 
   120 text {*
   121   in order to give dual fixed point representations of @{term "AF p"}
   122   and @{term "AG p"}:
   123 *}
   124 
   125 lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
   126 lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
   127 
   128 lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
   129 proof -
   130   have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
   131   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
   132 qed
   133 
   134 lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
   135 proof -
   136   have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
   137   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
   138 qed
   139 
   140 lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
   141 proof -
   142   have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
   143   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
   144 qed
   145 
   146 text {*
   147   From the greatest fixed point definition of @{term "\<AG> p"}, we
   148   derive as a consequence of the Knaster-Tarski theorem on the one
   149   hand that @{term "\<AG> p"} is a fixed point of the monotonic
   150   function @{term "\<lambda>s. p \<inter> \<AX> s"}.
   151 *}
   152 
   153 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
   154 proof -
   155   have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
   156   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
   157 qed
   158 
   159 text {*
   160   This fact may be split up into two inequalities (merely using
   161   transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
   162   @{text "\<le>"} in Isabelle/HOL).
   163 *}
   164 
   165 lemma AG_fp_1: "\<AG> p \<subseteq> p"
   166 proof -
   167   note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
   168   finally show ?thesis .
   169 qed
   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 subsection {* 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           moreover have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
   256           ultimately 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           by (rule Int_greatest)
   266         also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
   267         finally show ?thesis .
   268       qed
   269     qed
   270   qed
   271 next
   272   show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
   273   proof
   274     show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   275     show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
   276     proof -
   277       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   278       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
   279       also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
   280       finally show ?thesis .
   281     qed
   282   qed
   283 qed
   284 
   285 
   286 subsection {* An application of tree induction \label{sec:calc-ctl-commute} *}
   287 
   288 text {*
   289   Further interesting properties of CTL expressions may be
   290   demonstrated with the help of tree induction; here we show that
   291   @{text \<AX>} and @{text \<AG>} commute.
   292 *}
   293 
   294 theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
   295 proof -
   296   have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
   297   also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
   298   also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")
   299   proof  
   300     have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
   301     also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
   302     also note Int_mono AG_mono
   303     ultimately show "?lhs \<subseteq> \<AG> p" by fast
   304   next  
   305     have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   306     moreover 
   307     {
   308       have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   309       also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
   310       also note AG_mono
   311       ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
   312     } 
   313     ultimately show "\<AG> p \<subseteq> ?lhs" ..
   314   qed  
   315   finally show ?thesis .
   316 qed
   317 
   318 end