1structure translationsLib :> translationsLib = 2struct 3 4open HolKernel Parse boolLib bossLib; 5 6open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory prop_logicTheory 7 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory 8 temporal_deep_mixedTheory pred_setTheory rich_listTheory set_lemmataTheory 9 pairTheory pred_setSyntax ltl_to_automaton_formulaTheory numLib listLib translationsLibTheory 10 rltl_to_ltlTheory rltlTheory computeLib congLib temporal_deep_simplificationsLib 11 Trace symbolic_kripke_structureTheory psl_lemmataTheory ProjectionTheory psl_to_rltlTheory; 12 13exception NoLTLTerm; 14 15(* This function is recursive thus cannot be defined as a value *) 16fun SETIFY_CONV tm = 17 (SUB_CONV (SETIFY_CONV) THENC TRY_CONV (pred_setLib.INSERT_CONV NO_CONV)) tm; 18 19(* The translation of LTL to GEN_BUECHI using just rewrite rules *) 20fun ltl2omega_rewrite t l = let 21 val (typeString, ltl_type) = (dest_type (type_of l)); 22 val _ = if (typeString = "ltl") then T else raise NoLTLTerm; 23 val ltl_type = hd (ltl_type); 24 val thm = if t then LTL_TO_GEN_BUECHI___TRANSLATION_THM___MAX 25 else LTL_TO_GEN_BUECHI___TRANSLATION_THM___MIN; 26 val thm = INST_TYPE [alpha |-> ltl_type] thm; 27 val thm = SPECL [``F:bool``, l] thm; 28 val thm = SIMP_RULE list_ss [LTL_TO_GEN_BUECHI_def, 29 LTL_ALWAYS_def, LTL_EVENTUAL_def, 30 LTL_TO_GEN_BUECHI_DS___A_NDET_def, 31 LTL_TO_GEN_BUECHI_DS___A_UNIV_def, 32 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 33 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 34 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 35 XP_BIGAND_def, 36 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 37 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 38 A_BIGAND_def, 39 symbolic_semi_automaton_REWRITES, 40 LTL_TO_GEN_BUECHI___EXTEND_def, 41 P_USED_VARS_def, 42 XP_CURRENT_def, 43 XP_NEXT_def, 44 P_BIGAND_def, 45 UNION_INSERT, 46 LET_THM, EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 47 EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, 48 UNION_EMPTY, EMPTY_LTL_TO_GEN_BUECHI_DS_def] thm; 49 in 50 thm 51 end; 52 53(******************************************************************************) 54(* A more sophistacted translations, that is able to exploit term-sharing *) 55(******************************************************************************) 56 57(* some general helpers *) 58fun boolToHOL b = if b then T else F; 59fun HOLToBool b = (b ~~ T); 60 61fun dsExtractFromThm dsThm = 62 hd (snd (strip_comb(concl (dsThm)))); 63 64fun dsBindingsExtractFromThm dsThm = 65 let 66 val set = el 6 (snd (strip_comb(dsExtractFromThm dsThm))); 67 val result = strip_set set; 68 in 69 result 70 end; 71 72fun getBindingFor b1 b2 l [] = (false, false, ``dummy:num``) 73 | getBindingFor b1 b2 l (h::l1) = 74 let 75 val hList = strip_pair h; 76 val (l', a1, a2, pf) = (el 1 hList, HOLToBool(el 2 hList), HOLToBool(el 3 hList), el 4 hList); 77 in 78 if ((l' ~~ l) andalso ((not b1) orelse a1) andalso ((not b2) orelse a2)) then 79 (a1, a2, pf) 80 else 81 getBindingFor b1 b2 l l1 82 end; 83 84exception T_IMP_Error; 85val t_imp_elim_rwt = prove (``!x. (T ==> x) = x``, REWRITE_TAC[]); 86 87fun T_IMP_ELIM_RULE thm = 88 (CONV_RULE (REWR_CONV t_imp_elim_rwt) thm) handle _ => ( 89 let 90 val _ = print "Theorem not of the form T ==> x\n\n"; 91 val _ = print_thm thm; 92 in 93 raise T_IMP_Error 94 end 95 ); 96 97local 98 val bindings_compset = new_compset [IN_SING, IN_INSERT, OR_CLAUSES, AND_CLAUSES] 99in 100 fun SIMP_DS___BINDINGS thm = 101 let 102 val conv = (DEPTH_CONV (pred_setLib.IN_CONV NO_CONV)) THENC CBV_CONV bindings_compset 103 val thm = CONV_RULE (RATOR_CONV (RAND_CONV conv)) thm; 104 val thm = T_IMP_ELIM_RULE thm; 105 in 106 thm 107 end; 108end; 109 110(* ltl_to_omega_internal and ltl_to_omega *) 111local 112 exception UnsupportedLTLTerm; 113 exception UnsupportedTerm; 114 exception NotYetImplemented; 115 exception ImplementionError; 116 117 val SIMP_DS___BASIC = 118 let 119 val compset = new_compset [ltl_to_gen_buechi_ds_REWRITES, 120 NOT_CLAUSES, AND_CLAUSES] 121 in 122 CONV_RULE (CBV_CONV compset) 123 end; 124 125 val SIMP_DS___USED_VARS = 126 let 127 val compset = new_compset [UNION_EMPTY, P_USED_VARS_EVAL, UNION_SING, 128 INSERT_UNION_EQ, INSERT_INSERT] 129 val conv = CBV_CONV compset 130 in 131 CONV_RULE (RAND_CONV (RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV (conv)))))) 132 end; 133 134 val SIMP_DS___USED_VARS___DUPLICATES = 135 CONV_RULE (RAND_CONV (RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV (SETIFY_CONV)))))) 136 137 val SIMP_DS___USED_STATE_VARS = 138 let 139 val conv = REDUCE_CONV 140 in 141 CONV_RULE (RAND_CONV (RATOR_CONV (RATOR_CONV (RATOR_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV (conv)))))))) 142 end; 143 144 val SIMP_DS___FAIRNESS_CONSTRAINT = 145 let 146 val compset = new_compset [COND_CLAUSES, APPEND_NIL, APPEND] 147 val conv = CBV_CONV compset 148 in 149 CONV_RULE (RAND_CONV (RATOR_CONV (RAND_CONV (conv)))) 150 end; 151 152 fun BUILD_LIST_FIRST_CONV term conv = 153 if (is_comb term) then 154 BUILD_LIST_FIRST_CONV (rator term) (RATOR_CONV conv) 155 else 156 (term, conv); 157 158 val compset = new_compset [XP_CURRENT_def, XP_NEXT_def] 159 fun SIMP_DS___FIRST_TRANSITION thm = 160 let 161 val conv = CBV_CONV compset; 162 val term = rator(rand (rator (rator (rand (concl thm))))) 163 val (_, conv) = BUILD_LIST_FIRST_CONV term (RAND_CONV conv); 164 val conv = (RAND_CONV (RATOR_CONV (RATOR_CONV (RAND_CONV (conv))))) 165 in 166 CONV_RULE conv thm 167 end; 168 169 fun SIMP_DS___BODY thm = 170 let 171 val thm = SIMP_DS___USED_VARS thm 172 val thm = SIMP_DS___USED_STATE_VARS thm 173 val thm = SIMP_DS___FAIRNESS_CONSTRAINT thm 174 in 175 thm 176 end; 177 178 fun ltl2omega_internal2 b1 b2 l dsThm TSPECL = 179 let 180 fun extractFuncAndArgs l = 181 let 182 val (f, args) = strip_comb l; 183 val (fs, _) = dest_const f; 184 in 185 (f, args, fs) 186 end; 187 val (f, args, fs) = extractFuncAndArgs l handle _ => (l, [], "ERROR"); 188 189 fun addBindingFor b1 b2 l dsThm = 190 let 191 val dsB = dsBindingsExtractFromThm dsThm; 192 val (b1', b2', pf) = getBindingFor b1 b2 l dsB; 193 in 194 if (b1' orelse b2') then (b1', b2', pf, dsThm) else ( 195 let 196 val dsThm = ltl2omega_internal2 b1 b2 l dsThm TSPECL; 197 val dsB = dsBindingsExtractFromThm dsThm; 198 val (b1', b2', pf) = (getBindingFor b1 b2 l dsB); 199 val _ = if (b1' orelse b2') then T else 200 (let 201 val _ = print "After inserting a binding for ("; 202 val _ = print_term l; 203 val _ = print ", "; 204 val _ = print_term (boolToHOL b1); 205 val _ = print ", "; 206 val _ = print_term (boolToHOL b2); 207 val _ = print "), it still is not present in:\n\n"; 208 val _ = print_thm dsThm; 209 val _ = print "\n\nThere has to be an Implementation Error!\n\n"; 210 in 211 raise ImplementionError 212 end); 213 in 214 (b1', b2', pf, dsThm) 215 end 216 ) 217 end; 218 219 in 220 if fs = "LTL_PROP" then ( 221 let 222 val ds = dsExtractFromThm dsThm; 223 val thm = TSPECL [ds, hd args] 224 (CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP___eval); 225 val thm = MP thm dsThm; 226 val thm = SIMP_DS___BASIC thm; 227 val thm = SIMP_DS___USED_VARS thm 228 in 229 thm 230 end 231 ) else if fs = "LTL_NOT" then ( 232 let 233 val (b2', b1', pf, dsThm) = addBindingFor b2 b1 (hd args) dsThm; 234 val ds = dsExtractFromThm dsThm; 235 val thm = TSPECL [boolToHOL b2', boolToHOL b1'] 236 (CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___eval); 237 val thm = REWRITE_RULE [NOT_CLAUSES] thm 238 val thm = SPECL [ds, hd args, pf] thm 239 val thm = MP thm dsThm; 240 val thm = SIMP_DS___BASIC thm; 241 val thm = SIMP_DS___BINDINGS thm; 242 in 243 thm 244 end 245 ) else if fs = "LTL_NEXT" then ( 246 let 247 val (b1', b2', pf, dsThm) = addBindingFor b1 b2 (hd args) dsThm; 248 val ds = dsExtractFromThm dsThm; 249 val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf] 250 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___eval; 251 val thm = MP thm dsThm; 252 val thm = SIMP_DS___BASIC thm; 253 val thm = SIMP_DS___BINDINGS thm; 254 val thm = SIMP_DS___USED_STATE_VARS thm 255 val thm = SIMP_DS___FIRST_TRANSITION thm; 256 in 257 thm 258 end 259 ) else if fs = "LTL_PSNEXT" then ( 260 let 261 val (b1', b2', pf, dsThm) = addBindingFor b1 b2 (hd args) dsThm; 262 val ds = dsExtractFromThm dsThm; 263 val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf] 264 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___eval; 265 val thm = MP thm dsThm; 266 val thm = SIMP_DS___BASIC thm; 267 val thm = SIMP_DS___BINDINGS thm; 268 val thm = SIMP_DS___USED_STATE_VARS thm 269 val thm = SIMP_DS___FIRST_TRANSITION thm; 270 in 271 thm 272 end 273 ) else if fs = "LTL_PNEXT" then ( 274 let 275 val (b1', b2', pf, dsThm) = addBindingFor b1 b2 (hd args) dsThm; 276 val ds = dsExtractFromThm dsThm; 277 val thm = TSPECL [(boolToHOL b1'), (boolToHOL b2'), ds, hd args, pf] 278 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___eval; 279 val thm = MP thm dsThm; 280 val thm = SIMP_DS___BASIC thm; 281 val thm = SIMP_DS___BINDINGS thm; 282 val thm = SIMP_DS___USED_STATE_VARS thm 283 val thm = SIMP_DS___FIRST_TRANSITION thm; 284 in 285 thm 286 end 287 ) else if fs = "LTL_AND" then ( 288 let 289 val args = strip_pair (hd args); 290 val (l1, l2) = (el 1 args, el 2 args); 291 val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm; 292 val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm; 293 val ds = dsExtractFromThm dsThm; 294 val thm = TSPECL [ds, (boolToHOL b11), (boolToHOL b12), (boolToHOL b21), (boolToHOL b22), l1, l2, pf1, pf2] 295 (CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___eval); 296 val thm = MP thm dsThm; 297 val thm = SIMP_DS___BASIC thm; 298 val thm = SIMP_DS___BINDINGS thm; 299 in 300 thm 301 end 302 ) else if fs = "LTL_OR" then ( 303 let 304 val args = strip_pair (hd args); 305 val (l1, l2) = (el 1 args, el 2 args); 306 val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm; 307 val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm; 308 val ds = dsExtractFromThm dsThm; 309 val thm = TSPECL [ds, (boolToHOL b11), (boolToHOL b12), (boolToHOL b21), (boolToHOL b22), l1, l2, pf1, pf2] 310 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___eval; 311 val thm = MP thm dsThm; 312 val thm = SIMP_DS___BASIC thm; 313 val thm = SIMP_DS___BINDINGS thm; 314 in 315 thm 316 end 317 ) else if fs = "LTL_EQUIV" then ( 318 let 319 val args = strip_pair (hd args); 320 val (l1, l2) = (el 1 args, el 2 args); 321 val (b11, b12, pf1, dsThm) = addBindingFor true true l1 dsThm; 322 val (b21, b22, pf2, dsThm) = addBindingFor true true l2 dsThm; 323 val ds = dsExtractFromThm dsThm; 324 val thm = TSPECL [ds, l1, l2, pf1, pf2] 325 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___eval; 326 val thm = MP thm dsThm; 327 val thm = SIMP_DS___BASIC thm; 328 val thm = SIMP_DS___BINDINGS thm; 329 in 330 thm 331 end 332 ) else if fs = "LTL_SUNTIL" then ( 333 let 334 val args = strip_pair (hd args); 335 val (l1, l2) = (el 1 args, el 2 args); 336 val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm; 337 val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm; 338 val ds = dsExtractFromThm dsThm; 339 val thm = TSPECL [(boolToHOL b11), (boolToHOL b12), (boolToHOL b21), 340 (boolToHOL b22), (boolToHOL b1)] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___eval; 341 val thm = REWRITE_RULE [APPEND] thm; 342 val thm = SPECL [ds, l1, l2, pf1, pf2] thm; 343 val thm = MP thm dsThm; 344 val thm = SIMP_DS___BASIC thm; 345 val thm = SIMP_DS___BINDINGS thm; 346 val thm = SIMP_DS___USED_STATE_VARS thm 347 val thm = SIMP_DS___FIRST_TRANSITION thm; 348 in 349 thm 350 end 351 ) else if fs = "LTL_BEFORE" then ( 352 let 353 val args = strip_pair (hd args); 354 val (l1, l2) = (el 1 args, el 2 args); 355 val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm; 356 val (b21, b22, pf2, dsThm) = addBindingFor b2 b1 l2 dsThm; 357 val ds = dsExtractFromThm dsThm; 358 val thm = TSPECL [(boolToHOL b11), (boolToHOL b12), (boolToHOL b21), 359 (boolToHOL b22), (boolToHOL b2)] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___eval; 360 val thm = REWRITE_RULE [APPEND] thm; 361 val thm = SPECL [ds, l1, l2, pf1, pf2] thm; 362 val thm = MP thm dsThm; 363 val thm = SIMP_DS___BASIC thm; 364 val thm = SIMP_DS___BINDINGS thm; 365 val thm = SIMP_DS___USED_STATE_VARS thm 366 val thm = SIMP_DS___FIRST_TRANSITION thm; 367 in 368 thm 369 end 370 ) else if fs = "LTL_PBEFORE" then ( 371 let 372 val args = strip_pair (hd args); 373 val (l1, l2) = (el 1 args, el 2 args); 374 val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm; 375 val (b21, b22, pf2, dsThm) = addBindingFor b2 b1 l2 dsThm; 376 val ds = dsExtractFromThm dsThm; 377 val thm = TSPECL [(boolToHOL b11), (boolToHOL b12), (boolToHOL b21), 378 (boolToHOL b22)] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___eval; 379 val thm = REWRITE_RULE [APPEND] thm; 380 val thm = SPECL [ds, l1, l2, pf1, pf2] thm; 381 val thm = MP thm dsThm; 382 val thm = SIMP_DS___BASIC thm; 383 val thm = SIMP_DS___BINDINGS thm; 384 val thm = SIMP_DS___USED_STATE_VARS thm 385 val thm = SIMP_DS___FIRST_TRANSITION thm; 386 in 387 thm 388 end 389 ) else if fs = "LTL_PSUNTIL" then ( 390 let 391 val args = strip_pair (hd args); 392 val (l1, l2) = (el 1 args, el 2 args); 393 val (b11, b12, pf1, dsThm) = addBindingFor b1 b2 l1 dsThm; 394 val (b21, b22, pf2, dsThm) = addBindingFor b1 b2 l2 dsThm; 395 val ds = dsExtractFromThm dsThm; 396 val thm = TSPECL [(boolToHOL b11), (boolToHOL b12), (boolToHOL b21), 397 (boolToHOL b22), ds, l1, l2, pf1, pf2] 398 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___eval; 399 val thm = MP thm dsThm; 400 val thm = SIMP_DS___BASIC thm; 401 val thm = SIMP_DS___BINDINGS thm; 402 val thm = SIMP_DS___USED_STATE_VARS thm 403 val thm = SIMP_DS___FIRST_TRANSITION thm; 404 in 405 thm 406 end 407 ) else ( 408 let 409 val _ = print "\n\n\n"; 410 val _ = print_term f; 411 val _ = print "\n"; 412 val _ = print_term l; 413 val _ = print "\n\n\n"; 414 in 415 raise UnsupportedLTLTerm 416 end 417 ) 418 end; 419 420 fun dsSingBindingExtractFromThm dsThm = 421 let 422 val ds = dsExtractFromThm dsThm; 423 val set = el 6 (snd (strip_comb ds)); 424 val binding = hd (strip_set set); 425 val hList = strip_pair binding; 426 val (l, b1, b2, pf) = (el 1 hList, HOLToBool(el 2 hList), HOLToBool(el 3 hList), el 4 hList); 427 in 428 (ds, l, b1, b2, pf) 429 end; 430 431 local 432 val compset = new_compset [MAP, APPEND_NIL, 433 COND_CLAUSES, APPEND, ltl_to_gen_buechi_ds_REWRITES, 434 NOT_CLAUSES, t_imp_elim_rwt, ADD_CLAUSES]; 435 in 436 fun SIMP_DS___BODY___FORGET thm = 437 let 438 val thm = CONV_RULE (CBV_CONV compset) thm 439 val thm = SIMP_DS___USED_VARS thm 440 val thm = SIMP_DS___USED_STATE_VARS thm 441 in 442 thm 443 end; 444 end 445 446 fun ltl2omega_internal3_forget b1 b2 l TSPECL = 447 let 448 fun extractFuncAndArgs l = 449 let 450 val (f, args) = strip_comb l; 451 val (fs, _) = dest_const f; 452 in 453 (f, args, fs) 454 end; 455 val (f, args, fs) = extractFuncAndArgs l handle _ => (l, [], "ERROR"); 456 457 fun oneAncestor b1 b2 b11 b12 A thm = 458 (let 459 val dsThm = ltl2omega_internal3_forget b11 b12 A TSPECL; 460 val (ds, l, _, _, pf) = dsSingBindingExtractFromThm dsThm; 461 val thm = TSPECL [boolToHOL b1, boolToHOL b2, ds, l, pf] thm; 462 val thm = MP thm dsThm; 463 val thm = SIMP_DS___BODY___FORGET thm; 464 in 465 thm 466 end); 467 468 fun twoAncestors b1 b2 b11 b12 b21 b22 aPair thm = ( 469 let 470 val args = strip_pair (aPair); 471 val (l1, l2) = (el 1 args, el 2 args); 472 473 val ds1Thm = ltl2omega_internal3_forget b11 b12 l1 TSPECL; 474 val ds2Thm = ltl2omega_internal3_forget b21 b22 l2 TSPECL; 475 val (ds1, l1, _, _, pf1) = dsSingBindingExtractFromThm ds1Thm; 476 val (ds2, l2, _, _, pf2) = dsSingBindingExtractFromThm ds2Thm; 477 478 val thm = TSPECL [(boolToHOL b1), (boolToHOL b2), ds1, ds2, l1, l2, pf1, pf2] thm; 479 val thm = MP thm ds1Thm; 480 val thm = MP thm ds2Thm; 481 val thm = SIMP_DS___BODY___FORGET thm; 482 in 483 thm 484 end); 485 in 486 if fs = "LTL_PROP" then ( 487 let 488 val thm = TSPECL [(boolToHOL b1), (boolToHOL b2), hd args] 489 (CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP___forget_eval); 490 val thm = SIMP_DS___USED_VARS thm 491 in 492 thm 493 end 494 ) else if fs = "LTL_NOT" then ( 495 oneAncestor b1 b2 b2 b1 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___forget_eval 496 ) else if fs = "LTL_NEXT" then ( 497 oneAncestor b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___forget_eval 498 ) else if fs = "LTL_PSNEXT" then ( 499 oneAncestor b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___forget_eval 500 ) else if fs = "LTL_PNEXT" then ( 501 oneAncestor b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___forget_eval 502 ) else if fs = "LTL_AND" then ( 503 twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___forget_eval 504 ) else if fs = "LTL_EQUIV" then ( 505 twoAncestors b1 b2 true true true true (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___forget_eval 506 ) else if fs = "LTL_OR" then ( 507 twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___forget_eval 508 ) else if fs = "LTL_SUNTIL" then ( 509 twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___forget_eval 510 ) else if fs = "LTL_BEFORE" then ( 511 twoAncestors b1 b2 b1 b2 b2 b1 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___forget_eval 512 ) else if fs = "LTL_PBEFORE" then ( 513 twoAncestors b1 b2 b1 b2 b2 b1 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___forget_eval 514 ) else if fs = "LTL_PSUNTIL" then ( 515 twoAncestors b1 b2 b1 b2 b1 b2 (hd args) CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___forget_eval 516 ) else ( 517 let 518 val _ = print "\n\n\n"; 519 val _ = print_term f; 520 val _ = print "\n"; 521 val _ = print_term l; 522 val _ = print "\n\n\n"; 523 in 524 raise UnsupportedLTLTerm 525 end 526 ) 527 end; 528 529 530 fun ltl2omega_internal2_forget b1 b2 l TSPECL = 531 let 532 val thm = ltl2omega_internal3_forget b1 b2 l TSPECL; 533 val thm = SIMP_RULE list_ss [INSERT_UNION_EQ, 534 UNION_EMPTY] thm 535 in 536 thm 537 end; 538 539 val ltl_ss = std_ss ++ rewrites [LTL_ALWAYS_PALWAYS_ALTERNATIVE_DEFS, 540 LTL_IMPL_def, 541 LTL_COND_def, 542 LTL_EVENTUAL_def, 543 LTL_UNTIL_def, 544 LTL_SBEFORE_def, 545 LTL_WHILE_def, 546 LTL_SWHILE_def, 547 LTL_PEVENTUAL_def, 548 LTL_PUNTIL_def, 549 LTL_PSBEFORE_def, 550 LTL_PWHILE_def, 551 LTL_PSWHILE_def, 552 LTL_INIT_def]; 553 554 val emptyDSThm = SIMP_RULE std_ss [EMPTY_LTL_TO_GEN_BUECHI_DS_def] 555 EMPTY_LTL_TO_GEN_BUECHI_DS___SEM; 556 557 val basic_compset = new_compset [ltl_to_gen_buechi_ds_REWRITES, 558 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def] 559 560 val final_compset = new_compset [LTL_TO_GEN_BUECHI_DS___A_NDET_def, 561 LTL_TO_GEN_BUECHI_DS___A_UNIV_def, 562 ltl_to_gen_buechi_ds_REWRITES, 563 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 564 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 565 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 566 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 567 MAP] 568 569in 570 571 fun ltl2omega_internal fast b1 b2 t = 572 let 573 val ltl_type = hd (snd (dest_type (type_of t))); 574 fun TSPECL t thm = 575 SPECL t (INST_TYPE [alpha |-> ltl_type] thm); 576 val dsThm = (INST_TYPE [alpha |-> ltl_type] emptyDSThm); 577 val equiv_const = inst [alpha |-> ltl_type] ``LTL_EQUIVALENT:'a ltl -> 'a ltl -> bool`` 578 579 val equivTHM = CONGRUENCE_SIMP_CONV equiv_const ltl_nnf_cs ltl_ss [] t; 580 581 val equivTHM = CONV_RULE (RAND_CONV (REWRITE_CONV [LTL_FALSE_def, LTL_TRUE_def])) equivTHM; 582 val l = rand (concl (equivTHM)); 583 584 val thm = if fast then 585 ltl2omega_internal2_forget b1 b2 l TSPECL 586 else 587 ltl2omega_internal2 b1 b2 l dsThm TSPECL; 588 val thm = SIMP_DS___USED_VARS___DUPLICATES thm 589 590 val ds = dsExtractFromThm thm; 591 val dsB = dsBindingsExtractFromThm thm; 592 val (b1', b2', pf) = (getBindingFor b1 b2 l dsB); 593 in 594 (l, equivTHM, thm, ds, pf, b1', b2') 595 end; 596 597 fun ltl2omega fast neg l = 598 let 599 val (typeString, ltl_type) = (dest_type (type_of l)); 600 val _ = if (typeString = "ltl") then T else raise NoLTLTerm; 601 val ltl_type = hd (ltl_type); 602 val (b1, b2) = if neg then (true, false) else (false, true); 603 val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast b1 b2 l; 604 605 val thm = if neg then LTL_TO_GEN_BUECHI_DS___SEM___MAX___eval else 606 LTL_TO_GEN_BUECHI_DS___SEM___MIN___eval; 607 val a = if neg then b2' else b1'; 608 val thm = INST_TYPE [alpha |-> ltl_type] thm; 609 val thm = SPECL [ds, l, equivL, pf, boolToHOL a] thm; 610 val thm = MP thm dsThm 611 val thm = MP thm equivTHM 612 val thm = CONV_RULE (CBV_CONV basic_compset) thm 613 val thm = SIMP_DS___BINDINGS thm 614 val thm = CONV_RULE (CBV_CONV final_compset) thm 615 val thm = SIMP_RULE std_ss [] thm 616 in 617 thm 618 end; 619end; 620 621(* ltl_to_ks functions *) 622local 623 val final_compset_ks = new_compset [LTL_TO_GEN_BUECHI_DS___A_NDET_def, 624 LTL_TO_GEN_BUECHI_DS___A_UNIV_def, 625 ltl_to_gen_buechi_ds_REWRITES, 626 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 627 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 628 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 629 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 630 MAP, XP_NEXT_THM, XP_CURRENT_THM, P_BIGAND_def, XP_BIGAND_def]; 631 632 val final_compset_ks___product = new_compset [SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, 633 symbolic_kripke_structure_REWRITES, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 634 UNION_EMPTY, P_USED_VARS_EVAL, XP_USED_VARS_EVAL, UNION_SING, 635 INSERT_UNION_EQ, INSERT_INSERT]; 636 637 val special_CS = CSFRAG {rewrs = [], 638 relations = [], 639 dprocs = [], 640 congs = [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_cong]}; 641 642 val basic_compset = new_compset [ltl_to_gen_buechi_ds_REWRITES, 643 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def]; 644 645 val final_cs = mk_congset [prop_logic_CS, xprop_logic_CS, special_CS]; 646 647in 648 fun ltl_contradiction2ks_fair_emptyness fast l = 649 let 650 val (typeString, ltl_type) = (dest_type (type_of l)); 651 val _ = if (typeString = "ltl") then T else raise NoLTLTerm; 652 val ltl_type = hd (ltl_type); 653 val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast true false l; 654 655 val thm = LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___KRIPKE_STRUCTURE___eval 656 val thm = INST_TYPE [alpha |-> ltl_type] thm; 657 val thm = SPECL [ds, l, equivL, pf, boolToHOL b2'] thm; 658 val thm = MP thm dsThm 659 val thm = MP thm equivTHM 660 val thm = CONV_RULE (CBV_CONV basic_compset) thm 661 val thm = SIMP_DS___BINDINGS thm 662 val thm = CONV_RULE (CBV_CONV final_compset_ks) thm 663 val thm = CONGRUENCE_SIMP_RULE final_cs std_ss [] thm 664 in 665 thm 666 end; 667 668 fun ltl_equivalent2ks_fair_emptyness fast l1 l2 = 669 let 670 val contr_thm = ISPECL [l1, l2] LTL_EQUIVALENT___TO___CONTRADICTION; 671 val l = rand (rhs (concl contr_thm)) 672 val thm = ltl_contradiction2ks_fair_emptyness fast l 673 val thm = REWRITE_RULE [GSYM contr_thm] thm 674 in 675 thm 676 end; 677 678 fun ltl_equivalent_initial2ks_fair_emptyness fast l1 l2 = 679 let 680 val contr_thm = ISPECL [l1, l2] LTL_EQUIVALENT_INITIAL___TO___CONTRADICTION; 681 val l = rand (rhs (concl contr_thm)) 682 val thm = ltl_contradiction2ks_fair_emptyness fast l 683 val thm = REWRITE_RULE [GSYM contr_thm] thm 684 in 685 thm 686 end; 687 688 fun ltl_ks_sem2ks_fair_emptyness___no_ks fast l = 689 let 690 val (typeString, ltl_type) = (dest_type (type_of l)); 691 val _ = if (typeString = "ltl") then T else raise NoLTLTerm; 692 val ltl_type = hd (ltl_type); 693 val (equivL, equivTHM, dsThm, ds, pf, b1', b2') = ltl2omega_internal fast false true l; 694 695 val thm = LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE___eval 696 val thm = INST_TYPE [alpha |-> ltl_type] thm; 697 val thm = SPECL [ds, l, equivL, pf, boolToHOL b1'] thm; 698 val thm = MP thm dsThm 699 val thm = MP thm equivTHM 700 val thm = CONV_RULE (CBV_CONV basic_compset) thm 701 val thm = SIMP_DS___BINDINGS thm 702 val thm = CONV_RULE (CBV_CONV final_compset_ks) thm 703 val thm = SIMP_RULE std_ss [] thm 704 in 705 thm 706 end; 707 708 fun ltl_ks_sem2ks_fair_emptyness fast l M = 709 let 710 val thm = ltl_ks_sem2ks_fair_emptyness___no_ks fast l; 711 val thm = SPEC M thm; 712 val thm = CONV_RULE (CBV_CONV final_compset_ks___product) thm 713 val thm = CONGRUENCE_SIMP_RULE final_cs std_ss [] thm 714 in 715 thm 716 end; 717end; 718 719(* ltl_to_ks num functions *) 720local 721 val used_vars_compset = 722 new_compset [LTL_USED_VARS_EVAL, 723 P_USED_VARS_EVAL, 724 XP_USED_VARS_EVAL, 725 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 726 symbolic_kripke_structure_REWRITES, 727 UNION_EMPTY, 728 UNION_SING, INSERT_UNION_EQ] 729 730 val renaming_to_num_compset = 731 new_compset [LTL_VAR_RENAMING_EVAL, P_VAR_RENAMING_EVAL] 732 733 val renaming_to_num_compset_ks = 734 new_compset [LTL_VAR_RENAMING_EVAL, P_VAR_RENAMING_EVAL, 735 SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING_def, 736 P_VAR_RENAMING_EVAL, XP_VAR_RENAMING_EVAL, 737 symbolic_kripke_structure_REWRITES] 738 739 val pred_set_forall_compset = 740 new_compset [ 741 res_quanTheory.RES_FORALL_EMPTY, 742 RES_FORALL_INSERT, 743 prove (``!x:num n:num. x + n >= n``, DECIDE_TAC), 744 AND_CLAUSES] 745 746 val inj_thm_compset = 747 new_compset [MEM, OR_CLAUSES, IN_INSERT, NOT_IN_EMPTY, IMP_CLAUSES] 748 749 val all_distinct_compset = 750 new_compset [ALL_DISTINCT, AND_CLAUSES, MEM, OR_CLAUSES,DE_MORGAN_THM, NOT_CLAUSES] 751 752 fun enum_list n [] = [] 753 | enum_list n (h::l) = ((n, h)::(enum_list (n+1) l)) 754 755 val ks_var_renaming_compset = 756 new_compset [MAP, SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING_def, 757 symbolic_kripke_structure_REWRITES, 758 P_VAR_RENAMING_EVAL, XP_VAR_RENAMING_EVAL] 759 760 761 fun ks_fair_emptyness___num___initial thm num_thm ltl_type = 762 let 763 val used_vars_term = rand (rator (rand (rator (body (rand (concl thm)))))); 764 val num_thm = GSYM (UNDISCH (SPEC_ALL num_thm)); 765 766 val thm = ISPEC ``\n:num. n`` thm 767 val thm = REWRITE_RULE [num_thm, IS_ELEMENT_ITERATOR___ID] thm 768 val thm = DISCH_ALL thm; 769 val thm = CONV_RULE (RATOR_CONV (CBV_CONV used_vars_compset)) thm 770 771 val f_term = rand (rator (rator (rand (rator ((concl thm)))))) 772 val thm = GEN f_term thm 773 val new_f_term = ``\x. ((f:'a->num) x) + n``; 774 val new_f_term = inst [alpha |-> ltl_type] new_f_term; 775 val new_f_term = subst [(``n:num`` |-> used_vars_term), 776 ((mk_var ("f", ltl_type --> num)) |-> f_term)] new_f_term; 777 val thm = SPEC new_f_term thm 778 val thm = CONV_RULE (RAND_CONV (RATOR_CONV (CBV_CONV pred_set_forall_compset))) thm 779 val thm = REWRITE_RULE [INJ___ADD_FUNC] thm 780 val thm = BETA_RULE thm 781 val thm = CONV_RULE (RATOR_CONV (SETIFY_CONV)) thm; 782 val thm = GEN f_term thm 783 784 in 785 (thm, ltl_type, int_of_term used_vars_term) 786 end; 787 788 789fun ks_fair_emptyness___num___eq thm ltl_type used_vars_num = 790 let 791 val var_set_term = rand (rator (rand (rator (body (rand (concl thm)))))); 792 val var_list = strip_set var_set_term; 793 val var_list_term = listSyntax.mk_list (var_list, ltl_type); 794 795 val pos_start_term = ``\x:'a. PRE (POS_START (0:num) (l:'a list) x)``; 796 val pos_start_term = inst [alpha |-> ltl_type] pos_start_term 797 val pos_start_term = subst [mk_var("l", type_of var_list_term) |-> var_list_term] pos_start_term; 798 799 val thm = SPEC pos_start_term thm 800 801 val inj_thm = INJ_POS_START___MP_HELPER; 802 val inj_thm = ISPECL [var_list_term, var_set_term, ``0:num``] inj_thm 803 val inj_thm = CONV_RULE (RATOR_CONV (RAND_CONV (CBV_CONV inj_thm_compset))) inj_thm 804 val inj_thm = UNDISCH (REWRITE_RULE [] inj_thm) 805 806 807 val pos_start_term_concr = ``PRE (POS_START (0:num) (l:'a list) (x:'a))``; 808 val pos_start_term_concr = inst [alpha |-> ltl_type] pos_start_term_concr; 809 val pos_start_term_concr = subst [mk_var("l", type_of var_list_term) |-> var_list_term] pos_start_term_concr 810 val pos_start_thm_concr = REWRITE_CONV [PRE_POS_START___REWRITES] pos_start_term_concr; 811 val pos_start_thm_concr = REDUCE_RULE pos_start_thm_concr; 812 val pos_start_thm_concr = GEN (mk_var ("x", ltl_type)) pos_start_thm_concr; 813 814 val inj_pos_start_thm_list = map (fn x => (SPEC x pos_start_thm_concr)) var_list; 815 val inj_pos_start_thm = LIST_CONJ inj_pos_start_thm_list; 816 817 val all_distinct_term = hd (hyp inj_thm); 818 val all_distinct_eval_thm = CBV_CONV all_distinct_compset all_distinct_term; 819 820 val inj_pos_start_thm = ADD_ASSUM (rhs (concl all_distinct_eval_thm)) inj_pos_start_thm 821 val inj_pos_start_thm = ASM_REWRITE_RULE [] inj_pos_start_thm 822 val inj_pos_start_thm = DISCH_ALL inj_pos_start_thm 823 val inj_pos_start_thm = REWRITE_RULE [GSYM all_distinct_eval_thm] inj_pos_start_thm 824 val inj_pos_start_thm = UNDISCH_ALL inj_pos_start_thm 825 826 val thm = BETA_RULE thm 827 val thm = REWRITE_RULE [inj_thm, inj_pos_start_thm] thm 828 val thm = REDUCE_RULE thm 829 val thm = DISCH_ALL thm 830 in 831 (thm, enum_list used_vars_num var_list) 832 end 833 834fun ks_fair_emptyness___num___impl thm ltl_type used_vars_num = 835 let 836 val var_set_term = rand (rator (rand (rator (body (rand (concl thm)))))); 837 val var_list = strip_set var_set_term; 838 val var_list_term = listSyntax.mk_list (var_list, ltl_type); 839 840 841 val f_term = bvar(rand (concl thm)) 842 val rewrite = map (fn p => (mk_comb(f_term, snd p) |-> term_of_int (fst p))) (enum_list 0 var_list) 843 val is_empty_ks_term = rhs (rand (body (rand (concl thm)))); 844 val is_empty_ks_term = subst rewrite is_empty_ks_term 845 846 val renaming_cond = ``\x:num. (if (x = n:num) then (((f:'a->num) e) + y:num) else (m:num->num) x)``; 847 val renaming_cond = inst [alpha |-> ltl_type] renaming_cond; 848 849 val renaming_list = (enum_list used_vars_num var_list) 850 fun renaming_fun ((n, t), et) = 851 (subst [(mk_var("f", ltl_type --> num) |-> f_term), 852 (mk_var("y", num) |-> term_of_int used_vars_num), 853 (mk_var("n", num) |-> term_of_int n), 854 (mk_var("e", ltl_type) |-> t), 855 (mk_var("m", num --> num) |-> et)] renaming_cond) 856 val renaming_term = foldr renaming_fun ``\x:num. x`` renaming_list 857 858 val (term, fc) = dest_comb is_empty_ks_term; 859 val ks = rand term; 860 861 val imp_thm = IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___IDENTIFY_VARIABLES; 862 val imp_thm = ISPECL [renaming_term, ks, fc] imp_thm 863 val imp_thm = BETA_RULE imp_thm 864 val imp_thm = CONV_RULE (CBV_CONV ks_var_renaming_compset) imp_thm 865 (*if there are no variables, do not apply REDUCE_RULE, because then 866 the theorem is of the form X ==> X and will be simplified to T*) 867 val lhs = rand (rator (concl imp_thm)) 868 val rhs = rand (concl imp_thm) 869 val imp_thm = if (lhs ~~ rhs) then imp_thm else REDUCE_RULE imp_thm 870 871 val thm = SPEC_ALL thm 872 val thm = UNDISCH thm 873 val thm = REDUCE_RULE thm (*because x + 0 may have been reduced to x in imp_thm*) 874 val thm = CONV_RULE (RAND_CONV (REWRITE_CONV [GSYM thm])) imp_thm 875 val thm = DISCH_ALL thm 876 val thm = GEN f_term thm 877 val thm = SIMP_RULE std_ss [LEFT_FORALL_IMP_THM] thm 878 879 val inj_exists_term = rand (rator (concl thm)); 880 val inj_exists_thm = prove (inj_exists_term, 881 MATCH_MP_TAC NUM_FINITE_INJ_EXISTS THEN 882 REWRITE_TAC[FINITE_INSERT, FINITE_EMPTY]) 883 val thm = REWRITE_RULE [inj_exists_thm] thm 884 in 885 (thm, enum_list used_vars_num var_list) 886 end 887 888 fun ks_fair_emptyness___num mode thm num_thm ltl_type = 889 let 890 val (thm, ltl_type, used_vars_num) = ks_fair_emptyness___num___initial thm num_thm ltl_type 891 in 892 if (mode = 1) then 893 ks_fair_emptyness___num___eq thm ltl_type used_vars_num 894 else if mode = 2 then 895 ks_fair_emptyness___num___impl thm ltl_type used_vars_num 896 else 897 let 898 val (impl_thm, vl) = ks_fair_emptyness___num___impl thm ltl_type used_vars_num 899 val (eq_thm, _) = ks_fair_emptyness___num___eq thm ltl_type used_vars_num 900 in 901 (CONJ eq_thm impl_thm, vl) 902 end 903 end 904 905in 906 907 fun ltl_contradiction2ks_fair_emptyness___num mode fast l = 908 let 909 val (typeString, ltl_type) = (dest_type (type_of l)); 910 val _ = if (typeString = "ltl") then T else raise NoLTLTerm; 911 val ltl_type = hd (ltl_type); 912 913 val num_thm = INST_TYPE [beta |-> num] LTL_CONTRADICTION___VAR_RENAMING; 914 val num_thm = ISPEC l num_thm; 915 val num_thm = CONV_RULE (CBV_CONV renaming_to_num_compset) num_thm; 916 val num_l = rand (rhs (rand (body (rand (concl num_thm))))); 917 val thm = ltl_contradiction2ks_fair_emptyness fast num_l 918 919 in 920 ks_fair_emptyness___num mode thm num_thm ltl_type 921 end 922 923 924 fun ltl_equivalent2ks_fair_emptyness___num mode fast l1 l2 = 925 let 926 val contr_thm = ISPECL [l1, l2] LTL_EQUIVALENT___TO___CONTRADICTION; 927 val l = rand (rhs (concl contr_thm)) 928 val (thm, l) = ltl_contradiction2ks_fair_emptyness___num mode fast l 929 val thm = REWRITE_RULE [GSYM contr_thm] thm 930 in 931 (thm, l) 932 end; 933 934 fun ltl_equivalent_initial2ks_fair_emptyness___num mode fast l1 l2 = 935 let 936 val contr_thm = ISPECL [l1, l2] LTL_EQUIVALENT_INITIAL___TO___CONTRADICTION; 937 val l = rand (rhs (concl contr_thm)) 938 val (thm, l) = ltl_contradiction2ks_fair_emptyness___num mode fast l 939 val thm = REWRITE_RULE [GSYM contr_thm] thm 940 in 941 (thm, l) 942 end; 943 944 fun ltl_ks_sem2ks_fair_emptyness___num mode fast l M = 945 let 946 val (typeString, ltl_type) = (dest_type (type_of l)); 947 val _ = if (typeString = "ltl") then T else raise NoLTLTerm; 948 val ltl_type = hd (ltl_type); 949 950 val num_thm = INST_TYPE [beta |-> num] LTL_KS_SEM___VAR_RENAMING; 951 val num_thm = ISPECL [l, M] num_thm; 952 val num_thm = CONV_RULE (CBV_CONV renaming_to_num_compset_ks) num_thm; 953 val num_l = rand (rhs (rand (body (rand (concl num_thm))))) 954 val num_M = rand (rator (rhs (rand (body (rand (concl num_thm)))))) 955 956 val thm = ltl_ks_sem2ks_fair_emptyness fast num_l num_M 957 in 958 ks_fair_emptyness___num mode thm num_thm ltl_type 959 end 960end; 961 962 963(********************************************************************************* 964 * PSL stuff 965 ********************************************************************************) 966 967(*Given a PSL Term t, this function replaces all functions in t by its definition. 968 Thenit tries to prove that t is CLOCK_SERE_FREE and finally calculates the a 969 translation of t to ltl*) 970 971local 972 973 exception NOT_CLOCK_SERE_FREE; 974 975in 976 977 fun prepare_psl_term t = 978 let 979 val eval_thm = EVAL_CONV t 980 val cs_free_term = liteLib.mk_icomb (``F_CLOCK_SERE_FREE:'a fl->bool``, t); 981 val cs_free_thm = ((REWRITE_CONV [eval_thm]) THENC (REWRITE_CONV [ F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, F_SERE_FREE_def])) cs_free_term; 982 val _ = if ((rhs (concl cs_free_thm)) ~~ T) then true else ( 983 let 984 val _ = print "! ERROR: Could not prove that\n! "; 985 val _ = print_term t; 986 val _ = print "\n! contains no clocks or seres. Intermediate theorem:\n\n"; 987 val _ = print_thm cs_free_thm; 988 val _ = print "\n\n"; 989 in 990 raise NOT_CLOCK_SERE_FREE 991 end); 992 val cs_free_thm = ONCE_REWRITE_RULE [] cs_free_thm; 993 994 val ltl_term = liteLib.mk_icomb (``PSL_TO_LTL:'a fl->'a ltl``, t); 995 val ltl_thm = (REWRITE_CONV [eval_thm] THENC REWRITE_CONV[PSL_TO_LTL_def, 996 RLTL_TO_LTL_def, PSL_TO_RLTL_def, BEXP_TO_PROP_LOGIC_def]) ltl_term; 997 998 val ltl = rhs (concl ltl_thm); 999 in 1000 (eval_thm, cs_free_thm, ltl_thm, ltl) 1001 end; 1002 1003end; 1004 1005fun psl_contradiction2ks_fair_emptyness fast f = 1006 let 1007 val (eval_thm, cs_free_thm, ltl_thm, l) = prepare_psl_term f; 1008 val to_ltl_thm = ISPEC f PSL_TO_LTL___UF_CONTRADICTION; 1009 val to_ltl_thm = MP to_ltl_thm cs_free_thm 1010 1011 val thm = ltl_contradiction2ks_fair_emptyness fast l 1012 val thm = REWRITE_RULE [GSYM ltl_thm, GSYM to_ltl_thm] thm 1013 in 1014 thm 1015 end 1016 1017fun psl_contradiction2ks_fair_emptyness___num mode fast f = 1018 let 1019 val (eval_thm, cs_free_thm, ltl_thm, l) = prepare_psl_term f; 1020 val to_ltl_thm = ISPEC f PSL_TO_LTL___UF_CONTRADICTION; 1021 val to_ltl_thm = MP to_ltl_thm cs_free_thm 1022 1023 val (thm, uv) = ltl_contradiction2ks_fair_emptyness___num mode fast l 1024 val thm = REWRITE_RULE [GSYM ltl_thm, GSYM to_ltl_thm] thm 1025 in 1026 (thm, uv) 1027 end 1028 1029fun psl_ks_sem2ks_fair_emptyness___no_ks fast f = 1030 let 1031 val (eval_thm, cs_free_thm, ltl_thm, l) = prepare_psl_term f; 1032 val to_ltl_thm = ISPEC ``M:'b symbolic_kripke_structure`` PSL_TO_LTL___UF_KS_SEM; 1033 val to_ltl_thm = ISPEC f to_ltl_thm; 1034 val to_ltl_thm = MP to_ltl_thm cs_free_thm 1035 1036 val thm = ltl_ks_sem2ks_fair_emptyness___no_ks fast l 1037 val thm = REWRITE_RULE [GSYM ltl_thm, GSYM to_ltl_thm] thm 1038 in 1039 thm 1040 end 1041 1042fun psl_ks_sem2ks_fair_emptyness fast f M = 1043 let 1044 val (eval_thm, cs_free_thm, ltl_thm, l) = prepare_psl_term f; 1045 val to_ltl_thm = ISPECL [M, f] PSL_TO_LTL___UF_KS_SEM; 1046 val to_ltl_thm = MP to_ltl_thm cs_free_thm 1047 1048 val thm = ltl_ks_sem2ks_fair_emptyness fast l M 1049 val thm = REWRITE_RULE [GSYM ltl_thm, GSYM to_ltl_thm] thm 1050 in 1051 thm 1052 end 1053 1054fun psl_ks_sem2ks_fair_emptyness___num mode fast f M = 1055 let 1056 val (eval_thm, cs_free_thm, ltl_thm, l) = prepare_psl_term f; 1057 val to_ltl_thm = ISPECL [M, f] PSL_TO_LTL___UF_KS_SEM; 1058 val to_ltl_thm = MP to_ltl_thm cs_free_thm 1059 1060 val (thm, uv) = ltl_ks_sem2ks_fair_emptyness___num mode fast l M 1061 val thm = REWRITE_RULE [GSYM ltl_thm, GSYM to_ltl_thm] thm 1062 in 1063 (thm, uv) 1064 end 1065 1066fun psl_equivalent2ks_fair_emptyness fast f1 f2 = 1067 let 1068 val (eval_thm1, cs_free_thm1, ltl_thm1, _) = prepare_psl_term f1; 1069 val (eval_thm2, cs_free_thm2, ltl_thm2, _) = prepare_psl_term f2; 1070 1071 val to_ltl_thm = ISPECL [f1, f2] PSL_TO_LTL___UF_EQUIVALENT; 1072 val to_ltl_thm = MP to_ltl_thm cs_free_thm1 1073 val to_ltl_thm = MP to_ltl_thm cs_free_thm2 1074 val to_ltl_thm = ONCE_REWRITE_RULE [ltl_thm1, ltl_thm2] to_ltl_thm 1075 val l = rand (rhs (concl to_ltl_thm)) 1076 1077 val thm = ltl_contradiction2ks_fair_emptyness fast l 1078 val thm = REWRITE_RULE [GSYM to_ltl_thm] thm 1079 1080 in 1081 thm 1082 end; 1083 1084fun psl_equivalent2ks_fair_emptyness___num mode fast f1 f2 = 1085 let 1086 val (eval_thm1, cs_free_thm1, ltl_thm1, _) = prepare_psl_term f1; 1087 val (eval_thm2, cs_free_thm2, ltl_thm2, _) = prepare_psl_term f2; 1088 1089 val to_ltl_thm = ISPECL [f1, f2] PSL_TO_LTL___UF_EQUIVALENT; 1090 val to_ltl_thm = MP to_ltl_thm cs_free_thm1 1091 val to_ltl_thm = MP to_ltl_thm cs_free_thm2 1092 val to_ltl_thm = ONCE_REWRITE_RULE [ltl_thm1, ltl_thm2] to_ltl_thm 1093 val l = rand (rhs (concl to_ltl_thm)) 1094 1095 val (thm, uv) = ltl_contradiction2ks_fair_emptyness___num mode fast l 1096 val thm = REWRITE_RULE [GSYM to_ltl_thm] thm 1097 1098 in 1099 (thm, uv) 1100 end; 1101 1102end 1103