1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: 9 !loadPath; 10 11map load 12 ["symbolic_semi_automatonTheory", "prop_logicTheory", "xprop_logicTheory", "set_lemmataTheory", "pred_setTheory", "listTheory", "pairTheory", 13 "containerTheory", "infinite_pathTheory", "tuerk_tacticsLib", 14 "symbolic_kripke_structureTheory", "temporal_deep_mixedTheory"]; 15*) 16open symbolic_semi_automatonTheory prop_logicTheory xprop_logicTheory set_lemmataTheory pred_setTheory listTheory pairTheory 17 containerTheory infinite_pathTheory symbolic_kripke_structureTheory tuerk_tacticsLib 18 temporal_deep_mixedTheory; 19open Sanity; 20 21val _ = hide "S"; 22val _ = hide "I"; 23 24(* 25show_assums := false; 26show_assums := true; 27show_types := true; 28show_types := false; 29quietdec := false; 30*) 31 32 33val _ = new_theory "automaton_formula"; 34 35 36(***************************************************************************** 37 * Acceptance conditions 38 *****************************************************************************) 39val acceptance_condition = 40 Hol_datatype 41 `acceptance_condition = 42 ACCEPT_PROP of 'a prop_logic 43 | ACCEPT_TRUE 44 | ACCEPT_NOT of acceptance_condition 45 | ACCEPT_AND of acceptance_condition # acceptance_condition 46 | ACCEPT_G of acceptance_condition`; 47 48 49val acceptance_condition_induct = 50 save_thm 51 ("acceptance_condition_induct", 52 Q.GEN 53 `P` 54 (MATCH_MP 55 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 56 (SIMP_RULE 57 std_ss 58 [pairTheory.FORALL_PROD, 59 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 60 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 61 (Q.SPECL 62 [`P`,`\(f1,f2). P f1 /\ P f2`] 63 (TypeBase.induction_of ``:'a acceptance_condition``))))); 64 65 66val ACCEPT_COND_USED_VARS_def= 67 Define 68 `(ACCEPT_COND_USED_VARS (ACCEPT_PROP p) = P_USED_VARS p) /\ 69 (ACCEPT_COND_USED_VARS ACCEPT_TRUE = EMPTY) /\ 70 (ACCEPT_COND_USED_VARS (ACCEPT_NOT a) = ACCEPT_COND_USED_VARS a) /\ 71 (ACCEPT_COND_USED_VARS (ACCEPT_G a) = ACCEPT_COND_USED_VARS a) /\ 72 (ACCEPT_COND_USED_VARS (ACCEPT_AND(a, b)) = (ACCEPT_COND_USED_VARS a) UNION (ACCEPT_COND_USED_VARS b))`; 73 74(***************************************************************************** 75 * Automaton formulas 76 *****************************************************************************) 77val automaton_formula = 78 Hol_datatype 79 `automaton_formula = 80 ACCEPT_COND of 'a acceptance_condition 81 | A_NDET of 'a symbolic_semi_automaton # automaton_formula 82 | A_NOT of automaton_formula 83 | A_AND of automaton_formula # automaton_formula 84 | A_TRUE`; 85 86 87val automaton_formula_induct = 88 save_thm 89 ("automaton_formula_induct", 90 Q.GEN `P0` ( 91 (MATCH_MP 92 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 93 (SIMP_RULE 94 std_ss 95 [pairTheory.FORALL_PROD, 96 PROVE[]``(!x y. P0 x ==> Q(x,y)) = !x. P0 x ==> !y. Q(x,y)``, 97 PROVE[]``(!x y. P0 y ==> Q(x,y)) = !y. P0 y ==> !x. Q(x,y)``] 98 (Q.SPECL 99 [`P0`,`\(A, f). P0 f`,`\(f1,f2). P0 f1 /\ P0 f2`] 100 (TypeBase.induction_of ``:'a automaton_formula``)))))); 101 102 103val A_USED_INPUT_VARS_def= 104 Define 105 `(A_USED_INPUT_VARS (ACCEPT_COND p) = ACCEPT_COND_USED_VARS p) /\ 106 (A_USED_INPUT_VARS A_TRUE = EMPTY) /\ 107 (A_USED_INPUT_VARS (A_NDET(A, f)) = (SEMI_AUTOMATON_USED_INPUT_VARS A UNION 108 (A_USED_INPUT_VARS f DIFF A.S))) /\ 109 (A_USED_INPUT_VARS (A_NOT a) = (A_USED_INPUT_VARS a)) /\ 110 (A_USED_INPUT_VARS (A_AND(a, b)) = (A_USED_INPUT_VARS a) UNION (A_USED_INPUT_VARS b))`; 111 112 113val A_USED_STATE_VARS_def= 114 Define 115 `(A_USED_STATE_VARS (ACCEPT_COND p) = EMPTY) /\ 116 (A_USED_STATE_VARS A_TRUE = EMPTY) /\ 117 (A_USED_STATE_VARS (A_NDET(A, f)) = A.S UNION (A_USED_STATE_VARS f)) /\ 118 (A_USED_STATE_VARS (A_NOT a) = A_USED_STATE_VARS a) /\ 119 (A_USED_STATE_VARS (A_AND(a, b)) = (A_USED_STATE_VARS a) UNION (A_USED_STATE_VARS b))`; 120 121 122val A_USED_VARS_def = 123 Define 124 `A_USED_VARS a = (A_USED_INPUT_VARS a) UNION (A_USED_STATE_VARS a)`; 125 126 127val A_USED_VARS___DIRECT_DEF = 128 store_thm ( 129 "A_USED_VARS___DIRECT_DEF", 130 ``(A_USED_VARS (ACCEPT_COND p) = ACCEPT_COND_USED_VARS p) /\ 131 (A_USED_VARS A_TRUE = EMPTY) /\ 132 (A_USED_VARS (A_NDET(A, f)) = (SEMI_AUTOMATON_USED_VARS A UNION 133 (A_USED_VARS f))) /\ 134 (A_USED_VARS (A_NOT a) = (A_USED_VARS a)) /\ 135 (A_USED_VARS (A_AND(a, b)) = (A_USED_VARS a) UNION (A_USED_VARS b))``, 136 137 SIMP_TAC std_ss [A_USED_VARS_def, A_USED_INPUT_VARS_def, 138 A_USED_STATE_VARS_def, UNION_EMPTY] THEN 139 REPEAT STRIP_TAC THENL [ 140 SIMP_TAC std_ss [EXTENSION, IN_UNION, 141 SEMI_AUTOMATON_USED_VARS_def, IN_DIFF] THEN 142 PROVE_TAC[], 143 144 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 145 PROVE_TAC[] 146 ]); 147 148 149val STATE_VARDISJOINT_AUTOMATON_FORMULA_def= 150 Define 151 `(STATE_VARDISJOINT_AUTOMATON_FORMULA (ACCEPT_COND p) = T) /\ 152 (STATE_VARDISJOINT_AUTOMATON_FORMULA A_TRUE = T) /\ 153 (STATE_VARDISJOINT_AUTOMATON_FORMULA (A_NDET(A, f)) = ((DISJOINT A.S (A_USED_STATE_VARS f)) /\ (STATE_VARDISJOINT_AUTOMATON_FORMULA f))) /\ 154 (STATE_VARDISJOINT_AUTOMATON_FORMULA (A_NOT a) = STATE_VARDISJOINT_AUTOMATON_FORMULA a) /\ 155 (STATE_VARDISJOINT_AUTOMATON_FORMULA (A_AND(a, b)) = (DISJOINT (A_USED_STATE_VARS a) (A_USED_STATE_VARS b)) /\ (STATE_VARDISJOINT_AUTOMATON_FORMULA a) /\ (STATE_VARDISJOINT_AUTOMATON_FORMULA b))`; 156 157 158val VARDISJOINT_AUTOMATON_FORMULA_def= 159 Define 160 `(VARDISJOINT_AUTOMATON_FORMULA f = 161 (STATE_VARDISJOINT_AUTOMATON_FORMULA f) /\ DISJOINT (A_USED_STATE_VARS f) (A_USED_INPUT_VARS f))`; 162 163 164 165(***************************************************************************** 166 * Varibal renamings 167 *****************************************************************************) 168val ACCEPT_VAR_RENAMING_def = 169 Define 170 `(ACCEPT_VAR_RENAMING (f:'a->'b) (ACCEPT_TRUE) = ACCEPT_TRUE) /\ 171 (ACCEPT_VAR_RENAMING f (ACCEPT_PROP p) = (ACCEPT_PROP (P_VAR_RENAMING f p))) /\ 172 (ACCEPT_VAR_RENAMING f (ACCEPT_NOT b) = ACCEPT_NOT (ACCEPT_VAR_RENAMING f b)) /\ 173 (ACCEPT_VAR_RENAMING f (ACCEPT_G b) = ACCEPT_G (ACCEPT_VAR_RENAMING f b)) /\ 174 (ACCEPT_VAR_RENAMING f (ACCEPT_AND(b1,b2)) = (ACCEPT_AND(ACCEPT_VAR_RENAMING f b1, ACCEPT_VAR_RENAMING f b2)))`; 175 176 177val A_VAR_RENAMING_def= 178 Define 179 `((A_VAR_RENAMING (f:'a -> 'b) (ACCEPT_COND p)) = ACCEPT_COND (ACCEPT_VAR_RENAMING f p)) /\ 180 ((A_VAR_RENAMING f A_TRUE) = A_TRUE) /\ 181 ((A_VAR_RENAMING f (A_NDET(A:'a symbolic_semi_automaton, f'))) = A_NDET( 182 SEMI_AUTOMATON_VAR_RENAMING f A, A_VAR_RENAMING f f')) /\ 183 ((A_VAR_RENAMING f (A_NOT a)) = A_NOT(A_VAR_RENAMING f a)) /\ 184 (A_VAR_RENAMING f (A_AND(a, b)) = (A_AND (A_VAR_RENAMING f a, A_VAR_RENAMING f b)))`; 185 186 187 188(*============================================================================= 189= Semantic 190=============================================================================*) 191 192 193(***************************************************************************** 194 * Acceptance conditions 195 *****************************************************************************) 196val ACCEPT_COND_SEM_TIME_def= 197 Define 198 `(ACCEPT_COND_SEM_TIME t v (ACCEPT_PROP p) = P_SEM (v t) p) /\ 199 (ACCEPT_COND_SEM_TIME t v ACCEPT_TRUE = T) /\ 200 (ACCEPT_COND_SEM_TIME t v (ACCEPT_NOT a) = ~(ACCEPT_COND_SEM_TIME t v a)) /\ 201 (ACCEPT_COND_SEM_TIME t v (ACCEPT_G a) = (!t':num. (t' >= t) ==> (ACCEPT_COND_SEM_TIME t' v a))) /\ 202 (ACCEPT_COND_SEM_TIME t v (ACCEPT_AND(a, b)) = ((ACCEPT_COND_SEM_TIME t v a) /\ ACCEPT_COND_SEM_TIME t v b))`; 203 204 205val ACCEPT_COND_SEM_def= 206 Define 207 `(ACCEPT_COND_SEM v f = ACCEPT_COND_SEM_TIME 0 v f)`; 208 209 210(***************************************************************************** 211 * Automaton formulas 212 *****************************************************************************) 213val A_SEM_def= 214 Define 215 `((A_SEM i (ACCEPT_COND p)) = (ACCEPT_COND_SEM i p)) /\ 216 ((A_SEM i (A_TRUE)) = T) /\ 217 ((A_SEM i (A_NDET(A, f))) = (?w. (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w) /\ (A_SEM (INPUT_RUN_PATH_UNION A i w) f))) /\ 218 ((A_SEM i (A_NOT a)) = ~(A_SEM i a)) /\ 219 ((A_SEM i (A_AND(a, b))) = ((A_SEM i a) /\ A_SEM i b))`; 220 221 222val A_KS_SEM_def = 223 Define 224 `A_KS_SEM M A = 225 !i. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M i ==> A_SEM i A`; 226 227 228 229 230(*============================================================================= 231= Syntactic Sugar and elementary lemmata 232=============================================================================*) 233 234(***************************************************************************** 235 * Acceptance conditions 236*****************************************************************************) 237val ACCEPT_F_def = 238 Define 239 `ACCEPT_F b = ACCEPT_NOT(ACCEPT_G (ACCEPT_NOT b))`; 240 241 242val ACCEPT_FALSE_def = 243 Define 244 `ACCEPT_FALSE = ACCEPT_NOT(ACCEPT_TRUE)`; 245 246 247val ACCEPT_OR_def = 248 Define 249 `ACCEPT_OR(b1, b2) = ACCEPT_NOT(ACCEPT_AND(ACCEPT_NOT b1, ACCEPT_NOT b2))`; 250 251 252val ACCEPT_IMPL_def = 253 Define 254 `ACCEPT_IMPL(b1, b2) = ACCEPT_OR(ACCEPT_NOT b1, b2)`; 255 256 257val ACCEPT_EQUIV_def = 258 Define 259 `ACCEPT_EQUIV(b1, b2) = ACCEPT_AND(ACCEPT_IMPL(b1, b2),ACCEPT_IMPL(b2, b1))`; 260 261val ACCEPT_BIGAND_def = 262 Define 263 `(ACCEPT_BIGAND [] = ACCEPT_TRUE) /\ 264 (ACCEPT_BIGAND (e::C) = ACCEPT_AND(e, ACCEPT_BIGAND C))`; 265 266 267 268(***************************************************************************** 269 * Automaton formulas 270 *****************************************************************************) 271val A_BIGAND_def = 272 Define 273 `(A_BIGAND ([]:'a automaton_formula list) = (A_TRUE:'a automaton_formula)) /\ 274 (A_BIGAND (e::C) = A_AND(e, A_BIGAND C))`; 275 276 277val A_UNIV_def = 278 Define 279 `A_UNIV(A, f) = A_NOT(A_NDET(A, A_NOT f))`; 280 281 282val A_FALSE_def = 283 Define 284 `A_FALSE = A_NOT(A_TRUE)`; 285 286 287val A_OR_def = 288 Define 289 `A_OR(b1, b2) = A_NOT(A_AND(A_NOT b1, A_NOT b2))`; 290 291 292val A_IMPL_def = 293 Define 294 `A_IMPL(b1, b2) = A_OR(A_NOT b1, b2)`; 295 296 297val A_EQUIV_def = 298 Define 299 `A_EQUIV(b1, b2) = A_AND(A_IMPL(b1, b2),A_IMPL(b2, b1))`; 300 301 302val A_NDET_CONSTRAINED_def = 303 Define 304 `A_NDET_CONSTRAINED(A, C, f) = A_NDET(A, A_AND(f, A_BIGAND C))`; 305 306 307val A_UNIV_CONSTRAINED_def = 308 Define 309 `A_UNIV_CONSTRAINED(A, C, f) = A_UNIV(A, A_IMPL(A_BIGAND C, f))`; 310 311 312val A_SEM_THM = 313 store_thm 314 ("A_SEM_THM", 315 ``!A f v p a b. (((A_SEM v (ACCEPT_COND p)) = (ACCEPT_COND_SEM v p)) /\ 316 ((A_SEM v (A_UNIV(A, f))) = (!w. (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A v w) ==> (A_SEM (INPUT_RUN_PATH_UNION A v w) f))) /\ 317 ((A_SEM v (A_NDET(A, f))) = (?w. (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A v w) /\ (A_SEM (INPUT_RUN_PATH_UNION A v w) f))) /\ 318 (A_SEM v (A_TRUE)) /\ ~(A_SEM v (A_FALSE)) /\ 319 ((A_SEM v (A_NOT a)) = ~(A_SEM v a)) /\ 320 ((A_SEM v (A_AND(a, b))) = ((A_SEM v a) /\ A_SEM v b)) /\ 321 ((A_SEM v (A_OR(a, b))) = ((A_SEM v a) \/ A_SEM v b)) /\ 322 ((A_SEM v (A_IMPL(a, b))) = ((A_SEM v a) ==> A_SEM v b)) /\ 323 ((A_SEM v (A_EQUIV(a, b))) = ((A_SEM v a) = A_SEM v b)))``, 324 325 SIMP_TAC arith_ss [A_UNIV_def, A_FALSE_def, A_OR_def, A_IMPL_def, A_EQUIV_def, A_SEM_def] THEN 326 REPEAT STRIP_TAC THEN PROVE_TAC[] 327); 328 329 330val A_USED_STATE_VARS_COMPATIBLE_def = 331 Define 332 `A_USED_STATE_VARS_COMPATIBLE a1 a2 = 333 DISJOINT (A_USED_INPUT_VARS a1) (A_USED_STATE_VARS a2) /\ 334 DISJOINT (A_USED_INPUT_VARS a2) (A_USED_STATE_VARS a1) /\ 335 DISJOINT (A_USED_STATE_VARS a1) (A_USED_STATE_VARS a2)`; 336 337 338val VARDISJOINT_AUTOMATON_FORMULA___A_USED_STATE_VARS_COMPATIBLE = 339 store_thm 340 ("VARDISJOINT_AUTOMATON_FORMULA___A_USED_STATE_VARS_COMPATIBLE", 341 342 ``(VARDISJOINT_AUTOMATON_FORMULA (A_AND(a1, a2))) ==> 343 A_USED_STATE_VARS_COMPATIBLE a1 a2``, 344 345 REWRITE_TAC[VARDISJOINT_AUTOMATON_FORMULA_def, 346 A_USED_STATE_VARS_COMPATIBLE_def, 347 A_USED_STATE_VARS_def, 348 A_USED_INPUT_VARS_def, 349 STATE_VARDISJOINT_AUTOMATON_FORMULA_def, 350 DISJOINT_UNION_BOTH] THEN 351 PROVE_TAC[]); 352 353 354val AUTOMATON_EQUIV_def = 355 Define 356 `AUTOMATON_EQUIV a1 a2 = !v. (A_SEM v a1) = (A_SEM v a2)`; 357 358 359val AUTOMATON_EQUIV_THM = 360 store_thm 361 ("AUTOMATON_EQUIV_THM", 362 ``(!A f. AUTOMATON_EQUIV (A_NDET(A, f)) (A_NOT (A_UNIV(A, A_NOT f)))) /\ 363 (!A f. AUTOMATON_EQUIV (A_UNIV(A, f)) (A_NOT (A_NDET(A, A_NOT f)))) /\ 364 (!a1 a2. (AUTOMATON_EQUIV (A_NOT a1) (A_NOT a2)) = AUTOMATON_EQUIV a1 a2) /\ 365 (!a1 a2. (AUTOMATON_EQUIV (A_AND (a1,a2)) (A_AND (a2,a1)))) /\ 366 (!a1 a2 b. (AUTOMATON_EQUIV a1 a2) ==> (AUTOMATON_EQUIV (A_AND (a1,b)) (A_AND (a2,b)))) /\ 367 (!a1 a2. (!v. (A_SEM v (A_EQUIV(a1, a2)))) = (AUTOMATON_EQUIV a1 a2)) /\ 368 (!a1 a2. (AUTOMATON_EQUIV (A_OR (a1,a2)) (A_OR (a2,a1)))) /\ 369 (!a1 a2 b. (AUTOMATON_EQUIV a1 a2) ==> (AUTOMATON_EQUIV (A_OR (a1,b)) (A_OR (a2,b)))) /\ 370 (!a1 a2 b. (AUTOMATON_EQUIV a1 a2) ==> (AUTOMATON_EQUIV (A_IMPL (a1,b)) (A_IMPL (a2,b)))) /\ 371 (!a1 a2 b. (AUTOMATON_EQUIV a1 a2) ==> (AUTOMATON_EQUIV (A_IMPL (b,a1)) (A_IMPL (b,a2)))) /\ 372 (!A a1 a2. (AUTOMATON_EQUIV a1 a2) ==> AUTOMATON_EQUIV (A_NDET(A, a1)) (A_NDET(A, a2))) /\ 373 (!A a1 a2. (AUTOMATON_EQUIV a1 a2) ==> AUTOMATON_EQUIV (A_UNIV(A, a1)) (A_UNIV(A, a2))) /\ 374 (!a1 a2. (AUTOMATON_EQUIV a1 a2) = (AUTOMATON_EQUIV a2 a1)) /\ 375 (!a1. (AUTOMATON_EQUIV a1 a1)) /\ 376 (!a1 a2 a3. ((AUTOMATON_EQUIV a1 a2) /\ (AUTOMATON_EQUIV a2 a3)) ==> (AUTOMATON_EQUIV a1 a3))``, 377 378 REWRITE_TAC[AUTOMATON_EQUIV_def, A_SEM_THM] THEN 379 REPEAT STRIP_TAC THEN 380 PROVE_TAC []); 381 382 383val A_BIGAND___A_USED_INPUT_VARS = 384 store_thm 385 ("A_BIGAND___A_USED_INPUT_VARS", 386 ``!C1 C2. A_USED_INPUT_VARS (A_BIGAND (APPEND C1 C2)) = A_USED_INPUT_VARS (A_AND (A_BIGAND C1, 387 A_BIGAND C2))``, 388 389 REWRITE_TAC[A_USED_INPUT_VARS_def] THEN 390 Induct_on `C1` THENL [ 391 SIMP_TAC arith_ss [A_BIGAND_def, APPEND, A_USED_INPUT_VARS_def, UNION_EMPTY], 392 393 SIMP_TAC arith_ss [A_BIGAND_def, APPEND, A_USED_INPUT_VARS_def, UNION_EMPTY] THEN 394 PROVE_TAC [UNION_ASSOC] 395 ]); 396 397 398val A_BIGAND___A_USED_STATE_VARS = 399 store_thm 400 ("A_BIGAND___A_USED_STATE_VARS", 401 ``!C1 C2. A_USED_STATE_VARS (A_BIGAND (APPEND C1 C2)) = A_USED_STATE_VARS (A_AND (A_BIGAND C1, 402 A_BIGAND C2))``, 403 404 REWRITE_TAC[A_USED_STATE_VARS_def] THEN 405 Induct_on `C1` THENL [ 406 SIMP_TAC arith_ss [A_BIGAND_def, APPEND, A_USED_STATE_VARS_def, UNION_EMPTY], 407 408 SIMP_TAC arith_ss [A_BIGAND_def, APPEND, A_USED_STATE_VARS_def, UNION_EMPTY] THEN 409 PROVE_TAC [UNION_ASSOC] 410 ]); 411 412 413val A_BIGAND___A_SEM = 414 store_thm 415 ("A_BIGAND___A_SEM", 416 ``!C1 C2 v. A_SEM v (A_BIGAND (APPEND C1 C2)) = ((A_SEM v (A_BIGAND C1)) /\ (A_SEM v (A_BIGAND C2)))``, 417 418 Induct_on `C1` THENL [ 419 SIMP_TAC arith_ss [A_BIGAND_def, APPEND, A_SEM_def], 420 421 SIMP_TAC arith_ss [A_BIGAND_def, APPEND, A_SEM_def, UNION_EMPTY] THEN 422 PROVE_TAC [] 423 ]); 424 425 426val A_BIGAND_SEM = 427 store_thm 428 ("A_BIGAND_SEM", 429 ``!w C. A_SEM w (A_BIGAND C) = !e. MEM e C ==> A_SEM w e``, 430 431Induct_on `C` THENL [ 432 SIMP_TAC list_ss [A_BIGAND_def, A_SEM_def], 433 434 ASM_SIMP_TAC list_ss [A_BIGAND_def, A_SEM_def] THEN 435 PROVE_TAC[] 436]) 437 438 439val ACCEPT_BIGAND_SEM = 440 store_thm 441 ("ACCEPT_BIGAND_SEM", 442 ``!t w C. ACCEPT_COND_SEM_TIME t w (ACCEPT_BIGAND C) = !e. MEM e C ==> ACCEPT_COND_SEM_TIME t w e``, 443 444Induct_on `C` THENL [ 445 SIMP_TAC list_ss [ACCEPT_BIGAND_def, ACCEPT_COND_SEM_TIME_def], 446 447 ASM_SIMP_TAC list_ss [ACCEPT_BIGAND_def, ACCEPT_COND_SEM_TIME_def] THEN 448 METIS_TAC[] 449]) 450 451 452val ACCEPT_BIGAND___VAR_RENAMING = 453 store_thm 454 ("ACCEPT_BIGAND___VAR_RENAMING", 455 456 ``!f C. 457 ACCEPT_VAR_RENAMING f (ACCEPT_BIGAND C) = 458 (ACCEPT_BIGAND (MAP (ACCEPT_VAR_RENAMING f) C))``, 459 460 Induct_on `C` THENL [ 461 SIMP_TAC list_ss [ACCEPT_BIGAND_def, ACCEPT_VAR_RENAMING_def], 462 ASM_SIMP_TAC list_ss [ACCEPT_BIGAND_def, ACCEPT_VAR_RENAMING_def] 463 ]); 464 465 466val A_BIGAND___AUTOMATON_EQUIV = 467 store_thm 468 ("A_BIGAND___AUTOMATON_EQUIV", 469 ``!C1 C2. AUTOMATON_EQUIV (A_BIGAND (APPEND C1 C2)) (A_AND(A_BIGAND C1, A_BIGAND C2))``, 470 471 REWRITE_TAC[AUTOMATON_EQUIV_def, A_SEM_def, A_BIGAND___A_SEM]); 472 473 474val A_BIGAND___STATE_VARDISJOINT_AUTOMATON_FORMULA = 475 store_thm 476 ("A_BIGAND___STATE_VARDISJOINT_AUTOMATON_FORMULA", 477 ``!C1 C2. STATE_VARDISJOINT_AUTOMATON_FORMULA (A_BIGAND (APPEND C1 C2)) = STATE_VARDISJOINT_AUTOMATON_FORMULA (A_AND (A_BIGAND C1, A_BIGAND C2))``, 478 479 REWRITE_TAC[STATE_VARDISJOINT_AUTOMATON_FORMULA_def] THEN 480 Induct_on `C1` THENL [ 481 SIMP_TAC arith_ss [A_BIGAND_def, 482 APPEND, 483 DISJOINT_EMPTY, 484 STATE_VARDISJOINT_AUTOMATON_FORMULA_def, 485 A_USED_STATE_VARS_def], 486 487 SIMP_TAC arith_ss [A_BIGAND_def, 488 APPEND, 489 DISJOINT_EMPTY, 490 STATE_VARDISJOINT_AUTOMATON_FORMULA_def, 491 A_USED_STATE_VARS_def, 492 DISJOINT_UNION_BOTH, 493 A_BIGAND___A_USED_STATE_VARS] THEN 494 REPEAT STRIP_TAC THEN 495 EQ_TAC THEN REPEAT STRIP_TAC THEN 496 PROVE_TAC [DISJOINT_SYM] 497 ]); 498 499 500val A_BIGAND___VARDISJOINT_AUTOMATON_FORMULA = 501 store_thm 502 ("A_BIGAND___VARDISJOINT_AUTOMATON_FORMULA", 503 ``!C1 C2. VARDISJOINT_AUTOMATON_FORMULA (A_BIGAND (APPEND C1 C2)) = VARDISJOINT_AUTOMATON_FORMULA (A_AND (A_BIGAND C1, A_BIGAND C2))``, 504 505 REWRITE_TAC[VARDISJOINT_AUTOMATON_FORMULA_def, 506 A_BIGAND___A_USED_STATE_VARS, 507 A_BIGAND___A_USED_INPUT_VARS, 508 A_BIGAND___STATE_VARDISJOINT_AUTOMATON_FORMULA]); 509 510 511val A_BIGAND_EMPTY = 512 store_thm 513 ("A_BIGAND_EMPTY", 514 515 ``!C. (A_BIGAND C = A_TRUE) = (C = [])``, 516 517 Cases_on `C` THEN EVAL_TAC); 518 519 520val A_BIGAND_11 = 521 store_thm 522 ("A_BIGAND_11", 523 524 ``!C D. (A_BIGAND C = A_BIGAND D) = (C = D)``, 525 526 Induct_on `C` THEN 527 Cases_on `D` THEN 528 EVAL_TAC THEN PROVE_TAC[]); 529 530 531val EXISTS_RUN_WITH_PROPERTIES_def = 532 Define 533 `EXISTS_RUN_WITH_PROPERTIES A C = (!i. ?w. (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w) /\ (A_SEM (INPUT_RUN_PATH_UNION A i w) (A_BIGAND C)))`; 534 535 536val UNIQUE_RUN_WITH_PROPERTIES_def = 537 Define 538 `UNIQUE_RUN_WITH_PROPERTIES A C = (!i. ?!w. (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w) /\ (A_SEM (INPUT_RUN_PATH_UNION A i w) (A_BIGAND C)))`; 539 540 541val UNIQUE_RUN_WITH_PROPERTIES___IMPLIES_EXISTENCE = 542 store_thm ( 543 "UNIQUE_RUN_WITH_PROPERTIES___IMPLIES_EXISTENCE", 544 ``!A C. UNIQUE_RUN_WITH_PROPERTIES A C ==> EXISTS_RUN_WITH_PROPERTIES A C``, 545 546 REWRITE_TAC[UNIQUE_RUN_WITH_PROPERTIES_def, EXISTS_RUN_WITH_PROPERTIES_def] THEN METIS_TAC[]); 547 548 549val A_NDET_CONSTRAINED_11 = 550 store_thm 551 ("A_NDET_CONSTRAINED_11", 552 553 ``!A B C D p q. 554 ((A_NDET_CONSTRAINED(A, C, p)) = 555 (A_NDET_CONSTRAINED(B, D, q))) = 556 ((A = B) /\ (C = D) /\ (p = q))``, 557 558 EVAL_TAC THEN 559 Induct_on `C` THEN 560 Cases_on `D` THEN 561 EVAL_TAC THEN PROVE_TAC[]); 562 563 564(*Automaton Classes*) 565val ACCEPT_COND_PROP_def = 566 Define 567 `ACCEPT_COND_PROP b = ACCEPT_COND (ACCEPT_PROP b)`; 568 569 570val ACCEPT_COND_PROP_11 = 571 store_thm 572 ("ACCEPT_COND_PROP_11", 573 574 ``!p1 p2. (ACCEPT_COND_PROP p1 = ACCEPT_COND_PROP p2) = (p1 = p2)``, 575 576 EVAL_TAC THEN PROVE_TAC[]); 577 578 579val ACCEPT_COND_GF_def = 580 Define 581 `ACCEPT_COND_GF b = ACCEPT_COND (ACCEPT_G(ACCEPT_F (ACCEPT_PROP b)))`; 582 583 584val ACCEPT_COND_FG_def = 585 Define 586 `ACCEPT_COND_FG b = ACCEPT_COND (ACCEPT_F(ACCEPT_G (ACCEPT_PROP b)))`; 587 588 589val ACCEPT_COND_F_def = 590 Define 591 `ACCEPT_COND_F b = ACCEPT_COND (ACCEPT_F (ACCEPT_PROP b))`; 592 593 594val ACCEPT_COND_G_def = 595 Define 596 `ACCEPT_COND_G b = ACCEPT_COND (ACCEPT_G (ACCEPT_PROP b))`; 597 598 599val IS_EX_AUTOMATON_def = 600 Define 601 `IS_EX_AUTOMATON af = 602 ?A f. af = A_NDET(A, f)`; 603 604 605val IS_ALL_AUTOMATON_def = 606 Define 607 `IS_ALL_AUTOMATON af = 608 ?A f. af = A_UNIV(A, f)`; 609 610 611val IS_AUTOMATON_def = 612 Define 613 `IS_AUTOMATON af = (IS_EX_AUTOMATON af \/ IS_ALL_AUTOMATON af)`; 614 615 616val IS_DET_EX_AUTOMATON_def = 617 Define 618 `IS_DET_EX_AUTOMATON af = ?A f. ((af = A_NDET(A, f)) /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A)`; 619 620 621val IS_DET_ALL_AUTOMATON_def = 622 Define 623 `IS_DET_ALL_AUTOMATON af = ?A f. ((af = A_UNIV(A, f)) /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A)`; 624 625 626val IS_DET_AUTOMATON_def = 627 Define 628 `IS_DET_AUTOMATON af = (IS_DET_EX_AUTOMATON af \/ IS_DET_ALL_AUTOMATON af)`; 629 630 631val IS_NDET_GF_AUTOMATON_def = 632 Define 633 `IS_NDET_GF_AUTOMATON af = ?A b. ((af = A_NDET(A, ACCEPT_COND_GF b)))`; 634 635 636val IS_NDET_FG_AUTOMATON_def = 637 Define 638 `IS_NDET_FG_AUTOMATON af = ?A b. ((af = A_NDET(A, ACCEPT_COND_FG b)))`; 639 640 641val IS_NDET_F_AUTOMATON_def = 642 Define 643 `IS_NDET_F_AUTOMATON af = ?A b. ((af = A_NDET(A, ACCEPT_COND_F b)))`; 644 645 646val IS_NDET_G_AUTOMATON_def = 647 Define 648 `IS_NDET_G_AUTOMATON af = ?A b. ((af = A_NDET(A, ACCEPT_COND_G b)))`; 649 650 651val IS_DET_EX_GF_AUTOMATON_def= 652 Define 653 `IS_DET_EX_GF_AUTOMATON af = (?A b. (af = A_NDET (A,ACCEPT_COND_GF b)) /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A)`; 654 655 656val IS_DET_EX_FG_AUTOMATON_def= 657 Define 658 `IS_DET_EX_FG_AUTOMATON af = (?A b. (af = A_NDET (A,ACCEPT_COND_FG b)) /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A)`; 659 660 661val IS_DET_EX_G_AUTOMATON_def= 662 Define 663 `IS_DET_EX_G_AUTOMATON af = (?A b. (af = A_NDET (A,ACCEPT_COND_G b)) /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A)`; 664 665 666val IS_DET_EX_F_AUTOMATON_def= 667 Define 668 `IS_DET_EX_F_AUTOMATON af = (?A b. (af = A_NDET (A,ACCEPT_COND_F b)) /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A)`; 669 670 671val IS_UNIV_GF_AUTOMATON_def = 672 Define 673 `IS_UNIV_GF_AUTOMATON af = ?A b. ((af = A_UNIV(A, ACCEPT_COND_GF b)))`; 674 675 676val IS_UNIV_FG_AUTOMATON_def = 677 Define 678 `IS_UNIV_FG_AUTOMATON af = ?A b. ((af = A_UNIV(A, ACCEPT_COND_FG b)))`; 679 680 681val IS_UNIV_F_AUTOMATON_def = 682 Define 683 `IS_UNIV_F_AUTOMATON af = ?A b. ((af = A_UNIV(A, ACCEPT_COND_F b)))`; 684 685 686val IS_UNIV_G_AUTOMATON_def = 687 Define 688 `IS_UNIV_G_AUTOMATON af = ?A b. ((af = A_UNIV(A, ACCEPT_COND_G b)))`; 689 690 691val A_NDET_GEN_GF_def = 692 Define 693 `A_NDET_GEN_GF(A, C) = A_NDET(A, A_BIGAND (MAP (\p. ACCEPT_COND_GF p) C))`; 694 695 696 697 698 699val A_IS_EMPTY_def = 700 Define 701 `A_IS_EMPTY A = ~(?i. A_SEM i A)`; 702 703val A_IS_CONTRADICTION_def = 704 Define 705 `A_IS_CONTRADICTION A = A_IS_EMPTY A`; 706 707val A_IS_TAUTOLOGY_def = 708 Define 709 `A_IS_TAUTOLOGY A = (!i. A_SEM i A)`; 710 711 712val A_TAUTOLOGY_CONTRADICTION_DUAL = 713 store_thm 714 ("A_TAUTOLOGY_CONTRADICTION_DUAL", 715 716 ``(!A. A_IS_CONTRADICTION (A_NOT A) = A_IS_TAUTOLOGY A) /\ 717 (!A. A_IS_TAUTOLOGY (A_NOT A) = A_IS_CONTRADICTION A)``, 718 719 SIMP_TAC std_ss [A_IS_TAUTOLOGY_def, A_IS_CONTRADICTION_def, A_SEM_def, 720 A_IS_EMPTY_def]); 721 722 723val A_TAUTOLOGY_CONTRADICTION___TO___EQUIVALENT = 724 store_thm 725 ("A_TAUTOLOGY_CONTRADICTION___TO___EQUIVALENT", 726 727 ``(!A. A_IS_CONTRADICTION A = AUTOMATON_EQUIV A A_FALSE) /\ 728 (!A. A_IS_TAUTOLOGY A = AUTOMATON_EQUIV A A_TRUE)``, 729 730 SIMP_TAC std_ss [A_IS_TAUTOLOGY_def, A_IS_CONTRADICTION_def, A_IS_EMPTY_def, AUTOMATON_EQUIV_def, A_SEM_THM]); 731 732 733 734(***************************************************************************** 735 * Variable renamings 736 *****************************************************************************) 737 738 739val FINITE___ACCEPT_COND_USED_VARS = 740 store_thm 741 ("FINITE___ACCEPT_COND_USED_VARS", 742 743 ``!a. FINITE(ACCEPT_COND_USED_VARS a)``, 744 745 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THENL [ 746 REWRITE_TAC[ACCEPT_COND_USED_VARS_def, FINITE___P_USED_VARS], 747 REWRITE_TAC[ACCEPT_COND_USED_VARS_def, FINITE_EMPTY], 748 ASM_REWRITE_TAC[ACCEPT_COND_USED_VARS_def], 749 ASM_REWRITE_TAC[ACCEPT_COND_USED_VARS_def, FINITE_UNION], 750 ASM_REWRITE_TAC[ACCEPT_COND_USED_VARS_def] 751 ]); 752 753val ACCEPT_VAR_RENAMING___USED_VARS = 754 store_thm 755 ("ACCEPT_VAR_RENAMING___USED_VARS", 756 757 ``!a f. (ACCEPT_COND_USED_VARS (ACCEPT_VAR_RENAMING f a) = 758 (IMAGE f (ACCEPT_COND_USED_VARS a)))``, 759 760 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THENL [ 761 REWRITE_TAC [ACCEPT_COND_USED_VARS_def, ACCEPT_VAR_RENAMING_def, P_VAR_RENAMING___USED_VARS], 762 REWRITE_TAC [ACCEPT_COND_USED_VARS_def, ACCEPT_VAR_RENAMING_def, IMAGE_EMPTY], 763 ASM_REWRITE_TAC [ACCEPT_COND_USED_VARS_def, ACCEPT_VAR_RENAMING_def], 764 ASM_REWRITE_TAC [ACCEPT_COND_USED_VARS_def, ACCEPT_VAR_RENAMING_def, IMAGE_UNION], 765 ASM_REWRITE_TAC[ACCEPT_COND_USED_VARS_def, ACCEPT_VAR_RENAMING_def] 766 ]); 767 768 769 770val FINITE___A_USED_INPUT_VARS = 771 store_thm 772 ("FINITE___A_USED_INPUT_VARS", 773 774 ``!a. FINITE(A_USED_INPUT_VARS a)``, 775 776 INDUCT_THEN automaton_formula_induct ASSUME_TAC THENL [ 777 REWRITE_TAC[A_USED_INPUT_VARS_def, FINITE___ACCEPT_COND_USED_VARS], 778 779 REWRITE_TAC[A_USED_INPUT_VARS_def, FINITE_UNION, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS] THEN 780 METIS_TAC[FINITE_DIFF], 781 782 ASM_REWRITE_TAC[A_USED_INPUT_VARS_def], 783 ASM_REWRITE_TAC[A_USED_INPUT_VARS_def, FINITE_UNION], 784 ASM_REWRITE_TAC[A_USED_INPUT_VARS_def, FINITE_EMPTY] 785 ]); 786 787 788val A_VAR_RENAMING___USED_STATE_VARS = 789 store_thm 790 ("A_VAR_RENAMING___USED_STATE_VARS", 791 792 ``!a f. 793 (A_USED_STATE_VARS (A_VAR_RENAMING f a) = 794 (IMAGE f (A_USED_STATE_VARS a)))``, 795 796 797 INDUCT_THEN automaton_formula_induct ASSUME_TAC THENL [ 798 799 REWRITE_TAC [A_USED_STATE_VARS_def, A_VAR_RENAMING_def, IMAGE_EMPTY], 800 801 Cases_on `p_1` THEN 802 ASM_REWRITE_TAC [A_USED_STATE_VARS_def, 803 A_VAR_RENAMING_def, 804 SEMI_AUTOMATON_VAR_RENAMING_def, 805 symbolic_semi_automaton_REWRITES, 806 IMAGE_UNION], 807 808 ASM_REWRITE_TAC [A_USED_STATE_VARS_def, A_VAR_RENAMING_def], 809 ASM_REWRITE_TAC [A_USED_STATE_VARS_def, A_VAR_RENAMING_def, IMAGE_UNION], 810 REWRITE_TAC [A_USED_STATE_VARS_def, A_VAR_RENAMING_def, IMAGE_EMPTY] 811 ]); 812 813 814val A_VAR_RENAMING___USED_INPUT_VARS = 815 store_thm 816 ("A_VAR_RENAMING___USED_INPUT_VARS", 817 818 ``!a f. (INJ f (A_USED_VARS a) UNIV) ==> 819 820 (A_USED_INPUT_VARS (A_VAR_RENAMING f a) = 821 (IMAGE f (A_USED_INPUT_VARS a)))``, 822 823 INDUCT_THEN automaton_formula_induct ASSUME_TAC THENL [ 824 825 REWRITE_TAC [A_USED_INPUT_VARS_def, A_VAR_RENAMING_def, ACCEPT_VAR_RENAMING___USED_VARS], 826 827 828 Cases_on `p_1` THEN 829 ASM_SIMP_TAC std_ss [A_USED_VARS_def, 830 A_USED_INPUT_VARS_def, 831 A_USED_STATE_VARS_def, 832 A_VAR_RENAMING_def, 833 SEMI_AUTOMATON_USED_INPUT_VARS_def, 834 SEMI_AUTOMATON_VAR_RENAMING_def, 835 SEMI_AUTOMATON_USED_VARS_def, 836 DIFF_UNION, 837 symbolic_semi_automaton_REWRITES, 838 P_VAR_RENAMING___USED_VARS, XP_VAR_RENAMING___USED_VARS, 839 IMAGE_UNION] THEN 840 REPEAT STRIP_TAC THEN 841 Q.ABBREV_TAC `INJ_SET = (P_USED_VARS p UNION XP_USED_VARS x DIFF f UNION 842 (A_USED_INPUT_VARS a DIFF f) UNION 843 (f UNION A_USED_STATE_VARS a))` THEN 844 845 `((P_USED_VARS p UNION XP_USED_VARS x UNION f) SUBSET INJ_SET) /\ 846 ((XP_USED_VARS x UNION f) SUBSET INJ_SET) /\ 847 ((A_USED_INPUT_VARS a UNION f) SUBSET INJ_SET) /\ 848 ((A_USED_VARS a SUBSET INJ_SET))` by ( 849 Q.UNABBREV_TAC `INJ_SET` THEN 850 ASM_SIMP_TAC std_ss [UNION_DEF, SUBSET_DEF, GSPECIFICATION, DIFF_DEF, A_USED_VARS_def] THEN 851 METIS_TAC[]) THEN 852 853 METIS_TAC[INJ_SUBSET_DOMAIN, IMAGE_DIFF, IMAGE_UNION], 854 855 FULL_SIMP_TAC std_ss [A_USED_VARS_def, A_USED_STATE_VARS_def, A_USED_INPUT_VARS_def, A_VAR_RENAMING_def], 856 857 FULL_SIMP_TAC std_ss [A_USED_VARS_def, A_USED_STATE_VARS_def, A_USED_INPUT_VARS_def, A_VAR_RENAMING_def, IMAGE_UNION] THEN 858 REPEAT STRIP_TAC THEN 859 `(A_USED_INPUT_VARS a UNION A_USED_STATE_VARS a) SUBSET 860 (A_USED_INPUT_VARS a UNION A_USED_INPUT_VARS a' UNION 861 (A_USED_STATE_VARS a UNION A_USED_STATE_VARS a'))` by 862 METIS_TAC[SUBSET_UNION, UNION_COMM, UNION_ASSOC] THEN 863 864 `(A_USED_INPUT_VARS a' UNION A_USED_STATE_VARS a') SUBSET 865 (A_USED_INPUT_VARS a UNION A_USED_INPUT_VARS a' UNION 866 (A_USED_STATE_VARS a UNION A_USED_STATE_VARS a'))` by 867 METIS_TAC[SUBSET_UNION, UNION_COMM, UNION_ASSOC] THEN 868 METIS_TAC[INJ_SUBSET_DOMAIN], 869 870 REWRITE_TAC [A_USED_INPUT_VARS_def, A_VAR_RENAMING_def, ACCEPT_VAR_RENAMING___USED_VARS, IMAGE_EMPTY] 871 ]); 872 873 874val A_VAR_RENAMING___USED_VARS = 875 store_thm 876 ("A_VAR_RENAMING___USED_VARS", 877 878 ``!a f. (INJ f (A_USED_VARS a) UNIV) ==> 879 880 (A_USED_VARS (A_VAR_RENAMING f a) = 881 (IMAGE f (A_USED_VARS a)))``, 882 883 REPEAT STRIP_TAC THEN 884 REWRITE_TAC [A_USED_VARS_def, IMAGE_UNION, A_VAR_RENAMING___USED_STATE_VARS] THEN 885 METIS_TAC[A_VAR_RENAMING___USED_INPUT_VARS]); 886 887 888val A_VAR_RENAMING___A_BIGAND = 889 store_thm 890 ("A_VAR_RENAMING___A_BIGAND", 891 892 ``!f C. (A_VAR_RENAMING f (A_BIGAND C) = A_BIGAND (MAP (A_VAR_RENAMING f) C))``, 893 894 Induct_on `C` THENL [ 895 REWRITE_TAC [MAP, A_BIGAND_def, A_VAR_RENAMING_def], 896 ASM_REWRITE_TAC [MAP, A_BIGAND_def, A_VAR_RENAMING_def] 897 ]); 898 899 900val ACCEPT_COND_USED_VARS_INTER_SUBSET_THM = 901 store_thm 902 ("ACCEPT_COND_USED_VARS_INTER_SUBSET_THM", 903 ``!a S t v. ((ACCEPT_COND_USED_VARS a) SUBSET S) ==> (ACCEPT_COND_SEM_TIME t v a = ACCEPT_COND_SEM_TIME t (PATH_RESTRICT v S) a)``, 904 905 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THENL [ 906 SIMP_TAC std_ss [ACCEPT_COND_USED_VARS_def, ACCEPT_COND_SEM_TIME_def, PATH_RESTRICT_def, PATH_MAP_def] THEN 907 PROVE_TAC [P_USED_VARS_INTER_SUBSET_THM], 908 909 REWRITE_TAC[ACCEPT_COND_SEM_TIME_def], 910 911 REWRITE_TAC[ACCEPT_COND_SEM_TIME_def, ACCEPT_COND_USED_VARS_def] THEN 912 PROVE_TAC[], 913 914 REWRITE_TAC[ACCEPT_COND_SEM_TIME_def, ACCEPT_COND_USED_VARS_def, UNION_SUBSET] THEN 915 PROVE_TAC[], 916 917 REWRITE_TAC[ACCEPT_COND_SEM_TIME_def, ACCEPT_COND_USED_VARS_def] THEN 918 PROVE_TAC[] 919 ]); 920 921 922val ACCEPT_COND_USED_VARS_INTER_THM = 923 store_thm 924 ("ACCEPT_COND_USED_VARS_INTER_THM", 925 ``!a t v. (ACCEPT_COND_SEM_TIME t v a = ACCEPT_COND_SEM_TIME t (PATH_RESTRICT v (ACCEPT_COND_USED_VARS a)) a)``, 926 927 METIS_TAC [ACCEPT_COND_USED_VARS_INTER_SUBSET_THM, SUBSET_REFL]); 928 929 930val A_USED_INPUT_VARS_INTER_SUBSET_THM = 931 store_thm 932 ("A_USED_INPUT_VARS_INTER_SUBSET_THM", 933 ``!a S. ((A_USED_INPUT_VARS a) SUBSET S) ==> 934 (!i. (A_SEM i a = A_SEM (PATH_RESTRICT i S) a))``, 935 936 INDUCT_THEN automaton_formula_induct STRIP_ASSUME_TAC THENL [ 937 FULL_SIMP_TAC std_ss [A_SEM_def, A_USED_INPUT_VARS_def, ACCEPT_COND_SEM_def] THEN 938 PROVE_TAC [ACCEPT_COND_USED_VARS_INTER_SUBSET_THM], 939 940 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, A_SEM_def, IS_TRANSITION_def, INPUT_RUN_PATH_UNION_def, 941 A_USED_INPUT_VARS_def, UNION_SUBSET, DIFF_SUBSET_ELIM, SEMI_AUTOMATON_USED_INPUT_VARS_def] THEN 942 REPEAT STRIP_TAC THEN 943 EXISTS_EQ_STRIP_TAC THEN 944 BINOP_TAC THENL [ 945 SUBGOAL_TAC `!n. ((INPUT_RUN_STATE_UNION p_1 (i n) (w n)) INTER (S UNION p_1.S)) = 946 ((INPUT_RUN_STATE_UNION p_1 (PATH_RESTRICT i S n) (w n)) INTER (S UNION p_1.S))` THEN1 ( 947 948 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, INPUT_RUN_STATE_UNION_def, IN_DIFF, PATH_RESTRICT_def, 949 PATH_MAP_def] THEN 950 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 951 FULL_SIMP_TAC std_ss [] 952 ) THEN 953 PROVE_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, P_USED_VARS_INTER_SUBSET_THM], 954 955 956 REMAINS_TAC `(PATH_RESTRICT (\n. INPUT_RUN_STATE_UNION p_1 (i n) (w n)) (S UNION p_1.S)) = 957 (PATH_RESTRICT (\n. INPUT_RUN_STATE_UNION p_1 (PATH_RESTRICT i S n) (w n)) (S UNION p_1.S))` THEN1 ( 958 METIS_TAC[] 959 ) THEN 960 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INPUT_RUN_STATE_UNION_def] THEN 961 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 962 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] THEN 963 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 964 FULL_SIMP_TAC std_ss [] 965 ], 966 967 REWRITE_TAC [A_USED_INPUT_VARS_def, A_SEM_def] THEN 968 PROVE_TAC[], 969 970 REWRITE_TAC [UNION_SUBSET, A_USED_INPUT_VARS_def, A_SEM_def] THEN 971 PROVE_TAC[], 972 973 REWRITE_TAC [A_SEM_def] 974 ]); 975 976 977val A_USED_INPUT_VARS_INTER_THM = 978 store_thm 979 ("A_USED_INPUT_VARS_INTER_THM", 980 ``!a i. (A_SEM i a = A_SEM (PATH_RESTRICT i (A_USED_INPUT_VARS a)) a)``, 981 982 METIS_TAC[A_USED_INPUT_VARS_INTER_SUBSET_THM, SUBSET_REFL]); 983 984 985val A_USED_INPUT_VARS_DIFF_DISJOINT_THM = 986 store_thm 987 ("A_USED_INPUT_VARS_DIFF_DISJOINT_THM", 988 ``!a S. (DISJOINT (A_USED_INPUT_VARS a) S) ==> 989 (!i. (A_SEM i a = A_SEM (PATH_DIFF i S) a))``, 990 991 REPEAT STRIP_TAC THEN 992 `A_USED_INPUT_VARS a SUBSET COMPL S` by PROVE_TAC[SUBSET_COMPL_DISJOINT] THEN 993 PROVE_TAC[A_USED_INPUT_VARS_INTER_SUBSET_THM, PATH_DIFF_PATH_RESTRICT]); 994 995 996 997val A_AND___A_NDET = 998 store_thm 999 ("A_AND___A_NDET", 1000 1001 ``!A1 f1 A2 f2. (A_USED_STATE_VARS_COMPATIBLE (A_NDET(A1, f1)) (A_NDET(A2, f2))) ==> 1002 ((AUTOMATON_EQUIV (A_AND(A_NDET(A1, f1), A_NDET(A2, f2))) (A_NDET((PRODUCT_SEMI_AUTOMATON A1 A2), A_AND(f1,f2)))))``, 1003 1004 SIMP_TAC std_ss [A_USED_STATE_VARS_COMPATIBLE_def, 1005 A_USED_INPUT_VARS_def, 1006 A_USED_STATE_VARS_def, 1007 STATE_VARDISJOINT_AUTOMATON_FORMULA_def, 1008 DISJOINT_UNION_BOTH, 1009 AUTOMATON_EQUIV_def, 1010 DISJOINT_DIFF_ELIM_SYM, 1011 A_SEM_def 1012 ] THEN 1013 1014 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1015 1016 EXISTS_TAC ``PATH_UNION w w'`` THEN 1017 REPEAT STRIP_TAC THENL [ 1018 METIS_TAC [PRODUCT_SEMI_AUTOMATON_RUN, DISJOINT_SYM], 1019 1020 1021 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f1) A2.S) /\ 1022 ((PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) v (PATH_UNION w w')) A2.S) = 1023 (PATH_DIFF (INPUT_RUN_PATH_UNION A1 v w) A2.S))` THEN1 ( 1024 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1025 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, PATH_DIFF_def, IN_UNION, IN_DIFF, 1026 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, PATH_UNION_def, EXTENSION, PRODUCT_SEMI_AUTOMATON_REWRITES, 1027 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def] THEN 1028 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN PROVE_TAC[] 1029 ) THEN 1030 PROVE_TAC[A_USED_INPUT_VARS_DIFF_DISJOINT_THM], 1031 1032 1033 1034 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f2) A1.S) /\ 1035 ((PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) v (PATH_UNION w w')) A1.S) = 1036 (PATH_DIFF (INPUT_RUN_PATH_UNION A2 v w') A1.S))` THEN1 ( 1037 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1038 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, PATH_DIFF_def, IN_UNION, IN_DIFF, 1039 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, PATH_UNION_def, EXTENSION, PRODUCT_SEMI_AUTOMATON_REWRITES, 1040 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def] THEN 1041 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN PROVE_TAC[] 1042 ) THEN 1043 PROVE_TAC[A_USED_INPUT_VARS_DIFF_DISJOINT_THM] 1044 ], 1045 1046 1047 EXISTS_TAC ``(PATH_RESTRICT w A1.S)`` THEN 1048 REPEAT STRIP_TAC THENL [ 1049 PROVE_TAC [PRODUCT_SEMI_AUTOMATON_RUN2___FIRST, DISJOINT_SYM], 1050 1051 1052 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f1) A2.S) /\ 1053 ((PATH_DIFF (INPUT_RUN_PATH_UNION A1 v (PATH_RESTRICT w A1.S)) A2.S) = 1054 (PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) v w) A2.S))` THEN1 ( 1055 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1056 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, PATH_DIFF_def, IN_UNION, IN_DIFF, 1057 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, PATH_UNION_def, EXTENSION, PRODUCT_SEMI_AUTOMATON_REWRITES, 1058 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 1059 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN PROVE_TAC[] 1060 ) THEN 1061 PROVE_TAC[A_USED_INPUT_VARS_DIFF_DISJOINT_THM] 1062 ], 1063 1064 1065 EXISTS_TAC ``(PATH_RESTRICT w A2.S)`` THEN 1066 REPEAT STRIP_TAC THENL [ 1067 PROVE_TAC [PRODUCT_SEMI_AUTOMATON_RUN2___SECOND, DISJOINT_SYM], 1068 1069 1070 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f2) A1.S) /\ 1071 ((PATH_DIFF (INPUT_RUN_PATH_UNION A2 v (PATH_RESTRICT w A2.S)) A1.S) = 1072 (PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) v w) A1.S))` THEN1 ( 1073 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1074 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, PATH_DIFF_def, IN_UNION, IN_DIFF, 1075 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, PATH_UNION_def, EXTENSION, PRODUCT_SEMI_AUTOMATON_REWRITES, 1076 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 1077 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN PROVE_TAC[] 1078 ) THEN 1079 PROVE_TAC[A_USED_INPUT_VARS_DIFF_DISJOINT_THM] 1080 ] 1081 ]); 1082 1083 1084 1085 1086val PRODUCT_SEMI_AUTOMATON___EXISTS_RUN_WITH_PROPERTIES = 1087 store_thm 1088 ("PRODUCT_SEMI_AUTOMATON___EXISTS_RUN_WITH_PROPERTIES", 1089 1090 ``!A1 C1 A2 C2. (A_USED_STATE_VARS_COMPATIBLE (A_NDET(A1, A_BIGAND C1)) (A_NDET(A2, A_BIGAND C2))) ==> 1091 (((EXISTS_RUN_WITH_PROPERTIES A1 C1) /\ (EXISTS_RUN_WITH_PROPERTIES A2 C2)) ==> 1092 (EXISTS_RUN_WITH_PROPERTIES (PRODUCT_SEMI_AUTOMATON A1 A2) (C1++C2)))``, 1093 1094 1095 1096 REPEAT STRIP_TAC THEN 1097 SIMP_ALL_TAC std_ss [EXISTS_RUN_WITH_PROPERTIES_def, EXISTS_UNIQUE_DEF, A_BIGAND___A_SEM, A_SEM_def] THEN 1098 SUBGOAL_TAC `AUTOMATON_EQUIV (A_AND (A_NDET (A1, A_BIGAND C1),A_NDET (A2, A_BIGAND C2))) 1099 (A_NDET (PRODUCT_SEMI_AUTOMATON A1 A2,A_AND (A_BIGAND C1,A_BIGAND C2)))` THEN1 ( 1100 PROVE_TAC[A_AND___A_NDET] 1101 ) THEN 1102 SIMP_ALL_TAC std_ss [A_BIGAND_def, A_BIGAND___A_SEM, AUTOMATON_EQUIV_def, A_SEM_def] THEN 1103 PROVE_TAC[]); 1104 1105 1106val PRODUCT_SEMI_AUTOMATON___UNIQUE_RUN_WITH_PROPERTIES = 1107 store_thm 1108 ("PRODUCT_SEMI_AUTOMATON___UNIQUE_RUN_WITH_PROPERTIES", 1109 1110 ``!A1 C1 A2 C2. (A_USED_STATE_VARS_COMPATIBLE (A_NDET(A1, A_BIGAND C1)) (A_NDET(A2, A_BIGAND C2))) ==> 1111 (((UNIQUE_RUN_WITH_PROPERTIES A1 C1) /\ (UNIQUE_RUN_WITH_PROPERTIES A2 C2)) ==> 1112 (UNIQUE_RUN_WITH_PROPERTIES (PRODUCT_SEMI_AUTOMATON A1 A2) (C1++C2)))``, 1113 1114 REPEAT STRIP_TAC THEN 1115 SIMP_ALL_TAC std_ss [UNIQUE_RUN_WITH_PROPERTIES_def, EXISTS_UNIQUE_DEF, A_BIGAND___A_SEM, A_SEM_def] THEN 1116 REPEAT STRIP_TAC THENL [ 1117 `AUTOMATON_EQUIV (A_AND (A_NDET (A1, A_BIGAND C1),A_NDET (A2, A_BIGAND C2))) (A_NDET (PRODUCT_SEMI_AUTOMATON A1 A2,A_AND (A_BIGAND C1,A_BIGAND C2)))` by PROVE_TAC[A_AND___A_NDET] THEN 1118 SIMP_ALL_TAC std_ss [A_BIGAND_def, A_BIGAND___A_SEM, AUTOMATON_EQUIV_def, A_SEM_def] THEN 1119 PROVE_TAC[], 1120 1121 1122 REMAINS_TAC `(PATH_RESTRICT x A1.S = PATH_RESTRICT y A1.S) /\ 1123 (PATH_RESTRICT x A2.S = PATH_RESTRICT y A2.S)` THEN1 ( 1124 1125 `(x = PATH_UNION (PATH_RESTRICT x A1.S) (PATH_RESTRICT x A2.S)) /\ 1126 (y = PATH_UNION (PATH_RESTRICT y A1.S) (PATH_RESTRICT y A2.S))` 1127 by METIS_TAC[IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_PARTITION, PRODUCT_SEMI_AUTOMATON_REWRITES] THEN 1128 PROVE_TAC[] 1129 ) THEN 1130 1131 REMAINS_TAC `(IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A1 i (PATH_RESTRICT x A1.S) /\ IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A2 i (PATH_RESTRICT x A2.S) /\ 1132 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A1 i (PATH_RESTRICT y A1.S) /\ IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A2 i (PATH_RESTRICT y A2.S)) /\ 1133 (A_SEM (INPUT_RUN_PATH_UNION A1 i (PATH_RESTRICT x A1.S)) (A_BIGAND C1) /\ 1134 A_SEM (INPUT_RUN_PATH_UNION A1 i (PATH_RESTRICT y A1.S)) (A_BIGAND C1) /\ 1135 A_SEM (INPUT_RUN_PATH_UNION A2 i (PATH_RESTRICT x A2.S)) (A_BIGAND C2) /\ 1136 A_SEM (INPUT_RUN_PATH_UNION A2 i (PATH_RESTRICT y A2.S)) (A_BIGAND C2))` THEN1 ( 1137 METIS_TAC[] 1138 ) THEN 1139 1140 1141 SUBGOAL_TAC `DISJOINT A1.S A2.S /\ 1142 DISJOINT A2.S (SEMI_AUTOMATON_USED_INPUT_VARS A1) /\ 1143 DISJOINT A1.S (SEMI_AUTOMATON_USED_INPUT_VARS A2) /\ 1144 DISJOINT (A_USED_INPUT_VARS (A_BIGAND C2)) A1.S /\ 1145 DISJOINT (A_USED_INPUT_VARS (A_BIGAND C1)) A2.S` THEN1 ( 1146 SIMP_ALL_TAC std_ss [A_USED_STATE_VARS_COMPATIBLE_def, A_USED_STATE_VARS_def, 1147 A_USED_INPUT_VARS_def, DISJOINT_UNION_BOTH] THEN 1148 PROVE_TAC[DISJOINT_SYM, DISJOINT_DIFF_ELIM_SYM] 1149 ) THEN 1150 SUBGOAL_TAC `((PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) i x) A1.S) = 1151 (PATH_DIFF (INPUT_RUN_PATH_UNION A2 i (PATH_RESTRICT x A2.S)) A1.S)) /\ 1152 1153 ((PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) i x) A2.S) = 1154 (PATH_DIFF (INPUT_RUN_PATH_UNION A1 i (PATH_RESTRICT x A1.S)) A2.S)) /\ 1155 1156 ((PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) i y) A1.S) = 1157 (PATH_DIFF (INPUT_RUN_PATH_UNION A2 i (PATH_RESTRICT y A2.S)) A1.S)) /\ 1158 1159 ((PATH_DIFF (INPUT_RUN_PATH_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) i y) A2.S) = 1160 (PATH_DIFF (INPUT_RUN_PATH_UNION A1 i (PATH_RESTRICT y A1.S)) A2.S))` THEN1 ( 1161 1162 UNDISCH_NO_TAC 7 THEN UNDISCH_NO_TAC 9 THEN REPEAT WEAKEN_HD_TAC THEN 1163 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1164 SIMP_TAC std_ss [PATH_DIFF_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, EXTENSION, 1165 PATH_RESTRICT_def, PRODUCT_SEMI_AUTOMATON_REWRITES, IN_UNION, IN_DIFF, PATH_MAP_def, IN_INTER, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1166 PATH_SUBSET_def, SUBSET_DEF] THEN 1167 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 1168 PROVE_TAC[] 1169 ) THEN 1170 PROVE_TAC[PRODUCT_SEMI_AUTOMATON_RUN2___FIRST, PRODUCT_SEMI_AUTOMATON_RUN2___SECOND, A_USED_INPUT_VARS_DIFF_DISJOINT_THM] 1171 ]); 1172 1173 1174 1175val A_NDET___FLATTENING = 1176 store_thm 1177 ("A_NDET___FLATTENING", 1178 1179 ``!A1 A2 f. ( A_USED_STATE_VARS_COMPATIBLE (A_NDET(A1, A_TRUE)) (A_NDET(A2, f))) ==> 1180 ((AUTOMATON_EQUIV (A_NDET(A1, A_NDET(A2, f))) (A_NDET((PRODUCT_SEMI_AUTOMATON A1 A2), f))))``, 1181 1182 1183 SIMP_TAC std_ss [AUTOMATON_EQUIV_def, A_SEM_def, A_USED_STATE_VARS_COMPATIBLE_def, DISJOINT_UNION_BOTH, 1184 A_USED_INPUT_VARS_def, SEMI_AUTOMATON_USED_INPUT_VARS_def, EMPTY_DIFF, UNION_EMPTY, A_USED_STATE_VARS_def] THEN 1185 REPEAT STRIP_TAC THEN 1186 FULL_SIMP_TAC std_ss [DISJOINT_UNION_BOTH, DISJOINT_DIFF_ELIM_SYM] THEN 1187 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, PRODUCT_SEMI_AUTOMATON_REWRITES, PATH_SUBSET_def, SUBSET_DEF, IN_UNION, 1188 P_SEM_THM, INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def, XP_SEM_def] THEN 1189 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1190 EXISTS_TAC ``PATH_UNION w w'`` THEN 1191 SIMP_TAC std_ss [PATH_UNION_def, IN_UNION] THEN 1192 1193 SUBGOAL_TAC `!n. (((w n UNION w' n UNION (v n DIFF (A1.S UNION A2.S)))) = 1194 ((w' n UNION (w n UNION (v n DIFF A1.S) DIFF A2.S)))) /\ 1195 (((w n UNION w' n UNION (v n DIFF (A1.S UNION A2.S))) INTER (COMPL A2.S)) = 1196 ((w n UNION (v n DIFF A1.S)) INTER (COMPL A2.S)))` THEN1 ( 1197 SIMP_ALL_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, IN_COMPL, GSYM SUBSET_COMPL_DISJOINT, 1198 SUBSET_DEF, IN_COMPL] THEN 1199 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN PROVE_TAC[] 1200 ) THEN 1201 SUBGOAL_TAC `P_USED_VARS A1.S0 SUBSET (COMPL A2.S) /\ 1202 P_USED_VARS A2.S0 SUBSET (COMPL A1.S) /\ 1203 XP_USED_VARS A1.R SUBSET (COMPL A2.S) /\ 1204 XP_USED_VARS A2.R SUBSET (COMPL A1.S)` THEN1 ( 1205 PROVE_TAC[SUBSET_COMPL_DISJOINT] 1206 ) THEN 1207 REPEAT STRIP_TAC THENL [ 1208 PROVE_TAC[], 1209 PROVE_TAC[], 1210 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1211 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1212 PROVE_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM], 1213 PROVE_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM], 1214 ASM_SIMP_TAC std_ss [] 1215 ], 1216 1217 1218 EXISTS_TAC ``(PATH_RESTRICT w A1.S)`` THEN 1219 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 1220 SUBGOAL_TAC `!n. (((w n UNION (v n DIFF (A1.S UNION A2.S))) INTER (COMPL A2.S)) = 1221 ((w n INTER A1.S) UNION (v n DIFF A1.S)) INTER (COMPL A2.S))` THEN1 ( 1222 SIMP_ALL_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, IN_COMPL, GSYM SUBSET_COMPL_DISJOINT, 1223 SUBSET_DEF, IN_COMPL] THEN 1224 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN PROVE_TAC[] 1225 ) THEN 1226 SUBGOAL_TAC `P_USED_VARS A1.S0 SUBSET (COMPL A2.S) /\ 1227 XP_USED_VARS A1.R SUBSET (COMPL A2.S)` THEN1 ( 1228 PROVE_TAC[SUBSET_COMPL_DISJOINT] 1229 ) THEN 1230 REPEAT STRIP_TAC THENL [ 1231 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1232 PROVE_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM], 1233 1234 EXISTS_TAC ``(PATH_RESTRICT w A2.S)`` THEN 1235 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 1236 SUBGOAL_TAC `!n. (w n INTER A2.S UNION (w n INTER A1.S UNION (v n DIFF A1.S) DIFF A2.S)) = 1237 (w n UNION (v n DIFF (A1.S UNION A2.S)))` THEN1 ( 1238 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] THEN 1239 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN METIS_TAC[] 1240 ) THEN 1241 ASM_SIMP_TAC std_ss [] 1242 ] 1243 ]); 1244 1245 1246 1247 1248 1249 1250 1251 1252val TOTAL_DET_AUTOMATON_EX_ALL_EQUIV = 1253 store_thm 1254 ("TOTAL_DET_AUTOMATON_EX_ALL_EQUIV", 1255 ``!A. IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A ==> (!f. AUTOMATON_EQUIV (A_NDET(A,f)) (A_UNIV(A,f)))``, 1256 1257 REPEAT STRIP_TAC THEN 1258 REWRITE_TAC [AUTOMATON_EQUIV_def, A_SEM_THM] THEN 1259 METIS_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN]); 1260 1261 1262val UNIQUE_RUN_WITH_PROPERTIES___CONSTRAINED_AUTOMATON_EX_ALL_EQUIV = 1263 store_thm 1264 ("UNIQUE_RUN_WITH_PROPERTIES___CONSTRAINED_AUTOMATON_EX_ALL_EQUIV", 1265 ``!A C. (UNIQUE_RUN_WITH_PROPERTIES A C) ==> (!f. AUTOMATON_EQUIV (A_NDET_CONSTRAINED (A,C,f)) (A_UNIV_CONSTRAINED (A,C,f)))``, 1266 1267 REWRITE_TAC [AUTOMATON_EQUIV_def, 1268 A_NDET_CONSTRAINED_def, 1269 A_UNIV_CONSTRAINED_def, 1270 A_SEM_THM, 1271 UNIQUE_RUN_WITH_PROPERTIES_def] THEN 1272 METIS_TAC[]); 1273 1274 1275val NEG_ACCEPTANCE_CONDITION = 1276 store_thm 1277 ("NEG_ACCEPTANCE_CONDITION", 1278 ``!A f. AUTOMATON_EQUIV (A_NOT(A_NDET(A,f))) (A_UNIV(A, A_NOT f))``, 1279 1280 REPEAT STRIP_TAC THEN 1281 REWRITE_TAC [AUTOMATON_EQUIV_def, A_SEM_THM] THEN 1282 METIS_TAC[]); 1283 1284 1285val NEG_ACCEPTANCE_CONDITION_DET = 1286 store_thm 1287 ("NEG_ACCEPTANCE_CONDITION_DET", 1288 ``!A f. IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A ==> (AUTOMATON_EQUIV (A_NOT(A_NDET(A,f))) (A_NDET(A, A_NOT f)))``, 1289 1290 REPEAT STRIP_TAC THEN 1291 REWRITE_TAC [AUTOMATON_EQUIV_def, A_SEM_THM] THEN 1292 METIS_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN]); 1293 1294 1295 1296val ACCEPT_COND___VAR_RENAMING___NOT_INJ = 1297 store_thm 1298 ("ACCEPT_COND___VAR_RENAMING___NOT_INJ", 1299 ``!ac t i f. 1300 (ACCEPT_COND_SEM_TIME t i (ACCEPT_VAR_RENAMING f ac)) = 1301 (ACCEPT_COND_SEM_TIME t (\n x. f x IN i n) ac)``, 1302 1303 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THEN ( 1304 FULL_SIMP_TAC std_ss [ACCEPT_VAR_RENAMING_def, ACCEPT_COND_SEM_TIME_def, 1305 P_SEM___VAR_RENAMING___NOT_INJ] 1306 )); 1307 1308 1309val ACCEPT_COND___VAR_RENAMING = 1310 store_thm 1311 ("ACCEPT_COND___VAR_RENAMING", 1312 ``!a t i f. (INJ f (PATH_USED_VARS i UNION ACCEPT_COND_USED_VARS a) UNIV) ==> 1313 ((ACCEPT_COND_SEM_TIME t i a) = (ACCEPT_COND_SEM_TIME t (PATH_VAR_RENAMING f i) (ACCEPT_VAR_RENAMING f a)))``, 1314 1315 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THENL [ 1316 REPEAT STRIP_TAC THEN 1317 SIMP_ALL_TAC std_ss [ACCEPT_COND_SEM_TIME_def, ACCEPT_VAR_RENAMING_def, 1318 PATH_VAR_RENAMING_def, PATH_MAP_def, ACCEPT_COND_USED_VARS_def] THEN 1319 `(i t UNION P_USED_VARS p) SUBSET (PATH_USED_VARS i UNION P_USED_VARS p)` by ( 1320 SIMP_TAC std_ss [PATH_USED_VARS_def, SUBSET_DEF, IN_UNION, IN_BIGUNION, GSPECIFICATION] THEN 1321 PROVE_TAC[] 1322 ) THEN 1323 PROVE_TAC[P_SEM___VAR_RENAMING, INJ_SUBSET_DOMAIN], 1324 1325 SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def, ACCEPT_VAR_RENAMING_def], 1326 1327 ASM_SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def, ACCEPT_VAR_RENAMING_def, ACCEPT_COND_USED_VARS_def], 1328 1329 SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def, ACCEPT_VAR_RENAMING_def, ACCEPT_COND_USED_VARS_def] THEN 1330 PROVE_TAC[INJ_SUBSET_DOMAIN, SUBSET_UNION, UNION_COMM, UNION_ASSOC], 1331 1332 SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def, ACCEPT_VAR_RENAMING_def, ACCEPT_COND_USED_VARS_def] THEN 1333 PROVE_TAC[] 1334 ]); 1335 1336 1337 1338val AUTOMATON_FORMULA___VAR_RENAMING = 1339 store_thm 1340 ("AUTOMATON_FORMULA___VAR_RENAMING", 1341 ``!a i (f:'a->'b). (INJ f (PATH_USED_VARS i UNION A_USED_VARS a) UNIV) ==> 1342 ((A_SEM i a) = (A_SEM (PATH_VAR_RENAMING f i) (A_VAR_RENAMING f a)))``, 1343 INDUCT_THEN automaton_formula_induct ASSUME_TAC THENL [ 1344 REPEAT STRIP_TAC THEN 1345 REWRITE_TAC [A_SEM_def, A_VAR_RENAMING_def, ACCEPT_COND_SEM_def] THEN 1346 SIMP_ALL_TAC std_ss [A_USED_VARS___DIRECT_DEF] THEN 1347 PROVE_TAC[ACCEPT_COND___VAR_RENAMING, A_USED_VARS_def], 1348 1349 REPEAT STRIP_TAC THEN 1350 SIMP_TAC std_ss [A_SEM_def, A_VAR_RENAMING_def] THEN 1351 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1352 Q_TAC EXISTS_TAC `PATH_VAR_RENAMING f w` THEN 1353 REPEAT STRIP_TAC THENL [ 1354 UNDISCH_KEEP_NO_TAC 1 THEN 1355 IMP_TO_EQ_TAC THEN 1356 MATCH_MP_TAC SEMI_AUTOMATON___VAR_RENAMING THEN 1357 UNDISCH_NO_TAC 2 THEN 1358 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1359 SIMP_ALL_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1360 PATH_SUBSET_def, SUBSET_DEF] THEN 1361 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, A_USED_VARS___DIRECT_DEF, 1362 SEMI_AUTOMATON_USED_VARS_def, GSYM PATH_USED_VARS_THM] THEN 1363 PROVE_TAC[], 1364 1365 1366 SUBGOAL_TAC `(INPUT_RUN_PATH_UNION (SEMI_AUTOMATON_VAR_RENAMING f p_1) (PATH_VAR_RENAMING f i) (PATH_VAR_RENAMING f w)) = 1367 (PATH_VAR_RENAMING f ((INPUT_RUN_PATH_UNION p_1 i w)))` THEN1 ( 1368 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1369 Cases_on `p_1` THEN 1370 SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, EXTENSION, PATH_VAR_RENAMING_def, IN_UNION, 1371 PATH_MAP_def, IN_IMAGE, IN_DIFF, SEMI_AUTOMATON_VAR_RENAMING_def, symbolic_semi_automaton_REWRITES, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, SUBSET_DEF, 1372 INJ_DEF, IN_UNIV, 1373 GSYM PATH_USED_VARS_THM, 1374 A_USED_VARS___DIRECT_DEF, 1375 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1376 METIS_TAC[] 1377 ) THEN 1378 ASM_REWRITE_TAC[] THEN 1379 REMAINS_TAC `INJ f (PATH_USED_VARS (INPUT_RUN_PATH_UNION p_1 i w) UNION A_USED_VARS a) UNIV` THEN1 ( 1380 PROVE_TAC[] 1381 ) THEN 1382 UNDISCH_NO_TAC 3 THEN 1383 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1384 SIMP_ALL_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1385 PATH_SUBSET_def, SUBSET_DEF] THEN 1386 SIMP_TAC std_ss [EXTENSION, IN_UNION, A_USED_VARS___DIRECT_DEF, 1387 SUBSET_DEF, GSYM PATH_USED_VARS_THM, IN_DIFF, 1388 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1389 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1390 PROVE_TAC[] 1391 ], 1392 1393 SUBGOAL_TAC `?w'. PATH_SUBSET w' p_1.S /\ (w = PATH_VAR_RENAMING f w')` THEN1 ( 1394 MATCH_MP_TAC PATH_VAR_RENAMING___ORIG_PATH_EXISTS THEN 1395 Cases_on `p_1` THEN 1396 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1397 SEMI_AUTOMATON_VAR_RENAMING_def, symbolic_semi_automaton_REWRITES] 1398 ) THEN 1399 Q_TAC EXISTS_TAC `w'` THEN 1400 REPEAT STRIP_TAC THENL [ 1401 UNDISCH_NO_TAC 3 THEN 1402 IMP_TO_EQ_TAC THEN 1403 ASM_REWRITE_TAC [] THEN 1404 MATCH_MP_TAC (GSYM SEMI_AUTOMATON___VAR_RENAMING) THEN 1405 UNDISCH_NO_TAC 3 THEN 1406 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1407 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, A_USED_VARS___DIRECT_DEF, 1408 SEMI_AUTOMATON_USED_VARS_def, GSYM PATH_USED_VARS_THM] THEN 1409 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF] THEN 1410 PROVE_TAC[], 1411 1412 SUBGOAL_TAC `(INPUT_RUN_PATH_UNION (SEMI_AUTOMATON_VAR_RENAMING f p_1) (PATH_VAR_RENAMING f i) (PATH_VAR_RENAMING f w')) = 1413 (PATH_VAR_RENAMING f ((INPUT_RUN_PATH_UNION p_1 i w')))` THEN1 ( 1414 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1415 Cases_on `p_1` THEN 1416 SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, EXTENSION, PATH_VAR_RENAMING_def, IN_UNION, 1417 PATH_MAP_def, IN_IMAGE, IN_DIFF, SEMI_AUTOMATON_VAR_RENAMING_def, symbolic_semi_automaton_REWRITES, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, SUBSET_DEF, 1418 INJ_DEF, IN_UNIV, 1419 GSYM PATH_USED_VARS_THM, 1420 A_USED_VARS___DIRECT_DEF, 1421 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1422 METIS_TAC[] 1423 ) THEN 1424 REMAINS_TAC `INJ f (PATH_USED_VARS (INPUT_RUN_PATH_UNION p_1 i w') UNION A_USED_VARS a) UNIV` THEN1 ( 1425 PROVE_TAC[] 1426 ) THEN 1427 UNDISCH_NO_TAC 5 THEN 1428 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1429 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF] THEN 1430 SIMP_TAC std_ss [EXTENSION, IN_UNION, A_USED_VARS___DIRECT_DEF, 1431 SUBSET_DEF, GSYM PATH_USED_VARS_THM, IN_DIFF, 1432 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1433 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1434 PROVE_TAC[] 1435 ] 1436 ], 1437 1438 1439 1440 ASM_SIMP_TAC std_ss [A_USED_VARS___DIRECT_DEF, A_VAR_RENAMING_def, A_SEM_def], 1441 1442 1443 1444 ASM_SIMP_TAC std_ss [A_USED_VARS___DIRECT_DEF, A_VAR_RENAMING_def, A_SEM_def] THEN 1445 REPEAT STRIP_TAC THEN 1446 REMAINS_TAC `INJ f (PATH_USED_VARS i UNION A_USED_VARS a) UNIV /\ 1447 INJ f (PATH_USED_VARS i UNION A_USED_VARS a') UNIV` THEN1 ( 1448 PROVE_TAC[] 1449 ) THEN 1450 STRIP_TAC THEN 1451 UNDISCH_HD_TAC THEN 1452 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1453 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1454 PROVE_TAC[], 1455 1456 1457 1458 REWRITE_TAC[A_SEM_def, A_VAR_RENAMING_def] 1459 ]); 1460 1461 1462val AUTOMATON_FORMULA___STATE_VAR_RENAMING = 1463 store_thm 1464 ("AUTOMATON_FORMULA___STATE_VAR_RENAMING", 1465 ``!a i f. ((INJ f (PATH_USED_VARS i UNION A_USED_VARS a) UNIV) /\ (!x. x IN (A_USED_INPUT_VARS a) ==> (f x = x))) ==> 1466 ((A_SEM i a) = (A_SEM i (A_VAR_RENAMING f a)))``, 1467 1468 1469 REPEAT STRIP_TAC THEN 1470 REMAINS_TAC `(PATH_RESTRICT (PATH_VAR_RENAMING f i) (A_USED_INPUT_VARS (A_VAR_RENAMING f a))) = 1471 (PATH_RESTRICT i (A_USED_INPUT_VARS (A_VAR_RENAMING f a)))` THEN1 ( 1472 PROVE_TAC[AUTOMATON_FORMULA___VAR_RENAMING, A_USED_INPUT_VARS_INTER_THM] 1473 ) THEN 1474 1475 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1476 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_VAR_RENAMING_def, PATH_MAP_def, EXTENSION, IN_INTER] THEN 1477 REPEAT STRIP_TAC THEN CONJ_EQ_STRIP_TAC THEN 1478 SUBGOAL_TAC `x' IN IMAGE f (A_USED_INPUT_VARS a)` THEN1 ( 1479 `INJ f (A_USED_VARS a) UNIV` by METIS_TAC[INJ_SUBSET_DOMAIN, SUBSET_UNION] THEN 1480 FULL_SIMP_TAC std_ss [A_VAR_RENAMING___USED_INPUT_VARS] 1481 ) THEN 1482 SIMP_ALL_TAC std_ss [IN_IMAGE, INJ_DEF, IN_UNIV, IN_UNION, GSYM PATH_USED_VARS_THM, A_USED_VARS_def] THEN 1483 METIS_TAC[]); 1484 1485 1486val A_SEM_AUTOMATON_RUN___STATE_VAR_RENAMING = 1487 store_thm 1488 ("A_SEM_AUTOMATON_RUN___STATE_VAR_RENAMING", 1489 ``!A a f. ((INJ f UNIV UNIV) /\ (!x. x IN (SEMI_AUTOMATON_USED_INPUT_VARS A UNION (A_USED_INPUT_VARS a DIFF A.S)) ==> (f x = x))) ==> 1490 !i w. (A_SEM (INPUT_RUN_PATH_UNION A i w) a = A_SEM (INPUT_RUN_PATH_UNION (SEMI_AUTOMATON_VAR_RENAMING f A) i (PATH_VAR_RENAMING f w)) (A_VAR_RENAMING f a))``, 1491 1492 1493 REPEAT STRIP_TAC THEN 1494 REMAINS_TAC `(PATH_RESTRICT (PATH_VAR_RENAMING f (INPUT_RUN_PATH_UNION A i w)) (A_USED_INPUT_VARS (A_VAR_RENAMING f a))) = 1495 (PATH_RESTRICT (INPUT_RUN_PATH_UNION (SEMI_AUTOMATON_VAR_RENAMING f A) i (PATH_VAR_RENAMING f w)) (A_USED_INPUT_VARS (A_VAR_RENAMING f a)))` THEN1 ( 1496 PROVE_TAC[AUTOMATON_FORMULA___VAR_RENAMING, A_USED_INPUT_VARS_INTER_THM, 1497 INJ_SUBSET_DOMAIN, SUBSET_UNIV] 1498 ) THEN 1499 1500 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1501 Cases_on `A` THEN 1502 SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_VAR_RENAMING_def, PATH_MAP_def, EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 1503 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_IMAGE, SEMI_AUTOMATON_VAR_RENAMING_def, symbolic_semi_automaton_REWRITES] THEN 1504 REPEAT STRIP_TAC THEN CONJ_EQ_STRIP_TAC THEN 1505 `x'' IN IMAGE f (A_USED_INPUT_VARS a)` by PROVE_TAC[INJ_SUBSET_DOMAIN, SUBSET_UNIV, A_VAR_RENAMING___USED_INPUT_VARS] THEN 1506 SIMP_ALL_TAC std_ss [IN_IMAGE, INJ_DEF, IN_UNIV] THEN 1507 METIS_TAC[]); 1508 1509 1510 1511 1512 1513val STATE_VARDISJOINT_AUTOMATON_FORMULA___VAR_RENAMING = 1514 store_thm 1515 ("STATE_VARDISJOINT_AUTOMATON_FORMULA___VAR_RENAMING", 1516 1517 ``!a f. ((INJ f (A_USED_STATE_VARS a) UNIV)) ==> 1518 (STATE_VARDISJOINT_AUTOMATON_FORMULA (A_VAR_RENAMING f a) = STATE_VARDISJOINT_AUTOMATON_FORMULA a)``, 1519 1520 INDUCT_THEN automaton_formula_induct STRIP_ASSUME_TAC THENL [ 1521 1522 SIMP_TAC std_ss [A_USED_STATE_VARS_def, STATE_VARDISJOINT_AUTOMATON_FORMULA_def, 1523 A_VAR_RENAMING_def], 1524 1525 Cases_on `p_1` THEN 1526 SIMP_ALL_TAC std_ss [A_USED_STATE_VARS_def, STATE_VARDISJOINT_AUTOMATON_FORMULA_def, 1527 A_VAR_RENAMING_def, symbolic_semi_automaton_REWRITES, SEMI_AUTOMATON_VAR_RENAMING_def, 1528 A_VAR_RENAMING___USED_STATE_VARS] THEN 1529 REPEAT STRIP_TAC THEN 1530 BINOP_TAC THENL [ 1531 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, INJ_DEF, IN_UNIV, IN_UNION, IN_IMAGE] THEN 1532 PROVE_TAC[], 1533 1534 PROVE_TAC[SUBSET_UNION, INJ_SUBSET_DOMAIN, SUBSET_REFL] 1535 ], 1536 1537 ASM_SIMP_TAC std_ss [A_USED_STATE_VARS_def, STATE_VARDISJOINT_AUTOMATON_FORMULA_def, A_VAR_RENAMING_def], 1538 1539 ASM_SIMP_TAC std_ss [A_USED_STATE_VARS_def, STATE_VARDISJOINT_AUTOMATON_FORMULA_def, A_VAR_RENAMING_def, 1540 A_VAR_RENAMING___USED_STATE_VARS] THEN 1541 REPEAT STRIP_TAC THEN 1542 BINOP_TAC THENL [ 1543 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, INJ_DEF, IN_UNIV, IN_UNION, IN_IMAGE] THEN 1544 PROVE_TAC[], 1545 1546 PROVE_TAC[SUBSET_UNION, INJ_SUBSET_DOMAIN, SUBSET_REFL] 1547 ], 1548 1549 SIMP_TAC std_ss [A_VAR_RENAMING_def, STATE_VARDISJOINT_AUTOMATON_FORMULA_def] 1550 ]); 1551 1552 1553 1554 1555 1556val VARDISJOINT_AUTOMATON_FORMULA___VAR_RENAMING = 1557 store_thm 1558 ("VARDISJOINT_AUTOMATON_FORMULA___VAR_RENAMING", 1559 1560 ``!a f. ((INJ f (A_USED_VARS a) UNIV)) ==> 1561 (VARDISJOINT_AUTOMATON_FORMULA (A_VAR_RENAMING f a) = VARDISJOINT_AUTOMATON_FORMULA a)``, 1562 1563 REWRITE_TAC[VARDISJOINT_AUTOMATON_FORMULA_def, A_USED_VARS_def] THEN 1564 REPEAT GEN_TAC THEN DISCH_TAC THEN BINOP_TAC THENL[ 1565 PROVE_TAC[STATE_VARDISJOINT_AUTOMATON_FORMULA___VAR_RENAMING, INJ_SUBSET_DOMAIN, SUBSET_UNION, 1566 SUBSET_REFL], 1567 1568 `A_USED_INPUT_VARS (A_VAR_RENAMING f a) = IMAGE f (A_USED_INPUT_VARS a)` by 1569 PROVE_TAC[A_VAR_RENAMING___USED_INPUT_VARS, A_USED_VARS_def] THEN 1570 ASM_SIMP_TAC std_ss [A_VAR_RENAMING___USED_STATE_VARS, A_VAR_RENAMING___USED_INPUT_VARS, A_USED_VARS_def, 1571 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, IN_IMAGE] THEN 1572 SIMP_ASSUMPTIONS_TAC std_ss [INJ_DEF, IN_UNION, IN_UNIV] THEN 1573 PROVE_TAC[SUBSET_REFL] 1574 ]); 1575 1576 1577 1578 1579 1580 1581 1582val EXISTS_RUN_WITH_PROPERTIES___A_SEM_REWRITE = 1583 store_thm 1584 ("EXISTS_RUN_WITH_PROPERTIES___A_SEM_REWRITE", 1585 ``!A C. EXISTS_RUN_WITH_PROPERTIES A C = 1586 (!i. A_SEM i (A_NDET (A, A_BIGAND C)))``, 1587 1588 SIMP_TAC std_ss [EXISTS_RUN_WITH_PROPERTIES_def, A_SEM_def]); 1589 1590 1591 1592 1593 1594val EXISTS_RUN_WITH_PROPERTIES___STATE_VAR_RENAMING = 1595 store_thm 1596 ("EXISTS_RUN_WITH_PROPERTIES___STATE_VAR_RENAMING", 1597 ``!A C f. ((INJ f UNIV UNIV) /\ (!x. x IN (SEMI_AUTOMATON_USED_INPUT_VARS A 1598 UNION ((A_USED_INPUT_VARS (A_BIGAND C)) DIFF A.S)) ==> (f x = x))) ==> 1599 ((EXISTS_RUN_WITH_PROPERTIES (SEMI_AUTOMATON_VAR_RENAMING f A) (MAP (A_VAR_RENAMING f) C)) = (EXISTS_RUN_WITH_PROPERTIES A C))``, 1600 1601 1602 REPEAT STRIP_TAC THEN 1603 SIMP_TAC std_ss [EXISTS_RUN_WITH_PROPERTIES___A_SEM_REWRITE, GSYM A_VAR_RENAMING___A_BIGAND, 1604 GSYM A_VAR_RENAMING_def] THEN 1605 `SEMI_AUTOMATON_USED_INPUT_VARS A UNION (A_USED_INPUT_VARS (A_BIGAND C) DIFF A.S) = 1606 A_USED_INPUT_VARS (A_NDET (A,A_BIGAND C))` by SIMP_TAC std_ss [A_USED_INPUT_VARS_def] THEN 1607 PROVE_TAC[AUTOMATON_FORMULA___STATE_VAR_RENAMING, INJ_SUBSET_DOMAIN, SUBSET_UNIV, SUBSET_REFL]); 1608 1609 1610val UNIQUE_RUN_WITH_PROPERTIES___STATE_VAR_RENAMING = 1611 store_thm 1612 ("UNIQUE_RUN_WITH_PROPERTIES___STATE_VAR_RENAMING", 1613 ``!A C f. ((INJ f UNIV UNIV) /\ (!x. x IN (SEMI_AUTOMATON_USED_INPUT_VARS A 1614 UNION ((A_USED_INPUT_VARS (A_BIGAND C)) DIFF A.S)) ==> (f x = x))) ==> 1615 ((UNIQUE_RUN_WITH_PROPERTIES (SEMI_AUTOMATON_VAR_RENAMING f A) (MAP (A_VAR_RENAMING f) C)) = (UNIQUE_RUN_WITH_PROPERTIES A C))``, 1616 1617 1618 SIMP_TAC std_ss [UNIQUE_RUN_WITH_PROPERTIES_def, EXISTS_UNIQUE_DEF] THEN 1619 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [FORALL_AND_THM] THEN 1620 BINOP_TAC THEN1 METIS_TAC[EXISTS_RUN_WITH_PROPERTIES___STATE_VAR_RENAMING, EXISTS_RUN_WITH_PROPERTIES_def] THEN 1621 1622 REWRITE_TAC [GSYM A_VAR_RENAMING___A_BIGAND] THEN 1623 FORALL_EQ_STRIP_TAC THEN 1624 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1625 REMAINS_TAC `PATH_VAR_RENAMING f x = PATH_VAR_RENAMING f y` THEN1 ( 1626 UNDISCH_HD_TAC THEN 1627 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1628 SIMP_ALL_TAC std_ss [PATH_VAR_RENAMING_def, PATH_MAP_def, EXTENSION, IN_IMAGE, INJ_DEF, IN_UNIV] THEN 1629 METIS_TAC[] 1630 ) THEN 1631 Q_SPECL_NO_ASSUM 4 [`PATH_VAR_RENAMING f x`, `PATH_VAR_RENAMING f y`] THEN 1632 METIS_TAC[A_SEM_AUTOMATON_RUN___STATE_VAR_RENAMING, SEMI_AUTOMATON___STATE_VAR_RENAMING, IN_UNION, SUBSET_UNIV, INJ_SUBSET_DOMAIN, SUBSET_REFL], 1633 1634 1635 SUBGOAL_TAC `(?x'. x = PATH_VAR_RENAMING f x') /\ (?y'. y = PATH_VAR_RENAMING f y')` THEN1 ( 1636 SIMP_ASSUMPTIONS_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, SEMI_AUTOMATON_VAR_RENAMING_REWRITES] THEN 1637 METIS_TAC[PATH_VAR_RENAMING___ORIG_PATH_EXISTS] 1638 ) THEN 1639 METIS_TAC[A_SEM_AUTOMATON_RUN___STATE_VAR_RENAMING, SEMI_AUTOMATON___STATE_VAR_RENAMING, IN_UNION] 1640 ] 1641); 1642 1643 1644 1645val EXISTS_RUN_WITH_PROPERTIES___PROPERTIES_SPLIT = 1646 store_thm( 1647 "EXISTS_RUN_WITH_PROPERTIES___PROPERTIES_SPLIT", 1648 1649 ``(!A C1 C2. EXISTS_RUN_WITH_PROPERTIES A (C1++C2) ==> 1650 (EXISTS_RUN_WITH_PROPERTIES A C1 /\ EXISTS_RUN_WITH_PROPERTIES A C2)) /\ 1651 (!A c C. EXISTS_RUN_WITH_PROPERTIES A (c::C) ==> 1652 (EXISTS_RUN_WITH_PROPERTIES A [c] /\ EXISTS_RUN_WITH_PROPERTIES A C))``, 1653 1654 REWRITE_TAC[EXISTS_RUN_WITH_PROPERTIES_def, A_BIGAND___A_SEM, A_BIGAND_def, A_SEM_def] THEN 1655 METIS_TAC[]); 1656 1657 1658 1659val A_NDET___INITIAL_ACCEPTANCE_SYM = 1660 store_thm 1661 ("A_NDET___INITIAL_ACCEPTANCE_SYM", 1662 ``!S S0 R p C. AUTOMATON_EQUIV 1663 (A_NDET (symbolic_semi_automaton S S0 R,A_AND (ACCEPT_COND_PROP p,A_BIGAND C))) 1664 (A_NDET (symbolic_semi_automaton S (P_AND(p, S0)) R,A_BIGAND C))``, 1665 1666 SIMP_TAC std_ss [AUTOMATON_EQUIV_def, A_SEM_def, ACCEPT_COND_PROP_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 1667 IS_TRANSITION_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, ACCEPT_COND_SEM_def, 1668 ACCEPT_COND_SEM_TIME_def, P_SEM_def] THEN 1669 REPEAT GEN_TAC THEN EXISTS_EQ_STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC); 1670 1671 1672 1673val A_UNIV___INITIAL_ACCEPTANCE_SYM = 1674 store_thm 1675 ("A_UNIV___INITIAL_ACCEPTANCE_SYM", 1676 ``!S S0 R p C. AUTOMATON_EQUIV 1677 (A_UNIV (symbolic_semi_automaton S S0 R,A_IMPL (ACCEPT_COND_PROP p,A_BIGAND C))) 1678 (A_UNIV (symbolic_semi_automaton S (P_AND(p, S0)) R,A_BIGAND C))``, 1679 1680 SIMP_TAC std_ss [AUTOMATON_EQUIV_def, A_SEM_def, ACCEPT_COND_PROP_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 1681 IS_TRANSITION_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, ACCEPT_COND_SEM_def, 1682 ACCEPT_COND_SEM_TIME_def, P_SEM_def, A_UNIV_def, A_IMPL_def, A_OR_def] THEN 1683 METIS_TAC[]); 1684 1685 1686 1687val ACCEPT_COND_RESTN_SEM = 1688 store_thm 1689 ("ACCEPT_COND_RESTN_SEM", 1690 ``!f v t1 t2. ((ACCEPT_COND_SEM_TIME (t1+t2) v f) = (ACCEPT_COND_SEM_TIME t1 (PATH_RESTN v t2) f))``, 1691 1692 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THENL [ 1693 SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def, PATH_RESTN_def], 1694 SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def], 1695 ASM_SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def], 1696 ASM_SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def], 1697 1698 ASM_SIMP_TAC std_ss [ACCEPT_COND_SEM_TIME_def] THEN 1699 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1700 rename1 `t3 >= t1` THEN 1701 `t3 + t2 >= t1 + t2` by DECIDE_TAC THEN 1702 PROVE_TAC[], 1703 1704 rename1 `t3 >= t1 + t2` THEN 1705 `?t. t = (t3 - t2)` by METIS_TAC[] THEN 1706 `(t3 = t + t2) /\ (t >= t1)` by DECIDE_TAC THEN 1707 PROVE_TAC[] 1708 ] 1709 ]); 1710 1711 1712val ID_AUTOMATON_SEM = 1713 store_thm( 1714 "ID_AUTOMATON_SEM", 1715 ``!a. AUTOMATON_EQUIV a (A_NDET(ID_SEMI_AUTOMATON, a))``, 1716 1717 SIMP_TAC std_ss [AUTOMATON_EQUIV_def, EMPTY_PATH_def, A_SEM_def, 1718 ID_SEMI_AUTOMATON_RUN, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1719 ID_SEMI_AUTOMATON_REWRITES, UNION_EMPTY, DIFF_EMPTY] THEN 1720 METIS_TAC[]); 1721 1722 1723 1724 1725 1726 1727val A_NDET___SIMPLIFIED_SEMI_AUTOMATON_THM = 1728 store_thm ( 1729 "A_NDET___SIMPLIFIED_SEMI_AUTOMATON_THM", 1730 1731``!A A' f ac. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON A' A f /\ 1732 (DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A)) (ACCEPT_COND_USED_VARS ac)) ==> 1733 (!i. A_SEM i (A_NDET (A, ACCEPT_COND ac)) = 1734 A_SEM i (A_NDET (A', ACCEPT_COND (ACCEPT_VAR_RENAMING 1735 (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A then f x else x)) ac))))``, 1736 1737 1738SIMP_TAC std_ss [A_SEM_THM] THEN 1739REPEAT STRIP_TAC THEN 1740ASSUME_TAC IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS2 THEN 1741Q_SPECL_NO_ASSUM 0 [`A'`, `A`, `f`] THEN 1742PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 1743ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 1744EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1745 1746 Q_TAC EXISTS_TAC `\n. w n UNION (IMAGE f (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A))` THEN 1747 `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 1748 REPEAT STRIP_TAC THENL [ 1749 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_IMAGE, IN_INTER, SUBSET_REFL] THEN 1750 METIS_TAC[], 1751 1752 REMAINS_TAC `PATH_RESTRICT (\n. 1753 w n UNION IMAGE f (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A)) 1754 A.S = w` THEN1 ( 1755 ASM_REWRITE_TAC[] 1756 ) THEN 1757 1758 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 1759 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 1760 SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, IN_UNION, 1761 IN_IMAGE, IN_DIFF, IN_SING, PATH_RESTRICT_def, PATH_MAP_def, 1762 IN_INTER, PATH_SUBSET_def, SUBSET_DEF, SUBSET_REFL] THEN 1763 METIS_TAC[], 1764 1765 SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, IN_UNION, 1766 IN_IMAGE, IN_DIFF, IN_SING, PATH_RESTRICT_def, PATH_MAP_def, 1767 IN_INTER, PATH_SUBSET_def, SUBSET_DEF, SUBSET_REFL] THEN 1768 METIS_TAC[], 1769 1770 1771 SIMP_ALL_TAC std_ss [ACCEPT_COND___VAR_RENAMING___NOT_INJ, 1772 ACCEPT_COND_SEM_def] THEN 1773 UNDISCH_NO_TAC 1 THEN 1774 ONCE_REWRITE_TAC[ACCEPT_COND_USED_VARS_INTER_THM] THEN 1775 IMP_TO_EQ_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN 1776 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 1777 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 1778 SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, 1779 PATH_SUBSET_def, SUBSET_DEF, SUBSET_REFL, DISJOINT_DISJ_THM] THEN 1780 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1781 IN_UNION, IN_DIFF, IN_ABS, IN_IMAGE, 1782 symbolic_semi_automaton_REWRITES, IN_INTER, IN_SING, 1783 PATH_RESTRICT_def, PATH_MAP_def, SEMI_AUTOMATON_USED_INPUT_VARS_def] THEN 1784 METIS_TAC[] 1785 ], 1786 1787 1788 Q_TAC EXISTS_TAC `PATH_RESTRICT w A.S` THEN 1789 ASM_REWRITE_TAC[] THEN 1790 SIMP_ALL_TAC std_ss [ACCEPT_COND___VAR_RENAMING___NOT_INJ, 1791 ACCEPT_COND_SEM_def] THEN 1792 UNDISCH_NO_TAC 0 THEN 1793 ONCE_REWRITE_TAC[ACCEPT_COND_USED_VARS_INTER_THM] THEN 1794 IMP_TO_EQ_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN 1795 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 1796 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 1797 SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, 1798 PATH_SUBSET_def, SUBSET_DEF, DISJOINT_DISJ_THM] THEN 1799 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1800 IN_UNION, IN_DIFF, IN_ABS, IN_IMAGE, 1801 symbolic_semi_automaton_REWRITES, IN_INTER, IN_SING, 1802 PATH_RESTRICT_def, PATH_MAP_def, SEMI_AUTOMATON_USED_INPUT_VARS_def] THEN 1803 METIS_TAC[] 1804]); 1805 1806 1807 1808 1809val A_UNIV___SIMPLIFIED_SEMI_AUTOMATON_THM = 1810 store_thm ( 1811 "A_UNIV___SIMPLIFIED_SEMI_AUTOMATON_THM", 1812 1813``!A A' f ac. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON A' A f /\ 1814 (DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A)) (ACCEPT_COND_USED_VARS ac)) ==> 1815 (!i. A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = 1816 A_SEM i (A_UNIV (A', ACCEPT_COND (ACCEPT_VAR_RENAMING 1817 (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A then f x else x)) ac))))``, 1818 1819 REPEAT STRIP_TAC THEN 1820 REWRITE_TAC[A_UNIV_def] THEN 1821 ONCE_REWRITE_TAC[A_SEM_def] THEN 1822 SIMP_TAC std_ss [] THEN 1823 SUBGOAL_TAC `!A ac i. A_SEM i (A_NDET (A, A_NOT (ACCEPT_COND ac))) = 1824 A_SEM i (A_NDET (A, ACCEPT_COND (ACCEPT_NOT ac)))` THEN1 ( 1825 SIMP_TAC std_ss [A_SEM_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def] 1826 ) THEN 1827 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1828 1829 ASSUME_TAC A_NDET___SIMPLIFIED_SEMI_AUTOMATON_THM THEN 1830 Q_SPECL_NO_ASSUM 0 [`A`, `A'`, `f`, `ACCEPT_NOT ac`] THEN 1831 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1832 ASM_SIMP_TAC std_ss [ACCEPT_COND_USED_VARS_def] 1833 ) THEN 1834 ASM_SIMP_TAC std_ss [ACCEPT_VAR_RENAMING_def]); 1835 1836 1837 1838val _ = export_theory(); 1839