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