1structure ibmLib :> ibmLib = 2struct 3 4(* 5quietdec := true; 6 7val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 8loadPath := (concat home_dir "src/deep_embeddings") :: 9 (concat home_dir "src/translations") :: 10 (concat home_dir "src/tools") :: 11 (concat home_dir "src/model_check") :: 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", 18 "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "temporal_deep_mixedTheory", 19 "pairTheory", "symbolic_kripke_structureTheory", 20 "numLib", "semi_automatonTheory", "omega_automatonTheory", 21 "omega_automaton_translationsTheory", "ctl_starTheory", 22 "ltl_to_automaton_formulaTheory", "containerTheory", 23 "psl_to_rltlTheory", "rltl_to_ltlTheory", "temporal_deep_simplificationsLib", "congLib", "ibmTheory", 24 "psl_lemmataTheory", "translationsLib", "modelCheckLib", 25 "Travrules", "SyntacticSugarTheory", "RewritesTheory"]; 26*) 27 28open HolKernel boolLib bossLib 29 full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory 30 prop_logicTheory 31 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory 32 pred_setTheory rich_listTheory set_lemmataTheory temporal_deep_mixedTheory pairTheory symbolic_kripke_structureTheory 33 numLib semi_automatonTheory omega_automatonTheory 34 omega_automaton_translationsTheory ctl_starTheory 35 ltl_to_automaton_formulaTheory containerTheory 36 psl_to_rltlTheory rltl_to_ltlTheory temporal_deep_simplificationsLib congLib ibmTheory computeLib psl_lemmataTheory translationsLib 37 modelCheckLib Travrules SyntacticSugarTheory RewritesTheory; 38 39(* 40show_assums := false; 41show_assums := true; 42show_types := true; 43show_types := false; 44quietdec := false; 45*) 46 47val UF_KS_SEM___cong = 48 prove ( 49 ``!f f'. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f' ==> 50 !K. UF_KS_SEM K f = UF_KS_SEM K f'``, 51 52SIMP_TAC std_ss [UF_KS_SEM_def, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def] THEN 53METIS_TAC[CONVERT_PATH_LTL_PSL___IS_INFINITE_TOP_BOTTOM_FREE]); 54 55 56val P_USED_VARS___P_BIGOR___EVAL = 57 prove (``!n0 n1. P_USED_VARS (P_BIGOR (MAP P_PROP (INTERVAL_LIST n0 n1))) = (INTERVAL_SET n0 n1)``, 58 59 ONCE_REWRITE_TAC[EXTENSION] THEN 60 SIMP_TAC std_ss [P_BIGOR___P_USED_VARS, 61 MAP_MAP_o, combinTheory.o_DEF, P_USED_VARS_def, 62 IN_INTERVAL_SET, IN_LIST_BIGUNION, 63 MEM_MAP, IN_SING, MEM_INTERVAL_LIST, 64 GSYM LEFT_EXISTS_AND_THM]); 65 66 67val PROBLEM_TO_KRIPKE_STRUCTURE___eval = 68 store_simp_thm ("PROBLEM_TO_KRIPKE_STRUCTURE___eval", 69 ``!A i0 s0 p psl psl' sv. (sv = 70 (\(n :num). 71 (2 :num) * (2 :num) ** (SUC s0 - i0) + s0 + (3 :num) + n)) ==> 72 (i0 <= s0) ==> 73 (A.S = (INTERVAL_SET (SUC i0) s0)) ==> 74 (SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)) ==> 75 (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) ==> 76 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE psl psl' ==> 77 F_CLOCK_SERE_FREE psl' ==> 78 (F_USED_VARS psl' SUBSET (INTERVAL_SET 0 i0)) ==> 79 80 !a DS l' pf. 81 LTL_EQUIVALENT 82 (LTL_EQUIV 83 (LTL_ALWAYS 84 (LTL_EVENTUAL 85 (LTL_PROP 86 (P_NOT 87 (P_BIGOR 88 (MAP P_PROP 89 (INTERVAL_LIST 90 (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 91 (SUC (SUC s0) + 2 ** SUC (s0 - i0) + 92 PRE (2 ** SUC (s0 - i0))))))))), PSL_TO_LTL psl')) l' ==> 93 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 94 (l',a,T,pf) IN DS.B ==> 95 DS.IV SUBSET INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2) ==> 96 !S0 R. 97 ((P_AND 98 (P_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) 99 (P_EQUIV 100 (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0), 101 VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 102 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) 103 (SUC i0))), 104 P_AND 105 (P_NOT 106 (P_BIGOR 107 (MAP P_PROP 108 (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 109 (PRE (2 ** SUC (s0 - i0)) + 110 (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))), 111 P_AND 112 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, 113 P_NOT (pf sv))))) = S0) ==> 114 115 ( 116 (XP_AND 117 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) 118 (XP_EQUIV 119 (XP_NEXT 120 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 121 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) 122 (SUC i0)), 123 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0)) 124 (XP_AND 125 (XP_EQUIV 126 (XP_NEXT_PROP (SUC s0), 127 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))), 128 XP_AND 129 (A.R, 130 XP_CURRENT 131 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 132 (INTERVAL_LIST (SUC i0) (SUC s0)) 133 (SUC (SUC s0)) (SUC i0))))))), 134 XP_AND 135 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) 136 (XP_EQUIV 137 (XP_NEXT 138 (P_VAR_RENAMING 139 (\n. 140 (if n >= SUC (SUC s0) then 141 n + 2 ** SUC (s0 - i0) 142 else 143 n)) 144 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 145 (INTERVAL_LIST (SUC i0) (SUC s0)) 146 (SUC (SUC s0)) (SUC i0))), 147 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0)) 148 (XP_AND 149 (XP_EQUIV 150 (XP_NEXT_PROP (SUC s0), 151 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))), 152 XP_AND 153 (A.R, 154 XP_AND 155 (XP_NEXT (P_PROP (SUC s0)), 156 XP_COND 157 (XP_BIGOR 158 (MAP XP_PROP 159 (INTERVAL_LIST 160 (SUC (SUC s0) + 161 2 ** SUC (s0 - i0)) 162 (PRE (2 ** SUC (s0 - i0)) + 163 (SUC (SUC s0) + 164 2 ** SUC (s0 - i0))))), 165 XP_CURRENT 166 (P_VAR_RENAMING 167 (\n. 168 (if n >= SUC (SUC s0) then 169 n + 2 ** SUC (s0 - i0) 170 else 171 n)) 172 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 173 (INTERVAL_LIST (SUC i0) 174 (SUC s0)) (SUC (SUC s0)) 175 (SUC i0))), 176 XP_CURRENT 177 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 178 (INTERVAL_LIST (SUC i0) (SUC s0)) 179 (SUC (SUC s0)) (SUC i0))))))))), 180 XP_BIGAND (MAP (\xp. xp sv) DS.R)))) = R) ==> 181 ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 182 (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC)) 183 = 184 185 (!K. (A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = 186 UF_KS_SEM K psl))``, 187 188 REPEAT STRIP_TAC THEN 189 `!K. UF_KS_SEM K psl = UF_KS_SEM K psl'` by METIS_TAC [UF_KS_SEM___cong] THEN 190 ASM_SIMP_TAC std_ss [] THEN 191 192 MATCH_MP_TAC PROBLEM_TO_KRIPKE_STRUCTURE THEN 193 Q_TAC EXISTS_TAC `i0` THEN 194 Q_TAC EXISTS_TAC `s0` THEN 195 Q_TAC EXISTS_TAC `l'` THEN 196 Q_TAC EXISTS_TAC `pf` THEN 197 Q_TAC EXISTS_TAC `a` THEN 198 ASM_REWRITE_TAC[UNION_SUBSET, ETA_THM] THEN 199 REPEAT STRIP_TAC THENL [ 200 201 UNDISCH_NO_TAC 11 (*SEMI_AUTOMATON_USED_VARS*) THEN 202 UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN 203 ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, SUBSET_DEF, IN_UNION, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, 204 IN_DIFF] THEN 205 REPEAT WEAKEN_HD_TAC THEN 206 REPEAT STRIP_TAC THEN 207 RES_TAC, 208 209 FULL_SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_SEM_def, 210 LTL_EQUIVALENT_def], 211 212 METIS_TAC[PROP_LOGIC_EQUIVALENT_def], 213 METIS_TAC[XPROP_LOGIC_EQUIVALENT_def] 214 ] 215 ); 216 217 218 219val PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL___eval = 220 store_simp_thm ("PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL___eval", 221 ``!A i0 s0 p psl psl' sv. 222 IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A ==> 223 (sv = \n:num. 2**(s0 - i0) + s0 + 1 + n) ==> 224 (i0 <= s0) ==> 225 (A.S = (INTERVAL_SET (SUC i0) s0)) ==> 226 (SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)) ==> 227 (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) ==> 228 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE psl psl' ==> 229 F_CLOCK_SERE_FREE psl' ==> 230 (F_USED_VARS psl' SUBSET (INTERVAL_SET 0 i0)) ==> 231 !a DS l' pf. 232 LTL_EQUIVALENT 233 (LTL_EQUIV 234 (LTL_ALWAYS 235 (LTL_PROP 236 (P_FORALL (INTERVAL_LIST (SUC i0) s0) 237 (P_IMPL 238 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 239 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0), 240 p)))), PSL_TO_LTL psl')) l' ==> 241 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 242 (l',a,T,pf) IN DS.B ==> 243 DS.IV SUBSET INTERVAL_SET 0 (2**(s0 - i0) + s0) ==> 244 !S0 R. 245 246 ((P_AND 247 (P_FORALL (INTERVAL_LIST (SUC i0) s0) 248 (P_EQUIV 249 (A.S0, 250 VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 251 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0))), 252 P_AND 253 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,P_NOT (pf sv)))) = S0) /\ 254 ((XP_AND 255 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) s0) 256 (XP_EQUIV 257 (XP_NEXT 258 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 259 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0)), 260 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) s0) 261 (XP_AND 262 (A.R, 263 XP_CURRENT 264 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 265 (INTERVAL_LIST (SUC i0) s0) (SUC s0) 266 (SUC i0)))))), 267 XP_BIGAND (MAP (\xp. xp sv) DS.R))) = R) 268 ==> 269 270 ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 271 (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC)) 272 = 273 274 (!K. 275 ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = 276 UF_KS_SEM K psl)))``, 277 278 REPEAT STRIP_TAC THEN 279 `!K. UF_KS_SEM K psl = UF_KS_SEM K psl'` by METIS_TAC [UF_KS_SEM___cong] THEN 280 ASM_SIMP_TAC std_ss [] THEN 281 282 MATCH_MP_TAC PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL THEN 283 Q_TAC EXISTS_TAC `i0` THEN 284 Q_TAC EXISTS_TAC `s0` THEN 285 Q_TAC EXISTS_TAC `l'` THEN 286 Q_TAC EXISTS_TAC `pf` THEN 287 Q_TAC EXISTS_TAC `a` THEN 288 ASM_REWRITE_TAC[UNION_SUBSET, ETA_THM] THEN 289 REPEAT STRIP_TAC THENL [ 290 291 UNDISCH_NO_TAC 11 (*SEMI_AUTOMATON_USED_VARS*) THEN 292 UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN 293 ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, SUBSET_DEF, IN_UNION, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, 294 IN_DIFF] THEN 295 REPEAT WEAKEN_HD_TAC THEN 296 REPEAT STRIP_TAC THEN 297 RES_TAC, 298 299 FULL_SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_SEM_def, 300 LTL_EQUIVALENT_def], 301 302 METIS_TAC[PROP_LOGIC_EQUIVALENT_def], 303 METIS_TAC[XPROP_LOGIC_EQUIVALENT_def] 304 ]); 305 306 307 308 309 310 311val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___P_USED_VARS = 312 prove (`` 313!i:num j:num. (i <= j) ==> (P_USED_VARS ( 314VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 315 (INTERVAL_LIST i j) (SUC j) i) = 316INTERVAL_SET i (SUC j+PRE (2 ** SUC (j - i))))``, 317 318 319SIMP_TAC std_ss [GSYM VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST, 320 VAR_RENAMING_HASHTABLE_LIST___P_USED_VARS, LIST_TO_SET___INTERVAL_LIST, 321 UNION_EMPTY] THEN 322REPEAT STRIP_TAC THEN 323`(\x. SET_BINARY_ENCODING_SHIFT i (SUC j) x) = 324 SET_BINARY_ENCODING_SHIFT i (SUC j)` by SIMP_TAC std_ss [FUN_EQ_THM] THEN 325 326ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN 327SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTERVAL_SET] THEN 328REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN 329ASM_SIMP_TAC arith_ss []); 330 331 332 333 334 335fun prepare_input_automaton A = 336 let 337 val s0 = rand (rand(rator (rator A))) 338 val suc_i0 = rand (rator (rand(rator (rator A)))) 339 val i0 = term_of_int ((int_of_term suc_i0) - 1); 340 341 342 val i0_le_s0_term = ``(i0:num) <= (s0:num)``; 343 val i0_le_s0_term = subst [ 344 mk_var ("i0", num) |-> i0, 345 mk_var ("s0", num) |-> s0] i0_le_s0_term; 346 val i0_le_s0 = DECIDE i0_le_s0_term 347 348 val state_vars_term = ``(A:num symbolic_semi_automaton).S = INTERVAL_SET (SUC i0) s0``; 349 val state_vars_term = subst [ 350 mk_var ("A", ``:num symbolic_semi_automaton``) |-> A, 351 mk_var ("i0", num) |-> i0, 352 mk_var ("s0", num) |-> s0] state_vars_term; 353 val state_vars = EQT_ELIM (SIMP_CONV std_ss [symbolic_semi_automaton_REWRITES] state_vars_term) 354 355 356 val used_vars_term = ``SEMI_AUTOMATON_USED_VARS A SUBSET INTERVAL_SET 0 s0``; 357 val used_vars_term = subst [ 358 mk_var ("A", ``:num symbolic_semi_automaton``) |-> A, 359 mk_var ("s0", num) |-> s0] used_vars_term; 360 val used_vars = (EQT_ELIM (SIMP_CONV std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, SUBSET_DEF, IN_UNION, 361 IN_SING, XP_USED_VARS_EVAL, IN_INTERVAL_SET, DISJ_IMP_THM, 362 P_USED_VARS_EVAL, symbolic_semi_automaton_REWRITES, NOT_IN_EMPTY] used_vars_term)) 363 in 364 (s0, i0, i0_le_s0, state_vars, used_vars) 365 end; 366 367 368fun prepare_ctl p s0 = 369 let 370 val used_vars_term = ``P_USED_VARS p SUBSET INTERVAL_SET 0 s0``; 371 val used_vars_term = subst [ 372 mk_var ("p", ``:num prop_logic``) |-> p, 373 mk_var ("s0", num) |-> s0] used_vars_term; 374 val used_vars = EQT_ELIM (SIMP_CONV std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, SUBSET_DEF, IN_UNION, 375 IN_SING, XP_USED_VARS_EVAL, IN_INTERVAL_SET, DISJ_IMP_THM, NOT_IN_EMPTY, 376 P_USED_VARS_EVAL, symbolic_semi_automaton_REWRITES] used_vars_term) 377 in 378 used_vars 379 end; 380 381 382 383val PSL_EQUIVALENT_congs = 384 store_thm ( 385 "PSL_EQUIVALENT_congs", 386 387 ``(!f f'. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f' ==> 388 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_NOT f) (F_NOT f')) /\ 389 390 (!f1 f1' f2 f2'. 391 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f1' ==> 392 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f2' ==> 393 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_AND (f1, f2)) (F_AND (f1', f2'))) /\ 394 395 (!f f'. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f' ==> 396 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_NEXT f) (F_NEXT f')) /\ 397 398 (!f1 f1' f2 f2'. 399 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f1' ==> 400 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f2' ==> 401 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_UNTIL (f1, f2)) (F_UNTIL (f1', f2'))) /\ 402 403 (!f f' r. 404 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f' ==> 405 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_SUFFIX_IMP (r, f)) (F_SUFFIX_IMP (r, f'))) /\ 406 407 (!f f' c. 408 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f' ==> 409 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_U_CLOCK c f) (F_U_CLOCK c f')) /\ 410 411 (!f f' c. 412 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f' ==> 413 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_W_CLOCK c f) (F_W_CLOCK c f'))``, 414 415 SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 416 UnclockedSemanticsTheory.UF_SEM_def, F_U_CLOCK_def, F_W_CLOCK_def, 417 F_W_def, F_G_def, F_F_def, F_OR_def] THEN 418 REPEAT STRIP_TAC THENL [ 419 METIS_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT], 420 METIS_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN], 421 METIS_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN], 422 METIS_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN], 423 METIS_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN], 424 425 METIS_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN, IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT] 426 ]); 427 428 429val PSL_EQUIVALENT_rewrites = 430 store_thm ( 431 "PSL_EQUIVALENT_rewrites", 432 433 ``!f. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_NOT (F_NOT f)) f``, 434 435 SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 436 UnclockedSemanticsTheory.UF_SEM_def, 437 RewritesPropertiesTheory.COMPLEMENT_COMPLEMENT]); 438 439 440val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL_BIGCAT___EVAL = 441 prove ( 442``(!f:'a fl b c. 443 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 444 (F_CLOCK_COMP c (F_SUFFIX_IMP (S_BOOL_BIGCAT [b], f))) 445 (F_W_CLOCK c (F_NOT (F_AND (F_NOT (F_NOT (F_STRONG_BOOL b)), F_NOT (F_CLOCK_COMP c f))))) 446 ) /\ 447 (!f:'a fl b1 b2 l c. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 448 (F_CLOCK_COMP c (F_SUFFIX_IMP (S_BOOL_BIGCAT (b1::b2::l), f))) 449 (F_W_CLOCK c (F_NOT (F_AND ( 450 F_NOT (F_NOT (F_STRONG_BOOL b1)), F_NOT (F_NOT 451 (F_U_CLOCK c 452 (F_NEXT 453 (F_U_CLOCK c 454 (F_NOT (F_CLOCK_COMP c (F_SUFFIX_IMP (S_BOOL_BIGCAT (b2::l), f)))))))))))))``, 455 456 ASSUME_TAC UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL_BIGCAT THEN 457 ASSUME_TAC UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL THEN 458 FULL_SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def] THEN 459 FULL_SIMP_TAC std_ss [F_CLOCK_COMP_def, F_WEAK_X_def, F_IMPLIES_def, F_OR_def]); 460 461 462val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL_BIGCAT___EVAL = 463REWRITE_RULE [SyntacticSugarTheory.F_IMPLIES_def, SyntacticSugarTheory.F_OR_def] UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL_BIGCAT; 464 465 466 467val psl_equivalent_preorder = 468 mk_preorder (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TRANS, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___REFL); 469val psl_CS = CSFRAG 470 {rewrs = [PSL_EQUIVALENT_rewrites, 471 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL_BIGCAT___EVAL, 472 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL_BIGCAT___EVAL], 473 relations = [psl_equivalent_preorder], 474 dprocs = [], 475 congs = [PSL_EQUIVALENT_congs]}; 476val psl_cs = mk_congset [psl_CS]; 477 478val F_SUFFIX_IMP___S_BOOL_BIGCAT_def = Define 479 `F_SUFFIX_IMP___S_BOOL_BIGCAT l f = F_SUFFIX_IMP (S_BOOL_BIGCAT l, f)` 480 481 482 483fun prepare_psl psl i0 = 484 let 485 486 val eval_thm = (REWRITE_CONV [GSYM F_SUFFIX_IMP___S_BOOL_BIGCAT_def] THENC RESTR_EVAL_CONV [``F_SUFFIX_IMP___S_BOOL_BIGCAT``] THENC 487 REWRITE_CONV [F_SUFFIX_IMP___S_BOOL_BIGCAT_def]) psl; 488 val eval_term = rhs (concl eval_thm); 489 val equiv_thm = CONGRUENCE_SIMP_CONV ``UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE`` psl_cs std_ss [] eval_term 490 val equiv_thm = (CONV_RULE (RATOR_CONV (ONCE_REWRITE_CONV [GSYM eval_thm]))) equiv_thm 491 val equiv_thm = (CONV_RULE (RAND_CONV EVAL_CONV)) equiv_thm 492 493 val eval_term = rand (concl equiv_thm); 494 495 val cs_free_term = mk_comb (``F_CLOCK_SERE_FREE:num fl -> bool``, eval_term); 496 val cs_free_thm = EQT_ELIM ((REWRITE_CONV [F_CLOCK_SERE_FREE_def, ProjectionTheory.F_CLOCK_FREE_def, F_SERE_FREE_def]) cs_free_term) 497 498 499 val used_vars_term = ``F_USED_VARS psl SUBSET INTERVAL_SET 0 i0``; 500 val used_vars_term = subst [ 501 mk_var ("psl", ``:num fl``) |-> eval_term, 502 mk_var ("i0", num) |-> i0] used_vars_term; 503 val used_vars = EQT_ELIM ((SIMP_CONV std_ss [F_USED_VARS_def, SUBSET_DEF, IN_UNION, 504 IN_SING, XP_USED_VARS_EVAL, IN_INTERVAL_SET, DISJ_IMP_THM, 505 B_USED_VARS_def, NOT_IN_EMPTY]) used_vars_term) 506 507 val psl_to_ltl_term = mk_comb (``PSL_TO_LTL:num fl -> num ltl``, eval_term); 508 val psl_to_ltl = EVAL psl_to_ltl_term 509 in 510 (eval_term, equiv_thm, cs_free_thm, used_vars, psl_to_ltl) 511 end; 512 513 514(* 515val s0_cs = new_compset [P_ASSIGN_TRUE_FALSE___EVAL, IN_SING] 516val prop_logic_equivalent_trans_thm = prove ( 517 ``!p1 p2 p3. 518 PROP_LOGIC_EQUIVALENT p1 p2 ==> 519 PROP_LOGIC_EQUIVALENT p2 p3 ==> 520 PROP_LOGIC_EQUIVALENT p1 p3``, 521 SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def]); 522 523 524fun reduce_S0 S0_thm = 525 let 526 val thm = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [P_EXISTS_def])) S0_thm 527 val changed = not ((concl thm) = (concl S0_thm)); 528 in 529 if changed then 530 let 531 val thm = CONV_RULE (RAND_CONV (CBV_CONV s0_cs)) thm 532 val thm = CONV_RULE (RAND_CONV (DEPTH_CONV (reduceLib.RED_CONV))) thm 533 534 val equiv = CONGRUENCE_SIMP_CONV ``PROP_LOGIC_EQUIVALENT:'a prop_logic -> 'a prop_logic -> bool`` prop_logic_nnf_cs std_ss [] (rand (concl thm)) 535 536 val new_thm = MATCH_MP prop_logic_equivalent_trans_thm thm 537 val new_thm = MATCH_MP new_thm equiv 538 val new_thm = reduce_S0 new_thm 539 in 540 new_thm 541 end 542 else 543 thm 544 end; 545 546 547val r_cs = new_compset [XP_ASSIGN_TRUE_FALSE___EVAL, IN_SING, NOT_IN_EMPTY] 548val xprop_logic_equivalent_trans_thm = prove ( 549 ``!p1 p2 p3. 550 XPROP_LOGIC_EQUIVALENT p1 p2 ==> 551 XPROP_LOGIC_EQUIVALENT p2 p3 ==> 552 XPROP_LOGIC_EQUIVALENT p1 p3``, 553 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def]); 554 555 556fun reduce_R R_thm = 557 let 558 val thm = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [XP_CURRENT_EXISTS_def] THENC ONCE_REWRITE_CONV [XP_NEXT_EXISTS_def])) R_thm 559 val changed = not ((concl thm) = (concl R_thm)); 560 in 561 if changed then 562 let 563 val thm = CONV_RULE (RAND_CONV (CBV_CONV r_cs)) thm 564 val thm = CONV_RULE (RAND_CONV (DEPTH_CONV (reduceLib.RED_CONV))) thm 565 566 val equiv = CONGRUENCE_SIMP_CONV ``XPROP_LOGIC_EQUIVALENT:'a xprop_logic -> 'a xprop_logic -> bool`` xprop_logic_nnf_cs std_ss [] (rand (concl thm)) 567 568 val new_thm = MATCH_MP xprop_logic_equivalent_trans_thm thm 569 val new_thm = MATCH_MP new_thm equiv 570 val new_thm = reduce_R new_thm 571 val _ = print "STEP\n"; 572 in 573 thm 574 end 575 else 576 thm 577 end; 578 579 580 581fun num_compset () = 582 let open computeLib 583 val compset = bool_compset() 584 val _ = add_thms numeral_redns compset 585 val _ = add_conv (numSyntax.div_tm, 2, cbv_DIV_CONV) compset 586 val _ = add_conv (numSyntax.mod_tm, 2, cbv_MOD_CONV) compset 587 in 588 compset 589 end; 590 591val r_cs = reduceLib.num_compset () 592val _ = add_thms [XP_ASSIGN_TRUE_FALSE___EVAL, IN_SING, NOT_IN_EMPTY, XP_CURRENT_EXISTS_def, XP_NEXT_EXISTS_def] r_cs 593 594fun reduce_R thm = 595 let 596 val thm = CONV_RULE (RAND_CONV (CBV_CONV r_cs)) thm 597 in 598 thm 599 end 600 601 602 603val t = mk_thm ([], ``XPROP_LOGIC_EQUIVALENT A B``) 604fun testCONV t = mk_thm ([], mk_eq (t, mk_var ("XXXXXXXXXXXX", type_of t))); 605 606CONV_RULE (RAND_CONV (testCONV)) t 607 608val x = time (reduce_R) R_thm 609 610val t = ``XP_ASSIGN_FALSE {5} {} (XP_PROP 72)`` 611(CBV_CONV r_cs) t 612*) 613 614 615fun ibm_to_ks A p psl = 616 let 617 val thm = PROBLEM_TO_KRIPKE_STRUCTURE___eval; 618 619 val (s0, i0, i0_le_s0, state_vars, semi_automaton_used_vars) = 620 prepare_input_automaton A 621 val (psl', equiv_thm, cs_free_thm, psl_used_vars, psl_to_ltl) = prepare_psl psl i0 622 623 val thm = ISPECL [A, i0, s0, p, psl, psl'] thm; 624 val thm = MP thm i0_le_s0; 625 val thm = MP thm state_vars; 626 val thm = MP thm semi_automaton_used_vars; 627 val thm = MP thm (prepare_ctl p s0); 628 val thm = MP thm equiv_thm 629 val thm = MP thm cs_free_thm 630 val thm = MP thm psl_used_vars 631 632 val thm = SIMP_RULE arith_ss [psl_to_ltl] thm 633 634 val ltl_term = 635 let 636 val t = snd (strip_forall (concl thm)) 637 val t = rand (rator (rand (rator t))) 638 in 639 t 640 end 641 642 val (l', ltl_equiv, ds_thm, ds, pf, b1, b2) = ltl2omega_internal true false true ltl_term 643 val a = if b1 then ``T:bool`` else ``F:bool``; 644 val thm = ISPECL [a, ds, l', pf] thm; 645 val thm = MP thm ltl_equiv; 646 val thm = MP thm ds_thm; 647 648 val imp_term = rand (rator (concl thm)) 649 val imp_thm = EQT_ELIM (REWRITE_CONV [ltl_to_gen_buechi_ds_REWRITES, IN_SING] imp_term) 650 val thm = MP thm imp_thm 651 652 653 val imp_term = rand (rator (concl thm)) 654 val imp_thm = EQT_ELIM (SIMP_CONV arith_ss [ltl_to_gen_buechi_ds_REWRITES, P_USED_VARS___P_BIGOR___EVAL, SUBSET_DEF, 655 IN_INTERVAL_SET, IN_INSERT, NOT_IN_EMPTY, 656 IN_UNION] imp_term) 657 val thm = MP thm imp_thm 658 659 (*evaluate INTERVAL_LISTS*) 660 val i_term = ``INTERVAL_LIST (SUC i0) (SUC s0)`` 661 val i_term = subst [ 662 mk_var ("i0", num) |-> i0, 663 mk_var ("s0", num) |-> s0] i_term; 664 val i_term = rhs (concl (REDUCE_CONV i_term)) 665 val i1_thm = SIMP_CONV std_ss [INTERVAL_LIST_THM] i_term 666 667 val i_term = ``(INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 668 (PRE (2 ** SUC (s0 - i0)) + 669 (SUC (SUC s0) + 2 ** SUC (s0 - i0))))``; 670 val i_term = subst [ 671 mk_var ("i0", num) |-> i0, 672 mk_var ("s0", num) |-> s0] i_term; 673 val i_term = rhs (concl (REDUCE_CONV i_term)) 674 val i2_thm = SIMP_CONV std_ss [INTERVAL_LIST_THM] i_term 675 676 677 val i_term = ``VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 678 (INTERVAL_LIST (SUC i0) (SUC s0)) 679 (SUC (SUC s0)) (SUC i0)``; 680 val i_term = subst [ 681 mk_var ("i0", num) |-> i0, 682 mk_var ("s0", num) |-> s0] i_term; 683 val i_term = rhs (concl ((REDUCE_CONV THENC REWRITE_CONV [i1_thm]) i_term)) 684 val i3_thm = SIMP_CONV std_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def] i_term 685 686 687 val thm = SIMP_RULE list_ss [ltl_to_gen_buechi_ds_REWRITES, 688 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 689 symbolic_semi_automaton_REWRITES, 690 P_BIGOR_def, i1_thm, i2_thm, i3_thm, P_BIGAND_def, XP_BIGAND_def, 691 XP_BIGOR_def, P_VAR_RENAMING_EVAL, XP_NEXT_THM, XP_CURRENT_THM] thm 692 in 693 thm 694 end; 695 696 697fun make_total_thm A = 698 let 699 val t = liteLib.mk_icomb (``IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON:'a symbolic_semi_automaton -> bool``, A); 700 in 701 mk_oracle_thm "TotalityAssumed" ([], t) 702 end; 703 704 705 706val P_USED_VARS___P_FORALL___IMPL = 707 prove (`` 708 !l p P. (!x. x IN P_USED_VARS p ==> P x) ==> 709 (!x. x IN P_USED_VARS (P_FORALL l p) ==> P x)``, 710 SIMP_TAC std_ss [P_FORALL___P_USED_VARS, IN_DIFF]); 711 712fun ibm_to_ks_total A p psl total_thm = 713 let 714 val thm = PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL___eval; 715 716 val (s0, i0, i0_le_s0, state_vars, semi_automaton_used_vars) = 717 prepare_input_automaton A 718 val (psl', equiv_thm, cs_free_thm, psl_used_vars, psl_to_ltl) = prepare_psl psl i0 719 720 val thm = ISPECL [A, i0, s0, p, psl, psl'] thm; 721 val thm = MP thm total_thm; 722 val thm = MP thm i0_le_s0; 723 val thm = MP thm state_vars; 724 val thm = MP thm semi_automaton_used_vars; 725 val thm = MP thm (prepare_ctl p s0); 726 727 val thm = MP thm equiv_thm 728 val thm = MP thm cs_free_thm 729 val thm = MP thm psl_used_vars 730 731 val thm = SIMP_RULE arith_ss [psl_to_ltl] thm 732 733 val ltl_term = 734 let 735 val t = snd (strip_forall (concl thm)) 736 val t = rand (rator (rand (rator t))) 737 in 738 t 739 end 740 741 val (l', ltl_equiv, ds_thm, ds, pf, b1, b2) = ltl2omega_internal true false true ltl_term 742 val a = if b1 then ``T:bool`` else ``F:bool``; 743 val thm = ISPECL [a, ds, l', pf] thm; 744 val thm = MP thm ltl_equiv; 745 val thm = MP thm ds_thm; 746 747 val imp_term = rand (rator (concl thm)) 748 val imp_thm = EQT_ELIM (REWRITE_CONV [ltl_to_gen_buechi_ds_REWRITES, IN_SING] imp_term) 749 val thm = MP thm imp_thm 750 751 752 val imp_term = rand (rator (concl thm)) 753 val imp_thm = SIMP_CONV arith_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, 754 IN_INTERVAL_SET, IN_INSERT, NOT_IN_EMPTY, P_USED_VARS_EVAL, 755 IN_UNION, DISJ_IMP_THM] imp_term 756 val imp2_thm = 757 HO_PART_MATCH (fn t => rand t) P_USED_VARS___P_FORALL___IMPL (rhs (concl imp_thm)) 758 val imp2_thm = SIMP_RULE std_ss [P_USED_VARS_EVAL, 759 IN_UNION, DISJ_IMP_THM, IN_SING] imp2_thm 760 val (i, j) = let 761 val imp2_term = rand (rator (concl (imp2_thm))) 762 val interval_term = rand (rator (rator (rand (rand (rand (rator (snd (strip_forall (imp2_term))))))))); 763 val j = rand (interval_term) 764 val i = rand (rator (interval_term)) 765 in 766 (i, j) 767 end; 768 val P_USED_VARS___VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___EVAL = 769 SIMP_RULE std_ss [] (SPECL [i, j] VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___P_USED_VARS); 770 val imp2_thm = 771 SIMP_RULE std_ss [P_USED_VARS___VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___EVAL, 772 IN_INTERVAL_SET] imp2_thm 773 774 val imp_thm = REWRITE_RULE [imp2_thm] imp_thm 775 val thm = MP thm imp_thm 776 777 778 (*evaluate INTERVAL_LISTS*) 779 val i_term = ``INTERVAL_LIST (SUC i0) s0`` 780 val i_term = subst [ 781 mk_var ("i0", num) |-> i0, 782 mk_var ("s0", num) |-> s0] i_term; 783 val i_term = rhs (concl (REDUCE_CONV i_term)) 784 val i1_thm = SIMP_CONV std_ss [INTERVAL_LIST_THM] i_term 785 786 val i_term = ``VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 787 (INTERVAL_LIST (SUC i0) s0) 788 (SUC s0) (SUC i0)``; 789 val i_term = subst [ 790 mk_var ("i0", num) |-> i0, 791 mk_var ("s0", num) |-> s0] i_term; 792 val i_term = rhs (concl ((REDUCE_CONV THENC REWRITE_CONV [i1_thm]) i_term)) 793 val i2_thm = SIMP_CONV std_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def] i_term 794 795 796 val thm = SIMP_RULE list_ss [ltl_to_gen_buechi_ds_REWRITES, 797 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 798 symbolic_semi_automaton_REWRITES, 799 P_BIGOR_def, i1_thm, i2_thm, P_BIGAND_def, XP_BIGAND_def, 800 XP_BIGOR_def, P_VAR_RENAMING_EVAL, XP_NEXT_THM, XP_CURRENT_THM, 801 XP_CURRENT_NEXT___FORALL, XP_CURRENT_NEXT___EXISTS] thm 802 in 803 thm 804 end; 805 806 807fun ibm_to_ks_total_cheat A p psl = 808 ibm_to_ks_total A p psl (make_total_thm A); 809 810fun ibm_to_ks_clock A p psl = 811 let 812 val psl_nc = liteLib.mk_icomb (``(F_CLOCK_COMP:'a bexp -> 'a fl -> 'a fl) B_TRUE``, psl); 813 val thm = ibm_to_ks A p psl_nc; 814 val thm = REWRITE_RULE [GSYM F_KS_SEM___TO___UF_KS_SEM] thm; 815 in 816 thm 817 end; 818 819 820fun ibm_to_ks_clock_total A p psl total_thm = 821 let 822 val psl_nc = liteLib.mk_icomb (``(F_CLOCK_COMP:'a bexp -> 'a fl -> 'a fl) B_TRUE``, psl); 823 val thm = ibm_to_ks_total A p psl_nc total_thm; 824 val thm = REWRITE_RULE [GSYM F_KS_SEM___TO___UF_KS_SEM] thm; 825 in 826 thm 827 end; 828 829fun ibm_to_ks_clock_total_cheat A p psl = 830 let 831 val psl_nc = liteLib.mk_icomb (``(F_CLOCK_COMP:'a bexp -> 'a fl -> 'a fl) B_TRUE``, psl); 832 val thm = ibm_to_ks_total_cheat A p psl_nc; 833 val thm = REWRITE_RULE [GSYM F_KS_SEM___TO___UF_KS_SEM] thm; 834 in 835 thm 836 end; 837 838 839fun model_check_ibm total A p psl = 840 let 841 val _ = print "Translating problem to kripke structure ...\n"; 842 val thm = if total then ibm_to_ks_total_cheat A p psl else ibm_to_ks A p psl; 843 val ks_term = lhs (concl thm); 844 val _ = print "Running SMV ...\n"; 845 val erg = modelCheckFairEmptyness ks_term thm; 846 val _ = print "Done!\n"; 847 val thm = if erg then (SOME (mk_thm ([], rand (concl thm)))) else NONE 848 in 849 thm 850 end 851 852end 853 854 855