1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath; 9 10map load 11 ["tuerk_tacticsLib", "res_quanTools", "prop_logicTheory", 12 "infinite_pathTheory", "symbolic_kripke_structureTheory", "numLib", 13 "full_ltlTheory", "pred_setTheory", 14 "symbolic_semi_automatonTheory", "automaton_formulaTheory", 15 "temporal_deep_mixedTheory", "pairTheory", "set_lemmataTheory"]; 16*) 17 18open tuerk_tacticsLib res_quanTools prop_logicTheory infinite_pathTheory 19 symbolic_kripke_structureTheory numLib full_ltlTheory pred_setTheory 20 symbolic_semi_automatonTheory automaton_formulaTheory 21 temporal_deep_mixedTheory pairTheory set_lemmataTheory; 22open Sanity; 23 24val _ = hide "S"; 25val _ = hide "I"; 26 27(* 28show_assums := false; 29show_assums := true; 30show_types := true; 31show_types := false; 32quietdec := false; 33*) 34 35val _ = new_theory "ctl_star"; 36 37 38val ctl_star_def = 39 Hol_datatype 40 `ctl_star = CTL_STAR_PROP of 'a prop_logic (* boolean expression *) 41 | CTL_STAR_NOT of ctl_star (* \neg f *) 42 | CTL_STAR_AND of ctl_star # ctl_star (* f1 \wedge f2 *) 43 | CTL_STAR_PSNEXT of ctl_star (* X f *) 44 | CTL_STAR_PSUNTIL of ctl_star # ctl_star (* f1 U f2 *) 45 | CTL_STAR_NEXT of ctl_star (* X f *) 46 | CTL_STAR_SUNTIL of ctl_star # ctl_star (* f1 U f2 *) 47 | CTL_STAR_E of ctl_star`; (* E f *) 48 49 50val ctl_star_induct = 51 save_thm 52 ("ctl_star_induct", 53 Q.GEN 54 `P` 55 (MATCH_MP 56 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 57 (SIMP_RULE 58 std_ss 59 [pairTheory.FORALL_PROD, 60 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 61 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 62 (Q.SPECL 63 [`P`,`\(f1,f2). P f1 /\ P f2`] 64 (TypeBase.induction_of ``:'a ctl_star``))))); 65 66 67val CTL_STAR_SEM_PATH_TIME_def = 68 Define ` 69 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PROP b) p = (P_SEM (p t) b)) /\ 70 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_NOT f) p = ~(CTL_STAR_SEM_PATH_TIME t M f p)) /\ 71 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_AND(f1,f2)) p = CTL_STAR_SEM_PATH_TIME t M f1 p /\ CTL_STAR_SEM_PATH_TIME t M f2 p) /\ 72 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_NEXT f) p = CTL_STAR_SEM_PATH_TIME (SUC t) M f p) /\ 73 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PSNEXT f) p = (t > 0 /\ CTL_STAR_SEM_PATH_TIME (PRE t) M f p)) /\ 74 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_E f) p = (?p'. (p' 0 = p t) /\ 75 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p' /\ CTL_STAR_SEM_PATH_TIME 0 M f p')) /\ 76 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_SUNTIL(f1,f2)) p = (?k. k >= t /\ CTL_STAR_SEM_PATH_TIME k M f2 p /\ 77 (!j. (t <= j /\ j < k) ==> CTL_STAR_SEM_PATH_TIME j M f1 p ))) /\ 78 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PSUNTIL(f1,f2)) p = (?k. k <= t /\ CTL_STAR_SEM_PATH_TIME k M f2 p /\ 79 (!j. (k < j /\ j <= t) ==> CTL_STAR_SEM_PATH_TIME j M f1 p )))`; 80 81 82val CTL_STAR_SEM_PATH_def = 83 Define ` 84 CTL_STAR_SEM_PATH M f p = CTL_STAR_SEM_PATH_TIME 0 M f p`; 85 86 87 88val CTL_STAR_SEM_STATE_def = 89 Define 90 `(CTL_STAR_SEM_STATE M (CTL_STAR_PROP b) s = P_SEM s b) /\ 91 (CTL_STAR_SEM_STATE M (CTL_STAR_NOT f) s = ~(CTL_STAR_SEM_STATE M f s)) /\ 92 (CTL_STAR_SEM_STATE M (CTL_STAR_AND(f1,f2)) s = CTL_STAR_SEM_STATE M f1 s /\ CTL_STAR_SEM_STATE M f2 s) /\ 93 (CTL_STAR_SEM_STATE M (CTL_STAR_E f) s = (?p'. (p' 0 = s) /\ 94 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p' /\ CTL_STAR_SEM_PATH M f p'))`; 95 96 97val CTL_STAR_KS_SEM_def = 98 Define 99 `CTL_STAR_KS_SEM M f = (!s. P_SEM s M.S0 ==> CTL_STAR_SEM_STATE M f s)`; 100 101 102val IS_CTL_STAR_PATH_FORMULA_def = 103 Define ` 104 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_PROP b) = T) /\ 105 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_NOT f) = IS_CTL_STAR_PATH_FORMULA f) /\ 106 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_AND(f1,f2)) = IS_CTL_STAR_PATH_FORMULA f1 /\ IS_CTL_STAR_PATH_FORMULA f2) /\ 107 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_NEXT f) = IS_CTL_STAR_PATH_FORMULA f) /\ 108 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_PSNEXT f) = IS_CTL_STAR_PATH_FORMULA f) /\ 109 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_E f) = F) /\ 110 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_SUNTIL(f1,f2)) = IS_CTL_STAR_PATH_FORMULA f1 /\ IS_CTL_STAR_PATH_FORMULA f2) /\ 111 (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_PSUNTIL(f1,f2)) = IS_CTL_STAR_PATH_FORMULA f1 /\ IS_CTL_STAR_PATH_FORMULA f2)`; 112 113 114val IS_CTL_STAR_STATE_FORMULA_def = 115 Define ` 116 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_PROP b) = T) /\ 117 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_NOT f) = IS_CTL_STAR_STATE_FORMULA f) /\ 118 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_AND(f1,f2)) = IS_CTL_STAR_STATE_FORMULA f1 /\ IS_CTL_STAR_STATE_FORMULA f2) /\ 119 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_NEXT f) = F) /\ 120 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_PSNEXT f) = F) /\ 121 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_E f) = T) /\ 122 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_SUNTIL(f1,f2)) = F) /\ 123 (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_PSUNTIL(f1,f2)) = F)`; 124 125 126val IS_CTL_STAR_PROP_FORMULA_def = 127 Define ` 128 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_PROP b) = T) /\ 129 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_NOT f) = IS_CTL_STAR_PROP_FORMULA f) /\ 130 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_AND(f1,f2)) = IS_CTL_STAR_PROP_FORMULA f1 /\ IS_CTL_STAR_PROP_FORMULA f2) /\ 131 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_NEXT f) = F) /\ 132 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_PSNEXT f) = F) /\ 133 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_E f) = F) /\ 134 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_SUNTIL(f1,f2)) = F) /\ 135 (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_PSUNTIL(f1,f2)) = F)`; 136 137 138val CTL_STAR_USED_VARS_def = 139 Define ` 140 (CTL_STAR_USED_VARS (CTL_STAR_PROP b) = P_USED_VARS b) /\ 141 (CTL_STAR_USED_VARS (CTL_STAR_NOT f) = CTL_STAR_USED_VARS f) /\ 142 (CTL_STAR_USED_VARS (CTL_STAR_AND(f1,f2)) = CTL_STAR_USED_VARS f1 UNION CTL_STAR_USED_VARS f2) /\ 143 (CTL_STAR_USED_VARS (CTL_STAR_NEXT f) = CTL_STAR_USED_VARS f) /\ 144 (CTL_STAR_USED_VARS (CTL_STAR_PSNEXT f) = CTL_STAR_USED_VARS f) /\ 145 (CTL_STAR_USED_VARS (CTL_STAR_E f) = CTL_STAR_USED_VARS f) /\ 146 (CTL_STAR_USED_VARS (CTL_STAR_SUNTIL(f1,f2)) = CTL_STAR_USED_VARS f1 UNION CTL_STAR_USED_VARS f2) /\ 147 (CTL_STAR_USED_VARS (CTL_STAR_PSUNTIL(f1,f2)) = CTL_STAR_USED_VARS f1 UNION CTL_STAR_USED_VARS f2)`; 148 149 150val FINITE___CTL_STAR_USED_VARS = 151 store_thm 152 ("FINITE___CTL_STAR_USED_VARS", 153 154 ``!p. FINITE(CTL_STAR_USED_VARS p)``, 155 156 INDUCT_THEN ctl_star_induct ASSUME_TAC THEN ( 157 ASM_REWRITE_TAC[CTL_STAR_USED_VARS_def, FINITE___P_USED_VARS, 158 FINITE_UNION] 159 )); 160 161 162val IS_CTL_STAR_PROP_FORMULA___IS_PATH_STATE_FORMULA = 163 store_thm 164 ("IS_CTL_STAR_PROP_FORMULA___IS_PATH_STATE_FORMULA", 165 166 ``!f. IS_CTL_STAR_PROP_FORMULA f = (IS_CTL_STAR_STATE_FORMULA f /\ IS_CTL_STAR_PATH_FORMULA f)``, 167 168 INDUCT_THEN ctl_star_induct ASSUME_TAC THEN 169 FULL_SIMP_TAC std_ss [IS_CTL_STAR_STATE_FORMULA_def, 170 IS_CTL_STAR_PATH_FORMULA_def, IS_CTL_STAR_PROP_FORMULA_def] THEN 171 METIS_TAC[]); 172 173 174(*For state formulas just the first element of a path matters*) 175val IS_CTL_STAR_STATE_FORMULA___SEM = 176 store_thm 177 ("IS_CTL_STAR_STATE_FORMULA___SEM", 178 179 ``!f t M p s. (IS_CTL_STAR_STATE_FORMULA f /\ (p t = s)) ==> 180 (CTL_STAR_SEM_STATE M f s = CTL_STAR_SEM_PATH_TIME t M f p)``, 181 182 INDUCT_THEN ctl_star_induct ASSUME_TAC THEN 183 FULL_SIMP_TAC std_ss [IS_CTL_STAR_STATE_FORMULA_def, 184 CTL_STAR_SEM_STATE_def, CTL_STAR_SEM_PATH_def, 185 CTL_STAR_SEM_PATH_TIME_def]); 186 187 188(*This inspieres the following definitions*) 189val CTL_STAR_SEM_NO_MODEL_PATH_TIME_def = 190 Define ` 191 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_PROP b) p = (P_SEM (p t) b)) /\ 192 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_NOT f) p = ~(CTL_STAR_SEM_NO_MODEL_PATH_TIME t f p)) /\ 193 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_AND(f1,f2)) p = CTL_STAR_SEM_NO_MODEL_PATH_TIME t f1 p /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME t f2 p) /\ 194 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_NEXT f) p = CTL_STAR_SEM_NO_MODEL_PATH_TIME (SUC t) f p) /\ 195 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_PSNEXT f) p = (t > 0 /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME (PRE t) f p)) /\ 196 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_SUNTIL(f1,f2)) p = (?k. k >= t /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME k f2 p /\ 197 (!j. (t <= j /\ j < k) ==> CTL_STAR_SEM_NO_MODEL_PATH_TIME j f1 p ))) /\ 198 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_PSUNTIL(f1,f2)) p = (?k. k <= t /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME k f2 p /\ 199 (!j. (k < j /\ j <= t) ==> CTL_STAR_SEM_NO_MODEL_PATH_TIME j f1 p)))`; 200 201val CTL_STAR_SEM_NO_MODEL_PATH_def = 202 Define ` 203 CTL_STAR_SEM_NO_MODEL_PATH f p = CTL_STAR_SEM_NO_MODEL_PATH_TIME 0 f p`; 204 205 206val IS_CTL_STAR_PATH_FORMULA___NO_MODEL_SEM = 207 store_thm 208 ("IS_CTL_STAR_PATH_FORMULA___NO_MODEL_SEM", 209 210 ``!f t M p. IS_CTL_STAR_PATH_FORMULA f ==> 211 (CTL_STAR_SEM_PATH_TIME t M f p = 212 CTL_STAR_SEM_NO_MODEL_PATH_TIME t f p)``, 213 214 INDUCT_THEN ctl_star_induct ASSUME_TAC THEN 215 FULL_SIMP_TAC std_ss [IS_CTL_STAR_PATH_FORMULA_def, 216 CTL_STAR_SEM_PATH_TIME_def, CTL_STAR_SEM_NO_MODEL_PATH_TIME_def] THEN 217 METIS_TAC[]); 218 219 220 221val CTL_STAR_USED_VARS_LABEL_RESTRICT_THM___NO_MODEL_SEM_PATH_TIME = 222 store_thm 223 ("CTL_STAR_USED_VARS_LABEL_RESTRICT_THM___NO_MODEL_SEM_PATH_TIME", 224 ``!f t p S. (CTL_STAR_USED_VARS f SUBSET S /\ 225 IS_CTL_STAR_PATH_FORMULA f) ==> 226 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t f p = 227 CTL_STAR_SEM_NO_MODEL_PATH_TIME t f (PATH_RESTRICT p S))``, 228 229 INDUCT_THEN ctl_star_induct ASSUME_TAC THEN1 ( 230 (*Case PROP*) 231 SIMP_TAC std_ss [CTL_STAR_USED_VARS_def, CTL_STAR_SEM_NO_MODEL_PATH_TIME_def, 232 PATH_RESTRICT_def, PATH_MAP_def] THEN 233 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] 234 ) THEN 235 ASM_SIMP_TAC std_ss [CTL_STAR_USED_VARS_def, CTL_STAR_SEM_NO_MODEL_PATH_TIME_def, UNION_SUBSET, IS_CTL_STAR_PATH_FORMULA_def] THEN 236 PROVE_TAC[]); 237 238 239val CTL_STAR_USED_VARS_NO_MODEL_SEM_PATH_TIME___PATH_RESTRICT_THM = 240 store_thm 241 ("CTL_STAR_USED_VARS_NO_MODEL_SEM_PATH_TIME___PATH_RESTRICT_THM", 242 ``!f t p. IS_CTL_STAR_PATH_FORMULA f ==> 243 (CTL_STAR_SEM_NO_MODEL_PATH_TIME t f p = 244 CTL_STAR_SEM_NO_MODEL_PATH_TIME t f (PATH_RESTRICT p (CTL_STAR_USED_VARS f)))``, 245 246 PROVE_TAC[SUBSET_REFL, CTL_STAR_USED_VARS_LABEL_RESTRICT_THM___NO_MODEL_SEM_PATH_TIME]); 247 248 249 250 251(****************************************************************************** 252* Syntactic Sugar 253******************************************************************************) 254val CTL_STAR_A_def = Define `CTL_STAR_A f = CTL_STAR_NOT (CTL_STAR_E(CTL_STAR_NOT f))`; 255val CTL_STAR_OR_def = Define `CTL_STAR_OR(f1,f2) = CTL_STAR_NOT (CTL_STAR_AND((CTL_STAR_NOT f1),(CTL_STAR_NOT f2)))`; 256val CTL_STAR_IMPL_def = Define `CTL_STAR_IMPL(f1, f2) = CTL_STAR_OR(CTL_STAR_NOT f1, f2)`; 257val CTL_STAR_COND_def = Define `CTL_STAR_COND(c, f1, f2) = CTL_STAR_AND(CTL_STAR_IMPL(c, f1), CTL_STAR_IMPL(CTL_STAR_NOT c, f2))`; 258val CTL_STAR_EQUIV_def = Define `CTL_STAR_EQUIV(b1, b2) = CTL_STAR_AND(CTL_STAR_IMPL(b1, b2),CTL_STAR_IMPL(b2, b1))`; 259val CTL_STAR_EVENTUAL_def = Define `CTL_STAR_EVENTUAL f = CTL_STAR_SUNTIL (CTL_STAR_PROP(P_TRUE),f)`; 260val CTL_STAR_ALWAYS_def = Define `CTL_STAR_ALWAYS f = CTL_STAR_NOT (CTL_STAR_EVENTUAL (CTL_STAR_NOT f))`; 261val CTL_STAR_UNTIL_def = Define `CTL_STAR_UNTIL(f1,f2) = CTL_STAR_OR(CTL_STAR_SUNTIL(f1,f2),CTL_STAR_ALWAYS f1)`; 262val CTL_STAR_BEFORE_def = Define `CTL_STAR_BEFORE(f1,f2) = CTL_STAR_NOT(CTL_STAR_SUNTIL(CTL_STAR_NOT f1,f2))`; 263val CTL_STAR_SBEFORE_def = Define `CTL_STAR_SBEFORE(f1,f2) = CTL_STAR_SUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, CTL_STAR_NOT f2))`; 264val CTL_STAR_WHILE_def = Define `CTL_STAR_WHILE(f1,f2) = CTL_STAR_NOT(CTL_STAR_SUNTIL(CTL_STAR_OR(CTL_STAR_NOT f1, CTL_STAR_NOT f2),CTL_STAR_AND(f2, CTL_STAR_NOT f1)))`; 265val CTL_STAR_SWHILE_def = Define `CTL_STAR_SWHILE(f1,f2) = CTL_STAR_SUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, f2))`; 266val CTL_STAR_PEVENTUAL_def = Define `CTL_STAR_PEVENTUAL f = CTL_STAR_PSUNTIL (CTL_STAR_PROP(P_TRUE),f)`; 267val CTL_STAR_PALWAYS_def = Define `CTL_STAR_PALWAYS f = CTL_STAR_NOT (CTL_STAR_PEVENTUAL (CTL_STAR_NOT f))`; 268val CTL_STAR_PUNTIL_def = Define `CTL_STAR_PUNTIL(f1,f2) = CTL_STAR_OR(CTL_STAR_PSUNTIL(f1,f2),CTL_STAR_PALWAYS f1)`; 269val CTL_STAR_PNEXT_def = Define `CTL_STAR_PNEXT f = CTL_STAR_NOT(CTL_STAR_PSNEXT (CTL_STAR_NOT f))`; 270val CTL_STAR_PBEFORE_def = Define `CTL_STAR_PBEFORE(f1,f2) = CTL_STAR_NOT(CTL_STAR_PSUNTIL(CTL_STAR_NOT f1,f2))`; 271val CTL_STAR_PSBEFORE_def = Define `CTL_STAR_PSBEFORE(f1,f2) = CTL_STAR_PSUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, CTL_STAR_NOT f2))`; 272val CTL_STAR_PWHILE_def = Define `CTL_STAR_PWHILE(f1,f2) = CTL_STAR_NOT(CTL_STAR_PSUNTIL(CTL_STAR_OR(CTL_STAR_NOT f1, CTL_STAR_NOT f2),CTL_STAR_AND(f2, CTL_STAR_NOT f1)))`; 273val CTL_STAR_PSWHILE_def = Define `CTL_STAR_PSWHILE(f1,f2) = CTL_STAR_PSUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, f2))`; 274 275val CTL_STAR_FAIRNESS_def = 276 Define 277 `(CTL_STAR_FAIRNESS [] = (CTL_STAR_PROP (P_TRUE))) /\ 278 (CTL_STAR_FAIRNESS (f::FC) = (CTL_STAR_AND (CTL_STAR_ALWAYS(CTL_STAR_EVENTUAL (CTL_STAR_PROP f)), CTL_STAR_FAIRNESS FC)))`; 279 280val CTL_STAR_FAIR_E_def = Define `CTL_STAR_FAIR_E FC f = (CTL_STAR_E (CTL_STAR_AND(f, CTL_STAR_FAIRNESS FC)))`; 281val CTL_STAR_FAIR_A_def = Define `CTL_STAR_FAIR_A FC f = (CTL_STAR_A (CTL_STAR_IMPL(CTL_STAR_FAIRNESS FC, f)))`; 282 283 284val CTL_STAR_SEM___PROP_CASES = 285 prove (``!M f1 f2 p s t. 286 (CTL_STAR_SEM_PATH M (CTL_STAR_OR(f1, f2)) p = 287 (CTL_STAR_SEM_PATH M f1 p \/ CTL_STAR_SEM_PATH M f2 p)) /\ 288 (CTL_STAR_SEM_PATH M (CTL_STAR_IMPL(f1, f2)) p = 289 (CTL_STAR_SEM_PATH M f1 p ==> CTL_STAR_SEM_PATH M f2 p)) /\ 290 (CTL_STAR_SEM_PATH M (CTL_STAR_EQUIV(f1, f2)) p = 291 (CTL_STAR_SEM_PATH M f1 p = CTL_STAR_SEM_PATH M f2 p)) /\ 292 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_OR(f1, f2)) p = 293 (CTL_STAR_SEM_PATH_TIME t M f1 p \/ CTL_STAR_SEM_PATH_TIME t M f2 p)) /\ 294 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_IMPL(f1, f2)) p = 295 (CTL_STAR_SEM_PATH_TIME t M f1 p ==> CTL_STAR_SEM_PATH_TIME t M f2 p)) /\ 296 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_EQUIV(f1, f2)) p = 297 (CTL_STAR_SEM_PATH_TIME t M f1 p = CTL_STAR_SEM_PATH_TIME t M f2 p)) /\ 298 (CTL_STAR_SEM_STATE M (CTL_STAR_OR(f1, f2)) s = 299 (CTL_STAR_SEM_STATE M f1 s \/ CTL_STAR_SEM_STATE M f2 s)) /\ 300 (CTL_STAR_SEM_STATE M (CTL_STAR_IMPL(f1, f2)) s = 301 (CTL_STAR_SEM_STATE M f1 s ==> CTL_STAR_SEM_STATE M f2 s)) /\ 302 (CTL_STAR_SEM_STATE M (CTL_STAR_EQUIV(f1, f2)) s = 303 (CTL_STAR_SEM_STATE M f1 s = CTL_STAR_SEM_STATE M f2 s))``, 304 305 REPEAT GEN_TAC THEN 306 SIMP_TAC std_ss [CTL_STAR_SEM_PATH_def, CTL_STAR_SEM_PATH_TIME_def, CTL_STAR_SEM_STATE_def, 307 CTL_STAR_OR_def, CTL_STAR_IMPL_def, CTL_STAR_EQUIV_def, 308 CTL_STAR_SEM_STATE_def] THEN 309 METIS_TAC[]); 310 311 312val CTL_STAR_SEM___EVENTUAL_ALWAYS = 313 prove (``!M t f p. 314 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_EVENTUAL f) p = 315 (?k. k >= t /\ CTL_STAR_SEM_PATH_TIME k M f p)) /\ 316 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_ALWAYS f) p = 317 (!k. k >= t ==> CTL_STAR_SEM_PATH_TIME k M f p)) /\ 318 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PEVENTUAL f) p = 319 (?k. k <= t /\ CTL_STAR_SEM_PATH_TIME k M f p)) /\ 320 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PALWAYS f) p = 321 (!k. k <= t ==> CTL_STAR_SEM_PATH_TIME k M f p))``, 322 323 SIMP_TAC std_ss [CTL_STAR_SEM_PATH_TIME_def, CTL_STAR_EVENTUAL_def, 324 CTL_STAR_ALWAYS_def, P_SEM_THM, CTL_STAR_PALWAYS_def, CTL_STAR_PEVENTUAL_def] THEN 325 PROVE_TAC[]); 326 327 328 329val CTL_STAR_SEM___CTL_STAR_A = 330 prove (``!M f p s t. 331 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_A f) p = (!p'. ((p' 0 = p t) /\ 332 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p') ==> CTL_STAR_SEM_PATH M f p')) /\ 333 (CTL_STAR_SEM_STATE M (CTL_STAR_A f) s = (!p'. ((p' 0 = s) /\ 334 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p') ==> CTL_STAR_SEM_PATH M f p'))``, 335 336 SIMP_TAC std_ss [CTL_STAR_SEM_PATH_def, CTL_STAR_SEM_PATH_TIME_def, CTL_STAR_SEM_STATE_def, 337 CTL_STAR_A_def] THEN 338 METIS_TAC[]); 339 340 341 342val CTL_STAR_SEM___FAIRNESS = 343 store_thm ("CTL_STAR_SEM___FAIRNESS", 344 ``!M FC p t. 345 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_FAIRNESS FC) p = 346 (!b. MEM b FC ==> !t0. ?t. t >= t0 /\ P_SEM (p t) b))``, 347 348 Induct_on `FC` THENL [ 349 SIMP_TAC list_ss [CTL_STAR_FAIRNESS_def, CTL_STAR_SEM_PATH_TIME_def, P_SEM_THM], 350 351 SIMP_TAC list_ss [CTL_STAR_FAIRNESS_def, CTL_STAR_SEM_PATH_TIME_def, 352 CTL_STAR_SEM___EVENTUAL_ALWAYS, P_SEM_THM, 353 DISJ_IMP_THM, FORALL_AND_THM, PATH_RESTN_def] THEN 354 REPEAT GEN_TAC THEN 355 Tactical.REVERSE (BINOP_TAC) THEN1 ASM_REWRITE_TAC[] THEN 356 REPEAT WEAKEN_HD_TAC THEN 357 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 358 SUBGOAL_TAC `?t1. t1 >= t /\ t1 > t0` THEN1 ( 359 Cases_on `t > t0` THENL [ 360 EXISTS_TAC ``t:num`` THEN 361 ASM_SIMP_TAC arith_ss [], 362 363 EXISTS_TAC ``SUC t0`` THEN 364 FULL_SIMP_TAC arith_ss [] 365 ] 366 ) THEN 367 SPECL_NO_ASSUM 2 [``t1:num``] THEN 368 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN 369 EXISTS_TAC ``k':num`` THEN 370 ASM_SIMP_TAC arith_ss [], 371 372 SPECL_NO_ASSUM 1 [``k:num``] THEN 373 FULL_SIMP_TAC std_ss [] THEN 374 EXISTS_TAC ``t':num`` THEN 375 ASM_SIMP_TAC arith_ss [] 376 ] 377 ]); 378 379 380val CTL_STAR_SEM___FAIR_E_FAIR_A = 381 prove (``!M f t FC p s. 382 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_FAIR_E FC f) p = (?p'. (p' 0 = p t) /\ 383 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p' /\ CTL_STAR_SEM_PATH M f p')) /\ 384 (CTL_STAR_SEM_STATE M (CTL_STAR_FAIR_E FC f) s = (?p'. (p' 0 = s) /\ 385 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p' /\ CTL_STAR_SEM_PATH M f p')) /\ 386 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_FAIR_A FC f) p = (!p'. ((p' 0 = p t) /\ 387 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p') ==> CTL_STAR_SEM_PATH M f p')) /\ 388 (CTL_STAR_SEM_STATE M (CTL_STAR_FAIR_A FC f) s = (!p'. ((p' 0 = s) /\ 389 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p') ==> CTL_STAR_SEM_PATH M f p'))``, 390 391 SIMP_TAC std_ss [CTL_STAR_FAIR_E_def, CTL_STAR_FAIR_A_def, 392 CTL_STAR_SEM_STATE_def, CTL_STAR_SEM_PATH_def, CTL_STAR_SEM_PATH_TIME_def, 393 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, CTL_STAR_SEM___FAIRNESS, 394 CTL_STAR_SEM___CTL_STAR_A, CTL_STAR_SEM___PROP_CASES] THEN 395 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC arith_ss [] THEN 396 METIS_TAC[]); 397 398 399 400val CTL_STAR_SEM___EMPTY_FAIRNESS = 401 prove (``!M t f p s. 402 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_FAIR_E [] f) p = CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_E f) p) /\ 403 (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_FAIR_A [] f) p = CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_A f) p) /\ 404 (CTL_STAR_SEM_STATE M (CTL_STAR_FAIR_E [] f) s = CTL_STAR_SEM_STATE M (CTL_STAR_E f) s) /\ 405 (CTL_STAR_SEM_STATE M (CTL_STAR_FAIR_A [] f) s = CTL_STAR_SEM_STATE M (CTL_STAR_A f) s)``, 406 407 SIMP_TAC std_ss [CTL_STAR_SEM_PATH_def, CTL_STAR_SEM_PATH_TIME_def, CTL_STAR_SEM_STATE_def, 408 CTL_STAR_FAIR_E_def, CTL_STAR_FAIRNESS_def, P_SEM_THM, 409 CTL_STAR_FAIR_A_def, CTL_STAR_SEM___CTL_STAR_A, 410 CTL_STAR_SEM___PROP_CASES]); 411 412 413val CTL_STAR_SEM_THM = save_thm ("CTL_STAR_SEM_THM", 414 SIMP_RULE std_ss [FORALL_AND_THM] ( 415 LIST_CONJ [CTL_STAR_SEM_PATH_def, 416 CTL_STAR_SEM_PATH_TIME_def, 417 CTL_STAR_SEM_STATE_def, 418 CTL_STAR_SEM___PROP_CASES, 419 CTL_STAR_SEM___EVENTUAL_ALWAYS, 420 CTL_STAR_SEM___CTL_STAR_A, 421 CTL_STAR_SEM___EMPTY_FAIRNESS, 422 CTL_STAR_SEM___FAIR_E_FAIR_A])); 423 424 425 426 427(****************************************************************************** 428* SUBLANGUAGE LTL 429******************************************************************************) 430 431val LTL_TO_CTL_STAR_def = 432 Define 433 `(LTL_TO_CTL_STAR (LTL_PROP b) = (CTL_STAR_PROP b)) /\ 434 (LTL_TO_CTL_STAR (LTL_NOT f) = (CTL_STAR_NOT (LTL_TO_CTL_STAR f))) /\ 435 (LTL_TO_CTL_STAR (LTL_AND (f1, f2)) = (CTL_STAR_AND (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 436 (LTL_TO_CTL_STAR (LTL_NEXT f) = (CTL_STAR_NEXT (LTL_TO_CTL_STAR f))) /\ 437 (LTL_TO_CTL_STAR (LTL_SUNTIL (f1, f2)) = (CTL_STAR_SUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 438 (LTL_TO_CTL_STAR (LTL_PSNEXT f) = (CTL_STAR_PSNEXT (LTL_TO_CTL_STAR f))) /\ 439 (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))`; 440 441 442val LTL_TO_CTL_STAR_THM = 443 store_thm ("LTL_TO_CTL_STAR_THM", 444 ``!b f c f1 f2. 445 (LTL_TO_CTL_STAR (LTL_PROP b) = (CTL_STAR_PROP b)) /\ 446 (LTL_TO_CTL_STAR (LTL_NOT f) = (CTL_STAR_NOT (LTL_TO_CTL_STAR f))) /\ 447 (LTL_TO_CTL_STAR (LTL_AND (f1, f2)) = (CTL_STAR_AND (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 448 (LTL_TO_CTL_STAR (LTL_OR (f1, f2)) = (CTL_STAR_OR (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 449 (LTL_TO_CTL_STAR (LTL_IMPL (f1, f2)) = (CTL_STAR_IMPL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 450 (LTL_TO_CTL_STAR (LTL_COND (c, f1, f2)) = (CTL_STAR_COND (LTL_TO_CTL_STAR c, LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 451 (LTL_TO_CTL_STAR (LTL_EQUIV (f1, f2)) = (CTL_STAR_EQUIV (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 452 (LTL_TO_CTL_STAR (LTL_NEXT f) = (CTL_STAR_NEXT (LTL_TO_CTL_STAR f))) /\ 453 (LTL_TO_CTL_STAR (LTL_EVENTUAL f) = (CTL_STAR_EVENTUAL (LTL_TO_CTL_STAR f))) /\ 454 (LTL_TO_CTL_STAR (LTL_ALWAYS f) = (CTL_STAR_ALWAYS (LTL_TO_CTL_STAR f))) /\ 455 (LTL_TO_CTL_STAR (LTL_SUNTIL (f1, f2)) = (CTL_STAR_SUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 456 (LTL_TO_CTL_STAR (LTL_UNTIL (f1, f2)) = (CTL_STAR_UNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 457 (LTL_TO_CTL_STAR (LTL_BEFORE (f1, f2)) = (CTL_STAR_BEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 458 (LTL_TO_CTL_STAR (LTL_SBEFORE (f1, f2)) = (CTL_STAR_SBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 459 (LTL_TO_CTL_STAR (LTL_WHILE (f1, f2)) = (CTL_STAR_WHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 460 (LTL_TO_CTL_STAR (LTL_SWHILE (f1, f2)) = (CTL_STAR_SWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 461 (LTL_TO_CTL_STAR (LTL_PSNEXT f) = (CTL_STAR_PSNEXT (LTL_TO_CTL_STAR f))) /\ 462 (LTL_TO_CTL_STAR (LTL_PNEXT f) = (CTL_STAR_PNEXT (LTL_TO_CTL_STAR f))) /\ 463 (LTL_TO_CTL_STAR (LTL_PEVENTUAL f) = (CTL_STAR_PEVENTUAL (LTL_TO_CTL_STAR f))) /\ 464 (LTL_TO_CTL_STAR (LTL_PALWAYS f) = (CTL_STAR_PALWAYS (LTL_TO_CTL_STAR f))) /\ 465 (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 466 (LTL_TO_CTL_STAR (LTL_PUNTIL (f1, f2)) = (CTL_STAR_PUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 467 (LTL_TO_CTL_STAR (LTL_PBEFORE (f1, f2)) = (CTL_STAR_PBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 468 (LTL_TO_CTL_STAR (LTL_PSBEFORE (f1, f2)) = (CTL_STAR_PSBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 469 (LTL_TO_CTL_STAR (LTL_PWHILE (f1, f2)) = (CTL_STAR_PWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\ 470 (LTL_TO_CTL_STAR (LTL_PSWHILE (f1, f2)) = (CTL_STAR_PSWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))``, 471 472 EVAL_TAC THEN PROVE_TAC[]); 473 474 475val LTL_FORMULAS_ARE_PATH_FORMULAS = 476 store_thm ( 477 "LTL_FORMULAS_ARE_PATH_FORMULAS", 478 ``!f. IS_CTL_STAR_PATH_FORMULA (LTL_TO_CTL_STAR f)``, 479 480 INDUCT_THEN ltl_induct ASSUME_TAC THEN 481 ASM_SIMP_TAC std_ss [IS_CTL_STAR_PATH_FORMULA_def, 482 LTL_TO_CTL_STAR_def]); 483 484 485val LTL_TO_CTL_STAR_THM = 486 store_thm ("LTL_TO_CTL_STAR_THM", 487 ``!l p M t. 488 CTL_STAR_SEM_PATH_TIME t M (LTL_TO_CTL_STAR l) p = (LTL_SEM_TIME t p l)``, 489 490 INDUCT_THEN ltl_induct ASSUME_TAC THEN 491 FULL_SIMP_TAC arith_ss [LTL_TO_CTL_STAR_def, 492 LTL_SEM_THM, CTL_STAR_SEM_THM] THEN 493 PROVE_TAC[]); 494 495 496val LTL_TO_CTL_STAR_NO_MODEL_THM = 497 store_thm ("LTL_TO_CTL_STAR_NO_MODEL_THM", 498 ``!l p t. 499 CTL_STAR_SEM_NO_MODEL_PATH_TIME t (LTL_TO_CTL_STAR l) p = 500 LTL_SEM_TIME t p l``, 501 502 REPEAT STRIP_TAC THEN 503 `IS_CTL_STAR_PATH_FORMULA (LTL_TO_CTL_STAR l)` by 504 PROVE_TAC[LTL_FORMULAS_ARE_PATH_FORMULAS] THEN 505 PROVE_TAC [IS_CTL_STAR_PATH_FORMULA___NO_MODEL_SEM, 506 LTL_TO_CTL_STAR_THM]); 507 508 509 510val LTL_KS_SEM___TO___CTL_STAR_KS_SEM = 511 store_thm ("LTL_KS_SEM___TO___CTL_STAR_KS_SEM", 512 ``!M f. CTL_STAR_KS_SEM M (CTL_STAR_A (LTL_TO_CTL_STAR f)) = LTL_KS_SEM M f``, 513 514 SIMP_TAC std_ss [LTL_KS_SEM_def, CTL_STAR_KS_SEM_def, 515 LTL_TO_CTL_STAR_THM, CTL_STAR_SEM_THM, LTL_SEM_def, 516 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def] THEN 517 PROVE_TAC[]); 518 519 520 521(****************************************************************************** 522 * Fair CTL 523 ******************************************************************************) 524 525val fair_ctl_def = 526 Hol_datatype 527 `fair_ctl = FAIR_CTL_PROP of 'a prop_logic (* boolean expression *) 528 | FAIR_CTL_NOT of fair_ctl (* \neg f *) 529 | FAIR_CTL_AND of fair_ctl # fair_ctl (* f1 \wedge f2 *) 530 | FAIR_CTL_E_NEXT of ('a prop_logic list) => fair_ctl (* X f *) 531 | FAIR_CTL_E_SUNTIL of ('a prop_logic list) => (fair_ctl # fair_ctl) (* strong_until *) 532 | FAIR_CTL_E_UNTIL of ('a prop_logic list) => (fair_ctl # fair_ctl)`; (* weak until *) 533 534val fair_ctl_induct = 535 save_thm 536 ("fair_ctl_induct", 537 Q.GEN 538 `P` 539 (MATCH_MP 540 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 541 (SIMP_RULE 542 std_ss 543 [pairTheory.FORALL_PROD, 544 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 545 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 546 (Q.SPECL 547 [`P`,`\(f1,f2). P f1 /\ P f2`] 548 (TypeBase.induction_of ``:'a fair_ctl``))))); 549 550 551(*Since FAIR_CTL is a subset of CTL_STAR we can easily translate it to FAIR_CTL_STAR*) 552val FAIR_CTL_TO_CTL_STAR_def = 553 Define 554 `(FAIR_CTL_TO_CTL_STAR (FAIR_CTL_PROP b) = (CTL_STAR_PROP b)) /\ 555 (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_NOT f) = (CTL_STAR_NOT (FAIR_CTL_TO_CTL_STAR f))) /\ 556 (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_AND (f1, f2)) = (CTL_STAR_AND (FAIR_CTL_TO_CTL_STAR f1, FAIR_CTL_TO_CTL_STAR f2))) /\ 557 (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_E_NEXT FC f) = (CTL_STAR_FAIR_E FC (CTL_STAR_NEXT (FAIR_CTL_TO_CTL_STAR f)))) /\ 558 (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_E_SUNTIL FC (f1, f2)) = (CTL_STAR_FAIR_E FC (CTL_STAR_SUNTIL (FAIR_CTL_TO_CTL_STAR f1, FAIR_CTL_TO_CTL_STAR f2)))) /\ 559 (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_E_UNTIL FC (f1, f2)) = (CTL_STAR_FAIR_E FC (CTL_STAR_UNTIL (FAIR_CTL_TO_CTL_STAR f1, FAIR_CTL_TO_CTL_STAR f2))))`; 560 561 562val FAIR_CTL_SEM_def = 563 Define ` 564 FAIR_CTL_SEM M f s = CTL_STAR_SEM_STATE M (FAIR_CTL_TO_CTL_STAR f) s`; 565 566val FAIR_CTL_KS_SEM_def = 567 Define 568 `FAIR_CTL_KS_SEM M f = (!s. P_SEM s M.S0 ==> FAIR_CTL_SEM M f s)`; 569 570 571val FAIR_CTL_KS_SEM___TO___CTL_STAR_KS_SEM = 572 store_thm ("FAIR_CTL_KS_SEM___TO___CTL_STAR_KS_SEM", 573 ``!M f. FAIR_CTL_KS_SEM M f = CTL_STAR_KS_SEM M (FAIR_CTL_TO_CTL_STAR f)``, 574 575 SIMP_TAC std_ss [FAIR_CTL_KS_SEM_def, CTL_STAR_KS_SEM_def, 576 FAIR_CTL_SEM_def]); 577 578 579val FAIR_CTL_FORMULAS_ARE_STATE_FORMULAS = 580 store_thm ( 581 "FAIR_CTL_FORMULAS_ARE_STATE_FORMULAS", 582 ``!f. IS_CTL_STAR_STATE_FORMULA (FAIR_CTL_TO_CTL_STAR f)``, 583 584 INDUCT_THEN fair_ctl_induct ASSUME_TAC THEN 585 ASM_SIMP_TAC std_ss [IS_CTL_STAR_STATE_FORMULA_def, 586 FAIR_CTL_TO_CTL_STAR_def, CTL_STAR_FAIR_E_def]); 587 588 589val FAIR_CTL_USED_VARS_def = 590 Define ` 591 (FAIR_CTL_USED_VARS f = CTL_STAR_USED_VARS (FAIR_CTL_TO_CTL_STAR f))`; 592 593 594 595(*Syntactic Sugaring*) 596val FAIR_CTL_OR_def = Define `FAIR_CTL_OR(f1,f2) = FAIR_CTL_NOT (FAIR_CTL_AND((FAIR_CTL_NOT f1),(FAIR_CTL_NOT f2)))`; 597val FAIR_CTL_IMPL_def = Define `FAIR_CTL_IMPL(f1, f2) = FAIR_CTL_OR(FAIR_CTL_NOT f1, f2)`; 598val FAIR_CTL_COND_def = Define `FAIR_CTL_COND(c, f1, f2) = FAIR_CTL_AND(FAIR_CTL_IMPL(c, f1), FAIR_CTL_IMPL(FAIR_CTL_NOT c, f2))`; 599val FAIR_CTL_EQUIV_def = Define `FAIR_CTL_EQUIV(b1, b2) = FAIR_CTL_AND(FAIR_CTL_IMPL(b1, b2),FAIR_CTL_IMPL(b2, b1))`; 600val FAIR_CTL_A_NEXT_def = Define `FAIR_CTL_A_NEXT FC f = FAIR_CTL_NOT(FAIR_CTL_E_NEXT FC (FAIR_CTL_NOT f))`; 601val FAIR_CTL_E_EVENTUAL_def = Define `FAIR_CTL_E_EVENTUAL FC f = FAIR_CTL_E_SUNTIL FC (FAIR_CTL_PROP(P_TRUE),f)`; 602val FAIR_CTL_E_ALWAYS_def = Define `FAIR_CTL_E_ALWAYS FC f = FAIR_CTL_E_UNTIL FC (f, FAIR_CTL_PROP(P_FALSE))`; 603val FAIR_CTL_A_EVENTUAL_def = Define `FAIR_CTL_A_EVENTUAL FC f = FAIR_CTL_NOT (FAIR_CTL_E_ALWAYS FC (FAIR_CTL_NOT f))`; 604val FAIR_CTL_A_ALWAYS_def = Define `FAIR_CTL_A_ALWAYS FC f = FAIR_CTL_NOT (FAIR_CTL_E_EVENTUAL FC (FAIR_CTL_NOT f))`; 605val FAIR_CTL_A_UNTIL_def = Define `FAIR_CTL_A_UNTIL FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, (FAIR_CTL_AND(FAIR_CTL_NOT f1, FAIR_CTL_NOT f2))))`; 606val FAIR_CTL_A_SUNTIL_def = Define `FAIR_CTL_A_SUNTIL FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, (FAIR_CTL_AND(FAIR_CTL_NOT f1, FAIR_CTL_NOT f2))))`; 607val FAIR_CTL_E_BEFORE_def = Define `FAIR_CTL_E_BEFORE FC (f1,f2) = FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, FAIR_CTL_NOT f2))`; 608val FAIR_CTL_E_SBEFORE_def = Define `FAIR_CTL_E_SBEFORE FC (f1,f2) = FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, FAIR_CTL_NOT f2))`; 609val FAIR_CTL_A_BEFORE_def = Define `FAIR_CTL_A_BEFORE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f1, f2))`; 610val FAIR_CTL_A_SBEFORE_def = Define `FAIR_CTL_A_SBEFORE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f1, f2))`; 611val FAIR_CTL_E_WHILE_def = Define `FAIR_CTL_E_WHILE FC (f1,f2) = FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, f2))`; 612val FAIR_CTL_E_SWHILE_def = Define `FAIR_CTL_E_SWHILE FC (f1,f2) = FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, f2))`; 613val FAIR_CTL_A_WHILE_def = Define `FAIR_CTL_A_WHILE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(FAIR_CTL_NOT f1, f2)))`; 614val FAIR_CTL_A_SWHILE_def = Define `FAIR_CTL_A_SWHILE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(FAIR_CTL_NOT f1, f2)))`; 615 616 617 618val FAIR_CTL_SEM_THM___BASIC_CASES = prove( 619 ``!M b FC f f1 f2 s. 620 621 (FAIR_CTL_SEM M (FAIR_CTL_PROP b) s = (P_SEM s b)) /\ 622 623 (FAIR_CTL_SEM M (FAIR_CTL_NOT f) s = ~(FAIR_CTL_SEM M f s)) /\ 624 625 (FAIR_CTL_SEM M (FAIR_CTL_AND(f1,f2)) s = FAIR_CTL_SEM M f1 s /\ FAIR_CTL_SEM M f2 s) /\ 626 627 (FAIR_CTL_SEM M (FAIR_CTL_OR(f1,f2)) s = FAIR_CTL_SEM M f1 s \/ FAIR_CTL_SEM M f2 s) /\ 628 629 (FAIR_CTL_SEM M (FAIR_CTL_IMPL(f1,f2)) s = FAIR_CTL_SEM M f1 s ==> FAIR_CTL_SEM M f2 s) /\ 630 631 (FAIR_CTL_SEM M (FAIR_CTL_E_NEXT FC f) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 632 (p 0 = s) /\ FAIR_CTL_SEM M f (p 1))) /\ 633 634 (FAIR_CTL_SEM M (FAIR_CTL_E_SUNTIL FC (f1, f2)) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 635 (p 0 = s) /\ (?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j))))) /\ 636 637 (FAIR_CTL_SEM M (FAIR_CTL_E_UNTIL FC (f1, f2)) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 638 (p 0 = s) /\ 639 ((?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j))) \/ 640 (!j. FAIR_CTL_SEM M f1 (p j)))))``, 641 642 SIMP_TAC std_ss [FAIR_CTL_SEM_def, FAIR_CTL_TO_CTL_STAR_def, 643 CTL_STAR_SEM_THM, PATH_REST_def, 644 CTL_STAR_UNTIL_def, FAIR_CTL_OR_def, FAIR_CTL_IMPL_def] THEN 645 METIS_TAC[IS_CTL_STAR_STATE_FORMULA___SEM, FAIR_CTL_FORMULAS_ARE_STATE_FORMULAS] 646 ); 647 648 649 650val FAIR_CTL_SEM_THM___A_NEXT = prove( 651 ``!M f FC s. 652 FAIR_CTL_SEM M (FAIR_CTL_A_NEXT FC f) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 653 (p 0 = s)) ==> FAIR_CTL_SEM M f (p 1))``, 654 655 SIMP_TAC std_ss [FAIR_CTL_SEM_THM___BASIC_CASES, FAIR_CTL_TO_CTL_STAR_def, 656 FAIR_CTL_A_NEXT_def] THEN 657 PROVE_TAC[] 658 ); 659 660 661val FAIR_CTL_SEM_THM___E_EVENTUAL_ALWAYS = prove( 662 ``!M f FC s. 663 664 (FAIR_CTL_SEM M (FAIR_CTL_E_EVENTUAL FC f) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 665 (p 0 = s) /\ ?k. FAIR_CTL_SEM M f (p k))) /\ 666 (FAIR_CTL_SEM M (FAIR_CTL_E_ALWAYS FC f) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 667 (p 0 = s) /\ !k. FAIR_CTL_SEM M f (p k)))``, 668 669 SIMP_TAC std_ss [FAIR_CTL_SEM_def, FAIR_CTL_TO_CTL_STAR_def, 670 CTL_STAR_SEM_THM, FAIR_CTL_E_EVENTUAL_def, FAIR_CTL_E_ALWAYS_def, P_SEM_THM, 671 CTL_STAR_UNTIL_def] THEN 672 `!n (p:num->'b). (PATH_RESTN p n 0) = (p n)` by (EVAL_TAC THEN PROVE_TAC[]) THEN 673 METIS_TAC[IS_CTL_STAR_STATE_FORMULA___SEM, FAIR_CTL_FORMULAS_ARE_STATE_FORMULAS] 674 ); 675 676 677 678val FAIR_CTL_SEM_THM___A_EVENTUAL_ALWAYS = prove( 679 ``!M f FC s. 680 681 (FAIR_CTL_SEM M (FAIR_CTL_A_EVENTUAL FC f) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 682 (p 0 = s)) ==> ?k. FAIR_CTL_SEM M f (p k))) /\ 683 (FAIR_CTL_SEM M (FAIR_CTL_A_ALWAYS FC f) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 684 (p 0 = s)) ==> (!k. FAIR_CTL_SEM M f (p k))))``, 685 686 SIMP_TAC std_ss [FAIR_CTL_SEM_THM___BASIC_CASES, FAIR_CTL_A_EVENTUAL_def, FAIR_CTL_A_ALWAYS_def, 687 FAIR_CTL_TO_CTL_STAR_def, FAIR_CTL_SEM_THM___E_EVENTUAL_ALWAYS] THEN 688 PROVE_TAC[]); 689 690 691val FAIR_CTL_SEM_THM___A_SUNTIL = prove( 692 ``!M f1 f2 FC s. 693 (FAIR_CTL_SEM M (FAIR_CTL_A_SUNTIL FC (f1, f2)) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 694 (p 0 = s)) ==> (?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j)))))``, 695 696 697 SIMP_TAC std_ss [FAIR_CTL_SEM_THM___BASIC_CASES, FAIR_CTL_TO_CTL_STAR_def, 698 FAIR_CTL_A_SUNTIL_def] THEN 699 REPEAT STRIP_TAC THEN 700 FORALL_EQ_STRIP_TAC THEN 701 SIMP_TAC std_ss [IMP_DISJ_THM] THEN 702 REPEAT BOOL_EQ_STRIP_TAC THEN 703 Cases_on `?k. FAIR_CTL_SEM M f2 (p k)` THENL [ 704 POP_NO_ASSUM 0 (fn x=> (ASSUME_TAC (CONV_RULE EXISTS_LEAST_CONV x))), 705 METIS_TAC[] 706 ] THEN 707 CLEAN_ASSUMPTIONS_TAC THEN 708 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 709 EXISTS_TAC ``k:num`` THEN 710 ASM_REWRITE_TAC[] THEN 711 REPEAT STRIP_TAC THEN 712 rename1 `k' < k` THEN 713 RIGHT_DISJ_TAC THEN 714 SPECL_NO_ASSUM 2 [``k':num``] THEN 715 FULL_SIMP_TAC std_ss [] THENL [ 716 METIS_TAC[], 717 rename1 `j' < k'` THEN 718 `j' < k` by DECIDE_TAC THEN PROVE_TAC[] 719 ], 720 721 722 rename1 `FAIR_CTL_SEM M f1 (p j)` THEN 723 Cases_on `j < k'` THENL [ 724 PROVE_TAC[], 725 726 Cases_on `k' = j` THENL [ 727 FULL_SIMP_TAC std_ss [], 728 729 `k' < j` by DECIDE_TAC THEN 730 PROVE_TAC[] 731 ] 732 ], 733 734 PROVE_TAC[] 735 ]); 736 737 738val FAIR_CTL_SEM_THM___A_UNTIL = prove( 739 ``!M f1 f2 FC s. 740 (FAIR_CTL_SEM M (FAIR_CTL_A_UNTIL FC (f1, f2)) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\ 741 (p 0 = s)) ==> ((?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j))) \/ 742 (!j. FAIR_CTL_SEM M f1 (p j)))))``, 743 744 745 SIMP_TAC std_ss [FAIR_CTL_SEM_THM___BASIC_CASES, FAIR_CTL_TO_CTL_STAR_def, 746 FAIR_CTL_A_UNTIL_def] THEN 747 REPEAT STRIP_TAC THEN 748 FORALL_EQ_STRIP_TAC THEN 749 SIMP_TAC std_ss [IMP_DISJ_THM] THEN 750 REPEAT BOOL_EQ_STRIP_TAC THEN 751 Cases_on `?j. ~FAIR_CTL_SEM M f1 (p j)` THENL [ 752 POP_NO_ASSUM 0 (fn x=> (ASSUME_TAC (CONV_RULE EXISTS_LEAST_CONV x))), 753 PROVE_TAC[] 754 ] THEN 755 CLEAN_ASSUMPTIONS_TAC THEN 756 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 757 DISJ1_TAC THEN 758 SPECL_NO_ASSUM 0 [``j:num``] THEN 759 FULL_SIMP_TAC std_ss [] THENL [ 760 PROVE_TAC[], 761 762 EXISTS_TAC ``j:num`` THEN 763 ASM_REWRITE_TAC[] THEN 764 REPEAT STRIP_TAC THEN 765 RIGHT_DISJ_TAC THEN 766 FULL_SIMP_TAC std_ss [], 767 768 EXISTS_TAC ``j':num`` THEN 769 ASM_REWRITE_TAC[] THEN 770 REPEAT STRIP_TAC THEN 771 RIGHT_DISJ_TAC THEN 772 `j'' < j` by DECIDE_TAC THEN 773 FULL_SIMP_TAC std_ss [] 774 ], 775 776 777 Cases_on `k < k'` THENL [ 778 PROVE_TAC[], 779 780 Cases_on `k' = k` THENL [ 781 PROVE_TAC[], 782 783 `k' < k` by DECIDE_TAC THEN 784 PROVE_TAC[] 785 ] 786 ], 787 788 PROVE_TAC[] 789 ]); 790 791 792 793 794val FAIR_CTL_SEM_THM = 795 save_thm 796 ("FAIR_CTL_SEM_THM", 797 SIMP_RULE std_ss [FORALL_AND_THM] 798 (LIST_CONJ [FAIR_CTL_SEM_THM___BASIC_CASES, 799 FAIR_CTL_SEM_THM___A_NEXT, 800 FAIR_CTL_SEM_THM___E_EVENTUAL_ALWAYS, 801 FAIR_CTL_SEM_THM___A_EVENTUAL_ALWAYS, 802 FAIR_CTL_SEM_THM___A_SUNTIL, 803 FAIR_CTL_SEM_THM___A_UNTIL])); 804 805 806 807(****************************************************************************** 808 * CTL 809 ******************************************************************************) 810 811val ctl_def = 812 Hol_datatype 813 `ctl = CTL_PROP of 'a prop_logic (* boolean expression *) 814 | CTL_NOT of ctl (* \neg f *) 815 | CTL_AND of ctl # ctl (* f1 \wedge f2 *) 816 | CTL_E_NEXT of ctl (* X f *) 817 | CTL_E_SUNTIL of ctl # ctl (* strong_until *) 818 | CTL_E_UNTIL of ctl # ctl`; (* weak until *) 819 820 821val ctl_induct = 822 save_thm 823 ("ctl_induct", 824 Q.GEN 825 `P` 826 (MATCH_MP 827 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 828 (SIMP_RULE 829 std_ss 830 [pairTheory.FORALL_PROD, 831 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 832 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 833 (Q.SPECL 834 [`P`,`\(f1,f2). P f1 /\ P f2`] 835 (TypeBase.induction_of ``:'a ctl``))))); 836 837 838(*Since CTL is a subset of CTL_STAR we can easily translate it to CTL_STAR*) 839val CTL_TO_FAIR_CTL_def = 840 Define 841 `(CTL_TO_FAIR_CTL fc (CTL_PROP b) = (FAIR_CTL_PROP b)) /\ 842 (CTL_TO_FAIR_CTL fc (CTL_NOT f) = (FAIR_CTL_NOT (CTL_TO_FAIR_CTL fc f))) /\ 843 (CTL_TO_FAIR_CTL fc (CTL_AND (f1, f2)) = (FAIR_CTL_AND (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 844 (CTL_TO_FAIR_CTL fc (CTL_E_NEXT f) = (FAIR_CTL_E_NEXT fc (CTL_TO_FAIR_CTL fc f))) /\ 845 (CTL_TO_FAIR_CTL fc (CTL_E_SUNTIL (f1, f2)) = (FAIR_CTL_E_SUNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 846 (CTL_TO_FAIR_CTL fc (CTL_E_UNTIL (f1, f2)) = (FAIR_CTL_E_UNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2)))`; 847 848 849val CTL_SEM_def = 850 Define ` 851 CTL_SEM M f s = FAIR_CTL_SEM M (CTL_TO_FAIR_CTL [] f) s`; 852 853 854val CTL_FAIR_SEM_def = 855 Define ` 856 CTL_FAIR_SEM M f fc s = FAIR_CTL_SEM M (CTL_TO_FAIR_CTL fc f) s`; 857 858val CTL_KS_SEM_def = 859 Define 860 `CTL_KS_SEM M f = (!s. P_SEM s M.S0 ==> CTL_SEM M f s)`; 861 862val CTL_KS_FAIR_SEM_def = 863 Define 864 `CTL_KS_FAIR_SEM M f fc = (!s. P_SEM s M.S0 ==> CTL_FAIR_SEM M f fc s)`; 865 866 867val CTL_KS_SEM___TO___FAIR_CTL_KS_SEM = 868 store_thm ("CTL_KS_SEM___TO___FAIR_CTL_KS_SEM", 869 ``!M f. CTL_KS_SEM M f = FAIR_CTL_KS_SEM M (CTL_TO_FAIR_CTL [] f)``, 870 871 SIMP_TAC std_ss [CTL_KS_SEM_def, FAIR_CTL_KS_SEM_def, 872 CTL_SEM_def]); 873 874 875val CTL_KS_FAIR_SEM___TO___FAIR_CTL_KS_SEM = 876 store_thm ("CTL_KS_FAIR_SEM___TO___FAIR_CTL_KS_SEM", 877 ``!M f fc. CTL_KS_FAIR_SEM M f fc = FAIR_CTL_KS_SEM M (CTL_TO_FAIR_CTL fc f)``, 878 879 SIMP_TAC std_ss [CTL_KS_FAIR_SEM_def, FAIR_CTL_KS_SEM_def, 880 CTL_FAIR_SEM_def]); 881 882 883val CTL_USED_VARS_def = 884 Define ` 885 (CTL_USED_VARS f = FAIR_CTL_USED_VARS (CTL_TO_FAIR_CTL [] f))`; 886 887 888 889(*translation of the important FAIR_CTL definitions and lemmata*) 890val CTL_FALSE_def = Define `CTL_FALSE = CTL_PROP P_FALSE`; 891val CTL_TRUE_def = Define `CTL_TRUE = CTL_PROP P_TRUE`; 892val CTL_OR_def = Define `CTL_OR(f1,f2) = CTL_NOT (CTL_AND((CTL_NOT f1),(CTL_NOT f2)))`; 893val CTL_IMPL_def = Define `CTL_IMPL(f1, f2) = CTL_OR(CTL_NOT f1, f2)`; 894val CTL_COND_def = Define `CTL_COND(c, f1, f2) = CTL_AND(CTL_IMPL(c, f1), CTL_IMPL(CTL_NOT c, f2))`; 895val CTL_EQUIV_def = Define `CTL_EQUIV(b1, b2) = CTL_AND(CTL_IMPL(b1, b2),CTL_IMPL(b2, b1))`; 896val CTL_A_NEXT_def = Define `CTL_A_NEXT f = CTL_NOT(CTL_E_NEXT (CTL_NOT f))`; 897val CTL_E_EVENTUAL_def = Define `CTL_E_EVENTUAL f = CTL_E_SUNTIL (CTL_PROP(P_TRUE),f)`; 898val CTL_E_ALWAYS_def = Define `CTL_E_ALWAYS f = CTL_E_UNTIL (f, CTL_PROP(P_FALSE))`; 899val CTL_A_EVENTUAL_def = Define `CTL_A_EVENTUAL f = CTL_NOT (CTL_E_ALWAYS (CTL_NOT f))`; 900val CTL_A_ALWAYS_def = Define `CTL_A_ALWAYS f = CTL_NOT (CTL_E_EVENTUAL (CTL_NOT f))`; 901val CTL_A_UNTIL_def = Define `CTL_A_UNTIL(f1,f2) = CTL_NOT(CTL_E_SUNTIL(CTL_NOT f2, (CTL_AND(CTL_NOT f1, CTL_NOT f2))))`; 902val CTL_A_SUNTIL_def = Define `CTL_A_SUNTIL(f1,f2) = CTL_NOT(CTL_E_UNTIL(CTL_NOT f2, (CTL_AND(CTL_NOT f1, CTL_NOT f2))))`; 903val CTL_E_BEFORE_def = Define `CTL_E_BEFORE(f1,f2) = CTL_E_UNTIL(CTL_NOT f2, CTL_AND(f1, CTL_NOT f2))`; 904val CTL_E_SBEFORE_def = Define `CTL_E_SBEFORE(f1,f2) = CTL_E_SUNTIL(CTL_NOT f2, CTL_AND(f1, CTL_NOT f2))`; 905val CTL_A_BEFORE_def = Define `CTL_A_BEFORE(f1,f2) = CTL_NOT(CTL_E_SUNTIL(CTL_NOT f1, f2))`; 906val CTL_A_SBEFORE_def = Define `CTL_A_SBEFORE(f1,f2) = CTL_NOT(CTL_E_UNTIL(CTL_NOT f1, f2))`; 907val CTL_E_WHILE_def = Define `CTL_E_WHILE(f1,f2) = CTL_E_UNTIL(CTL_NOT f2, CTL_AND(f1, f2))`; 908val CTL_E_SWHILE_def = Define `CTL_E_SWHILE(f1,f2) = CTL_E_SUNTIL(CTL_NOT f2, CTL_AND(f1, f2))`; 909val CTL_A_WHILE_def = Define `CTL_A_WHILE(f1,f2) = CTL_NOT(CTL_E_SUNTIL(CTL_NOT f2, CTL_AND(CTL_NOT f1, f2)))`; 910val CTL_A_SWHILE_def = Define `CTL_A_SWHILE(f1,f2) = CTL_NOT(CTL_E_UNTIL(CTL_NOT f2, CTL_AND(CTL_NOT f1, f2)))`; 911 912 913 914val CTL_TO_FAIR_CTL_THM = 915 store_thm ("CTL_TO_FAIR_CTL_THM", 916 ``!b f f1 f2 c fc. 917 (CTL_TO_FAIR_CTL fc (CTL_PROP b) = (FAIR_CTL_PROP b)) /\ 918 (CTL_TO_FAIR_CTL fc (CTL_NOT f) = (FAIR_CTL_NOT (CTL_TO_FAIR_CTL fc f))) /\ 919 (CTL_TO_FAIR_CTL fc (CTL_AND (f1, f2)) = (FAIR_CTL_AND (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 920 (CTL_TO_FAIR_CTL fc (CTL_OR (f1, f2)) = (FAIR_CTL_OR (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 921 (CTL_TO_FAIR_CTL fc (CTL_IMPL (f1, f2)) = (FAIR_CTL_IMPL (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 922 (CTL_TO_FAIR_CTL fc (CTL_COND (c, f1, f2)) = (FAIR_CTL_COND (CTL_TO_FAIR_CTL fc c, CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 923 (CTL_TO_FAIR_CTL fc (CTL_EQUIV (f1, f2)) = (FAIR_CTL_EQUIV (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 924 (CTL_TO_FAIR_CTL fc (CTL_E_NEXT f) = (FAIR_CTL_E_NEXT fc (CTL_TO_FAIR_CTL fc f))) /\ 925 (CTL_TO_FAIR_CTL fc (CTL_A_NEXT f) = (FAIR_CTL_A_NEXT fc (CTL_TO_FAIR_CTL fc f))) /\ 926 (CTL_TO_FAIR_CTL fc (CTL_E_ALWAYS f) = (FAIR_CTL_E_ALWAYS fc (CTL_TO_FAIR_CTL fc f))) /\ 927 (CTL_TO_FAIR_CTL fc (CTL_A_ALWAYS f) = (FAIR_CTL_A_ALWAYS fc (CTL_TO_FAIR_CTL fc f))) /\ 928 (CTL_TO_FAIR_CTL fc (CTL_E_EVENTUAL f) = (FAIR_CTL_E_EVENTUAL fc (CTL_TO_FAIR_CTL fc f))) /\ 929 (CTL_TO_FAIR_CTL fc (CTL_A_EVENTUAL f) = (FAIR_CTL_A_EVENTUAL fc (CTL_TO_FAIR_CTL fc f))) /\ 930 (CTL_TO_FAIR_CTL fc (CTL_E_SUNTIL (f1, f2)) = (FAIR_CTL_E_SUNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 931 (CTL_TO_FAIR_CTL fc (CTL_A_SUNTIL (f1, f2)) = (FAIR_CTL_A_SUNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 932 (CTL_TO_FAIR_CTL fc (CTL_E_UNTIL (f1, f2)) = (FAIR_CTL_E_UNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 933 (CTL_TO_FAIR_CTL fc (CTL_A_UNTIL (f1, f2)) = (FAIR_CTL_A_UNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 934 (CTL_TO_FAIR_CTL fc (CTL_E_BEFORE (f1, f2)) = (FAIR_CTL_E_BEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 935 (CTL_TO_FAIR_CTL fc (CTL_A_BEFORE (f1, f2)) = (FAIR_CTL_A_BEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 936 (CTL_TO_FAIR_CTL fc (CTL_E_SBEFORE (f1, f2)) = (FAIR_CTL_E_SBEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 937 (CTL_TO_FAIR_CTL fc (CTL_A_SBEFORE (f1, f2)) = (FAIR_CTL_A_SBEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 938 (CTL_TO_FAIR_CTL fc (CTL_E_WHILE (f1, f2)) = (FAIR_CTL_E_WHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 939 (CTL_TO_FAIR_CTL fc (CTL_A_WHILE (f1, f2)) = (FAIR_CTL_A_WHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 940 (CTL_TO_FAIR_CTL fc (CTL_E_SWHILE (f1, f2)) = (FAIR_CTL_E_SWHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\ 941 (CTL_TO_FAIR_CTL fc (CTL_A_SWHILE (f1, f2)) = (FAIR_CTL_A_SWHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2)))``, 942 943 EVAL_TAC THEN PROVE_TAC[]); 944 945 946 947val CTL_SEM_THM = store_thm ("CTL_SEM_THM", 948 ``!M b f f1 f2 s. 949 950 (CTL_SEM M CTL_TRUE s) /\ ~(CTL_SEM M CTL_FALSE s) /\ 951 952 (CTL_SEM M (CTL_PROP b) s = (P_SEM s b)) /\ 953 954 (CTL_SEM M (CTL_NOT f) s = ~(CTL_SEM M f s)) /\ 955 956 (CTL_SEM M (CTL_AND(f1,f2)) s = CTL_SEM M f1 s /\ CTL_SEM M f2 s) /\ 957 958 (CTL_SEM M (CTL_E_NEXT f) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 959 (p 0 = s) /\ CTL_SEM M f (p 1))) /\ 960 961 (CTL_SEM M (CTL_E_SUNTIL(f1, f2)) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 962 (p 0 = s) /\ (?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))))) /\ 963 964 (CTL_SEM M (CTL_E_UNTIL(f1, f2)) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 965 (p 0 = s) /\ 966 ((?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))) \/ 967 (!j. CTL_SEM M f1 (p j))))) /\ 968 969 (CTL_SEM M (CTL_A_NEXT f) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 970 (p 0 = s)) ==> CTL_SEM M f (p 1))) /\ 971 972 (CTL_SEM M (CTL_E_EVENTUAL f) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 973 (p 0 = s) /\ ?k. CTL_SEM M f (p k))) /\ 974 (CTL_SEM M (CTL_E_ALWAYS f) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 975 (p 0 = s) /\ !k. CTL_SEM M f (p k))) /\ 976 977 (CTL_SEM M (CTL_A_EVENTUAL f) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 978 (p 0 = s)) ==> ?k. CTL_SEM M f (p k))) /\ 979 (CTL_SEM M (CTL_A_ALWAYS f) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 980 (p 0 = s)) ==> (!k. CTL_SEM M f (p k)))) /\ 981 982 (CTL_SEM M (CTL_A_SUNTIL(f1, f2)) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 983 (p 0 = s)) ==> (?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))))) /\ 984 985 (CTL_SEM M (CTL_A_UNTIL(f1, f2)) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\ 986 (p 0 = s)) ==> ((?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))) \/ 987 (!j. CTL_SEM M f1 (p j)))))``, 988 989 990 SIMP_TAC std_ss [CTL_SEM_def, CTL_TO_FAIR_CTL_THM, FAIR_CTL_SEM_THM, 991 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___EMPTY_FAIRNESS, 992 CTL_TRUE_def, CTL_FALSE_def, P_SEM_THM]); 993 994 995val IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___TO___CTL_KS_FAIR_SEM = 996 store_thm ("IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___TO___CTL_KS_FAIR_SEM", 997 ``!M fc. IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE M fc = 998 CTL_KS_FAIR_SEM M (CTL_A_EVENTUAL CTL_FALSE) fc``, 999 1000 SIMP_TAC std_ss [CTL_KS_FAIR_SEM_def, CTL_FAIR_SEM_def, 1001 CTL_TO_FAIR_CTL_THM, CTL_FALSE_def, FAIR_CTL_SEM_THM, P_SEM_THM, 1002 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 1003 IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def] THEN 1004 METIS_TAC[]); 1005 1006 1007 1008val _ = export_theory(); 1009