src/HOL/ex/CTL.thy
changeset 15871 e524119dbf19
child 16417 9bc16273c2d4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/CTL.thy	Thu Apr 28 17:08:08 2005 +0200
     1.3 @@ -0,0 +1,317 @@
     1.4 +
     1.5 +(*  Title:      HOL/ex/CTL.thy
     1.6 +    ID:         $Id$
     1.7 +    Author:     Gertrud Bauer
     1.8 +*)
     1.9 +
    1.10 +header {* CTL formulae *}
    1.11 +
    1.12 +theory CTL = Main:
    1.13 +
    1.14 +
    1.15 +
    1.16 +text {*
    1.17 +  We formalize basic concepts of Computational Tree Logic (CTL)
    1.18 +  \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
    1.19 +  simply-typed set theory of HOL.
    1.20 +
    1.21 +  By using the common technique of ``shallow embedding'', a CTL
    1.22 +  formula is identified with the corresponding set of states where it
    1.23 +  holds.  Consequently, CTL operations such as negation, conjunction,
    1.24 +  disjunction simply become complement, intersection, union of sets.
    1.25 +  We only require a separate operation for implication, as point-wise
    1.26 +  inclusion is usually not encountered in plain set-theory.
    1.27 +*}
    1.28 +
    1.29 +lemmas [intro!] = Int_greatest Un_upper2 Un_upper1 Int_lower1 Int_lower2
    1.30 +
    1.31 +types 'a ctl = "'a set"
    1.32 +constdefs
    1.33 +  imp :: "'a ctl \<Rightarrow> 'a ctl \<Rightarrow> 'a ctl"    (infixr "\<rightarrow>" 75)
    1.34 +  "p \<rightarrow> q \<equiv> - p \<union> q"
    1.35 +
    1.36 +lemma [intro!]: "p \<inter> p \<rightarrow> q \<subseteq> q" by (unfold imp_def) auto
    1.37 +lemma [intro!]: "p \<subseteq> (q \<rightarrow> p)" by (unfold imp_def) rule
    1.38 +
    1.39 +
    1.40 +text {*
    1.41 +  \smallskip The CTL path operators are more interesting; they are
    1.42 +  based on an arbitrary, but fixed model @{text \<M>}, which is simply
    1.43 +  a transition relation over states @{typ "'a"}.
    1.44 +*}
    1.45 +
    1.46 +consts model :: "('a \<times> 'a) set"    ("\<M>")
    1.47 +
    1.48 +text {*
    1.49 +  The operators @{text \<EX>}, @{text \<EF>}, @{text \<EG>} are taken
    1.50 +  as primitives, while @{text \<AX>}, @{text \<AF>}, @{text \<AG>} are
    1.51 +  defined as derived ones.  The formula @{text "\<EX> p"} holds in a
    1.52 +  state @{term s}, iff there is a successor state @{term s'} (with
    1.53 +  respect to the model @{term \<M>}), such that @{term p} holds in
    1.54 +  @{term s'}.  The formula @{text "\<EF> p"} holds in a state @{term
    1.55 +  s}, iff there is a path in @{text \<M>}, starting from @{term s},
    1.56 +  such that there exists a state @{term s'} on the path, such that
    1.57 +  @{term p} holds in @{term s'}.  The formula @{text "\<EG> p"} holds
    1.58 +  in a state @{term s}, iff there is a path, starting from @{term s},
    1.59 +  such that for all states @{term s'} on the path, @{term p} holds in
    1.60 +  @{term s'}.  It is easy to see that @{text "\<EF> p"} and @{text
    1.61 +  "\<EG> p"} may be expressed using least and greatest fixed points
    1.62 +  \cite{McMillan-PhDThesis}.
    1.63 +*}
    1.64 +
    1.65 +constdefs
    1.66 +  EX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EX> _" [80] 90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
    1.67 +  EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _" [80] 90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
    1.68 +  EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _" [80] 90)    "\<EG> p \<equiv> gfp (\<lambda>s. p \<inter> \<EX> s)"
    1.69 +
    1.70 +text {*
    1.71 +  @{text "\<AX>"}, @{text "\<AF>"} and @{text "\<AG>"} are now defined
    1.72 +  dually in terms of @{text "\<EX>"}, @{text "\<EF>"} and @{text
    1.73 +  "\<EG>"}.
    1.74 +*}
    1.75 +
    1.76 +constdefs
    1.77 +  AX :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AX> _" [80] 90)    "\<AX> p \<equiv> - \<EX> - p"
    1.78 +  AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _" [80] 90)    "\<AF> p \<equiv> - \<EG> - p"
    1.79 +  AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _" [80] 90)    "\<AG> p \<equiv> - \<EF> - p"
    1.80 +
    1.81 +lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
    1.82 +
    1.83 +
    1.84 +section {* Basic fixed point properties *}
    1.85 +
    1.86 +text {*
    1.87 +  First of all, we use the de-Morgan property of fixed points
    1.88 +*}
    1.89 +
    1.90 +lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
    1.91 +proof
    1.92 +  show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
    1.93 +  proof
    1.94 +    fix x assume l: "x \<in> lfp f"
    1.95 +    show "x \<in> - gfp (\<lambda>s. - f (- s))"
    1.96 +    proof
    1.97 +      assume "x \<in> gfp (\<lambda>s. - f (- s))"
    1.98 +      then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
    1.99 +      then have "f (- u) \<subseteq> - u" by auto
   1.100 +      then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
   1.101 +      from l and this have "x \<notin> u" by auto
   1.102 +      then show False by contradiction
   1.103 +    qed
   1.104 +  qed
   1.105 +  show "- gfp (\<lambda>s. - f (- s)) \<subseteq> lfp f"
   1.106 +  proof (rule lfp_greatest)
   1.107 +    fix u assume "f u \<subseteq> u"
   1.108 +    then have "- u \<subseteq> - f u" by auto
   1.109 +    then have "- u \<subseteq> - f (- (- u))" by simp
   1.110 +    then have "- u \<subseteq> gfp (\<lambda>s. - f (- s))" by (rule gfp_upperbound)
   1.111 +    then show "- gfp (\<lambda>s. - f (- s)) \<subseteq> u" by auto
   1.112 +  qed
   1.113 +qed
   1.114 +
   1.115 +lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
   1.116 +  by (simp add: lfp_gfp)
   1.117 +
   1.118 +lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
   1.119 +  by (simp add: lfp_gfp)
   1.120 +
   1.121 +text {*
   1.122 +  in order to give dual fixed point representations of @{term "AF p"}
   1.123 +  and @{term "AG p"}:
   1.124 +*}
   1.125 +
   1.126 +lemma AF_lfp: "\<AF> p = lfp (\<lambda>s. p \<union> \<AX> s)" by (simp add: lfp_gfp)
   1.127 +lemma AG_gfp: "\<AG> p = gfp (\<lambda>s. p \<inter> \<AX> s)" by (simp add: lfp_gfp)
   1.128 +
   1.129 +lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
   1.130 +proof -
   1.131 +  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
   1.132 +  then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
   1.133 +qed
   1.134 +
   1.135 +lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
   1.136 +proof -
   1.137 +  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
   1.138 +  then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
   1.139 +qed
   1.140 +
   1.141 +lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
   1.142 +proof -
   1.143 +  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
   1.144 +  then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
   1.145 +qed
   1.146 +
   1.147 +text {*
   1.148 +  From the greatest fixed point definition of @{term "\<AG> p"}, we
   1.149 +  derive as a consequence of the Knaster-Tarski theorem on the one
   1.150 +  hand that @{term "\<AG> p"} is a fixed point of the monotonic
   1.151 +  function @{term "\<lambda>s. p \<inter> \<AX> s"}.
   1.152 +*}
   1.153 +
   1.154 +lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
   1.155 +proof -
   1.156 +  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
   1.157 +  then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
   1.158 +qed
   1.159 +
   1.160 +text {*
   1.161 +  This fact may be split up into two inequalities (merely using
   1.162 +  transitivity of @{text "\<subseteq>" }, which is an instance of the overloaded
   1.163 +  @{text "\<le>"} in Isabelle/HOL).
   1.164 +*}
   1.165 +
   1.166 +lemma AG_fp_1: "\<AG> p \<subseteq> p"
   1.167 +proof -
   1.168 +  note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> p" by auto
   1.169 +  finally show ?thesis .
   1.170 +qed
   1.171 +
   1.172 +text {**}
   1.173 +
   1.174 +lemma AG_fp_2: "\<AG> p \<subseteq> \<AX> \<AG> p"
   1.175 +proof -
   1.176 +  note AG_fp also have "p \<inter> \<AX> \<AG> p \<subseteq> \<AX> \<AG> p" by auto
   1.177 +  finally show ?thesis .
   1.178 +qed
   1.179 +
   1.180 +text {*
   1.181 +  On the other hand, we have from the Knaster-Tarski fixed point
   1.182 +  theorem that any other post-fixed point of @{term "\<lambda>s. p \<inter> AX s"} is
   1.183 +  smaller than @{term "AG p"}.  A post-fixed point is a set of states
   1.184 +  @{term q} such that @{term "q \<subseteq> p \<inter> AX q"}.  This leads to the
   1.185 +  following co-induction principle for @{term "AG p"}.
   1.186 +*}
   1.187 +
   1.188 +lemma AG_I: "q \<subseteq> p \<inter> \<AX> q \<Longrightarrow> q \<subseteq> \<AG> p"
   1.189 +  by (simp only: AG_gfp) (rule gfp_upperbound)
   1.190 +
   1.191 +
   1.192 +section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
   1.193 +
   1.194 +text {*
   1.195 +  With the most basic facts available, we are now able to establish a
   1.196 +  few more interesting results, leading to the \emph{tree induction}
   1.197 +  principle for @{text AG} (see below).  We will use some elementary
   1.198 +  monotonicity and distributivity rules.
   1.199 +*}
   1.200 +
   1.201 +lemma AX_int: "\<AX> (p \<inter> q) = \<AX> p \<inter> \<AX> q" by auto 
   1.202 +lemma AX_mono: "p \<subseteq> q \<Longrightarrow> \<AX> p \<subseteq> \<AX> q" by auto
   1.203 +lemma AG_mono: "p \<subseteq> q \<Longrightarrow> \<AG> p \<subseteq> \<AG> q"
   1.204 +  by (simp only: AG_gfp, rule gfp_mono) auto 
   1.205 +
   1.206 +text {*
   1.207 +  The formula @{term "AG p"} implies @{term "AX p"} (we use
   1.208 +  substitution of @{text "\<subseteq>"} with monotonicity).
   1.209 +*}
   1.210 +
   1.211 +lemma AG_AX: "\<AG> p \<subseteq> \<AX> p"
   1.212 +proof -
   1.213 +  have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
   1.214 +  also have "\<AG> p \<subseteq> p" by (rule AG_fp_1) moreover note AX_mono
   1.215 +  finally show ?thesis .
   1.216 +qed
   1.217 +
   1.218 +text {*
   1.219 +  Furthermore we show idempotency of the @{text "\<AG>"} operator.
   1.220 +  The proof is a good example of how accumulated facts may get
   1.221 +  used to feed a single rule step.
   1.222 +*}
   1.223 +
   1.224 +lemma AG_AG: "\<AG> \<AG> p = \<AG> p"
   1.225 +proof
   1.226 +  show "\<AG> \<AG> p \<subseteq> \<AG> p" by (rule AG_fp_1)
   1.227 +next
   1.228 +  show "\<AG> p \<subseteq> \<AG> \<AG> p"
   1.229 +  proof (rule AG_I)
   1.230 +    have "\<AG> p \<subseteq> \<AG> p" ..
   1.231 +    moreover have "\<AG> p \<subseteq> \<AX> \<AG> p" by (rule AG_fp_2)
   1.232 +    ultimately show "\<AG> p \<subseteq> \<AG> p \<inter> \<AX> \<AG> p" ..
   1.233 +  qed
   1.234 +qed
   1.235 +
   1.236 +text {*
   1.237 +  \smallskip We now give an alternative characterization of the @{text
   1.238 +  "\<AG>"} operator, which describes the @{text "\<AG>"} operator in
   1.239 +  an ``operational'' way by tree induction: In a state holds @{term
   1.240 +  "AG p"} iff in that state holds @{term p}, and in all reachable
   1.241 +  states @{term s} follows from the fact that @{term p} holds in
   1.242 +  @{term s}, that @{term p} also holds in all successor states of
   1.243 +  @{term s}.  We use the co-induction principle @{thm [source] AG_I}
   1.244 +  to establish this in a purely algebraic manner.
   1.245 +*}
   1.246 +
   1.247 +theorem AG_induct: "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p"
   1.248 +proof
   1.249 +  show "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> p"  (is "?lhs \<subseteq> _")
   1.250 +  proof (rule AG_I)
   1.251 +    show "?lhs \<subseteq> p \<inter> \<AX> ?lhs"
   1.252 +    proof
   1.253 +      show "?lhs \<subseteq> p" ..
   1.254 +      show "?lhs \<subseteq> \<AX> ?lhs"
   1.255 +      proof -
   1.256 +	{
   1.257 +	  have "\<AG> (p \<rightarrow> \<AX> p) \<subseteq> p \<rightarrow> \<AX> p" by (rule AG_fp_1)
   1.258 +          also have "p \<inter> p \<rightarrow> \<AX> p \<subseteq> \<AX> p" ..
   1.259 +          finally have "?lhs \<subseteq> \<AX> p" by auto
   1.260 +	}  
   1.261 +	moreover
   1.262 +	{
   1.263 +	  have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) \<subseteq> \<AG> (p \<rightarrow> \<AX> p)" ..
   1.264 +          also have "\<dots> \<subseteq> \<AX> \<dots>" by (rule AG_fp_2)
   1.265 +          finally have "?lhs \<subseteq> \<AX> \<AG> (p \<rightarrow> \<AX> p)" .
   1.266 +	}  
   1.267 +	ultimately have "?lhs \<subseteq> \<AX> p \<inter> \<AX> \<AG> (p \<rightarrow> \<AX> p)" ..
   1.268 +	also have "\<dots> = \<AX> ?lhs" by (simp only: AX_int)
   1.269 +	finally show ?thesis .
   1.270 +      qed
   1.271 +    qed
   1.272 +  qed
   1.273 +next
   1.274 +  show "\<AG> p \<subseteq> p \<inter> \<AG> (p \<rightarrow> \<AX> p)"
   1.275 +  proof
   1.276 +    show "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   1.277 +    show "\<AG> p \<subseteq> \<AG> (p \<rightarrow> \<AX> p)"
   1.278 +    proof -
   1.279 +      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   1.280 +      also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX) moreover note AG_mono
   1.281 +      also have "\<AX> p \<subseteq> (p \<rightarrow> \<AX> p)" .. moreover note AG_mono
   1.282 +      finally show ?thesis .
   1.283 +    qed
   1.284 +  qed
   1.285 +qed
   1.286 +
   1.287 +
   1.288 +section {* An application of tree induction \label{sec:calc-ctl-commute} *}
   1.289 +
   1.290 +text {*
   1.291 +  Further interesting properties of CTL expressions may be
   1.292 +  demonstrated with the help of tree induction; here we show that
   1.293 +  @{text \<AX>} and @{text \<AG>} commute.
   1.294 +*}
   1.295 +
   1.296 +theorem AG_AX_commute: "\<AG> \<AX> p = \<AX> \<AG> p"
   1.297 +proof -
   1.298 +  have "\<AG> \<AX> p = \<AX> p \<inter> \<AX> \<AG> \<AX> p" by (rule AG_fp)
   1.299 +  also have "\<dots> = \<AX> (p \<inter> \<AG> \<AX> p)" by (simp only: AX_int)
   1.300 +  also have "p \<inter> \<AG> \<AX> p = \<AG> p"  (is "?lhs = _")
   1.301 +  proof  
   1.302 +    have "\<AX> p \<subseteq> p \<rightarrow> \<AX> p" ..
   1.303 +    also have "p \<inter> \<AG> (p \<rightarrow> \<AX> p) = \<AG> p" by (rule AG_induct)
   1.304 +    also note Int_mono AG_mono
   1.305 +    ultimately show "?lhs \<subseteq> \<AG> p" by fast
   1.306 +  next  
   1.307 +    have "\<AG> p \<subseteq> p" by (rule AG_fp_1)
   1.308 +    moreover 
   1.309 +    {
   1.310 +      have "\<AG> p = \<AG> \<AG> p" by (simp only: AG_AG)
   1.311 +      also have "\<AG> p \<subseteq> \<AX> p" by (rule AG_AX)
   1.312 +      also note AG_mono
   1.313 +      ultimately have "\<AG> p \<subseteq> \<AG> \<AX> p" .
   1.314 +    } 
   1.315 +    ultimately show "\<AG> p \<subseteq> ?lhs" ..
   1.316 +  qed  
   1.317 +  finally show ?thesis .
   1.318 +qed
   1.319 +
   1.320 +end