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> _"  90)    "\<EX> p \<equiv> {s. \<exists>s'. (s, s') \<in> \<M> \<and> s' \<in> p}"
1.67 +  EF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EF> _"  90)    "\<EF> p \<equiv> lfp (\<lambda>s. p \<union> \<EX> s)"
1.68 +  EG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<EG> _"  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> _"  90)    "\<AX> p \<equiv> - \<EX> - p"
1.78 +  AF :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AF> _"  90)    "\<AF> p \<equiv> - \<EG> - p"
1.79 +  AG :: "'a ctl \<Rightarrow> 'a ctl"    ("\<AG> _"  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