1open HolKernel Parse boolLib bossLib pred_setTheory relationTheory set_relationTheory prim_recTheory 2 3open generalHelpersTheory wordTheory 4 5val _ = new_theory "ltl" 6 7val _ = Datatype` 8 ltl_frml 9 = VAR 'a 10 | N_VAR 'a 11 | DISJ ltl_frml ltl_frml 12 | CONJ ltl_frml ltl_frml 13 | X ltl_frml 14 | U ltl_frml ltl_frml 15 | R ltl_frml ltl_frml`; 16 17val MODELS_def = 18 Define 19 `(MODELS w (VAR a) = (a IN (at w 0))) 20 /\ (MODELS w (N_VAR a) = ~(a IN (at w 0))) 21 /\ (MODELS w (DISJ f1 f2) = (MODELS w f1) \/ (MODELS w f2)) 22 /\ (MODELS w (CONJ f1 f2) = (MODELS w f1) /\ (MODELS w f2)) 23 /\ (MODELS w (X f) = (MODELS (suff w 1) f)) 24 /\ (MODELS w (U f1 f2) = 25 ?n. (MODELS (suff w n) f2) /\ !i. (i < n) ==> (MODELS (suff w i) f1)) 26 /\ (MODELS w (R f1 f2) = 27 !n. (MODELS (suff w n) f2) \/ ?i. (i < n) /\ (MODELS (suff w i) f1))`; 28 29val R_COND_LEMM = store_thm 30 ("R_COND_LEMM", 31 ``!w f1 f2. (!n. (MODELS (suff w n) f2) \/ ?i. (i < n) /\ (MODELS (suff w i) f1)) 32 = ((!n. MODELS (suff w n) f2) \/ 33 ?n. MODELS (suff w n) f1 /\ !i. i <= n ==> MODELS (suff w i) f2)``, 34 rpt strip_tac >> rw[EQ_IMP_THM] 35 >- (Cases_on `!n. MODELS (suff w n) f2` >> fs[] 36 >> qabbrev_tac `N = LEAST n. ~MODELS (suff w n) f2` 37 >> `(!i. i < N ==> MODELS (suff w i) f2) ��� ~MODELS (suff w N) f2` by ( 38 simp[Abbr `N`] >> numLib.LEAST_ELIM_TAC 39 >> simp[] >> metis_tac[] 40 ) 41 >> disj2_tac 42 >> `MODELS (suff w N) f2 ��� ���i. i < N ��� MODELS (suff w i) f1` by metis_tac[] 43 >> qexists_tac `i` >> fs[] 44 ) 45 >- metis_tac[] 46 >- (Cases_on `n' <= n` 47 >- metis_tac[] 48 >- (`n < n'` by simp[] >> metis_tac[]) 49 ) 50 ); 51 52val TRUE_def = Define `TRUE = DISJ (VAR ARB) (N_VAR ARB)`; 53val FALSE_def = Define `FALSE = CONJ (VAR ARB) (N_VAR ARB)`; 54 55(* 56 57 Subformulae 58 59*) 60 61val subForms_def = Define 62 ` (subForms (VAR a) = {VAR a}) 63 /\ (subForms (N_VAR a) = {N_VAR a}) 64 /\ (subForms (DISJ f1 f2) = {DISJ f1 f2} ��� (subForms f1) ��� (subForms f2)) 65 /\ (subForms (CONJ f1 f2) = {CONJ f1 f2} ��� (subForms f1) ��� (subForms f2)) 66 /\ (subForms (X f) = {X f} ��� (subForms f)) 67 /\ (subForms (U f1 f2) = {U f1 f2} ��� (subForms f1) ��� (subForms f2)) 68 /\ (subForms (R f1 f2) = {R f1 f2} ��� (subForms f1) ��� (subForms f2))`; 69 70val SUBFORMS_REFL = store_thm 71 ("SUBFORMS_REFL", 72 ``!f. f ��� subForms f``, 73 Induct_on `f` >> simp[subForms_def]); 74 75val SUBFORMS_TRANS = store_thm 76 ("SUBFORMS_TRANS", 77 ``!f1 f2 f3. f1 ��� subForms f2 /\ f2 ��� subForms f3 ==> f1 ��� subForms f3``, 78 Induct_on `f3` >> rpt strip_tac >> dsimp[] >> fs[subForms_def, UNION_DEF] 79 >> fs[subForms_def, UNION_DEF] 80 >> metis_tac[] 81 ); 82 83val no_tmp_op_def = Define 84`(no_tmp_op (VAR a) = 1) 85 /\ (no_tmp_op (N_VAR a) = 1) 86 /\ (no_tmp_op (DISJ f1 f2) = (no_tmp_op f1) + (no_tmp_op f2)) 87 /\ (no_tmp_op (CONJ f1 f2) = (no_tmp_op f1) + (no_tmp_op f2)) 88 /\ (no_tmp_op (X f) = (no_tmp_op f) + 1) 89 /\ (no_tmp_op (U f1 f2) =(no_tmp_op f1) + (no_tmp_op f2) +1) 90 /\ (no_tmp_op (R f1 f2) =(no_tmp_op f1) + (no_tmp_op f2) +1)`; 91 92val NO_TMP_LEMM = store_thm 93 ("NO_TMP_LEMM", ``!f. no_tmp_op f >= 1``, 94 Induct_on `f` >> simp[no_tmp_op_def]); 95 96val TMP_OP_DECR_WITH_SF = store_thm 97 ("TMP_OP_DECR_WITH_SF", 98 ``!f f'. (f' ��� subForms f ==> (no_tmp_op f' <= no_tmp_op f))``, 99 Induct_on `f` >> fs[subForms_def, no_tmp_op_def] >> rpt strip_tac 100 >> simp[no_tmp_op_def] 101 >- (`no_tmp_op f'' <= no_tmp_op f` by metis_tac[] >> simp[]) 102 >- (`no_tmp_op f'' <= no_tmp_op f'` by metis_tac[] >> simp[]) 103 >- (`no_tmp_op f'' <= no_tmp_op f` by metis_tac[] >> simp[]) 104 >- (`no_tmp_op f'' <= no_tmp_op f'` by metis_tac[] >> simp[]) 105 >- (`no_tmp_op f' <= no_tmp_op f` by metis_tac[] >> simp[]) 106 >- (`no_tmp_op f'' <= no_tmp_op f` by metis_tac[] >> simp[]) 107 >- (`no_tmp_op f'' <= no_tmp_op f'` by metis_tac[] >> simp[]) 108 >- (`no_tmp_op f'' <= no_tmp_op f` by metis_tac[] >> simp[]) 109 >- (`no_tmp_op f'' <= no_tmp_op f'` by metis_tac[] >> simp[]) 110 ); 111 112val TMP_OP_EQ_LEMM = store_thm 113 ("TMP_OP_EQ_LEMM", 114 ``!f g. f ��� subForms g ��� (no_tmp_op f = no_tmp_op g) ==> (f = g)``, 115 Induct_on `g` >> fs[] >> rpt strip_tac 116 >> fs[subForms_def, no_tmp_op_def] 117 >- (`no_tmp_op f <= no_tmp_op g` by metis_tac[TMP_OP_DECR_WITH_SF] 118 >> `~(no_tmp_op g' >= 1)` by fs[] >> metis_tac[NO_TMP_LEMM]) 119 >- (`no_tmp_op f <= no_tmp_op g'` by metis_tac[TMP_OP_DECR_WITH_SF] 120 >> `~(no_tmp_op g >= 1)` by fs[] >> metis_tac[NO_TMP_LEMM]) 121 >- (`no_tmp_op f <= no_tmp_op g` by metis_tac[TMP_OP_DECR_WITH_SF] 122 >> `~(no_tmp_op g' >= 1)` by fs[] >> metis_tac[NO_TMP_LEMM]) 123 >- (`no_tmp_op f <= no_tmp_op g'` by metis_tac[TMP_OP_DECR_WITH_SF] 124 >> `~(no_tmp_op g >= 1)` by fs[] >> metis_tac[NO_TMP_LEMM]) 125 >- (`no_tmp_op f <= no_tmp_op g` by metis_tac[TMP_OP_DECR_WITH_SF] >> fs[]) 126 >- (`no_tmp_op f <= no_tmp_op g` by metis_tac[TMP_OP_DECR_WITH_SF] 127 >> fs[]) 128 >- (`no_tmp_op f <= no_tmp_op g'` by metis_tac[TMP_OP_DECR_WITH_SF] 129 >> fs[]) 130 >- (`no_tmp_op f <= no_tmp_op g` by metis_tac[TMP_OP_DECR_WITH_SF] 131 >> fs[]) 132 >- (`no_tmp_op f <= no_tmp_op g'` by metis_tac[TMP_OP_DECR_WITH_SF] 133 >> fs[]) 134 ); 135 136val SF_ANTISYM_LEMM = store_thm 137 ("SF_ANTISYM_LEMM", 138 ``!f1 f2. (f1 ��� subForms f2) /\ (f2 ��� subForms f1) ==> (f1 = f2)``, 139 Induct_on `f1` >> simp[subForms_def] >> rpt strip_tac >> simp[] 140 >> `!f1 f2. (f1 ��� subForms f2) ==> (no_tmp_op f1 <= no_tmp_op f2)` 141 by metis_tac[TMP_OP_DECR_WITH_SF] 142 >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF] 143 >> `no_tmp_op (DISJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 144 >> fs[no_tmp_op_def] >> `no_tmp_op f1' = 0` by simp[] 145 >> `no_tmp_op f1' >= 1` by metis_tac[NO_TMP_LEMM] >> fs[] 146 ) 147 >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF] 148 >> `no_tmp_op (DISJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 149 >> fs[no_tmp_op_def] >> `no_tmp_op f1 = 0` by simp[] 150 >> `no_tmp_op f1 >= 1` by metis_tac[NO_TMP_LEMM] >> fs[] 151 ) 152 >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF] 153 >> `no_tmp_op (CONJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 154 >> fs[no_tmp_op_def] >> `no_tmp_op f1' = 0` by simp[] 155 >> `no_tmp_op f1' >= 1` by metis_tac[NO_TMP_LEMM] >> fs[] 156 ) 157 >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF] 158 >> `no_tmp_op (CONJ f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 159 >> fs[no_tmp_op_def] >> `no_tmp_op f1 = 0` by simp[] 160 >> `no_tmp_op f1 >= 1` by metis_tac[NO_TMP_LEMM] >> fs[] 161 ) 162 >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF] 163 >> `no_tmp_op (X f1) <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 164 >> fs[no_tmp_op_def] >> `1 = 0` by simp[] >> fs[] 165 ) 166 >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF] 167 >> `no_tmp_op (U f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 168 >> fs[no_tmp_op_def] 169 ) 170 >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF] 171 >> `no_tmp_op (U f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 172 >> fs[no_tmp_op_def] 173 ) 174 >- (`no_tmp_op f2 <= no_tmp_op f1` by metis_tac[TMP_OP_DECR_WITH_SF] 175 >> `no_tmp_op (R f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 176 >> fs[no_tmp_op_def] 177 ) 178 >- (`no_tmp_op f2 <= no_tmp_op f1'` by metis_tac[TMP_OP_DECR_WITH_SF] 179 >> `no_tmp_op (R f1 f1') <= no_tmp_op f2` by metis_tac[TMP_OP_DECR_WITH_SF] 180 >> fs[no_tmp_op_def] 181 ) 182 ); 183 184val is_until_def = Define` 185 (is_until (U f1 f2) = T) 186 ��� (is_until _ = F)`; 187 188(* 189 190 Temporal subformulae 191 192*) 193 194 195val tempSubForms_def = Define 196 `(tempSubForms (VAR a) = {VAR a}) 197 /\ (tempSubForms (N_VAR a) = {N_VAR a}) 198 /\ (tempSubForms (DISJ f1 f2) = (tempSubForms f1) ��� (tempSubForms f2)) 199 /\ (tempSubForms (CONJ f1 f2) = (tempSubForms f1) ��� (tempSubForms f2)) 200 /\ (tempSubForms (X f) = {X f} ��� (tempSubForms f)) 201 /\ (tempSubForms (U f1 f2) = {U f1 f2} ��� (tempSubForms f1) ��� (tempSubForms f2)) 202 /\ (tempSubForms (R f1 f2) = {R f1 f2} ��� (tempSubForms f1) ��� (tempSubForms f2))`; 203 204val TSF_def = Define ` 205 TSF (x,y) = x ��� tempSubForms y`; 206 207val TSF_REFL = store_thm 208 ("TSF_REFL", 209 ``!f. reflexive (rrestrict TSF (tempSubForms f)) (tempSubForms f)``, 210 fs[reflexive_def, rrestrict_def, TSF_def] 211 >> Induct_on `f` >> fs[IN_DEF, TSF_def, tempSubForms_def] >> rpt strip_tac >> fs[] 212 >- (`x ��� tempSubForms x` suffices_by metis_tac[tempSubForms_def,IN_DEF] 213 >> simp[tempSubForms_def] >> metis_tac[]) 214 >- (`!f1 f2. (U f1 f2) ��� tempSubForms (U f1 f2)` by rw[tempSubForms_def] 215 >> metis_tac[IN_DEF]) 216 >- (`!f1 f2. (R f1 f2) ��� tempSubForms (R f1 f2)` by rw[tempSubForms_def] 217 >> metis_tac[IN_DEF]) 218); 219 220val TSF_SF_TRANS_LEMM = store_thm 221 ("TSF_SF_TRANS_LEMM", 222 ``!f1 f2 f3. f1 ��� tempSubForms f2 /\ f2 ��� subForms f3 ==> f1 ��� tempSubForms f3``, 223 Induct_on `f3` >> rpt strip_tac >> fs[tempSubForms_def, subForms_def] 224 >> fs[tempSubForms_def] >> metis_tac[] 225 ); 226 227val TSF_IMPL_SF = store_thm 228 ("TSF_IMPL_SF", 229 ``!f g. f ��� tempSubForms g ==> f ��� subForms g``, 230 Induct_on `g` >> rpt strip_tac >> fs[tempSubForms_def, subForms_def] 231 ); 232 233val TSF_TRANS_LEMM = store_thm 234 ("TSF_TRANS_LEMM", 235 ``transitive TSF``, 236 simp[transitive_def,IN_DEF,TSF_def,tempSubForms_def] 237 >> `!x y. tempSubForms x y = (y ��� tempSubForms x)` by metis_tac[IN_DEF] 238 >> Induct_on `z` >> dsimp[tempSubForms_def] >> metis_tac[] 239 ); 240 241(* val TSF_TRANS_LEMM2 = store_thm *) 242(* ("TSF_TRANS_LEMM2", *) 243(* ``!x y z. (x,y) ��� TSF ��� (y,z) ��� TSF ==> (x,z) ��� TSF``, *) 244 245(* ) *) 246 247 248val TSF_TRANS = store_thm 249 ("TSF_TRANS", 250 ``!f. transitive (rrestrict TSF (tempSubForms f))``, 251 metis_tac[RRESTRICT_TRANS, TSF_TRANS_LEMM] 252 ); 253 254val TSF_FINITE = store_thm 255 ("TSF_FINITE", 256 ``!f. FINITE (tempSubForms f)``, 257 Induct_on `f` >> fs[tempSubForms_def] >> strip_tac 258 ); 259 260val TSF_ANTISYM_LEMM = store_thm 261 ("TSF_ANTISYM_LEMM", 262 ``!f1 f2. (f1 ��� tempSubForms f2) /\ (f2 ��� tempSubForms f1) ==> (f1 = f2)``, 263 rpt strip_tac >> metis_tac[TSF_IMPL_SF, SF_ANTISYM_LEMM] 264 ); 265 266val TSF_ANTISYM = store_thm 267 ("TSF_ANTISYM", 268 ``!f. antisym (rrestrict TSF (tempSubForms f))``, 269 `antisym TSF` suffices_by metis_tac[RRESTRICT_ANTISYM] 270 >> fs[TSF_def, antisym_def,IN_DEF] >> metis_tac[TSF_ANTISYM_LEMM,IN_DEF] 271 ); 272 273val TSF_PO = store_thm 274 ("TSF_PO", 275 ``!f. partial_order (rrestrict TSF (tempSubForms f)) (tempSubForms f)``, 276 fs[partial_order_def] 277 >> rpt strip_tac 278 >- (fs[domain_def, SUBSET_DEF, rrestrict_def] >> rpt strip_tac) 279 >- (fs[range_def, SUBSET_DEF, rrestrict_def] >> rpt strip_tac) 280 >- metis_tac[TSF_TRANS] 281 >- metis_tac[TSF_REFL] 282 >- metis_tac[TSF_ANTISYM] 283 ); 284 285val STRICT_TSF_WF = store_thm 286 ("STRICT_TSF_WF", 287 ``WF (��f1 f2. f1 ��� tempSubForms f2 ��� ~(f1 = f2))``, 288 rw[WF_IFF_WELLFOUNDED] >> simp[wellfounded_def] >> rpt strip_tac 289 >> CCONTR_TAC >> fs[] 290 >> `!n. no_tmp_op (f (SUC n)) < no_tmp_op (f n)` by ( 291 rpt strip_tac >> first_x_assum (qspec_then `n` mp_tac) 292 >> rpt strip_tac 293 >> imp_res_tac TSF_IMPL_SF 294 >> imp_res_tac TMP_OP_DECR_WITH_SF 295 >> Cases_on `(no_tmp_op (f (SUC n)) = no_tmp_op (f n))` 296 >> fs[TMP_OP_EQ_LEMM] 297 ) 298 >> `!n. (no_tmp_op o f) (SUC n) < (no_tmp_op o f) n` by fs[] 299 >> `~wellfounded (\a b. (no_tmp_op o f) a < (no_tmp_op o f) b)` by ( 300 fs[wellfounded_def] >> metis_tac[] 301 ) 302 >> `~wellfounded (inv_image ($<) (no_tmp_op o f))` by fs[inv_image_def] 303 >> metis_tac[WF_LESS,WF_inv_image,WF_IFF_WELLFOUNDED] 304 ); 305 306val DISJ_TEMP_SUBF = store_thm 307 ("DISJ_TEMP_SUBF", 308 ``!f f1 f2. ~(DISJ f1 f2 ��� tempSubForms f)``, 309 Induct_on `f` >> simp[tempSubForms_def]); 310 311val CONJ_TEMP_SUBF = store_thm 312 ("CONJ_TEMP_SUBF", 313 ``!f f1 f2. ~(CONJ f1 f2 ��� tempSubForms f)``, 314 Induct_on `f` >> simp[tempSubForms_def]); 315 316 317(* 318 319 Temporal DNF 320 321*) 322 323val tempDNF_def = Define 324 `(tempDNF (VAR a) = {{VAR a}}) 325 /\ (tempDNF (N_VAR a) = {{N_VAR a}}) 326 /\ (tempDNF (DISJ f1 f2) = (tempDNF f1) ��� (tempDNF f2)) 327 /\ (tempDNF (CONJ f1 f2) = {f' ��� f'' | (f' ��� tempDNF f1) /\ (f'' ��� tempDNF f2)}) 328 /\ (tempDNF (X f) = {{X f}}) 329 /\ (tempDNF (U f1 f2) = {{U f1 f2}}) 330 /\ (tempDNF (R f1 f2) = {{R f1 f2}})`; 331 332val TEMPDNF_NOT_EMPTY = store_thm 333 ("TEMPDNF_NOT_EMPTY", 334 ``!f qs. qs ��� tempDNF f ==> ~(qs = {})``, 335 Induct_on `f` >> fs[tempDNF_def] 336 ); 337 338val TEMPDNF_TEMPSUBF = store_thm 339 ("TEMPDNF_TEMPSUBF", 340 ``!f s. (s ��� tempDNF f) ==> (s ��� tempSubForms f)``, 341 Induct_on `f` >> simp[tempSubForms_def, tempDNF_def] 342 >- (strip_tac >> ASM_CASES_TAC ``s ��� tempDNF f`` >> simp[] 343 >- (`tempSubForms f ��� tempSubForms f ��� tempSubForms f'` 344 by metis_tac[SUBSET_UNION] 345 >> `s ��� tempSubForms f` suffices_by metis_tac[SUBSET_TRANS] 346 >> simp[]) 347 >- (`tempSubForms f' ��� tempSubForms f ��� tempSubForms f'` 348 by metis_tac[SUBSET_UNION] 349 >> strip_tac 350 >> `s ��� tempSubForms f'` suffices_by metis_tac[SUBSET_TRANS] 351 >> simp[])) 352 >- (rpt strip_tac 353 >> `f'' ��� tempSubForms f` by metis_tac[] 354 >> `f''' ��� tempSubForms f'` by metis_tac[] 355 >> fs[SUBSET_DEF] 356 >> rpt strip_tac >> metis_tac[]) 357 ); 358 359(* 360 LTL language 361*) 362 363val props_def = Define 364`props f = {a | (VAR a) ��� (subForms f) \/ (N_VAR a) ��� (subForms f) }`; 365 366val ltl_lang_def = Define 367`ltl_lang f = {w | MODELS w f /\ word_range w ��� POW (props f)}`; 368 369(* 370 EXAMPLES 371*) 372 373val W1_def = Define `W1 = WORD (\x. {x})`; 374 375val EX_1 = store_thm 376 ("EX1", ``(MODELS W1 TRUE)``, fs[MODELS_def,TRUE_def]); 377 378val EX_2 = store_thm 379 ("EX2", ``MODELS W1 (VAR 0)``, simp[MODELS_def, at_def, W1_def]); 380 381val EX_3 = store_thm 382 ("EX3",``MODELS W1 (U TRUE (VAR 23))``, 383 simp [MODELS_def, TRUE_def, suff_def, at_def, W1_def]); 384 385val EX_4 = store_thm 386 ("EX4",``!x. ?y. MODELS (suff W1 x) (U (VAR x) (VAR y))``, 387 simp [MODELS_def, suff_def, at_def, W1_def] >> rpt strip_tac 388 >> exists_tac ``0`` >> simp[] 389 ); 390 391(* Full LTL *) 392 393val _ = Datatype` 394 full_ltl_frml 395 = F_VAR 'a 396 | F_CONJ full_ltl_frml full_ltl_frml 397 | F_NEG full_ltl_frml 398 | F_X full_ltl_frml 399 | F_U full_ltl_frml full_ltl_frml`; 400 401val FLTL_MODELS_def = 402 Define 403 `(FLTL_MODELS w (F_VAR a) = (a ��� (at w 0))) 404 /\ (FLTL_MODELS w (F_CONJ f1 f2) = (FLTL_MODELS w f1) /\ (FLTL_MODELS w f2)) 405 /\ (FLTL_MODELS w (F_NEG f) = ~(FLTL_MODELS w f)) 406 /\ (FLTL_MODELS w (F_X f) = (FLTL_MODELS (suff w 1) f)) 407 /\ (FLTL_MODELS w (F_U f1 f2) = 408 ?n. (FLTL_MODELS (suff w n) f2) /\ !i. (i < n) ==> (FLTL_MODELS (suff w i) f1))`; 409 410val NNF_def = Define` 411 (NNF (F_VAR a) = VAR a) 412 ��� (NNF (F_CONJ f1 f2) = CONJ (NNF f1) (NNF f2)) 413 ��� (NNF (F_NEG (F_VAR a)) = N_VAR a) 414 ��� (NNF (F_NEG (F_CONJ f1 f2)) = DISJ (NNF (F_NEG f1)) (NNF (F_NEG f2))) 415 ��� (NNF (F_NEG (F_NEG f)) = NNF f) 416 ��� (NNF (F_NEG (F_X f)) = X (NNF (F_NEG f))) 417 ��� (NNF (F_NEG (F_U f1 f2)) = R (NNF (F_NEG f1)) (NNF (F_NEG f2))) 418 ��� (NNF (F_X f) = X (NNF f)) 419 ��� (NNF (F_U f1 f2) = U (NNF f1) (NNF f2))`; 420 421val NNF_NEG_LEMM = store_thm 422 ("NNF_NEG_LEMM", 423 ``!f w. MODELS w (NNF (F_NEG f)) = ~MODELS w (NNF f)``, 424 Induct_on `f` >> fs[MODELS_def, NNF_def] 425 ); 426 427val NNF_THM = store_thm 428 ("NNF_THM", 429 ``!f w. FLTL_MODELS w f = MODELS w (NNF f)``, 430 Induct_on `f` >> fs[FLTL_MODELS_def, MODELS_def, NNF_def] 431 >> metis_tac[NNF_NEG_LEMM] 432 ); 433 434val LTL_FALSE_def = zDefine ` 435 LTL_FALSE p = F_CONJ (F_VAR p) (F_NEG (F_VAR p))`; 436 437val LTL_TRUE_def = zDefine ` 438 LTL_TRUE p = F_NEG (LTL_FALSE p)`; 439 440val LTL_F_def = zDefine ` 441 LTL_F �� p = F_U (LTL_TRUE p) ��` 442 443val LTL_G_def = zDefine ` 444 LTL_G �� p = F_NEG (LTL_F (F_NEG ��) p)`; 445 446(* Some example formulae*) 447 448val LTL_EX1_def = Define` 449 LTL_EX1 = VAR 0`; 450 451val LTL_EX2_def = Define` 452 LTL_EX2 = U (VAR 0) (VAR 1)`; 453 454val LTL_EX3_def = Define` 455 LTL_EX3 = R (VAR 0) (VAR 1)`; 456 457val LTL_EX4_def = Define` 458 LTL_EX4 = NNF (F_CONJ (LTL_G (LTL_F (F_VAR 1) 0) 0) 459 ((LTL_F (F_CONJ (F_VAR 2) (LTL_G (F_NEG (F_VAR 3)) 0)) 0)))`; 460 461val LTL_EX5_def = Define` 462 LTL_EX5 = NNF (F_CONJ (F_CONJ (LTL_G (LTL_F (F_VAR 1) 0) 0) 463 (LTL_G (LTL_F (F_VAR 2) 0) 0) 464 ) 465 ((LTL_F (F_CONJ (F_VAR 3) (LTL_G (F_NEG (F_VAR 4)) 0)) 0)))`; 466 467val LTL_EX5_def = Define` 468LTL_EX5 = NNF (F_CONJ (F_CONJ (F_CONJ (LTL_G (LTL_F (F_VAR 1) 0) 0) 469 (LTL_G (LTL_F (F_VAR 2) 0) 0) 470 ) 471 (LTL_G (LTL_F (F_VAR 3) 0) 0) 472 ) 473 ((LTL_F (F_CONJ (F_VAR 4) (LTL_G (F_NEG (F_VAR 5)) 0)) 0)))`; 474 475val _ = export_theory(); 476