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