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