1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val base_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat base_dir "src/tools") :: (concat base_dir "src/deep_embeddings") :: !loadPath; 8map load 9 ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory", 10 "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory", 11 "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "temporal_deep_mixedTheory", 12 "pairTheory", "symbolic_kripke_structureTheory", 13 "numLib", "semi_automatonTheory", "omega_automatonTheory", 14 "kripke_structureTheory", "containerTheory", "relationTheory"]; 15*) 16 17open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory 18 prop_logicTheory 19 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory 20 pred_setTheory rich_listTheory set_lemmataTheory temporal_deep_mixedTheory pairTheory symbolic_kripke_structureTheory 21 numLib semi_automatonTheory omega_automatonTheory kripke_structureTheory 22 containerTheory relationTheory; 23open Sanity; 24 25val _ = hide "K"; 26val _ = hide "S"; 27val _ = hide "I"; 28 29 30(* 31show_assums := false; 32show_assums := true; 33show_types := true; 34show_types := false; 35quietdec := false; 36*) 37 38 39val _ = new_theory "omega_automaton_translations"; 40 41 42 43 44val DETERMINISED_SEMI_AUTOMATON_def = 45 Define 46 `DETERMINISED_SEMI_AUTOMATON A = 47 (semi_automaton (POW A.S) A.I ((\(s, i). (i SUBSET A.I) /\ 48 (!x. (x IN s) = ((x, i) IN A.S0)))) 49 (\(s1, i, s2, i'). (s1 SUBSET A.S /\ i SUBSET A.I /\ 50 (!x. x IN s2 = (?s1'. s1' IN s1 /\ (s1', i, x, i') IN A.R)))))`; 51 52 53val DETERMINISED_SEMI_AUTOMATON___IS_DET_TOTAL = 54 store_thm ( 55 "DETERMINISED_SEMI_AUTOMATON___IS_DET_TOTAL", 56 ``!A. IS_DET_TOTAL_SEMI_AUTOMATON (DETERMINISED_SEMI_AUTOMATON A)``, 57 58 SIMP_TAC std_ss [IS_DET_TOTAL_SEMI_AUTOMATON_def, 59 DETERMINISED_SEMI_AUTOMATON_def, 60 semi_automaton_REWRITES, SING, 61 IN_POW, 62 EXISTS_UNIQUE_THM, 63 INTER_SUBSET, 64 prove(``!P s i i' s'. ((s, i, s', i') IN \(s, i, s', i'). P s i s' i') = P s i s' i'``, 65 SIMP_TAC std_ss [IN_DEF]), 66 prove(``!P s i. ((s, i) IN \(s, i). P s i) = P s i``, 67 SIMP_TAC std_ss [IN_DEF]) 68 ] THEN 69 REPEAT STRIP_TAC THENL [ 70 Q_TAC EXISTS_TAC `\x. (x, i INTER A.I) IN A.S0` THEN 71 SIMP_TAC std_ss [IN_DEF], 72 73 ASM_SIMP_TAC std_ss [EXTENSION], 74 75 Q_TAC EXISTS_TAC `\x. (?s1'. s1' IN s /\ (s1',i,x, i') IN A.R)` THEN 76 SIMP_TAC std_ss [IN_DEF], 77 78 METIS_TAC[EXTENSION] 79 ]); 80 81 82val SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE_def = 83 Define 84 `SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE (A:('a, 'a) semi_automaton) = 85 (kripke_structure (A.S CROSS (POW A.I)) A.S0 86 (\((s1, i1),(s2, i2)). (s1, i1, s2, i2) IN A.R /\ i1 SUBSET A.I /\ i2 SUBSET A.I) 87 (A.S UNION A.I) (\(s,i). s INSERT i))`; 88 89 90 91 92val SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE___IS_WELL_FORMED = 93 store_thm ( 94 "SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE___IS_WELL_FORMED", 95 ``!A. IS_WELL_FORMED_SEMI_AUTOMATON A ==> 96 IS_WELL_FORMED_KRIPKE_STRUCTURE (SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE A)``, 97 98 SIMP_TAC std_ss [IS_WELL_FORMED_KRIPKE_STRUCTURE_def, 99 SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE_def, 100 kripke_structure_REWRITES, SUBSET_DEF, 101 IN_CROSS, IN_POW, 102 IS_WELL_FORMED_SEMI_AUTOMATON_def] THEN 103 GEN_TAC THEN STRIP_TAC THEN 104 STRIP_TAC THEN1 ( 105 PROVE_TAC[FINITE_CROSS, FINITE_POW_IFF] 106 ) THEN 107 STRIP_TAC THEN1 ( 108 ASM_SIMP_TAC std_ss [FINITE_UNION] 109 ) THEN 110 STRIP_TAC THEN1 ( 111 PROVE_TAC[] 112 ) THEN 113 STRIP_TAC THENL [ 114 GEN_TAC THEN 115 Cases_on `x` THEN Cases_on `r` THEN Cases_on `q` THEN 116 SIMP_ALL_TAC std_ss [IN_DEF] THEN 117 METIS_TAC[FST, SND], 118 119 Cases_on `s` THEN 120 SIMP_TAC std_ss [IN_UNION, IN_INSERT] THEN 121 PROVE_TAC[] 122 ]); 123 124 125val SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE___LANGUAGE_EQ = 126 store_thm ( 127 "SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE___LANGUAGE_EQ", 128 129 ``!A i p. 130 IS_WELL_FORMED_SEMI_AUTOMATON A ==> 131 (IS_RUN_THROUGH_SEMI_AUTOMATON A i p = 132 IS_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE (SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE A) 133 (\n. (p n, i n INTER A.I)))``, 134 135 SIMP_TAC std_ss [SEMI_AUTOMATON_TO_KRIPKE_STRUCTURE_def, 136 kripke_structure_REWRITES, 137 IS_RUN_THROUGH_SEMI_AUTOMATON_def, 138 IS_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE_def, 139 IS_PATH_THROUGH_KRIPKE_STRUCTURE_def, 140 IN_CROSS, IN_POW, 141 SUBSET_DEF, IS_WELL_FORMED_SEMI_AUTOMATON_def, 142 FORALL_AND_THM, 143 prove(``!x1 x2 x3 x4 P1 P2. 144 (((x1,x2),x3,x4) IN (\((x1,x2),x3,x4). P1 (x1,x2,x3,x4) /\ P2 x2 x4)) = 145 (P1 (x1,x2,x3,x4) /\ P2 x2 x4)``, SIMP_TAC std_ss [IN_DEF])] THEN 146 REPEAT STRIP_TAC THEN 147 REPEAT BOOL_EQ_STRIP_TAC THEN 148 METIS_TAC[FST, SND]); 149 150 151 152 153 154val SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON_def = 155 Define 156 `SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON (A:'a symbolic_semi_automaton) I = 157 (semi_automaton (POW A.S) I (\(s, i). s SUBSET A.S /\ i SUBSET I /\ 158 P_SEM (s UNION (i DIFF A.S)) A.S0) 159 (\(s1, i, s2, i'). ((s1 SUBSET A.S /\ s2 SUBSET A.S /\ i SUBSET I /\ i' SUBSET I /\ 160 XP_SEM A.R ((s1 UNION (i DIFF A.S)), s2 UNION (i' DIFF A.S))))))`; 161 162val SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___IS_WELL_FORMED = 163 store_thm ( 164 "SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___IS_WELL_FORMED", 165 166 ``!A I. (FINITE A.S /\ FINITE I) ==> 167 IS_WELL_FORMED_SEMI_AUTOMATON (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A I)``, 168 169 170 SIMP_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def, 171 SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON_def, 172 semi_automaton_REWRITES, 173 FINITE_POW_IFF, SUBSET_DEF, IN_POW, 174 IN_CROSS, FORALL_PROD] THEN 175 SIMP_TAC std_ss [IN_DEF]); 176 177 178val SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___LANGUAGE_EQ = 179 store_thm ( 180 "SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___LANGUAGE_EQ", 181 182 ``!A I i w. (!n. (i n INTER (SEMI_AUTOMATON_USED_INPUT_VARS A)) SUBSET I) ==> 183 184 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w = 185 IS_RUN_THROUGH_SEMI_AUTOMATON (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A I) i w)``, 186 187 REPEAT STRIP_TAC THEN 188 ASM_SIMP_TAC std_ss [ IS_TRANSITION_def, 189 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 190 IS_RUN_THROUGH_SEMI_AUTOMATON_def, 191 SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON_def, 192 semi_automaton_REWRITES, 193 PATH_SUBSET_def, 194 IN_POW, INTER_SUBSET, 195 IN_ABS, 196 INPUT_RUN_STATE_UNION_def, 197 INPUT_RUN_PATH_UNION_def, 198 prove (``!f x1 x2 x3 x4. (x1,x2,x3,x4) IN (\(s1,s2,s3,s4). f s1 s2 s3 s4) = f x1 x2 x3 x4``, SIMP_TAC std_ss [IN_DEF]), 199 prove (``!f x1 x2. (x1,x2) IN (\(s1,s2). f s1 s2) = f x1 x2 ``, SIMP_TAC std_ss [IN_DEF])] THEN 200 REPEAT BOOL_EQ_STRIP_TAC THEN 201 REMAINS_TAC `!n. (((w n UNION (i n DIFF A.S)) INTER (XP_USED_VARS A.R)) = 202 ((w n UNION ((i n INTER I) DIFF A.S)) INTER (XP_USED_VARS A.R))) /\ 203 (((w n UNION (i n DIFF A.S)) INTER (P_USED_VARS A.S0)) = 204 ((w n UNION ((i n INTER I) DIFF A.S)) INTER (P_USED_VARS A.S0)))` THEN1 ( 205 BINOP_TAC THENL [ 206 METIS_TAC[P_USED_VARS_INTER_THM], METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, SUBSET_REFL] 207 ] 208 ) THEN 209 SIMP_ALL_TAC std_ss [EXTENSION, SUBSET_DEF, IN_INTER, 210 IN_UNION, IN_DIFF, 211 SEMI_AUTOMATON_USED_INPUT_VARS_def, 212 XP_USED_VARS_def] THEN 213 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 214 METIS_TAC[]); 215 216 217 218 219 220 221 222 223 224 225 226 227 228(*============================================================================= 229= Connection to kripke_structures 230=============================================================================*) 231 232 233val SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def = 234 Define 235 `SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE (A:'a symbolic_semi_automaton) = 236 symbolic_kripke_structure A.S0 A.R`; 237 238val SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___RUN = 239 store_thm 240 ("SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___RUN", 241 ``!A i w. 242 ((IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w) = 243 ((PATH_SUBSET w A.S) /\ 244 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE A) (INPUT_RUN_PATH_UNION A i w)))``, 245 246 SIMP_TAC std_ss [PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 247 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 248 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 249 symbolic_kripke_structure_REWRITES, 250 IS_TRANSITION_def, 251 INPUT_RUN_PATH_UNION_def] THEN 252 PROVE_TAC[]); 253 254 255 256val SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH = 257 store_thm 258 ("SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH", 259 ``!A i. 260 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE A) i = 261 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i (PATH_RESTRICT i A.S))``, 262 263 SUBGOAL_TAC `!a b. ((a INTER b) UNION (a DIFF b)) = a` THEN1 ( 264 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] THEN 265 PROVE_TAC[] 266 ) THEN 267 ASM_SIMP_TAC std_ss [PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 268 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 269 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 270 symbolic_kripke_structure_REWRITES, 271 IS_TRANSITION_def, 272 INPUT_RUN_PATH_UNION_def, 273 INPUT_RUN_STATE_UNION_def, 274 PATH_RESTRICT_def, PATH_MAP_def, 275 PATH_SUBSET_def, INTER_SUBSET] THEN 276 PROVE_TAC[]); 277 278 279val SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT_def = 280 Define 281 `SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A = 282 SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT K (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE A)`; 283 284 285val SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT = 286 store_thm 287 ("SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT", 288 ``!K A. SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A = 289 symbolic_kripke_structure (P_AND(K.S0, A.S0)) (XP_AND(K.R, A.R))``, 290 291 SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT_def, 292 SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, 293 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 294 symbolic_kripke_structure_REWRITES]); 295 296 297 298val IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def= 299 Define 300 `(IS_RABIN_SCOTT_SUBSET_CONSTRUCTION (A:'a symbolic_semi_automaton) (A':'a symbolic_semi_automaton) (IV:'a set) (f:'a set->'a) (g:'a -> 'a set)) = 301 ((INJ f (POW A.S) UNIV /\ (DISJOINT (IMAGE f (POW A.S)) IV)) /\ 302 (!(z:'a set). ((z SUBSET A.S) ==> (g(f(z)) = z))) /\ 303 (A'.S = (IMAGE f (POW A.S))) /\ 304 (!i Z. (Z SUBSET A'.S) ==> (((P_SEM (INPUT_RUN_STATE_UNION A' i Z) A'.S0) = 305 (Z = {z | (z IN A'.S) /\ P_SEM (INPUT_RUN_STATE_UNION A i (g z)) A.S0})))) /\ 306 (!S1:('a set) S2:('a set) i1:('a set) i2:('a set). 307 (S1 SUBSET A'.S /\ S2 SUBSET A'.S) ==> 308 309 ((IS_TRANSITION A' S1 i1 S2 i2) = 310 (S2 = {s2 | (s2 IN A'.S /\ ?s1. (s1 IN S1 /\ IS_TRANSITION A (g s1) i1 (g s2) i2))}))))`; 311 312 313val RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def= 314(* by Sven Lamberti *) 315 Define 316 `RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f = 317 symbolic_semi_automaton 318 (IMAGE f (POW A.S)) 319 (P_FORALL (SET_TO_LIST A.S) (P_EQUIV(A.S0, VAR_RENAMING_HASHTABLE A.S f))) 320 (XP_NEXT_FORALL (SET_TO_LIST A.S) (XP_EQUIV( 321 XP_NEXT (VAR_RENAMING_HASHTABLE A.S f), 322 XP_CURRENT_EXISTS (SET_TO_LIST A.S) ( 323 XP_AND(A.R, XP_CURRENT (VAR_RENAMING_HASHTABLE A.S f))))))`; 324 325 326 327 328val RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_THM = 329 store_thm 330 ("RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_THM", 331(* by Sven Lamberti *) 332 ``!A A' IV f g. 333 334 (FINITE A.S /\ 335 (A' = RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f) /\ 336 (INJ f (POW A.S) UNIV /\ (DISJOINT (IMAGE f (POW A.S)) IV) /\ 337 (DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A))) /\ 338 (!(z:'a set). ((z SUBSET A.S) ==> (g(f(z)) = z)))) ==> 339 340 (IS_RABIN_SCOTT_SUBSET_CONSTRUCTION (A:'a symbolic_semi_automaton) (A':'a symbolic_semi_automaton) (IV:'a set) (f:'a set->'a) (g:'a -> 'a set))``, 341 342REPEAT GEN_TAC THEN 343ONCE_ASM_REWRITE_TAC [GSYM SYMBOLIC_SEMI_AUTOMATON___REWRITE] THEN 344REWRITE_TAC [symbolic_semi_automaton_11, SYMBOLIC_SEMI_AUTOMATON___REWRITE] THEN 345REPEAT STRIP_TAC THEN 346FULL_SIMP_TAC std_ss [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, 347 RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, SEMI_AUTOMATON_USED_VARS_def, 348 SEMI_AUTOMATON_USED_INPUT_VARS_def, symbolic_semi_automaton_REWRITES] THEN 349FULL_SIMP_TAC std_ss [DISJOINT_UNION_BOTH] THEN 350FULL_SIMP_TAC std_ss [DISJOINT_DIFF_ELIM, DISJOINT_UNION_BOTH] THEN 351 352 353SUBGOAL_TAC `!s. ~(f (s INTER A.S) IN A.S)` THEN1 ( 354 FULL_SIMP_TAC std_ss [DISJOINT_DEF, IMAGE_DEF, EXTENSION, IN_POW, IN_INTER, NOT_IN_EMPTY, GSPECIFICATION] THEN 355 PROVE_TAC[INTER_SUBSET] 356) THEN 357`!s s'. (s' SUBSET A.S) ==> ~(f (s INTER A.S) IN s')` by PROVE_TAC[SUBSET_DEF] THEN 358SUBGOAL_TAC `!l'' i s. ((f:'a set->'a) (l'' INTER A.S) IN (INPUT_RUN_STATE_UNION A' i s)) = (f (l'' INTER A.S) IN s)` THEN1 ( 359 ASM_SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF, IN_IMAGE, IN_POW] THEN 360 PROVE_TAC[INTER_SUBSET] 361) THEN 362SUBGOAL_TAC `!l. l SUBSET A.S ==> ((l INTER A.S) = l)` THEN1 ( 363 SIMP_TAC std_ss [SUBSET_DEF, EXTENSION, IN_INTER] THEN PROVE_TAC[] 364) THEN 365SUBGOAL_TAC `!s s' s''. (s DIFF s'' UNION s') INTER s'' = s' INTER s''` THEN1 ( 366 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] THEN PROVE_TAC[] 367) THEN 368 369SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_POW] THEN 370REPEAT STRIP_TAC THENL [ 371 ASM_SIMP_TAC std_ss [P_FORALL_SEM, SET_TO_LIST_INV, VAR_RENAMING_HASHTABLE_SEM, P_SEM_THM, IN_DIFF, EXTENSION, 372 GSPECIFICATION, IN_UNION] THEN 373 374 SUBGOAL_TAC `!l'. P_SEM (INPUT_RUN_STATE_UNION A' i Z DIFF A.S UNION l') A.S0 = 375 P_SEM (INPUT_RUN_STATE_UNION A i l') A.S0` THEN1 ( 376 ONCE_REWRITE_TAC [P_USED_VARS_INTER_THM] THEN 377 REPEAT GEN_TAC THEN 378 REMAINS_TAC `(INPUT_RUN_STATE_UNION A' i Z DIFF A.S UNION l') INTER P_USED_VARS A.S0 = 379 (INPUT_RUN_STATE_UNION A i l') INTER P_USED_VARS A.S0` THEN1 ( 380 ASM_SIMP_TAC std_ss [] 381 ) THEN 382 UNDISCH_HD_TAC THEN 383 SIMP_ALL_TAC std_ss [EXTENSION, IN_INTER, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF, 384 IN_IMAGE, IN_POW, SUBSET_DEF, GSYM SUBSET_COMPL_DISJOINT, IN_COMPL] THEN 385 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 386 METIS_TAC[] 387 ) THEN 388 389 ASM_REWRITE_TAC[] THEN 390 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 391 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 392 METIS_TAC[], 393 394 `?l':'a set. l' SUBSET A.S /\ ((x:'a) = f l')` by PROVE_TAC [SUBSET_DEF, IN_IMAGE, 395 IN_POW] THEN 396 METIS_TAC[], 397 398 METIS_TAC[SUBSET_DEF] 399 ], 400 401 METIS_TAC[SUBSET_DEF] 402 ], 403 404 405 ASM_SIMP_TAC std_ss [IS_TRANSITION_def, XP_CURRENT_FORALL_SEM, 406 XP_NEXT_FORALL_SEM, XP_CURRENT_EXISTS_SEM, VAR_RENAMING_HASHTABLE_SEM, 407 MEM_SET_TO_LIST, SET_TO_LIST_INV, XP_SEM___XP_NEXT, XP_SEM___XP_CURRENT, IN_UNION, 408 IN_DIFF, EXTENSION, GSPECIFICATION, XP_SEM_THM] THEN 409 SUBGOAL_TAC `!l' l''. XP_SEM A.R 410 (INPUT_RUN_STATE_UNION A' i1 S1 DIFF A.S UNION l', 411 INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') = 412 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 l', INPUT_RUN_STATE_UNION A i2 l'')` THEN1 ( 413 ONCE_REWRITE_TAC [XP_USED_VARS_INTER_THM] THEN 414 415 REPEAT GEN_TAC THEN 416 REMAINS_TAC `((INPUT_RUN_STATE_UNION A' i1 S1 DIFF A.S UNION l') INTER XP_USED_CURRENT_VARS A.R = 417 (INPUT_RUN_STATE_UNION A i1 l') INTER XP_USED_CURRENT_VARS A.R) /\ 418 ((INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') INTER XP_USED_X_VARS A.R = 419 (INPUT_RUN_STATE_UNION A i2 l'') INTER XP_USED_X_VARS A.R)` THEN1 ( 420 ASM_REWRITE_TAC[] 421 ) THEN 422 FULL_SIMP_TAC std_ss [EXTENSION, IN_INTER, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF, 423 IN_IMAGE, IN_POW, SUBSET_DEF, GSYM SUBSET_COMPL_DISJOINT, IN_COMPL, 424 XP_USED_VARS_def] THEN 425 METIS_TAC[] 426 ) THEN 427 ASM_SIMP_TAC std_ss [] THEN 428 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 429 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 430 METIS_TAC[], 431 432 `?l':'a set. l' SUBSET A.S /\ ((x:'a) = f l')` by PROVE_TAC [SUBSET_DEF, IN_IMAGE, 433 IN_POW] THEN 434 METIS_TAC[], 435 436 437 `?l':'a set. l' SUBSET A.S /\ ((s1:'a) = f l')` by PROVE_TAC [SUBSET_DEF, IN_IMAGE] THEN 438 `x' SUBSET A.S` by PROVE_TAC[SUBSET_DEF] THEN 439 METIS_TAC[] 440 ], 441 442 443 ASM_REWRITE_TAC[] THEN 444 SIMP_TAC std_ss [GSYM SUBSET_DEF] THEN 445 SUBGOAL_TAC `!x. ((f l' = f x) /\ x SUBSET A.S) = (x = l')` THEN1 ( 446 METIS_TAC [INJ_DEF, IN_POW, IN_UNIV] 447 ) THEN 448 ASM_SIMP_TAC std_ss [] THEN 449 METIS_TAC[SUBSET_DEF] 450 ] 451]); 452 453 454 455val RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS = 456 store_thm ( 457 "RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS", 458 ``!A f. (FINITE A.S /\ 459 DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A)) ==> 460 (SEMI_AUTOMATON_USED_INPUT_VARS 461 (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f) = 462 SEMI_AUTOMATON_USED_INPUT_VARS A)``, 463 464 REPEAT GEN_TAC THEN 465 ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, 466 SEMI_AUTOMATON_USED_INPUT_VARS_def, 467 symbolic_semi_automaton_REWRITES, 468 P_USED_VARS_EVAL, XP_USED_VARS_EVAL, 469 XP_COND_def, P_BIGOR___P_USED_VARS, 470 P_FORALL___P_USED_VARS, VAR_RENAMING_HASHTABLE_def, 471 XP_FORALL___XP_USED_VARS, 472 XP_EXISTS___XP_USED_VARS, 473 XP_USED_VARS_def, 474 XP_USED_VARS_EVAL, 475 XP_BIGOR___XP_USED_VARS, 476 SET_TO_LIST_INV, UNION_EMPTY, 477 P_PROP_SET_MODEL___P_USED_VARS] THEN 478 479 ONCE_REWRITE_TAC[EXTENSION] THEN 480 REPEAT STRIP_TAC THEN 481 482 ASM_SIMP_TAC std_ss [IN_UNION, IN_DIFF, 483 IN_LIST_BIGUNION, MEM_MAP, GSYM LEFT_EXISTS_AND_THM, 484 MEM_SET_TO_LIST, FINITE_POW_IFF, IMAGE_FINITE, 485 IN_IMAGE, P_USED_VARS_EVAL, IN_SING, 486 XP_USED_VARS_EVAL, 487 IN_POW, 488 P_PROP_SET_MODEL___P_USED_VARS, NOT_IN_EMPTY] THEN 489 490 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, IN_POW, 491 IN_IMAGE, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, 492 XP_USED_VARS_def] THEN 493 494 EQ_TAC THEN REPEAT STRIP_TAC THEN 495 METIS_TAC[SUBSET_DEF, IN_UNION]); 496 497 498val RABIN_SCOTT_SUBSET_CONSTRUCTION___EXISTS = 499 store_thm 500 ("RABIN_SCOTT_SUBSET_CONSTRUCTION___EXISTS", 501 ``!A IV. (INFINITE (UNIV:'a set) /\ FINITE A.S /\ FINITE (IV:'a set)) ==> (?f g A'. IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g)``, 502 503 REPEAT STRIP_TAC THEN 504 505 `?f. INJ f (POW A.S) UNIV /\ (DISJOINT (IMAGE f (POW A.S)) (IV UNION (SEMI_AUTOMATON_USED_INPUT_VARS A) UNION A.S))` 506 by METIS_TAC[POW_VARRENAMING_EXISTS, 507 FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, FINITE_UNION] THEN 508 SUBGOAL_THEN ``?g:('a -> 'a set). (!(z:'a set). ((z SUBSET (A:'a symbolic_semi_automaton).S) ==> (g(f(z)) = z)))`` STRIP_ASSUME_TAC THEN1 ( 509 EXISTS_TAC ``\z:'a. @x:'a set. ((x SUBSET (A:'a symbolic_semi_automaton).S) /\ (f x = z))`` THEN 510 REPEAT STRIP_TAC THEN 511 SIMP_TAC std_ss [] THEN 512 SELECT_ELIM_TAC THEN 513 REPEAT STRIP_TAC THENL [ 514 METIS_TAC[], 515 516 `x IN (POW A.S)` by METIS_TAC[IN_POW] THEN 517 `z IN (POW A.S)` by METIS_TAC[IN_POW] THEN 518 METIS_TAC[INJ_DEF] 519 ] 520 ) THEN 521 522 EXISTS_TAC ``f:'a set->'a`` THEN 523 EXISTS_TAC ``g:'a -> 'a set`` THEN 524 525 SUBGOAL_TAC `(DISJOINT (IMAGE f (POW A.S)) IV) /\ 526 (DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A))` THEN1 ( 527 528 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, DISJOINT_UNION_BOTH, DISJOINT_SYM] 529 ) THEN 530 531 PROVE_TAC[RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_THM]); 532 533 534 535val RABIN_SCOTT_SUBSET_CONSTRUCTION___IS_TOTAL_DET = 536 store_thm 537 ("RABIN_SCOTT_SUBSET_CONSTRUCTION___IS_TOTAL_DET", 538 ``!A A' IV f g. IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g ==> 539 IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A'``, 540 541SIMP_TAC std_ss [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, 542 IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_THM] THEN 543REPEAT STRIP_TAC THENL [ 544 FULL_SIMP_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 545 REPEAT STRIP_TAC THENL [ 546 547 `?Z. Z = {z | z IN A'.S /\ P_SEM (INPUT_RUN_STATE_UNION A i (g z)) A.S0}` by PROVE_TAC[] THEN 548 SUBGOAL_TAC `Z SUBSET A'.S` THEN1 ( 549 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] 550 ) THEN 551 EXISTS_TAC ``Z:'a set`` THEN 552 REPEAT STRIP_TAC THEN1 PROVE_TAC[] THEN 553 ASM_SIMP_TAC std_ss [], 554 555 METIS_TAC[] 556 ], 557 558 559 FULL_SIMP_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 560 REPEAT STRIP_TAC THENL [ 561 562 ONCE_REWRITE_TAC[TRANSITION_CURRENT_STATE_CLEANING] THEN 563 `?S1. s1 INTER A'.S = S1` by PROVE_TAC[] THEN 564 `?i1'. i1 UNION s1 = i1'` by PROVE_TAC[] THEN 565 ASM_REWRITE_TAC[] THEN 566 567 `?S2. S2 = {s2 | s2 IN A'.S /\ ?s1'. s1' IN S1 /\ 568 IS_TRANSITION A (g s1') i1' (g s2) i2}` by PROVE_TAC[] THEN 569 SUBGOAL_TAC `S1 SUBSET A'.S /\ S2 SUBSET A'.S` THEN1 ( 570 GSYM_NO_TAC 2 THEN 571 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_INTER] 572 ) THEN 573 EXISTS_TAC ``S2:'a set`` THEN 574 575 REPEAT STRIP_TAC THEN1 PROVE_TAC[] THEN 576 ASM_SIMP_TAC std_ss [], 577 578 METIS_TAC[TRANSITION_CURRENT_STATE_CLEANING, INTER_SUBSET] 579 ] 580]); 581 582 583 584val RABIN_SCOTT_SUBSET_CONSTRUCTION___UNIQUE_RUN = 585 store_thm 586 ("RABIN_SCOTT_SUBSET_CONSTRUCTION___UNIQUE_RUN", 587 ``!A A' IV f g. (IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g) ==> 588 (!i. ?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i w)``, 589 590 REPEAT STRIP_TAC THEN 591 `IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A'` by PROVE_TAC[RABIN_SCOTT_SUBSET_CONSTRUCTION___IS_TOTAL_DET] THEN 592 PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN]); 593 594 595val RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN = 596 store_thm 597 ("RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN", 598 ``!A A' IV f g i w'. (IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g) ==> (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i w' = 599 ((w' 0 = {z | 600 z IN A'.S /\ P_SEM (INPUT_RUN_STATE_UNION A (i 0) (g z)) A.S0}) /\ 601 (!n. w' (SUC n) = {s2 | 602 s2 IN A'.S /\ 603 ?s1. s1 IN (w' n) /\ IS_TRANSITION A (g s1) (i n) (g s2) (i (SUC n))})))``, 604 605 REWRITE_TAC [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 606 PATH_SUBSET_def, INPUT_RUN_PATH_UNION_def] THEN 607 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 608 METIS_TAC[], 609 610 STRIP_TAC THEN 611 SUBGOAL_TAC `(!n. w' n SUBSET A'.S)` THEN1 ( 612 Cases_on `n` THEN 613 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] 614 ) THEN 615 METIS_TAC[] 616 ]); 617 618 619 620val RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN_SUBSET = 621 store_thm 622 ("RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN_SUBSET", 623 ``!A A' IV f g i w w'. ((IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g) /\ 624 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w /\ IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i w') ==> 625 (!n. (f (w n)) IN w' n)``, 626 627 REPEAT STRIP_TAC THEN 628 `(w' 0 = {z | z IN A'.S /\ 629 P_SEM (INPUT_RUN_STATE_UNION A (i 0) (g z)) A.S0}) /\ 630 (!n. w' (SUC n) = {s2 | s2 IN A'.S /\ 631 ?s1. s1 IN (w' n) /\ IS_TRANSITION A (g s1) (i n) (g s2) (i (SUC n))})` by 632 METIS_TAC[RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN] THEN 633 Induct_on `n` THEN ( 634 FULL_SIMP_TAC std_ss [IN_POW, 635 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, GSPECIFICATION, IN_IMAGE, 636 IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, PATH_SUBSET_def] THEN 637 METIS_TAC[] 638 )); 639 640 641val RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN_REACHABLE = 642 store_thm 643 ("RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN_REACHABLE", 644 ``!A A' IV f g i w'. ((IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g) /\ IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i w') ==> 645 (!n s. (f s IN w' n /\ s SUBSET A.S) = (?w. (PATH_SUBSET w A.S) /\ P_SEM (INPUT_RUN_PATH_UNION A i w 0) A.S0 /\ (w n = s) /\ !m. m < n ==> (IS_TRANSITION A (w m) (i m) (w (SUC m)) (i (SUC m)))))``, 646 647 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 648 FULL_SIMP_TAC std_ss [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, 649 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def] THEN 650 UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN 651 SPEC_TAC (``s:'a set``, ``s:'a set``) THEN 652 Induct_on `n` THEN 653 REPEAT STRIP_TAC THENL [ 654 EXISTS_TAC ``\n:num. (s:'a set)`` THEN 655 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def] THEN 656 `w' 0 = {z | 657 z IN A'.S /\ P_SEM (INPUT_RUN_STATE_UNION A (i 0) (g z)) A.S0}` by 658 METIS_TAC[] THEN 659 FULL_SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN 660 PROVE_TAC[EXTENSION], 661 662 663 REPEAT STRIP_TAC THEN 664 `(!n. w' (SUC n) = {s2 | s2 IN A'.S /\ 665 ?s1. s1 IN (w' n) /\ IS_TRANSITION A (g s1) (i n) (g s2) (i (SUC n))})` by METIS_TAC[] THEN 666 FULL_SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN 667 `s1 IN (IMAGE f (POW A.S))` by PROVE_TAC[SUBSET_DEF] THEN 668 SUBGOAL_TAC `?s1':'a set. (s1' SUBSET A.S) /\ (s1 = f (s1'))` THEN1 ( 669 REWRITE_ASSUMPTIONS_TAC [IN_IMAGE, IN_POW] THEN 670 PROVE_TAC[] 671 ) THEN 672 FULL_SIMP_TAC std_ss [] THEN 673 674 `?w. (!n. w n SUBSET A.S) /\ 675 P_SEM (INPUT_RUN_PATH_UNION A i w 0) A.S0 /\ (w n = s1') /\ 676 !m. 677 m < n ==> 678 IS_TRANSITION A (w m) (i m) (w (SUC m)) (i (SUC m))` by METIS_TAC[EXTENSION] THEN 679 EXISTS_TAC ``\m:num. if (m = SUC n) then (s:'a set) else (w m)`` THEN 680 REPEAT STRIP_TAC THENL [ 681 METIS_TAC[], 682 683 FULL_SIMP_TAC arith_ss [INPUT_RUN_PATH_UNION_def], 684 SIMP_TAC std_ss [], 685 686 Cases_on `m < n` THENL [ 687 FULL_SIMP_TAC arith_ss [], 688 689 `m = n` by DECIDE_TAC THEN 690 METIS_TAC[EXTENSION] 691 ] 692 ] 693 ], 694 695 696 UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN 697 SPEC_TAC (``s:'a set``, ``s:'a set``) THEN 698 SIMP_TAC std_ss [] THEN 699 `(w' 0 = {z | z IN A'.S /\ 700 P_SEM (INPUT_RUN_STATE_UNION A (i 0) (g z)) A.S0}) /\ 701 (!n. w' (SUC n) = {s2 | s2 IN A'.S /\ 702 ?s1. s1 IN (w' n) /\ IS_TRANSITION A (g s1) (i n) (g s2) (i (SUC n))})` by 703 METIS_TAC[RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN] THEN 704 705 Induct_on `n` THENL [ 706 FULL_SIMP_TAC arith_ss [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, 707 INPUT_RUN_PATH_UNION_def, IN_POW, GSPECIFICATION, IN_IMAGE, PATH_SUBSET_def] THEN 708 PROVE_TAC[], 709 710 REPEAT STRIP_TAC THEN 711 FULL_SIMP_TAC arith_ss [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def, IN_IMAGE, PATH_SUBSET_def, 712 INPUT_RUN_PATH_UNION_def, IN_POW, GSPECIFICATION] THEN 713 714 `n < SUC n /\ (!m. m < n ==> m < SUC n)` by DECIDE_TAC THEN 715 METIS_TAC[] 716 ], 717 718 PROVE_TAC[PATH_SUBSET_def] 719 ]); 720 721 722 723 724 725val SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___THM = 726 store_thm ("SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___THM", 727 728``!A A' IV f g p p'. 729(IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ 730IS_RABIN_SCOTT_SUBSET_CONSTRUCTION A A' IV f g /\ 731(!i s. s SUBSET A'.S ==> 732 ((P_SEM (INPUT_RUN_STATE_UNION A' i s) p') = 733 !s'. s' IN IMAGE g (s INTER (IMAGE f (POW A.S))) ==> 734 P_SEM (INPUT_RUN_STATE_UNION A i s') p)) 735) ==> 736!i. 737(A_SEM i (A_UNIV (A, ACCEPT_COND_G p)) = 738A_SEM i (A_UNIV (A', ACCEPT_COND_G p')))``, 739 740 741REPEAT STRIP_TAC THEN 742SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_G_def, ACCEPT_COND_SEM_def, 743 ACCEPT_COND_SEM_TIME_def] THEN 744EQ_TAC THEN REPEAT STRIP_TAC THEN rename1 `INPUT_RUN_PATH_UNION _ i w t` THENL [ 745 ASSUME_TAC RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN_REACHABLE THEN 746 Q_SPECL_NO_ASSUM 0 [`A`, `A'`, `IV`, `f`, `g`, `i`, `w`] THEN 747 PROVE_CONDITION_NO_ASSUM 0 THEN 748 ASM_REWRITE_TAC[] THEN 749 750 `IMAGE f (POW A.S) = A'.S` by 751 FULL_SIMP_TAC std_ss [IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def] THEN 752 `PATH_SUBSET w A'.S` by PROVE_TAC[IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 753 SUBGOAL_TAC `INPUT_RUN_PATH_UNION A' i w t' INTER IMAGE f (POW A.S) = 754 w t'` THEN1 ( 755 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 756 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, INPUT_RUN_PATH_UNION_def, 757 INPUT_RUN_STATE_UNION_def, SUBSET_DEF, IN_INTER, IN_UNION, IN_DIFF] THEN 758 METIS_TAC[] 759 ) THEN 760 `w t SUBSET A'.S` by PROVE_TAC[PATH_SUBSET_def] THEN 761 ASM_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN 762 NTAC 2 WEAKEN_HD_TAC THEN 763 764 SIMP_TAC std_ss [IN_IMAGE, IN_INTER] THEN 765 REPEAT STRIP_TAC THEN 766 `x IN IMAGE f (POW A.S)` by METIS_TAC[] THEN 767 FULL_SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 768 `g (f x') = x'` by METIS_TAC[IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def] THEN 769 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 770 771 REMAINS_TAC `?v. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i v /\ (v t = x')` THEN1 ( 772 METIS_TAC[INPUT_RUN_PATH_UNION_def] 773 ) THEN 774 775 Q_SPECL_NO_ASSUM 7 [`t`, `x'`] THEN 776 UNDISCH_HD_TAC THEN FULL_SIMP_TAC std_ss [] THEN STRIP_TAC THEN 777 ASSUME_TAC TOTAL_SYMBOLIC_SEMI_AUTOMATON_TRANS_FUNC THEN 778 Q_SPEC_NO_ASSUM 0 `A` THEN 779 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 780 781 SIMP_ALL_TAC std_ss [] THEN 782 783 784 `?v'. v' = CHOOSEN_PATH {x'} (\s1 n. {R_FUNC s1 (i (PRE n + t)) (i (n + t))})` by METIS_TAC[] THEN 785 786 Q_TAC EXISTS_TAC `\t2. if (t2 <= t) then w' t2 else v' (t2-t)` THEN 787 788 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, 789 INPUT_RUN_PATH_UNION_def] THEN 790 REPEAT STRIP_TAC THENL [ 791 Cases_on `t2 <= t` THEN ASM_REWRITE_TAC[] THEN 792 Q.ABBREV_TAC `t3 = t2 - t` THEN 793 WEAKEN_HD_TAC THEN 794 Induct_on `t3` THEN ( 795 ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_SING] 796 ), 797 798 799 Cases_on `SUC t2 <= t` THEN ASM_SIMP_TAC arith_ss [] THEN 800 Cases_on `t2 = t` THENL [ 801 `SUC t - t = SUC 0` by DECIDE_TAC THEN 802 `1 + t = SUC t` by DECIDE_TAC THEN 803 ASM_REWRITE_TAC [CHOOSEN_PATH_def] THEN 804 ASM_SIMP_TAC std_ss [IN_SING], 805 806 807 ASM_SIMP_TAC arith_ss [] THEN 808 `(SUC t2 - t = SUC (t2 - t)) /\ 809 (t + (t2 - t) = t2) /\ 810 ((SUC (t2 - t) + t) = SUC t2)` by DECIDE_TAC THEN 811 ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_SING] 812 ] 813 ], 814 815 816 817 `?w'. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i w'` by 818 METIS_TAC[RABIN_SCOTT_SUBSET_CONSTRUCTION___UNIQUE_RUN, 819 EXISTS_UNIQUE_THM] THEN 820 `P_SEM (INPUT_RUN_PATH_UNION A' i w' t) p'` by PROVE_TAC[] THEN 821 WEAKEN_NO_TAC 3 THEN 822 UNDISCH_HD_TAC THEN 823 ASM_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN 824 REPEAT STRIP_TAC THEN 825 826 `w' t SUBSET A'.S` by 827 METIS_TAC[IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 828 PATH_SUBSET_def] THEN 829 REMAINS_TAC `w t IN IMAGE g (w' t INTER IMAGE f (POW A.S))` THEN1 METIS_TAC[] THEN 830 WEAKEN_HD_TAC THEN 831 832 `f (w t) IN w' t` by METIS_TAC[ 833 RABIN_SCOTT_SUBSET_CONSTRUCTION___RUN_SUBSET] THEN 834 835 SIMP_TAC std_ss [IN_IMAGE, IN_INTER, IN_POW] THEN 836 Q_TAC EXISTS_TAC `f (w t)` THEN 837 838 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, 839 IS_RABIN_SCOTT_SUBSET_CONSTRUCTION_def] THEN 840 METIS_TAC[] 841]); 842 843 844 845 846 847val SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___CONCRETE_THM = 848 store_simp_thm ("SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___CONCRETE_THM", 849``!A p f A' p'. 850 (FINITE A.S /\ 851 IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ 852 (A' = RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f) /\ 853 (p' = (P_FORALL (SET_TO_LIST A.S) (P_IMPL( VAR_RENAMING_HASHTABLE A.S f, p)))) /\ 854 INJ f (POW A.S) UNIV /\ 855 DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p)) ==> 856 857((!i. 858(A_SEM i (A_UNIV (A, ACCEPT_COND_G p)) = 859A_SEM i (A_UNIV (A', ACCEPT_COND_G p')))) /\ 860IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A')``, 861 862 863REPEAT GEN_TAC THEN STRIP_TAC THEN 864SUBGOAL_TAC `?g. !x. (x SUBSET A.S) ==> (g (f x) = x)` THEN1 ( 865 PROVE_TAC[INJ_INVERSE, IN_POW] 866) THEN 867 868ASSUME_TAC RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_THM THEN 869Q_SPECL_NO_ASSUM 0 [`A`, `A'`, `EMPTY`, `f`, `g`] THEN 870PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 871 ASM_REWRITE_TAC[DISJOINT_EMPTY] THEN 872 METIS_TAC[DISJOINT_UNION_BOTH] 873) THEN 874 875STRIP_TAC THENL [ 876 ALL_TAC, 877 PROVE_TAC[RABIN_SCOTT_SUBSET_CONSTRUCTION___IS_TOTAL_DET] 878] THEN 879MATCH_MP_TAC SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___THM THEN 880 881EXISTS_TAC ``EMPTY`` THEN 882Q_TAC EXISTS_TAC `f` THEN 883Q_TAC EXISTS_TAC `g` THEN 884ASM_REWRITE_TAC[] THEN 885 886ASM_SIMP_TAC std_ss [P_FORALL_SEM, 887 SET_TO_LIST_INV, P_SEM_THM, 888 VAR_RENAMING_HASHTABLE_SEM, 889 RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, 890 symbolic_semi_automaton_REWRITES, 891 INPUT_RUN_STATE_UNION_def] THEN 892REPEAT STRIP_TAC THEN 893 894SUBGOAL_TAC `!l'. (l' SUBSET A.S) ==> 895 ((s UNION (i DIFF IMAGE f (POW A.S)) DIFF A.S UNION l') INTER A.S = l')` THEN1 ( 896 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, SUBSET_DEF] THEN 897 METIS_TAC[] 898) THEN 899ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 900 901SUBGOAL_TAC `!l'. (l' SUBSET A.S) ==> 902((f l' IN s UNION (i DIFF IMAGE f (POW A.S)) DIFF A.S UNION l') = (f l' IN s))` THEN1 ( 903 SIMP_ALL_TAC std_ss [EXTENSION, SUBSET_DEF, IN_UNION, IN_DIFF, 904 IN_IMAGE, IN_POW, DISJOINT_DISJ_THM, 905 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 906 METIS_TAC[] 907) THEN 908ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 909 910FORALL_EQ_STRIP_TAC THEN 911 912SIMP_TAC std_ss [IN_IMAGE, IN_INTER, IN_POW, 913 GSYM RIGHT_EXISTS_AND_THM] THEN 914 915`(?x'. (l' = g (f x')) /\ f x' IN s /\ x' SUBSET A.S) = 916 (l' SUBSET A.S /\ f l' IN s)` by METIS_TAC[] THEN 917ASM_REWRITE_TAC[AND_IMP_INTRO] THEN WEAKEN_HD_TAC THEN 918REPEAT BOOL_EQ_STRIP_TAC THEN 919 920ONCE_REWRITE_TAC [P_USED_VARS_INTER_THM] THEN 921AP_THM_TAC THEN AP_TERM_TAC THEN 922SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 923 IN_IMAGE, IN_POW] THEN 924REPEAT STRIP_TAC THEN 925REPEAT BOOL_EQ_STRIP_TAC THEN 926 927SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, SUBSET_DEF, 928 IN_IMAGE, IN_POW] THEN 929METIS_TAC[]); 930 931 932 933 934 935val NDET_F___TO___NDET_FG___THM = 936 store_simp_thm 937 ("NDET_F___TO___NDET_FG___THM", 938 939 ``!A A' p i. 940 (IS_EXPLICIT_PROP_ACCEPT_COND p /\ 941 EXPLICIT_ACCEPT_COND_USED_INPUT_VARS p SUBSET A.I /\ 942 (A' = (semi_automaton (A.S CROSS UNIV:bool set) A.I 943 (\((s, a),i). ((a = F) /\ ((s, i) IN A.S0))) 944 (\((s1, b1), i, (s2, b2), i'). (s1, i, s2, i') IN A.R /\ 945 (b2 = (b1 \/ EXPLICIT_PROP_ACCEPT_COND_SEM i s1 p)))))) ==> 946 947 ((EXISTENTIAL_OMEGA_AUTOMATON_SEM (A, EXPLICIT_ACCEPT_F p) i) = 948 (EXISTENTIAL_OMEGA_AUTOMATON_SEM (A', EXPLICIT_ACCEPT_FG (EXPLICIT_ACCEPT_STATE 949 (\(s,b). b))) i))``, 950 951 952SIMP_TAC std_ss [EXISTENTIAL_OMEGA_AUTOMATON_SEM_def, 953 EXPLICIT_ACCEPT_COND_SEM_def, 954 EXPLICIT_ACCEPT_COND_SEM_TIME_def, 955 EXPLICIT_ACCEPT_F_def, 956 EXPLICIT_ACCEPT_FG_def, 957 IS_RUN_THROUGH_SEMI_AUTOMATON_def, 958 semi_automaton_REWRITES, 959 EXPLICIT_PROP_ACCEPT_COND_SEM_THM, 960 IN_CROSS, IN_UNIV, IN_SING, 961prove (``!P. (?w:num->('a # 'b). P w) = (?w1 w2. P (\n. (w1 n, w2 n)))``, 962 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 963 Q_TAC EXISTS_TAC `\n. FST (w n)` THEN 964 Q_TAC EXISTS_TAC `\n. SND (w n)` THEN 965 SIMP_TAC std_ss [] THEN 966 METIS_TAC[], 967 968 METIS_TAC[] 969 ]), 970prove (``!P x1 x2 x3 x4 x5. (((x1, x2), x3, (x4, x5), x6) IN \((x1, x2), x3, (x4, x5), x6). P x1 x2 x3 x4 x5 x6) = P x1 x2 x3 x4 x5 x6``, SIMP_TAC std_ss [IN_DEF]), 971prove (``!P x1 x2. ((x1, x2) IN \(x1, x2). P x1 x2) = P x1 x2``, SIMP_TAC std_ss [IN_DEF]), 972prove (``!P x1 x2 x3. (((x1, x2), x3) IN \((x1, x2), x3). P x1 x2 x3) = P x1 x2 x3``, SIMP_TAC std_ss [IN_DEF]) 973] THEN 974REPEAT STRIP_TAC THEN 975SUBGOAL_TAC `!w. (?t'. EXPLICIT_PROP_ACCEPT_COND_SEM (i t') (w t') p) = 976 (?t'. EXPLICIT_PROP_ACCEPT_COND_SEM (i t' INTER A.I) (w t') p)` THEN1 ( 977 GEN_TAC THEN EXISTS_EQ_STRIP_TAC THEN 978 SIMP_TAC std_ss [EXPLICIT_PROP_ACCEPT_COND_SEM_def] THEN 979 SUBGOAL_TAC `(\n. i t' INTER A.I) = PATH_RESTRICT (\n. i t') A.I` THEN1 ( 980 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] 981 ) THEN 982 ASM_SIMP_TAC std_ss [] THEN 983 PROVE_TAC[EXPLICIT_ACCEPT_COND_USED_INPUT_VARS_INTER_SUBSET_THM] 984) THEN 985ASM_REWRITE_TAC[] THEN 986WEAKEN_HD_TAC THEN 987EQ_TAC THEN REPEAT STRIP_TAC THENL [ 988 rename1 `w t` THEN 989 SUBGOAL_TAC `?t'. EXPLICIT_PROP_ACCEPT_COND_SEM (i t' INTER A.I) (w t') p /\ 990 !t''. t'' < t' ==> ~EXPLICIT_PROP_ACCEPT_COND_SEM (i t'' INTER A.I) (w t'') p` THEN1 ( 991 Q_TAC (fn t => (ASSUME_TAC (EXISTS_LEAST_CONV t))) `?t'. EXPLICIT_PROP_ACCEPT_COND_SEM (i t' INTER A.I) (w t') p` THEN 992 METIS_TAC[] 993 ) THEN 994 Q_TAC EXISTS_TAC `w` THEN 995 Q_TAC EXISTS_TAC `\n. t' < n` THEN 996 ASM_SIMP_TAC std_ss [] THEN 997 REPEAT STRIP_TAC THENL [ 998 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 999 RIGHT_DISJ_TAC THEN 1000 `n = t'` by DECIDE_TAC THEN 1001 ASM_REWRITE_TAC[], 1002 1003 DECIDE_TAC, 1004 1005 `~(n < t')` by PROVE_TAC[] THEN 1006 DECIDE_TAC 1007 ], 1008 1009 EXISTS_TAC ``SUC t'`` THEN 1010 DECIDE_TAC 1011 ], 1012 1013 1014 rename1 `~(_ >= t') \/ _` THEN 1015 Q_TAC EXISTS_TAC `w1` THEN 1016 ASM_SIMP_TAC std_ss [] THEN 1017 SUBGOAL_TAC `?t. w2 t /\ !t'. t' < t ==> ~(w2 t')` THEN1 ( 1018 Q_TAC (fn t => (ASSUME_TAC (EXISTS_LEAST_CONV t))) `?t. w2 t` THEN 1019 `t' >= t'` by DECIDE_TAC THEN 1020 METIS_TAC[] 1021 ) THEN 1022 `~(t = 0)` by PROVE_TAC[] THEN 1023 `(SUC (PRE t) = t) /\ ((PRE t) < t)` by DECIDE_TAC THEN 1024 METIS_TAC[] 1025]); 1026 1027 1028 1029 1030val BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def = 1031 Define 1032 `BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON A S = 1033 (semi_automaton (POW A.S CROSS POW A.S) A.I 1034 (\(s,i). (i SUBSET A.I) /\ ((SND s) = EMPTY) /\ (!x. (x IN (FST s)) = ((x, i) IN A.S0))) 1035 (\((s11, s12), i, (s21, s22), i'). 1036 (i SUBSET A.I /\ i' SUBSET A.I /\ s11 SUBSET A.S /\ s12 SUBSET A.S /\ 1037 (!x. x IN s21 = (x IN A.S /\ (?s1'. s1' IN s11 /\ (s1', i, x, i') IN A.R))) /\ 1038 (((s12 = {}) /\ (s22 = s21 INTER S)) \/ 1039 (~(s12 = {}) /\ 1040 (!x. x IN s22 = (x IN S /\ x IN A.S /\ (?s1'. s1' IN s12 /\ (s1', i, x, i') IN A.R))))) 1041 )))`; 1042 1043 1044 1045val BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_DET_TOTAL = 1046 store_thm ( 1047 "BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_DET_TOTAL", 1048 ``!A S. IS_DET_TOTAL_SEMI_AUTOMATON (BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON A S)``, 1049 1050 SIMP_TAC std_ss [IS_DET_TOTAL_SEMI_AUTOMATON_def, 1051 BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 1052 semi_automaton_REWRITES, SING, IN_CROSS, 1053 IN_POW, 1054 EXISTS_UNIQUE_THM, 1055 prove(``!P s i s'. ((s, i, s', i') IN \((s11, s12), i, (s21, s22), i'). P s11 s12 i s21 s22 i') = P (FST s) (SND s) i (FST s') (SND s') i'``, 1056 Cases_on `s` THEN Cases_on `s'` THEN 1057 SIMP_TAC std_ss [IN_DEF]), 1058 prove(``(x, y) IN (\(x, y). P x y) = P x y``, SIMP_TAC std_ss [IN_DEF])] THEN 1059 REPEAT STRIP_TAC THENL [ 1060 Q_TAC EXISTS_TAC `((\x'. (x',i INTER A.I) IN A.S0), EMPTY:'b set)` THEN 1061 SIMP_TAC std_ss [IN_ABS, INTER_SUBSET], 1062 1063 Cases_on `x` THEN Cases_on `x'` THEN 1064 FULL_SIMP_TAC std_ss [EXTENSION], 1065 1066 1067 Cases_on `s` THEN 1068 FULL_SIMP_TAC std_ss [] THEN 1069 Cases_on `r = {}` THENL [ 1070 ASM_SIMP_TAC std_ss [EMPTY_SUBSET] THEN 1071 `?q'. q' = \x. (x IN A.S) /\ (?s1'. s1' IN q /\ (s1',i,x, i') IN A.R)` by METIS_TAC[] THEN 1072 Q_TAC EXISTS_TAC `(q', q' INTER S)` THEN 1073 ASM_SIMP_TAC std_ss [IN_DEF, SUBSET_DEF], 1074 1075 ASM_SIMP_TAC std_ss [] THEN 1076 `?q'. q' = (\x. x IN A.S /\ (?s1'. s1' IN q /\ (s1',i,x, i') IN A.R))` by METIS_TAC[] THEN 1077 `?r'. r' = \x. (x IN S /\ x IN A.S /\ (?s1'. s1' IN r /\ (s1',i,x, i') IN A.R))` by METIS_TAC[] THEN 1078 Q_TAC EXISTS_TAC `(q', r')` THEN 1079 ASM_SIMP_TAC std_ss [IN_DEF] 1080 ], 1081 1082 1083 Cases_on `s'` THEN Cases_on `s''` THEN 1084 FULL_SIMP_TAC std_ss [] THEN 1085 LEFT_CONJ_TAC THENL [ 1086 METIS_TAC[EXTENSION], 1087 ASM_REWRITE_TAC[] 1088 ], 1089 1090 Cases_on `s'` THEN Cases_on `s''` THEN 1091 FULL_SIMP_TAC std_ss [] THEN 1092 METIS_TAC[EXTENSION] 1093 ]); 1094 1095 1096 1097val BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_WELL_FORMED = 1098 store_thm ( 1099 "BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_WELL_FORMED", 1100 ``!A S. IS_WELL_FORMED_SEMI_AUTOMATON A ==> 1101 IS_WELL_FORMED_SEMI_AUTOMATON (BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON A S)``, 1102 1103 SIMP_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def, 1104 BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 1105 semi_automaton_REWRITES, SUBSET_DEF, 1106 IN_SING, IN_CROSS, IN_POW, 1107 NOT_IN_EMPTY, FINITE_CROSS, FINITE_POW_IFF, 1108 FORALL_PROD, FORALL_AND_THM] THEN 1109 SIMP_TAC std_ss [IN_DEF, FORALL_AND_THM, EMPTY_applied] THEN 1110 REPEAT STRIP_TAC THENL [ 1111 PROVE_TAC[], 1112 METIS_TAC[IN_INTER, IN_DEF], 1113 PROVE_TAC[] 1114 ]); 1115 1116 1117val NDET_FG___TO___DET_FG___THM = 1118 store_thm 1119 ("NDET_FG___TO___DET_FG___THM", 1120 1121 ``!A S i. IS_WELL_FORMED_SEMI_AUTOMATON A ==> 1122 ((EXISTENTIAL_OMEGA_AUTOMATON_SEM (A, EXPLICIT_ACCEPT_FG (EXPLICIT_ACCEPT_STATE S)) i) = 1123 (EXISTENTIAL_OMEGA_AUTOMATON_SEM (BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON A S, EXPLICIT_ACCEPT_FG (EXPLICIT_ACCEPT_STATE (\(s1, s2). (s1 SUBSET A.S) /\ (s2 SUBSET A.S) /\ ~(s2 = EMPTY)))) i))``, 1124 1125 1126 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1127 ASM_SIMP_TAC std_ss [BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_DET_TOTAL, 1128 BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_WELL_FORMED, 1129 IS_DET_TOTAL_SEMI_AUTOMATON___EXISTENTIAL_UNIVERSAL_SEM], 1130 ALL_TAC 1131 ] THEN 1132 UNDISCH_ALL_TAC THEN 1133 SIMP_ALL_TAC std_ss [EXISTENTIAL_OMEGA_AUTOMATON_SEM_def, 1134 UNIVERSAL_OMEGA_AUTOMATON_SEM_def, 1135 IS_RUN_THROUGH_SEMI_AUTOMATON_def, 1136 BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 1137 semi_automaton_REWRITES, IN_SING, IN_CROSS, 1138 EXPLICIT_ACCEPT_F_def, 1139 EXPLICIT_ACCEPT_FG_def, 1140 EXPLICIT_ACCEPT_COND_SEM_def, 1141 EXPLICIT_ACCEPT_COND_SEM_TIME_def, 1142 IN_POW, 1143 INTER_SUBSET, FORALL_AND_THM, 1144prove (``!P. (!w:num->('a # 'b). P w) = (!w1 w2. P (\n. (w1 n, w2 n)))``, 1145 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1146 PROVE_TAC[], 1147 1148 1149 Q_SPECL_NO_ASSUM 0 [`\n. FST (w n)`, `\n. SND (w n)`] THEN 1150 SIMP_ALL_TAC std_ss [] THEN 1151 METIS_TAC[] 1152 ]), 1153prove (``!P. (?w:num->('a # 'b). P w) = (?w1 w2. P (\n. (w1 n, w2 n)))``, 1154 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1155 Q_TAC EXISTS_TAC `\n. FST (w n)` THEN 1156 Q_TAC EXISTS_TAC `\n. SND (w n)` THEN 1157 SIMP_TAC std_ss [] THEN 1158 METIS_TAC[], 1159 1160 METIS_TAC[] 1161 ]), 1162prove(``!P x11 x12 i x21 x22 i'. (((x11,x12),i,(x21,x22),i') IN \((x11,x12),i,(x21,x22),i'). P x11 x12 i x21 x22 i') = P x11 x12 i x21 x22 i'``, SIMP_TAC std_ss [IN_DEF]), 1163prove (``!P x1 x2. ((x1, x2) IN \(x1, x2). P x1 x2) = P x1 x2``, SIMP_TAC std_ss [IN_DEF])] THEN 1164 REPEAT STRIP_TAC THENL [ 1165 1166 rename1 `~(_ >= t1) \/ _` THEN 1167 SUBGOAL_TAC `!n. w n IN w1 n` THEN1 ( 1168 Induct_on `n` THEN ( 1169 METIS_TAC[] 1170 ) 1171 ) THEN 1172 CCONTR_TAC THEN 1173 FULL_SIMP_TAC std_ss [] THEN 1174 `?u. (u >= t1) /\ (w2 u = {})` by METIS_TAC[] THEN 1175 SUBGOAL_TAC `!n. w ((SUC u) + n) IN w2 ((SUC u) + n)` THEN1 ( 1176 Induct_on `n` THENL [ 1177 ASM_SIMP_TAC std_ss [] THEN 1178 Q_SPEC_NO_ASSUM 4 `u` THEN 1179 UNDISCH_HD_TAC THEN 1180 ASM_SIMP_TAC std_ss [IN_INTER] THEN 1181 `SUC u >= t1` by DECIDE_TAC THEN 1182 PROVE_TAC[], 1183 1184 1185 Q_SPEC_NO_ASSUM 5 `SUC u + n` THEN 1186 `(SUC u + SUC n) = SUC((SUC u + n))` by DECIDE_TAC THEN 1187 `~(w2 (SUC u + n) = EMPTY)` by PROVE_TAC[MEMBER_NOT_EMPTY] THEN 1188 FULL_SIMP_TAC std_ss [] THEN 1189 `SUC (SUC u + n) >= t1` by DECIDE_TAC THEN 1190 PROVE_TAC[] 1191 ] 1192 ) THEN 1193 Q_SPEC_NO_ASSUM 3 `SUC u` THEN 1194 SIMP_ALL_TAC std_ss [] THEN 1195 rename1 `w2 t2 = EMPTY` THEN 1196 Q_SPEC_NO_ASSUM 2 `t2 - SUC u` THEN 1197 `SUC u + (t2 - SUC u) = t2` by DECIDE_TAC THEN 1198 FULL_SIMP_TAC std_ss [] THEN 1199 PROVE_TAC[MEMBER_NOT_EMPTY], 1200 1201 1202 1203 1204 1205 rename1 `~(_ >= t1) \/ _` THEN 1206 Q.ABBREV_TAC `R = (\(s1, n1) (s2, n2). (n2 = SUC n1) /\ 1207 (s1, i n1 INTER A.I, s2, i n2 INTER A.I) IN A.R /\ 1208 (n1 >= t1 ==> s2 IN S))` THEN 1209 REMAINS_TAC `(!x. FINITE {y | R x y}) /\ 1210 (?s0. ((s0, i 0 INTER A.I) IN A.S0) /\ (~FINITE {y | RTC R (s0,0) y}))` THEN1 ( 1211 `?f. (f 0 = (s0, 0)) /\ !n. R (f n) (f (SUC n))` by METIS_TAC[KoenigsLemma] THEN 1212 Q_TAC EXISTS_TAC `\n. FST (f n)` THEN 1213 NTAC 2 UNDISCH_HD_TAC THEN 1214 GSYM_NO_TAC 3 (*Def R*) THEN 1215 ASM_SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [FORALL_AND_THM] THEN 1216 DISCH_TAC THEN DISCH_TAC THEN 1217 SUBGOAL_TAC `!n. SND (f n) = n` THEN1 ( 1218 Induct_on `n` THEN ASM_REWRITE_TAC[] 1219 ) THEN 1220 FULL_SIMP_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def, SUBSET_DEF, IN_CROSS, 1221 IN_POW] THEN 1222 REPEAT STRIP_TAC THENL [ 1223 METIS_TAC[FST, SND], 1224 1225 EXISTS_TAC ``SUC t1`` THEN 1226 GEN_TAC THEN RIGHT_DISJ_TAC THEN 1227 rename1 `FST (f t2) IN S` THEN 1228 `(PRE t2 >= t1) /\ (SUC (PRE t2) = t2)` by DECIDE_TAC THEN 1229 PROVE_TAC[] 1230 ] 1231 ) THEN 1232 REPEAT STRIP_TAC THENL [ 1233 GSYM_NO_TAC 0 (*Def R*) THEN 1234 SIMP_ALL_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def, 1235 SUBSET_DEF, IN_CROSS] THEN 1236 REMAINS_TAC `{y | R x y} SUBSET A.S CROSS {SUC (SND x)}` THEN1 ( 1237 PROVE_TAC[SUBSET_FINITE, FINITE_CROSS, FINITE_SING] 1238 ) THEN 1239 ASM_SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [SUBSET_DEF, GSPECIFICATION, IN_CROSS, IN_SING] THEN 1240 METIS_TAC[FST, SND], 1241 1242 1243 1244 1245 Q.ABBREV_TAC `P = (\s0 y. (?w. IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w (FST y) (SND y) /\ (w 0 = s0) /\ (!n. ((n > t1) /\ (SND y >= n)) ==> w n IN S)))` THEN 1246 SUBGOAL_TAC `!s0. ((s0, i 0 INTER A.I) IN A.S0 /\ ~FINITE {y | RTC R (s0,0) y}) = 1247 ((s0, i 0 INTER A.I) IN A.S0 /\ ~FINITE {y | P s0 y})` THEN1 ( 1248 GSYM_NO_TAC 0 (*Def P*) THEN 1249 ASM_REWRITE_TAC[] THEN 1250 REPEAT STRIP_TAC THEN 1251 BOOL_EQ_STRIP_TAC THEN 1252 REPEAT AP_TERM_TAC THEN 1253 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 1254 SIMP_TAC std_ss [] THEN 1255 GEN_TAC THEN 1256 1257 ASM_SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE_def] THEN 1258 Induct_on `SND x` THENL [ 1259 GSYM_NO_TAC 2 (*Def R*) THEN 1260 Cases_on `x` THEN 1261 ONCE_REWRITE_TAC[RTC_CASES2] THEN 1262 ASM_SIMP_TAC (arith_ss++pairSimps.gen_beta_ss) [] THEN 1263 REPEAT STRIP_TAC THEN 1264 GSYM_NO_TAC 0 THEN 1265 ASM_SIMP_TAC arith_ss [] THEN 1266 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1267 Q_TAC EXISTS_TAC `\n:num. s0` THEN 1268 FULL_SIMP_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def, SUBSET_DEF, IN_CROSS] THEN 1269 PROVE_TAC[FST], 1270 1271 NTAC 2 (GSYM_NO_TAC 1) THEN 1272 ASM_REWRITE_TAC[] 1273 ], 1274 1275 1276 Cases_on `x` THEN 1277 ONCE_REWRITE_TAC[RTC_CASES2] THEN 1278 SIMP_TAC arith_ss [] THEN 1279 REPEAT STRIP_TAC THEN 1280 SUBGOAL_TAC `!y. (RTC R (s0,0) y /\ R y (q,r)) = 1281 ((?w. 1282 ((!n. n <= SND y ==> w n IN A.S) /\ (w 0, i 0 INTER A.I) IN A.S0 /\ 1283 (w (SND y) = FST y) /\ 1284 !n. 1285 n < SND y ==> 1286 (w n,i n INTER A.I,w (SUC n), i (SUC n) INTER A.I) IN A.R) /\ 1287 (w 0 = s0) /\ (!n. ((n > t1) /\ (SND y >= n)) ==> w n IN S)) /\ (R y (q,r)))` THEN1 ( 1288 1289 SUBGOAL_TAC `!y. R y (q,r) ==> (v = SND y)` THEN1 ( 1290 GSYM_NO_TAC 4 (*Def R*) THEN 1291 ASM_SIMP_TAC (arith_ss++pairSimps.gen_beta_ss) [] 1292 ) THEN 1293 1294 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 1295 STRIP_TAC THEN 1296 RES_TAC THEN 1297 Q_SPEC_NO_ASSUM 6 `y` THEN 1298 UNDISCH_HD_TAC THEN 1299 ASM_SIMP_TAC std_ss [], 1300 1301 METIS_TAC[] 1302 ] 1303 ) THEN 1304 ASM_REWRITE_TAC[] THEN 1305 WEAKEN_HD_TAC THEN 1306 GSYM_NO_TAC 0 (*Def r*) THEN 1307 GSYM_NO_TAC 4 (*Def R*) THEN 1308 ASM_SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [] THEN 1309 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1310 GSYM_NO_TAC 2 (*Def v*) THEN 1311 FULL_SIMP_TAC std_ss [] THEN 1312 Q_TAC EXISTS_TAC `\m. if (m = SUC v) then q else (w m)` THEN 1313 ASM_SIMP_TAC arith_ss [] THEN 1314 REPEAT STRIP_TAC THENL [ 1315 Cases_on `n = SUC v` THENL [ 1316 SIMP_ALL_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def, 1317 SUBSET_DEF, IN_CROSS] THEN 1318 ASM_SIMP_TAC std_ss [] THEN 1319 METIS_TAC[FST, SND], 1320 1321 `n <= v` by DECIDE_TAC THEN 1322 ASM_SIMP_TAC std_ss [] 1323 ], 1324 1325 Cases_on `n < v` THENL [ 1326 ASM_SIMP_TAC arith_ss [], 1327 1328 `n = v` by DECIDE_TAC THEN 1329 ASM_SIMP_TAC std_ss [] 1330 ], 1331 1332 Cases_on `v >= n` THEN 1333 ASM_SIMP_TAC arith_ss [] 1334 ], 1335 1336 1337 Q_TAC EXISTS_TAC `(w v, v)` THEN 1338 ASM_SIMP_TAC std_ss [] THEN 1339 REPEAT STRIP_TAC THENL [ 1340 Q_TAC EXISTS_TAC `w` THEN 1341 ASM_SIMP_TAC arith_ss [], 1342 1343 `v < SUC v` by DECIDE_TAC THEN 1344 METIS_TAC[], 1345 1346 `(SUC v > t1) /\ (SUC v >= SUC v)` by DECIDE_TAC THEN 1347 METIS_TAC[] 1348 ] 1349 ] 1350 ] 1351 ) THEN 1352 ASM_SIMP_TAC std_ss [] THEN 1353 WEAKEN_HD_TAC THEN 1354 WEAKEN_NO_TAC 1 (*Def R*) THEN 1355 CCONTR_TAC THEN 1356 SIMP_ALL_TAC std_ss [IS_WELL_FORMED_SEMI_AUTOMATON_def] THEN 1357 1358 SUBGOAL_TAC `!n x. x IN w1 n ==> (?w. IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w x n)` THEN1 ( 1359 SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE_def] THEN 1360 Induct_on `n` THENL [ 1361 REPEAT STRIP_TAC THEN 1362 Q_TAC EXISTS_TAC `\n:num. x` THEN 1363 ASM_SIMP_TAC std_ss [] THEN 1364 METIS_TAC[SUBSET_DEF], 1365 1366 1367 ASM_SIMP_TAC std_ss [] THEN 1368 REPEAT STRIP_TAC THEN 1369 Q_SPEC_NO_ASSUM 3 `s1'` THEN 1370 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 1371 Q_TAC EXISTS_TAC `\m. if (m = SUC n) then x else (w m)` THEN 1372 ASM_SIMP_TAC arith_ss [] THEN 1373 REPEAT STRIP_TAC THENL [ 1374 Cases_on `n' = SUC n` THEN 1375 ASM_SIMP_TAC arith_ss [], 1376 1377 Cases_on `n' < n` THENL [ 1378 ASM_SIMP_TAC arith_ss [], 1379 1380 `n' = n` by DECIDE_TAC THEN 1381 ASM_SIMP_TAC std_ss [] 1382 ] 1383 ] 1384 ] 1385 ) THEN 1386 1387 SUBGOAL_TAC `!n x. (x IN w2 n) ==> 1388 (?w. IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w x n /\ 1389 (!m. ((m > t1) /\ (n >= m)) ==> (w m IN S)))` THEN1 ( 1390 Induct_on `n` THENL [ 1391 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY], 1392 1393 1394 Q_SPEC_NO_ASSUM 5 `n` THEN 1395 Cases_on `w2 n = EMPTY` THENL [ 1396 WEAKEN_NO_TAC 7 (*x IN w1 (SUC n)*) THEN 1397 `~(n >= t1)` by PROVE_TAC[] THEN 1398 FULL_SIMP_TAC std_ss [NOT_IN_EMPTY, IN_INTER] THEN 1399 REPEAT STRIP_TAC THEN 1400 `?w. IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w x (SUC n)` by METIS_TAC[] THEN 1401 Q_TAC EXISTS_TAC `w` THEN 1402 ASM_SIMP_TAC std_ss [] THEN 1403 REPEAT STRIP_TAC THEN 1404 `n >= t1` by DECIDE_TAC, 1405 1406 1407 FULL_SIMP_TAC std_ss [] THEN 1408 REPEAT STRIP_TAC THEN 1409 `?w. IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w s1' n /\ 1410 (!m. ((m > t1) /\ (n >= m)) ==> (w m IN S))` by METIS_TAC[] THEN 1411 Q_TAC EXISTS_TAC `\m:num. if (m = SUC n) then x else w m` THEN 1412 REPEAT STRIP_TAC THENL [ 1413 SIMP_ALL_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE_def] THEN 1414 REPEAT STRIP_TAC THENL [ 1415 rename1 `m <= SUC n` THEN 1416 Cases_on `m = SUC n` THEN ASM_REWRITE_TAC[] THEN 1417 `m <= n` by DECIDE_TAC THEN 1418 RES_TAC, 1419 1420 ASM_SIMP_TAC arith_ss [], 1421 1422 1423 rename1 `m < SUC n` THEN 1424 ASM_SIMP_TAC arith_ss [] THEN 1425 Cases_on `m = n` THENL [ 1426 ASM_SIMP_TAC std_ss [], 1427 1428 `m < n` by DECIDE_TAC THEN 1429 ASM_SIMP_TAC std_ss [] 1430 ] 1431 ], 1432 1433 rename1 `SUC n >= m` THEN 1434 Cases_on `m = SUC n` THENL [ 1435 ASM_SIMP_TAC std_ss [], 1436 1437 `n >= m` by DECIDE_TAC THEN 1438 ASM_SIMP_TAC std_ss [] 1439 ] 1440 ] 1441 ] 1442 ] 1443 ) THEN 1444 1445 1446 `?A_S0'. A_S0' = \s0. (s0, i 0 INTER A.I) IN A.S0` by METIS_TAC[] THEN 1447 SUBGOAL_TAC `FINITE A_S0'` THEN1 ( 1448 `FINITE A.S0` by METIS_TAC[SUBSET_FINITE, FINITE_CROSS, FINITE_POW_IFF] THEN 1449 `?A_S0. A_S0 = A.S0 INTER (\(x, i'). (i' = (i 0 INTER A.I)))` by METIS_TAC[] THEN 1450 `FINITE A_S0` by PROVE_TAC[INTER_FINITE] THEN 1451 SUBGOAL_TAC `A_S0' = IMAGE FST A_S0` THEN1 ( 1452 ASM_SIMP_TAC std_ss [EXTENSION, IN_ABS, IN_IMAGE, IN_INTER] THEN 1453 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1454 Q_TAC EXISTS_TAC `(x, i 0 INTER A.I)` THEN 1455 ASM_SIMP_TAC std_ss [IN_INTER, 1456 prove (``!P x y. (((x, y) IN \(x,y). P x y) = P x y)``, SIMP_TAC std_ss [IN_DEF]) 1457 ], 1458 1459 Cases_on `x'` THEN 1460 REMAINS_TAC `(x = q) /\ ((i 0 INTER A.I) = r)` THEN1 ASM_REWRITE_TAC[] THEN 1461 NTAC 3 UNDISCH_HD_TAC THEN 1462 SIMP_TAC std_ss [IN_INTER, EXTENSION, 1463 prove (``!P x y. (((x, y) IN \(x,y). P x y) = P x y)``, SIMP_TAC std_ss [IN_DEF]) 1464 ] 1465 ] 1466 ) THEN 1467 METIS_TAC[IMAGE_FINITE] 1468 ) THEN 1469 SUBGOAL_TAC `FINITE (BIGUNION (IMAGE (\s0. {y | P s0 y}) A_S0'))` THEN1 ( 1470 MATCH_MP_TAC FINITE_BIGUNION THEN 1471 ASM_SIMP_TAC std_ss [IMAGE_FINITE, IN_IMAGE, GSYM LEFT_FORALL_IMP_THM, IN_ABS] THEN 1472 METIS_TAC[] 1473 ) THEN 1474 1475 `?f. f = \n. ((@s. s IN (w2 (t1+n))), t1+n)` by METIS_TAC[] THEN 1476 SUBGOAL_TAC `IMAGE f UNIV SUBSET (BIGUNION (IMAGE (\s0. {y | P s0 y}) A_S0'))` THEN1 ( 1477 GSYM_NO_TAC 7 (*Def P*) THEN 1478 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_BIGUNION, IN_UNIV, 1479 GSYM RIGHT_EXISTS_AND_THM, GSPECIFICATION, 1480 GSYM LEFT_EXISTS_AND_THM] THEN 1481 REPEAT STRIP_TAC THEN 1482 Cases_on `x` THEN 1483 SIMP_ALL_TAC std_ss [] THEN 1484 ASM_SIMP_TAC std_ss [IN_ABS] THEN 1485 SELECT_ELIM_TAC THEN 1486 REPEAT STRIP_TAC THENL [ 1487 `t1 + x' >= t1` by DECIDE_TAC THEN 1488 METIS_TAC[MEMBER_NOT_EMPTY], 1489 1490 Q_SPECL_NO_ASSUM 8 [`t1 + x'`, `x`] THEN 1491 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN 1492 REPEAT STRIP_TAC THEN 1493 Q_TAC EXISTS_TAC `w` THEN 1494 ASM_SIMP_TAC std_ss [] THEN 1495 FULL_SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE_def] 1496 ] 1497 ) THEN 1498 REMAINS_TAC `INFINITE (IMAGE f UNIV)` THEN1 ( 1499 METIS_TAC[SUBSET_FINITE] 1500 ) THEN 1501 MATCH_MP_TAC (SIMP_RULE std_ss [prove (``!P Q R. ((P ==> Q ==> R) = ((P /\ Q) ==> R))``, METIS_TAC[]), GSYM RIGHT_FORALL_IMP_THM] IMAGE_11_INFINITE) THEN 1502 STRIP_TAC THENL [ 1503 ASM_SIMP_TAC std_ss [], 1504 1505 REWRITE_TAC[INFINITE_UNIV] THEN 1506 EXISTS_TAC ``\n:num. SUC n`` THEN 1507 SIMP_TAC arith_ss [] THEN 1508 EXISTS_TAC ``0`` THEN 1509 SIMP_TAC arith_ss [] 1510 ] 1511 ] 1512 ]); 1513 1514 1515val A_SEM___NDET_F___TO___NDET_FG = 1516 store_thm ( 1517 "A_SEM___NDET_F___TO___NDET_FG", 1518 ``!A p x. (~(x IN (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p))) ==> 1519 (AUTOMATON_EQUIV (A_NDET (A, ACCEPT_COND_F p)) 1520 (A_NDET (symbolic_semi_automaton (x INSERT A.S) 1521 (P_AND (P_EQUIV(P_PROP x, p), A.S0)) 1522 (XP_AND (XP_EQUIV(XP_NEXT_PROP x, XP_OR(XP_PROP x, XP_NEXT p)), A.R)), 1523 (ACCEPT_COND_FG (P_PROP x)))))``, 1524 1525 SIMP_TAC std_ss [IN_UNION, SEMI_AUTOMATON_USED_VARS_def, 1526 SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, AUTOMATON_EQUIV_def, 1527 A_SEM_THM, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1528 IS_TRANSITION_def, symbolic_semi_automaton_REWRITES, 1529 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, 1530 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1531 ACCEPT_COND_F_def, ACCEPT_COND_FG_def, ACCEPT_F_def] THEN 1532 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1533 rename1 `P_SEM (w t UNION _) p` THEN 1534 Q_EXISTS_LEAST_TAC `?t'. P_SEM (w t' UNION (v t' DIFF A.S)) p` THEN 1535 FULL_SIMP_TAC std_ss [] THEN 1536 Q_TAC EXISTS_TAC `\n. if n < t' then (w n) else (x INSERT (w n))` THEN 1537 SUBGOAL_TAC `(!n. (w n UNION (v n DIFF (x INSERT A.S))) INTER (COMPL {x}) = 1538 (w n UNION (v n DIFF A.S)) INTER (COMPL {x})) /\ 1539 (!n. ((x INSERT w n) UNION (v n DIFF (x INSERT A.S))) INTER (COMPL {x}) = 1540 (w n UNION (v n DIFF A.S)) INTER (COMPL {x}))` THEN1 ( 1541 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_COMPL, IN_SING, IN_UNION, IN_DIFF, 1542 IN_INSERT] THEN 1543 METIS_TAC[] 1544 ) THEN 1545 `(P_USED_VARS p SUBSET COMPL {x}) /\ (P_USED_VARS A.S0 SUBSET COMPL {x}) /\ 1546 (XP_USED_VARS A.R SUBSET COMPL {x})` by ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_COMPL, IN_SING] THEN 1547 `!n. ~(x IN w n)` by PROVE_TAC[PATH_SUBSET_def, SUBSET_DEF] THEN 1548 REPEAT STRIP_TAC THENL [ 1549 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_INSERT, COND_RAND, 1550 COND_RATOR] THEN 1551 PROVE_TAC[], 1552 1553 Cases_on `0 < t'` THENL [ 1554 ASM_SIMP_TAC std_ss [P_SEM_THM, IN_UNION, IN_DIFF, IN_INSERT] THEN 1555 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1556 1557 `t' = 0` by DECIDE_TAC THEN 1558 ASM_SIMP_TAC std_ss [P_SEM_THM, IN_UNION, IN_INSERT] THEN 1559 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1560 ], 1561 1562 Cases_on `SUC n < t'` THENL [ 1563 `n < t'` by DECIDE_TAC THEN 1564 ASM_SIMP_TAC std_ss [XP_SEM_THM, IN_UNION, IN_DIFF, IN_INSERT, 1565 XP_SEM___XP_NEXT] THEN 1566 REPEAT STRIP_TAC THENL [ 1567 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1568 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] 1569 ], 1570 1571 Cases_on `SUC n = t'` THENL [ 1572 `n < t'` by DECIDE_TAC THEN 1573 ASM_SIMP_TAC std_ss [XP_SEM_THM, IN_UNION, IN_DIFF, IN_INSERT, 1574 XP_SEM___XP_NEXT] THEN 1575 REPEAT STRIP_TAC THENL [ 1576 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1577 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] 1578 ], 1579 1580 `~(n < t')` by DECIDE_TAC THEN 1581 ASM_SIMP_TAC std_ss [XP_SEM_THM, IN_UNION, IN_DIFF, IN_INSERT, 1582 XP_SEM___XP_NEXT] THEN 1583 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] 1584 ] 1585 ], 1586 1587 1588 EXISTS_TAC ``SUC t'`` THEN 1589 REPEAT STRIP_TAC THEN 1590 RIGHT_DISJ_TAC THEN 1591 rename1 `~~(t'' >= SUC t')` THEN 1592 `~(t'' < t')` by DECIDE_TAC THEN 1593 ASM_SIMP_TAC std_ss [P_SEM_THM, IN_UNION, IN_DIFF, COND_RAND, COND_RATOR, 1594 IN_INSERT] 1595 ], 1596 1597 1598 rename1 `~(_ >= t)` THEN 1599 Q_TAC EXISTS_TAC `PATH_RESTRICT w A.S` THEN 1600 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, PATH_SUBSET_def, INTER_SUBSET] THEN 1601 SUBGOAL_TAC `!n. (w n UNION (v n DIFF (x INSERT A.S))) INTER (COMPL {x}) = 1602 ((w n INTER A.S) UNION (v n DIFF A.S)) INTER (COMPL {x})` THEN1 ( 1603 SIMP_ALL_TAC std_ss [EXTENSION, IN_INTER, IN_COMPL, IN_SING, IN_UNION, IN_DIFF, 1604 IN_INSERT, PATH_SUBSET_def, SUBSET_DEF, IN_INSERT] THEN 1605 METIS_TAC[] 1606 ) THEN 1607 REPEAT STRIP_TAC THENL [ 1608 `P_USED_VARS A.S0 SUBSET COMPL {x}` by ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_COMPL, IN_SING] THEN 1609 SIMP_ALL_TAC std_ss [P_SEM_THM] THEN 1610 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1611 1612 `XP_USED_VARS A.R SUBSET COMPL {x}` 1613 by ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_COMPL, IN_SING] THEN 1614 SIMP_ALL_TAC std_ss [XP_SEM_THM] THEN 1615 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM], 1616 1617 1618 `P_USED_VARS p SUBSET COMPL {x}` by ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_COMPL, IN_SING] THEN 1619 SIMP_ALL_TAC std_ss [XP_SEM_THM, P_SEM_THM, XP_SEM___XP_NEXT, IN_UNION, IN_DIFF, IN_INSERT] THEN 1620 `t >= t` by DECIDE_TAC THEN 1621 Q_EXISTS_LEAST_TAC `?u. x IN w u` THEN 1622 SIMP_ALL_TAC std_ss [] THEN 1623 REMAINS_TAC `P_SEM (w u UNION (v u DIFF (x INSERT A.S))) p` THEN1 ( 1624 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1625 ) THEN 1626 Cases_on `u` THENL [ 1627 PROVE_TAC[], 1628 1629 `n < SUC n` by DECIDE_TAC THEN 1630 `~(x IN w n)` by PROVE_TAC[] THEN 1631 PROVE_TAC[] 1632 ] 1633 ] 1634 ]); 1635 1636 1637val A_SEM___UNIV_G___TO___UNIV_GF = 1638 store_thm ( 1639 "A_SEM___UNIV_G___TO___UNIV_GF", 1640 ``!A p x. (~(x IN (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p))) ==> 1641 (AUTOMATON_EQUIV (A_UNIV (A, ACCEPT_COND_G p)) 1642 (A_UNIV (symbolic_semi_automaton (x INSERT A.S) 1643 (P_AND (P_EQUIV(P_PROP x, P_NOT p), A.S0)) 1644 (XP_AND (XP_EQUIV(XP_NEXT_PROP x, XP_OR(XP_PROP x, XP_NEXT (P_NOT p))), A.R)), 1645 (ACCEPT_COND_GF (P_NOT (P_PROP x))))))``, 1646 1647 SIMP_TAC std_ss [AUTOMATON_EQUIV_def] THEN 1648 REPEAT STRIP_TAC THEN 1649 1650 SUBGOAL_TAC `!A p. (A_SEM v (A_UNIV (A,ACCEPT_COND_G p)) = 1651 ~A_SEM v (A_NDET (A,ACCEPT_COND_F (P_NOT p)))) /\ 1652 (A_SEM v (A_UNIV (A,ACCEPT_COND_GF p)) = 1653 ~A_SEM v (A_NDET (A,ACCEPT_COND_FG (P_NOT p))))` THEN1 ( 1654 SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_GF_def, ACCEPT_COND_G_def, 1655 ACCEPT_COND_F_def, ACCEPT_F_def, P_SEM_def, 1656 ACCEPT_COND_FG_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def] THEN 1657 METIS_TAC[] 1658 ) THEN 1659 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 1660 1661 ASSUME_TAC A_SEM___NDET_F___TO___NDET_FG THEN 1662 Q_SPECL_NO_ASSUM 0 [`A`, `P_NOT p`, `x`] THEN 1663 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[P_USED_VARS_def] THEN 1664 FULL_SIMP_TAC std_ss [AUTOMATON_EQUIV_def] THEN WEAKEN_HD_TAC THEN 1665 1666 SIMP_TAC std_ss [A_SEM_THM, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1667 P_SEM_THM, ACCEPT_COND_FG_def, ACCEPT_F_def, ACCEPT_COND_SEM_def, 1668 ACCEPT_COND_SEM_TIME_def]); 1669 1670 1671 1672 1673val ACCEPT_COND_TO_LTL_def = 1674 Define 1675 `(ACCEPT_COND_TO_LTL (ACCEPT_PROP b) = (LTL_PROP b)) /\ 1676 (ACCEPT_COND_TO_LTL ACCEPT_TRUE = LTL_TRUE) /\ 1677 (ACCEPT_COND_TO_LTL (ACCEPT_NOT f) = (LTL_NOT (ACCEPT_COND_TO_LTL f))) /\ 1678 (ACCEPT_COND_TO_LTL (ACCEPT_AND (f1, f2)) = (LTL_AND (ACCEPT_COND_TO_LTL f1, ACCEPT_COND_TO_LTL f2))) /\ 1679 (ACCEPT_COND_TO_LTL (ACCEPT_G f) = (LTL_ALWAYS (ACCEPT_COND_TO_LTL f)))`; 1680 1681 1682 1683val ACCEPT_COND_TO_LTL_THM = 1684 store_thm ("ACCEPT_COND_TO_LTL_THM", 1685 ``(!ac:'a acceptance_condition v t. (ACCEPT_COND_SEM_TIME t v ac = LTL_SEM_TIME t v (ACCEPT_COND_TO_LTL ac))) /\ 1686 (!ac:'a acceptance_condition v. (ACCEPT_COND_SEM v ac = LTL_SEM v (ACCEPT_COND_TO_LTL ac)))``, 1687 1688 LEFT_CONJ_TAC THENL [ 1689 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THEN 1690 ASM_SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def, ACCEPT_COND_SEM_TIME_def, LTL_SEM_THM], 1691 1692 ASM_REWRITE_TAC[ACCEPT_COND_SEM_def, LTL_SEM_def] 1693 ]); 1694 1695 1696val LTL_USED_VARS___ACCEPT_COND_TO_LTL = 1697 store_thm ("LTL_USED_VARS___ACCEPT_COND_TO_LTL", 1698 ``!ac. LTL_USED_VARS (ACCEPT_COND_TO_LTL ac) = 1699 ACCEPT_COND_USED_VARS ac``, 1700 1701 INDUCT_THEN acceptance_condition_induct ASSUME_TAC THEN ( 1702 ASM_SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def, 1703 ACCEPT_COND_USED_VARS_def, LTL_USED_VARS_EVAL] 1704 )); 1705 1706 1707 1708 1709val A_NDET_FG___SYM__TO__CONRETE = 1710 store_thm ( 1711 "A_NDET_FG___SYM__TO__CONRETE", 1712 ``!A I p. 1713 (P_USED_VARS p SUBSET A.S /\ 1714 SEMI_AUTOMATON_USED_INPUT_VARS A SUBSET I) ==> 1715 1716 (!i. A_SEM i (A_NDET (A,ACCEPT_COND_FG p)) = 1717 EXISTENTIAL_OMEGA_AUTOMATON_SEM (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A I, 1718 EXPLICIT_ACCEPT_FG (EXPLICIT_ACCEPT_STATE (\s. P_SEM s p))) i)``, 1719 1720 REPEAT STRIP_TAC THEN 1721 SUBGOAL_TAC `!n. (i n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A SUBSET I` THEN1 ( 1722 PROVE_TAC[SUBSET_TRANS, INTER_SUBSET] 1723 ) THEN 1724 ASM_SIMP_TAC std_ss [A_SEM_THM, EXISTENTIAL_OMEGA_AUTOMATON_SEM_def, 1725 GSYM SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___LANGUAGE_EQ 1726 ] THEN 1727 EXISTS_EQ_STRIP_TAC THEN 1728 BOOL_EQ_STRIP_TAC THEN 1729 SIMP_TAC std_ss [EXPLICIT_ACCEPT_COND_SEM_def, 1730 EXPLICIT_ACCEPT_COND_SEM_TIME_def, 1731 EXPLICIT_ACCEPT_FG_def, 1732 EXPLICIT_ACCEPT_F_def, 1733 IN_ABS, 1734 ACCEPT_COND_FG_def, 1735 ACCEPT_F_def, 1736 A_SEM_THM, 1737 ACCEPT_COND_SEM_def, 1738 ACCEPT_COND_SEM_TIME_def] THEN 1739 EXISTS_EQ_STRIP_TAC THEN FORALL_EQ_STRIP_TAC THEN BOOL_EQ_STRIP_TAC THEN 1740 rename1 `t2 >= t1` THEN 1741 REMAINS_TAC `INPUT_RUN_PATH_UNION A i w t2 INTER A.S = w t2 INTER A.S` THEN1 ( 1742 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1743 ) THEN 1744 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, EXTENSION, 1745 IN_INTER, IN_UNION, IN_DIFF] THEN 1746 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC); 1747 1748 1749 1750 1751val A_SEM___PRUNE_ACCEPTANCE_CONDITION = 1752 store_thm ( 1753 "A_SEM___PRUNE_ACCEPTANCE_CONDITION", 1754 ``!A f ac I A' ac'. ((I = ACCEPT_COND_USED_VARS ac DIFF A.S) /\ 1755 (INJ f I UNIV) /\ 1756 (DISJOINT (IMAGE f I) (SEMI_AUTOMATON_USED_VARS A UNION I)) /\ 1757 (A' = symbolic_semi_automaton (A.S UNION (IMAGE f I)) A.S0 1758 (XP_AND(A.R, XP_BIGAND (MAP (\i. XP_EQUIV(XP_PROP(f i), XP_PROP i)) (SET_TO_LIST I))))) /\ 1759 (ac' = ACCEPT_VAR_RENAMING (\x. if (x IN I) then f x else x) ac)) ==> 1760 1761 1762 1763 ((ACCEPT_COND_USED_VARS ac' SUBSET A'.S) /\ 1764 (!i. A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = 1765 A_SEM i (A_UNIV (A',ACCEPT_COND ac'))))``, 1766 1767 REPEAT GEN_TAC THEN STRIP_TAC THEN 1768 LEFT_CONJ_TAC THENL [ 1769 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, 1770 ACCEPT_VAR_RENAMING___USED_VARS, SUBSET_DEF, IN_IMAGE, IN_DIFF, IN_UNION] THEN 1771 GEN_TAC THEN STRIP_TAC THEN 1772 Cases_on `~(x' IN A.S)` THEN FULL_SIMP_TAC std_ss [] THEN 1773 PROVE_TAC[], 1774 1775 1776 1777 SUBGOAL_TAC `FINITE (ACCEPT_COND_USED_VARS p DIFF A.S)` THEN1 ( 1778 ASM_SIMP_TAC std_ss [FINITE_DIFF, FINITE___ACCEPT_COND_USED_VARS] 1779 ) THEN 1780 ASM_SIMP_TAC std_ss [A_SEM_THM, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1781 symbolic_semi_automaton_REWRITES, 1782 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def, 1783 XP_SEM_THM, FORALL_AND_THM, XP_BIGAND_SEM, MEM_MAP, 1784 GSYM LEFT_FORALL_IMP_THM, containerTheory.MEM_SET_TO_LIST, 1785 IN_DIFF, IN_UNION, IN_IMAGE, 1786 FINITE___ACCEPT_COND_USED_VARS, 1787 FINITE_DIFF] THEN 1788 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1789 `?w'. w' = PATH_RESTRICT w A.S` by METIS_TAC[] THEN 1790 SUBGOAL_TAC `!n. (((w n UNION (i n DIFF (A.S UNION IMAGE f (ACCEPT_COND_USED_VARS ac DIFF A.S)))) INTER (COMPL (IMAGE f I))) = 1791 ((w' n UNION (i n DIFF A.S)) INTER (COMPL (IMAGE f I))))` THEN1 ( 1792 UNDISCH_NO_TAC 4 (*PATH_SUBSET w*) THEN 1793 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_COMPL, IN_UNION, IN_DIFF, 1794 PATH_RESTRICT_def, PATH_MAP_def, PATH_SUBSET_def, SUBSET_DEF] THEN 1795 REPEAT WEAKEN_HD_TAC THEN 1796 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 1797 PROVE_TAC[] 1798 ) THEN 1799 1800 Q_SPEC_NO_ASSUM 6 `w'` THEN 1801 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1802 REPEAT STRIP_TAC THENL [ 1803 ASM_SIMP_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, 1804 INTER_SUBSET], 1805 1806 REMAINS_TAC `(P_USED_VARS A.S0 SUBSET COMPL (IMAGE f I))` THEN1 ( 1807 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1808 ) THEN 1809 UNDISCH_NO_TAC 10 (*DISJOINT IMAGE*) THEN 1810 REPEAT WEAKEN_HD_TAC THEN 1811 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 1812 IN_UNION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1813 PROVE_TAC[], 1814 1815 1816 REMAINS_TAC `(XP_USED_VARS A.R SUBSET COMPL (IMAGE f I))` THEN1 ( 1817 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] 1818 ) THEN 1819 UNDISCH_NO_TAC 10 (*DISJOINT IMAGE*) THEN 1820 REPEAT WEAKEN_HD_TAC THEN 1821 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 1822 IN_UNION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1823 PROVE_TAC[] 1824 ] 1825 ) THEN 1826 FULL_SIMP_TAC std_ss [ACCEPT_COND_SEM_def, ACCEPT_COND___VAR_RENAMING___NOT_INJ] THEN 1827 UNDISCH_HD_TAC THEN IMP_TO_EQ_TAC THEN 1828 ONCE_REWRITE_TAC [ACCEPT_COND_USED_VARS_INTER_THM] THEN 1829 AP_THM_TAC THEN AP_TERM_TAC THEN 1830 UNDISCH_NO_TAC 10 (*DISJOINT*) THEN 1831 UNDISCH_NO_TAC 5 (*PATH_SUBSET w*) THEN 1832 UNDISCH_NO_TAC 2 (*i f i ON w*) THEN 1833 UNDISCH_NO_TAC 8 (*INJ f*) THEN 1834 ASM_SIMP_TAC std_ss [EXTENSION, IN_ABS, 1835 IN_INTER, COND_RAND, COND_RATOR] THEN 1836 REPEAT WEAKEN_HD_TAC THEN 1837 REPEAT DISCH_TAC THEN 1838 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 1839 SIMP_ALL_TAC std_ss [IN_UNION, IN_DIFF, PATH_RESTRICT_def, 1840 PATH_MAP_def, IN_INTER, COND_EXPAND_IMP, 1841 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 1842 PATH_SUBSET_def, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, INJ_DEF, 1843 IN_UNIV, IN_IMAGE, IN_DIFF, EXTENSION, IN_ABS] THEN 1844 METIS_TAC[], 1845 1846 1847 1848 `?w'. w' = \n. (w n) UNION (IMAGE f (i n INTER I))` by METIS_TAC[] THEN 1849 SUBGOAL_TAC `!n. (((w' n UNION (i n DIFF (A.S UNION IMAGE f (ACCEPT_COND_USED_VARS ac DIFF A.S)))) INTER (COMPL (IMAGE f I))) = 1850 ((w n UNION (i n DIFF A.S)) INTER (COMPL (IMAGE f I))))` THEN1 ( 1851 UNDISCH_NO_TAC 3 (*PATH_SUBSET w*) THEN 1852 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_COMPL, IN_UNION, IN_DIFF, 1853 PATH_RESTRICT_def, PATH_MAP_def, PATH_SUBSET_def, SUBSET_DEF, IN_IMAGE] THEN 1854 REPEAT WEAKEN_HD_TAC THEN 1855 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 1856 METIS_TAC[] 1857 ) THEN 1858 Q_SPEC_NO_ASSUM 5 `w'` THEN 1859 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1860 REPEAT STRIP_TAC THENL [ 1861 UNDISCH_NO_TAC 4 THEN (*PATH_SUBSET w*) 1862 ASM_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_IMAGE, IN_INTER, IN_DIFF] THEN 1863 REPEAT WEAKEN_HD_TAC THEN 1864 METIS_TAC[], 1865 1866 REMAINS_TAC `(P_USED_VARS A.S0 SUBSET COMPL (IMAGE f I))` THEN1 ( 1867 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1868 ) THEN 1869 UNDISCH_NO_TAC 9 (*DISJOINT IMAGE*) THEN 1870 REPEAT WEAKEN_HD_TAC THEN 1871 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 1872 IN_UNION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1873 PROVE_TAC[], 1874 1875 1876 REMAINS_TAC `(XP_USED_VARS A.R SUBSET COMPL (IMAGE f I))` THEN1 ( 1877 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] 1878 ) THEN 1879 UNDISCH_NO_TAC 9 (*DISJOINT IMAGE*) THEN 1880 REPEAT WEAKEN_HD_TAC THEN 1881 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 1882 IN_UNION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1883 PROVE_TAC[], 1884 1885 1886 NTAC 2 UNDISCH_HD_TAC THEN 1887 UNDISCH_NO_TAC 10 THEN (*INJ I*) 1888 UNDISCH_NO_TAC 9 THEN (*DISJOINT IMAGE f I*) 1889 UNDISCH_NO_TAC 4 THEN (*PATH_SUBSET w*) 1890 ASM_SIMP_TAC std_ss [IN_UNION, IN_IMAGE, IN_INTER, IN_DIFF] THEN 1891 REPEAT WEAKEN_HD_TAC THEN REPEAT STRIP_TAC THEN 1892 SIMP_ALL_TAC std_ss [INJ_DEF, IN_DIFF, IN_UNIV, 1893 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, IN_IMAGE, 1894 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, PATH_SUBSET_def] THEN 1895 METIS_TAC[] 1896 ] 1897 ) THEN 1898 FULL_SIMP_TAC std_ss [ACCEPT_COND_SEM_def, ACCEPT_COND___VAR_RENAMING___NOT_INJ] THEN 1899 UNDISCH_HD_TAC THEN IMP_TO_EQ_TAC THEN 1900 ONCE_REWRITE_TAC [ACCEPT_COND_USED_VARS_INTER_THM] THEN 1901 AP_THM_TAC THEN AP_TERM_TAC THEN 1902 UNDISCH_NO_TAC 9 (*DISJOINT*) THEN 1903 UNDISCH_NO_TAC 4 (*PATH_SUBSET w*) THEN 1904 UNDISCH_NO_TAC 8 (*INJ f*) THEN 1905 ASM_SIMP_TAC std_ss [EXTENSION, IN_ABS, 1906 IN_INTER, COND_RAND, COND_RATOR] THEN 1907 REPEAT WEAKEN_HD_TAC THEN 1908 REPEAT DISCH_TAC THEN 1909 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 1910 SIMP_ALL_TAC std_ss [IN_UNION, IN_DIFF, PATH_RESTRICT_def, 1911 PATH_MAP_def, IN_INTER, COND_EXPAND_IMP, 1912 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 1913 PATH_SUBSET_def, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, INJ_DEF, 1914 IN_UNIV, IN_IMAGE, IN_DIFF, EXTENSION, IN_ABS] THEN 1915 METIS_TAC[] 1916 ] 1917 ]) 1918 1919 1920 1921val A_NDET_FG___SYM__TO__CONRETE___MIN_I = 1922 save_thm ("A_NDET_FG___SYM__TO__CONRETE___MIN_I", 1923 GEN ``A:'a symbolic_semi_automaton`` ( 1924 REWRITE_RULE [SUBSET_REFL] (SPECL [``A:'a symbolic_semi_automaton``, ``SEMI_AUTOMATON_USED_INPUT_VARS A``] A_NDET_FG___SYM__TO__CONRETE))) 1925 1926 1927val IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def= 1928 Define 1929 `IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION (A:'a symbolic_semi_automaton) (A':'a symbolic_semi_automaton) (IV:'a set) (f:'a set->'a) (g:'a -> 'a set) 1930 (f':'a set->'a) S = ( 1931 (S SUBSET (POW A.S)) /\ 1932 (INJ f (POW A.S) UNIV) /\ 1933 (INJ f' (POW A.S) UNIV) /\ 1934 (DISJOINT (IMAGE f (POW A.S)) IV) /\ 1935 (DISJOINT (IMAGE f' (POW A.S)) IV) /\ 1936 (DISJOINT (IMAGE f (POW A.S)) (IMAGE f' (POW A.S))) /\ 1937 (!z. z SUBSET A.S ==> (g (f z) = z)) /\ 1938 (!z. z SUBSET A.S ==> (g (f' z) = z)) /\ 1939 1940 1941 (A'.S = (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) /\ 1942 1943 (!i Z. (Z SUBSET A'.S) ==> (((P_SEM (INPUT_RUN_STATE_UNION A' i Z) A'.S0) = 1944 (Z = {z | (z IN (IMAGE f (POW A.S))) /\ P_SEM (INPUT_RUN_STATE_UNION A i (g z)) A.S0})))) /\ 1945 1946 (!S1 S2 i1 i2. 1947 (S1 SUBSET A'.S /\ S2 SUBSET A'.S) ==> 1948 ((IS_TRANSITION A' S1 i1 S2 i2) = 1949 (S2 = {s2 | (s2 IN (IMAGE f (POW A.S))) /\ ?s1. (s1 IN S1 /\ 1950 s1 IN (IMAGE f (POW A.S)) /\ 1951 IS_TRANSITION A (g s1) i1 (g s2) i2)} UNION 1952 {s2 | (s2 IN (IMAGE f' (POW A.S))) /\ ?s1. (s1 IN S1 /\ 1953 (COND (S1 INTER (IMAGE f' (POW A.S)) = EMPTY) (s1 IN (IMAGE f (POW A.S))) (s1 IN (IMAGE f' (POW A.S)))) /\ 1954 IS_TRANSITION A (g s1) i1 (g s2) i2 1955 /\ (g s2) IN S)}))) 1956 1957 1958 )`; 1959 1960 1961 1962val SYMBOLIC___NDET_FG___TO___DET_FG___THM = 1963 store_thm ("SYMBOLIC___NDET_FG___TO___DET_FG___THM", 1964 1965``!A A' IV f f' g S p p'. 1966(FINITE A.S /\ 1967 (P_USED_VARS p SUBSET A.S) /\ 1968 (P_USED_VARS p' SUBSET A'.S) /\ 1969 ((SEMI_AUTOMATON_USED_INPUT_VARS A') = (SEMI_AUTOMATON_USED_INPUT_VARS A)) /\ 1970(S = (\s. s SUBSET A.S /\ P_SEM s p)) /\ 1971IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION A A' IV f g f' S /\ 1972(!s. (P_SEM s p') = 1973 ~((s INTER (IMAGE f' (POW A.S)) = EMPTY))) 1974) ==> 1975!i. 1976(A_SEM i (A_NDET (A, ACCEPT_COND_FG p)) = 1977A_SEM i (A_NDET (A', ACCEPT_COND_FG p')))``, 1978 1979REPEAT STRIP_TAC THEN 1980ASM_SIMP_TAC std_ss [A_NDET_FG___SYM__TO__CONRETE___MIN_I] THEN 1981 1982ASSUME_TAC (INST_TYPE [beta |-> (alpha --> ``:bool``)] NDET_FG___TO___DET_FG___THM) THEN 1983Q_SPECL_NO_ASSUM 0 [`SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A 1984 (SEMI_AUTOMATON_USED_INPUT_VARS A)`, `\s. P_SEM s p`, `i`] THEN 1985SUBGOAL_TAC `IS_WELL_FORMED_SEMI_AUTOMATON 1986 (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A 1987 (SEMI_AUTOMATON_USED_INPUT_VARS A))` THEN1 ( 1988 MATCH_MP_TAC SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___IS_WELL_FORMED THEN 1989 ASM_REWRITE_TAC[FINITE___SEMI_AUTOMATON_USED_INPUT_VARS] 1990) THEN 1991FULL_SIMP_TAC std_ss [] THEN NTAC 2 WEAKEN_HD_TAC 1992 1993THEN 1994 1995`?h. h = \(S1, S2). (IMAGE f S1) UNION (IMAGE f' S2)` by METIS_TAC[] THEN 1996`?h'. h' = \S:'a set. (IMAGE g (S INTER (IMAGE f (POW A.S))), IMAGE g (S INTER (IMAGE f' (POW A.S))))` by METIS_TAC[] THEN 1997SUBGOAL_TAC `INJ h (POW (POW A.S) CROSS POW (POW A.S)) UNIV` THEN1 ( 1998 ASM_SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [INJ_DEF, IN_CROSS, IN_POW, IN_UNIV] THEN 1999 Cases_on `x` THEN Cases_on `y` THEN 2000 SIMP_ALL_TAC std_ss [IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def] THEN 2001 NTAC 2 (UNDISCH_NO_TAC 4) THEN (*INJ f, f'*) 2002 UNDISCH_NO_TAC 6 (*DISJOINT IMAGE*) THEN 2003 REPEAT WEAKEN_HD_TAC THEN 2004 REPEAT DISCH_TAC THEN 2005 CLEAN_ASSUMPTIONS_TAC THEN 2006 SUBGOAL_TAC `(IMAGE f q = IMAGE f q') /\ 2007 (IMAGE f' r = IMAGE f' r')` THEN1 ( 2008 UNDISCH_HD_TAC THEN 2009 SIMP_ALL_TAC std_ss [EXTENSION, IN_UNION, GSYM SUBSET_COMPL_DISJOINT, 2010 SUBSET_DEF, IN_COMPL] THEN 2011 METIS_TAC[IMAGE_SUBSET, SUBSET_DEF] 2012 ) THEN 2013 WEAKEN_NO_TAC 2 THEN 2014 2015 SIMP_ALL_TAC std_ss [INJ_DEF, IN_UNIV, SUBSET_DEF] THEN 2016 REPEAT STRIP_TAC THENL [ 2017 UNDISCH_NO_TAC 1 THEN 2018 IMP_TO_EQ_TAC THEN 2019 MATCH_MP_TAC INJECTIVE_IMAGE_EQ THEN 2020 SIMP_TAC std_ss [IN_UNION] THEN 2021 METIS_TAC[], 2022 2023 UNDISCH_NO_TAC 0 THEN 2024 IMP_TO_EQ_TAC THEN 2025 MATCH_MP_TAC INJECTIVE_IMAGE_EQ THEN 2026 SIMP_TAC std_ss [IN_UNION] THEN 2027 METIS_TAC[] 2028 ] 2029) THEN 2030 2031SUBGOAL_TAC `!s. s IN (POW (POW A.S) CROSS POW (POW A.S)) ==> (h' (h s) = s)` THEN1 ( 2032 Cases_on `s` THEN 2033 ASM_SIMP_TAC std_ss [IN_CROSS, IN_POW] THEN 2034 SIMP_ALL_TAC std_ss [IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def] THEN 2035 STRIP_TAC THEN 2036 SUBGOAL_TAC `((IMAGE f q UNION IMAGE f' r) INTER IMAGE f (POW A.S) = 2037 IMAGE f q) /\ 2038 ((IMAGE f q UNION IMAGE f' r) INTER IMAGE f' (POW A.S) = 2039 IMAGE f' r)` THEN1 ( 2040 NTAC 2 UNDISCH_HD_TAC (*r, q SUBSET POWERSET A.S*) THEN 2041 UNDISCH_NO_TAC 9 (*DISJOINT IMAGE IMAGE*) THEN 2042 REPEAT WEAKEN_HD_TAC THEN 2043 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, EXTENSION, IN_INTER, IN_UNION] THEN 2044 METIS_TAC[IMAGE_SUBSET, SUBSET_DEF] 2045 ) THEN 2046 ASM_REWRITE_TAC[GSYM IMAGE_COMPOSE] THEN 2047 REPEAT STRIP_TAC THEN 2048 MATCH_MP_TAC IMAGE_ID_SUBSET THEN 2049 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_POW] THEN 2050 METIS_TAC[] 2051) THEN 2052 2053 2054ASSUME_TAC (INST_TYPE [beta |-> (pairLib.mk_prod ((alpha --> bool) --> bool, (alpha --> bool) --> bool)), gamma |-> alpha --> bool] OMEGA_AUTOMATON___STATE_VAR_RENAMING) THEN 2055Q_SPECL_NO_ASSUM 0 [`BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON 2056 (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A 2057 (SEMI_AUTOMATON_USED_INPUT_VARS A)) (\s. P_SEM s p)`, 2058 ` EXPLICIT_ACCEPT_FG (EXPLICIT_ACCEPT_STATE 2059 (\(s1,s2). 2060 s1 SUBSET 2061 (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A 2062 (SEMI_AUTOMATON_USED_INPUT_VARS A)).S /\ 2063 s2 SUBSET 2064 (SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON A 2065 (SEMI_AUTOMATON_USED_INPUT_VARS A)).S /\ 2066 ~(s2 = {}))):('a, (('a -> bool) -> bool) # (('a -> bool) -> bool)) 2067 explicit_acceptance_condition`, 2068 `h`, `h'`] THEN 2069PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 2070 REPEAT STRIP_TAC THENL [ 2071 MATCH_MP_TAC BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON___IS_WELL_FORMED THEN 2072 MATCH_MP_TAC SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON___IS_WELL_FORMED THEN 2073 ASM_SIMP_TAC std_ss [FINITE___SEMI_AUTOMATON_USED_INPUT_VARS], 2074 2075 2076 2077 SIMP_TAC std_ss [EXPLICIT_ACCEPT_COND_USED_STATE_VARS_def, 2078 BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 2079 semi_automaton_REWRITES, SUBSET_DEF, 2080 EXPLICIT_ACCEPT_FG_def, EXPLICIT_ACCEPT_F_def] THEN 2081 Cases_on `x` THEN 2082 SIMP_TAC std_ss [IN_POW, SUBSET_DEF, IN_CROSS, 2083 prove (``!P x1 x2. ((x1, x2) IN \(x1,x2). P x1 x2) = P x1 x2``, SIMP_TAC std_ss [IN_DEF])], 2084 2085 2086 2087 SIMP_TAC std_ss [BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 2088 semi_automaton_REWRITES, SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON_def] THEN 2089 ASM_REWRITE_TAC[], 2090 2091 2092 UNDISCH_HD_TAC THEN 2093 SIMP_TAC std_ss [BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 2094 semi_automaton_REWRITES, SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON_def] THEN 2095 ASM_REWRITE_TAC[] 2096 ] 2097) THEN 2098ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 2099 2100 2101FULL_SIMP_TAC std_ss [EXISTENTIAL_OMEGA_AUTOMATON_SEM_def, 2102 BREAKPOINT_CONSTRUCTION_SEMI_AUTOMATON_def, 2103 SYMBOLIC_SEMI_AUTOMATON_TO_SEMI_AUTOMATON_def, 2104 semi_automaton_REWRITES, IS_RUN_THROUGH_SEMI_AUTOMATON_def, 2105 IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def, 2106 INTER_SUBSET, SEMI_AUTOMATON_STATE_VAR_RENAMING_def, 2107 prove (``!P x1 x2 x3 x4. ((x1, x2,x3,x4) IN \(x1, x2,x3, x4). P x1 x2 x3 x4) = 2108 P x1 x2 x3 x4``, SIMP_TAC std_ss [IN_DEF]), 2109 prove (``!P x1 x2 x3 x4. ((x1, x2,x3,x4) IN \((x1, x2), x3, (x4,x5), x6). P x1 x2 x3 x4 x5 x6) = P (FST x1) (SND x1) x2 (FST x3) (SND x3) x4``, 2110 Cases_on `x1` THEN Cases_on `x3` THEN SIMP_TAC std_ss [IN_DEF]), 2111 prove (``!P x1 x2. ((x1, x2) IN \(x1, x2). P x1 x2) = 2112 P x1 x2``, SIMP_TAC std_ss [IN_DEF])] THEN 2113 2114EXISTS_EQ_STRIP_TAC THEN 2115SUBGOAL_TAC `IMAGE (\(S1,S2). IMAGE f S1 UNION IMAGE f' S2) 2116 (POW (POW A.S) CROSS POW (POW A.S)) = 2117 POW 2118 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))` THEN1 ( 2119 2120 SIMP_TAC std_ss [EXTENSION] THEN 2121 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 2122 REPEAT WEAKEN_HD_TAC THEN 2123 SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [IN_IMAGE, EXTENSION, IN_UNION, IN_CROSS, 2124 IN_POW, SUBSET_DEF] THEN 2125 METIS_TAC[], 2126 2127 ASM_SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [IN_POW, IN_IMAGE] THEN 2128 REPEAT STRIP_TAC THEN 2129 Q_TAC EXISTS_TAC `(IMAGE g (x INTER (IMAGE f (POW A.S))), IMAGE g (x INTER (IMAGE f' (POW A.S))))` THEN 2130 SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, IN_CROSS, IN_POW] THEN 2131 REPEAT STRIP_TAC THENL [ 2132 SIMP_TAC std_ss [EXTENSION, SUBSET_DEF, IN_IMAGE, IN_UNION, 2133 IN_POW, GSYM SUBSET_COMPL_DISJOINT, IN_COMPL, 2134 GSYM RIGHT_EXISTS_AND_THM] THEN 2135 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 2136 REPEAT STRIP_TAC THEN 2137 `x' IN IMAGE f (POW A.S) UNION IMAGE f' (POW A.S)` by 2138 PROVE_TAC[SUBSET_DEF] THEN 2139 SIMP_ALL_TAC std_ss [IN_UNION] THENL [ 2140 DISJ1_TAC THEN 2141 Q_TAC EXISTS_TAC `x'` THEN 2142 ASM_REWRITE_TAC[IN_INTER] THEN 2143 UNDISCH_HD_TAC THEN 2144 SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2145 METIS_TAC[], 2146 2147 DISJ2_TAC THEN 2148 Q_TAC EXISTS_TAC `x'` THEN 2149 ASM_REWRITE_TAC[IN_INTER] THEN 2150 UNDISCH_HD_TAC THEN 2151 SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2152 METIS_TAC[] 2153 ], 2154 2155 SIMP_TAC std_ss [IN_IMAGE, IN_POW, IN_INTER, 2156 GSYM RIGHT_EXISTS_AND_THM] THEN 2157 METIS_TAC[] 2158 ], 2159 2160 SIMP_TAC std_ss [EXTENSION, SUBSET_DEF, IN_IMAGE, IN_UNION, IN_INTER, 2161 IN_POW] THEN 2162 METIS_TAC[SUBSET_DEF], 2163 2164 SIMP_TAC std_ss [EXTENSION, SUBSET_DEF, IN_IMAGE, IN_UNION, IN_INTER, 2165 IN_POW] THEN 2166 METIS_TAC[SUBSET_DEF] 2167 ] 2168 ] 2169) THEN 2170 2171ASM_SIMP_TAC std_ss [IN_POW] THEN 2172REPEAT BOOL_EQ_STRIP_TAC THEN 2173ASM_SIMP_TAC std_ss [] THEN 2174BINOP_TAC THENL [ 2175 BINOP_TAC, 2176 ALL_TAC 2177] THENL [ 2178 2179 Q_SPECL_NO_ASSUM 8 [`i 0 INTER SEMI_AUTOMATON_USED_INPUT_VARS A' `, `w 0`] THEN 2180 UNDISCH_HD_TAC THEN 2181 ASM_SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, IMAGE_EQ_EMPTY] THEN 2182 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2183 EQ_TAC THENL [ 2184 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_UNION, IN_SING, NOT_IN_EMPTY, IN_INTER] THEN 2185 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 2186 `(x IN (IMAGE f (POW A.S)))` by PROVE_TAC[SUBSET_DEF, IN_UNION] THEN 2187 ASM_REWRITE_TAC[] THEN 2188 Q_SPEC_NO_ASSUM 2 `g x` THEN 2189 SUBGOAL_TAC `g x IN IMAGE g (w 0 INTER IMAGE f (POW A.S))` THEN1 ( 2190 SIMP_TAC std_ss [IN_IMAGE] THEN 2191 PROVE_TAC[IN_INTER] 2192 ) THEN 2193 FULL_SIMP_TAC std_ss [], 2194 2195 SUBGOAL_TAC `g x SUBSET A.S` THEN1 ( 2196 SIMP_ALL_TAC std_ss [IN_IMAGE, IN_POW] THEN 2197 METIS_TAC[] 2198 ) THEN 2199 `g x IN IMAGE g (w 0 INTER IMAGE f (POW A.S))` by METIS_TAC[] THEN 2200 UNDISCH_HD_TAC THEN 2201 UNDISCH_NO_TAC 2 (*x IN IMAGE f*) THEN 2202 SIMP_TAC std_ss [IN_IMAGE, IN_INTER, GSYM RIGHT_EXISTS_AND_THM, IN_POW] THEN 2203 SIMP_ALL_TAC std_ss [IN_IMAGE, IN_POW] THEN 2204 METIS_TAC[] 2205 ], 2206 2207 SIMP_TAC std_ss [] THEN 2208 REPEAT STRIP_TAC THENL [ 2209 UNDISCH_NO_TAC 12 (*DISJOINT IMAGE IMAGE*) THEN 2210 REPEAT WEAKEN_HD_TAC THEN 2211 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, EXTENSION, GSPECIFICATION, IN_INTER, NOT_IN_EMPTY] THEN 2212 METIS_TAC[], 2213 2214 2215 SIMP_TAC std_ss [IN_IMAGE, IN_INTER, GSPECIFICATION, IN_POW, GSYM RIGHT_EXISTS_AND_THM] THEN 2216 METIS_TAC[] 2217 ] 2218 ], 2219 2220 2221 2222 SUBGOAL_TAC `(!n. IMAGE g (w n INTER IMAGE f (POW A.S)) SUBSET POW A.S) /\ !n. 2223 IMAGE g (w n INTER IMAGE f' (POW A.S)) SUBSET POW A.S` THEN1 ( 2224 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_POW, IN_IMAGE, IN_INTER, 2225 GSYM RIGHT_EXISTS_AND_THM] THEN 2226 METIS_TAC[SUBSET_DEF] 2227 ) THEN 2228 ASM_REWRITE_TAC[] THEN 2229 FORALL_EQ_STRIP_TAC THEN 2230 Q_SPECL_NO_ASSUM 9 [`w n`, `w (SUC n)`, `i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A'`, 2231 `i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A'`] THEN 2232 UNDISCH_HD_TAC THEN 2233 ASM_SIMP_TAC std_ss [IS_TRANSITION_def, INPUT_RUN_STATE_UNION_def, 2234 IMAGE_EQ_EMPTY] THEN 2235 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2236 2237 SUBGOAL_TAC `(w (SUC n) = 2238 {s2 | 2239 s2 IN IMAGE f (POW A.S) /\ 2240 ?s1. 2241 s1 IN w n /\ s1 IN IMAGE f (POW A.S) /\ 2242 XP_SEM A.R 2243 (g s1 UNION (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF A.S), 2244 g s2 UNION 2245 (i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF 2246 A.S))} UNION 2247 {s2 | 2248 s2 IN IMAGE f' (POW A.S) /\ 2249 ?s1. 2250 s1 IN w n /\ 2251 (if w n INTER IMAGE f' (POW A.S) = {} then 2252 s1 IN IMAGE f (POW A.S) 2253 else 2254 s1 IN IMAGE f' (POW A.S)) /\ 2255 XP_SEM A.R 2256 (g s1 UNION (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF A.S), 2257 g s2 UNION 2258 (i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF A.S)) /\ 2259 g s2 IN (\s. s SUBSET A.S /\ P_SEM s p)}) = ( 2260(w (SUC n) INTER (IMAGE f (POW A.S)) = 2261 {s2 | 2262 s2 IN IMAGE f (POW A.S) /\ 2263 ?s1. 2264 s1 IN w n /\ s1 IN IMAGE f (POW A.S) /\ 2265 XP_SEM A.R 2266 (g s1 UNION 2267 (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF A.S), 2268 g s2 UNION 2269 (i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF 2270 A.S))}) /\ 2271 (w (SUC n) INTER (IMAGE f' (POW A.S)) = 2272 {s2 | 2273 s2 IN IMAGE f' (POW A.S) /\ 2274 ?s1. 2275 s1 IN w n /\ 2276 (if w n INTER IMAGE f' (POW A.S) = {} then 2277 s1 IN IMAGE f (POW A.S) 2278 else 2279 s1 IN IMAGE f' (POW A.S)) /\ 2280 XP_SEM A.R 2281 (g s1 UNION 2282 (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF A.S), 2283 g s2 UNION 2284 (i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A DIFF 2285 A.S)) /\ g s2 IN (\s. s SUBSET A.S /\ P_SEM s p)}))` THEN1 ( 2286 UNDISCH_NO_TAC 13 THEN (*DISJOINT IMAGE IMAGE*) 2287 UNDISCH_NO_TAC 2 THEN (*w n SUBSET*) 2288 REPEAT WEAKEN_HD_TAC THEN 2289 SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, GSPECIFICATION, 2290 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, GSYM FORALL_AND_THM] THEN 2291 REPEAT STRIP_TAC THEN 2292 FORALL_EQ_STRIP_TAC THEN 2293 METIS_TAC[] 2294 ) THEN 2295 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 2296 MATCH_MP_TAC (prove (``((A = C) /\ (A ==> (B = D))) ==> (A /\ B = C /\ D)``, PROVE_TAC[])) THEN 2297 REPEAT STRIP_TAC THENL [ 2298 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_IMAGE, IN_INTER, 2299 IN_POW, GSYM LEFT_EXISTS_AND_THM, 2300 GSYM RIGHT_EXISTS_AND_THM] THEN 2301 2302 `!s1' x' n. ((!x. x IN s1' = x IN g (f x')) /\ f x' IN w n /\ x' SUBSET A.S) = ((s1' = x') /\ f x' IN w n /\ x' SUBSET A.S)` by METIS_TAC[EXTENSION] THEN 2303 ASM_SIMP_TAC std_ss [] THEN 2304 METIS_TAC[], 2305 2306 Cases_on `w n INTER IMAGE f' (POW A.S) = {}` THEN ( 2307 ASM_REWRITE_TAC [] THEN 2308 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER] THEN 2309 WEAKEN_NO_TAC 1 THEN 2310 SIMP_TAC std_ss [GSPECIFICATION, IN_IMAGE, IN_INTER, 2311 IN_POW, GSYM LEFT_EXISTS_AND_THM, 2312 GSYM RIGHT_EXISTS_AND_THM, IN_ABS] THEN 2313 METIS_TAC[] 2314 ) 2315 ], 2316 2317 2318 SIMP_TAC std_ss [ 2319 EXPLICIT_ACCEPT_FG_def, 2320 EXPLICIT_ACCEPT_F_def, 2321 EXPLICIT_ACCEPT_COND___STATE_VAR_RENAMING_def, 2322 EXPLICIT_ACCEPT_COND_SEM_def, 2323 EXPLICIT_ACCEPT_COND_SEM_TIME_def, 2324 IN_ABS] THEN 2325 EXISTS_EQ_STRIP_TAC THEN 2326 FORALL_EQ_STRIP_TAC THEN 2327 BOOL_EQ_STRIP_TAC THEN 2328 rename1 `t2 >= t1` THEN 2329 SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [IN_IMAGE, 2330 prove (``!P x. (x IN \(x1, x2). P x1 x2) = (P (FST x) (SND x))``, 2331 Cases_on `x` THEN SIMP_TAC std_ss [IN_DEF])] THEN 2332 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2333 NTAC 5 UNDISCH_HD_TAC THEN 2334 UNDISCH_NO_TAC 13 (*DISJOINT IMAGE IMAGE*) THEN 2335 REPEAT WEAKEN_HD_TAC THEN 2336 SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL] THEN 2337 REPEAT STRIP_TAC THEN 2338 SUBGOAL_TAC `IMAGE f' (SND x) = EMPTY` THEN1 ( 2339 FULL_SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_IMAGE, IN_POW, IN_INTER, NOT_IN_EMPTY, IN_UNION] THEN 2340 METIS_TAC[] 2341 ) THEN 2342 SIMP_ALL_TAC std_ss [IMAGE_EQ_EMPTY], 2343 2344 2345 `?w1. w1 = (w t2 INTER (IMAGE f (POW A.S)))` by PROVE_TAC[] THEN 2346 `?w2. w2 = (w t2 INTER (IMAGE f' (POW A.S)))` by PROVE_TAC[] THEN 2347 SUBGOAL_TAC `w t2 = w1 UNION w2` THEN1 ( 2348 NTAC 2 UNDISCH_HD_TAC THEN 2349 UNDISCH_NO_TAC 2 (*w n SUBSET*) THEN 2350 REPEAT WEAKEN_HD_TAC THEN 2351 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, SUBSET_DEF] THEN 2352 METIS_TAC[] 2353 ) THEN 2354 SUBGOAL_TAC `?gw1 gw2. (gw1 SUBSET (POW A.S)) /\ 2355 (gw2 SUBSET (POW A.S)) /\ 2356 (w1 = IMAGE f gw1) /\ 2357 (w2 = IMAGE f' gw2)` THEN1 ( 2358 NTAC 2 (UNDISCH_NO_TAC 1) THEN 2359 REPEAT WEAKEN_HD_TAC THEN 2360 REPEAT STRIP_TAC THEN 2361 2362 ASSUME_TAC (INST_TYPE [alpha |-> alpha --> bool, beta |-> alpha] SUBSET_IMAGE___ORGINAL_EXISTS) THEN 2363 Q_SPECL_NO_ASSUM 0 [`f`, `POW A.S`, `w1`] THEN 2364 2365 ASSUME_TAC (INST_TYPE [alpha |-> alpha --> bool, beta |-> alpha] SUBSET_IMAGE___ORGINAL_EXISTS) THEN 2366 Q_SPECL_NO_ASSUM 0 [`f'`, `POW A.S`, `w2`] THEN 2367 2368 METIS_TAC[INTER_SUBSET, SUBSET_IMAGE___ORGINAL_EXISTS] 2369 ) THEN 2370 2371 Q_TAC EXISTS_TAC `(gw1, gw2)` THEN 2372 ASM_SIMP_TAC std_ss [] THEN 2373 METIS_TAC[IMAGE_EQ_EMPTY] 2374 ] 2375]); 2376 2377 2378 2379 2380val SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_TOTAL = 2381 store_thm ( 2382 "SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_TOTAL", 2383 ``!A A' IV f f' g S. 2384 IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION A A' IV f g f' S ==> IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A'``, 2385 2386 2387 SIMP_TAC std_ss [IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def, IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON_def] THEN 2388 REPEAT STRIP_TAC THENL [ 2389 Q_TAC EXISTS_TAC `{z | 2390 z IN IMAGE f (POW A.S) /\ 2391 P_SEM (INPUT_RUN_STATE_UNION A i (g z)) A.S0}` THEN 2392 LEFT_CONJ_TAC THENL [ 2393 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_UNION], 2394 METIS_TAC[] 2395 ], 2396 2397 2398 ONCE_REWRITE_TAC[TRANSITION_CURRENT_STATE_CLEANING] THEN 2399 `?s2. s2 = {s2 | 2400 s2 IN IMAGE f (POW A.S) /\ 2401 ?s1'. 2402 s1' IN s1 INTER A'.S /\ s1' IN IMAGE f (POW A.S) /\ 2403 IS_TRANSITION A (g s1') (i1 UNION s1) (g s2) i2} UNION 2404 {s2 | 2405 s2 IN IMAGE f' (POW A.S) /\ 2406 ?s1'. 2407 s1' IN s1 INTER A'.S /\ 2408 (if s1 INTER A'.S INTER IMAGE f' (POW A.S) = {} then 2409 s1' IN IMAGE f (POW A.S) 2410 else 2411 s1' IN IMAGE f' (POW A.S)) /\ 2412 IS_TRANSITION A (g s1') (i1 UNION s1) (g s2) i2 /\ 2413 g s2 IN S}` by METIS_TAC[] THEN 2414 Q_TAC EXISTS_TAC `s2` THEN 2415 LEFT_CONJ_TAC THENL [ 2416 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_UNION] THEN 2417 METIS_TAC[], 2418 2419 METIS_TAC[INTER_SUBSET] 2420 ] 2421 ]); 2422 2423 2424 2425 2426 2427val SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_DET = 2428 store_thm ( 2429 "SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_DET", 2430 ``!A A' IV f f' g S. 2431 IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION A A' IV f g f' S ==> 2432 IS_DET_SYMBOLIC_SEMI_AUTOMATON A'``, 2433 2434 2435 SIMP_TAC std_ss [IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def, IS_DET_SYMBOLIC_SEMI_AUTOMATON_def, EXISTS_AT_MOST_ONE_def] THEN 2436 REPEAT STRIP_TAC THENL [ 2437 METIS_TAC[], 2438 METIS_TAC[TRANSITION_CURRENT_STATE_CLEANING, INTER_SUBSET] 2439 ]); 2440 2441 2442 2443val SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_DET_TOTAL = 2444 store_thm ( 2445 "SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_DET_TOTAL", 2446 ``!A A' IV f f' g S. 2447 IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION A A' IV f g f' S ==> 2448 IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A'``, 2449 2450 2451 PROVE_TAC [IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_def, 2452 SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_DET, SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_TOTAL]); 2453 2454 2455 2456 2457val SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def= 2458(* Idea by Sven Lamberti *) 2459 Define 2460 `SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A f f' pS = 2461 symbolic_semi_automaton 2462 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S)) 2463 (P_AND (P_FORALL (SET_TO_LIST A.S) (P_EQUIV(A.S0, VAR_RENAMING_HASHTABLE A.S f)), 2464 P_NOT (P_BIGOR (SET_TO_LIST (IMAGE (\s. P_PROP (f' s)) (POW A.S)))))) 2465 (XP_AND( 2466 (XP_NEXT_FORALL (SET_TO_LIST A.S) (XP_EQUIV( 2467 XP_NEXT (VAR_RENAMING_HASHTABLE A.S f), 2468 XP_CURRENT_EXISTS (SET_TO_LIST A.S) ( 2469 XP_AND(A.R, XP_CURRENT (VAR_RENAMING_HASHTABLE A.S f)))))), 2470 (XP_COND ((XP_NOT (XP_BIGOR (SET_TO_LIST (IMAGE (\s. XP_PROP (f' s)) (POW A.S))))), 2471 (XP_NEXT_FORALL (SET_TO_LIST A.S) (XP_EQUIV( 2472 XP_NEXT (VAR_RENAMING_HASHTABLE A.S f'), 2473 XP_CURRENT_EXISTS (SET_TO_LIST A.S) ( 2474 XP_AND(XP_AND(A.R, XP_NEXT pS), XP_CURRENT (VAR_RENAMING_HASHTABLE A.S f)))))), 2475 (XP_NEXT_FORALL (SET_TO_LIST A.S) (XP_EQUIV( 2476 XP_NEXT (VAR_RENAMING_HASHTABLE A.S f'), 2477 XP_CURRENT_EXISTS (SET_TO_LIST A.S) ( 2478 XP_AND(XP_AND(A.R, XP_NEXT pS), XP_CURRENT (VAR_RENAMING_HASHTABLE A.S f'))))))))))`; 2479 2480 2481val SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_THM = 2482 store_thm 2483 ("SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_THM", 2484 ``!A A' IV f g f' pS. 2485 2486 ((A' = SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A f f' pS) /\ 2487 FINITE A.S /\ 2488 SEMI_AUTOMATON_USED_VARS A SUBSET IV /\ 2489 P_USED_VARS pS SUBSET A.S /\ 2490 INJ f (POW A.S) UNIV /\ 2491 INJ f' (POW A.S) UNIV /\ 2492 DISJOINT (IMAGE f (POW A.S)) IV /\ 2493 DISJOINT (IMAGE f' (POW A.S)) IV /\ 2494 DISJOINT (IMAGE f (POW A.S)) (IMAGE f' (POW A.S)) /\ 2495 (!z. z SUBSET A.S ==> (g (f z) = z)) /\ 2496 (!z. z SUBSET A.S ==> (g (f' z) = z))) ==> 2497 2498 (IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION A A' IV f g f' (\s. s SUBSET A.S /\ P_SEM s pS))``, 2499 2500 2501SIMP_TAC std_ss [IS_SYMBOLIC_BREAKPOINT_CONSTRUCTION_def, 2502 SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, symbolic_semi_automaton_REWRITES] THEN 2503REPEAT STRIP_TAC THENL [ 2504 2505 SIMP_TAC std_ss [SUBSET_DEF, IN_ABS, IN_POW], 2506 2507 2508 ASM_SIMP_TAC std_ss [P_FORALL_SEM, SET_TO_LIST_INV, 2509 P_SEM_THM, VAR_RENAMING_HASHTABLE_SEM, 2510 INPUT_RUN_STATE_UNION_def, symbolic_semi_automaton_REWRITES, 2511 P_BIGOR_SEM, MEM_SET_TO_LIST, FINITE_POW_IFF, IMAGE_FINITE] THEN 2512 2513 SUBGOAL_TAC `!l'. (l' SUBSET A.S) ==> ((Z UNION 2514 (i DIFF 2515 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) DIFF 2516 A.S UNION l') INTER A.S = l')` THEN1 ( 2517 UNDISCH_HD_TAC (*Z SUBSET IMAGE*) THEN 2518 UNDISCH_NO_TAC 2 (*DISJOINT IMAGE IMAGE*) THEN 2519 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, SUBSET_DEF, 2520 GSYM SUBSET_COMPL_DISJOINT, IN_COMPL] THEN 2521 METIS_TAC[] 2522 ) THEN 2523 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2524 2525 SUBGOAL_TAC `!l'. (l' SUBSET A.S) ==> ( 2526 (f l' IN 2527 Z UNION 2528 (i DIFF 2529 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) DIFF 2530 A.S UNION l') = (f l' IN Z))` THEN1 ( 2531 2532 SIMP_ALL_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 2533 UNION_SUBSET] THEN 2534 UNDISCH_NO_TAC 5 (*DISJOINT IMAGE f IV*) THEN 2535 UNDISCH_NO_TAC 10 (*A.S SUBSET IV*) THEN 2536 REPEAT WEAKEN_HD_TAC THEN 2537 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, SUBSET_DEF, 2538 GSYM SUBSET_COMPL_DISJOINT, IN_COMPL, IN_IMAGE, IN_POW] THEN 2539 METIS_TAC[] 2540 ) THEN 2541 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2542 2543 SUBGOAL_TAC `!l'. (P_SEM 2544 (Z UNION 2545 (i DIFF 2546 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) DIFF 2547 A.S UNION l') A.S0) = (P_SEM (l' UNION (i DIFF A.S)) A.S0)` THEN1 ( 2548 GEN_TAC THEN 2549 ONCE_REWRITE_TAC[P_USED_VARS_INTER_THM] THEN 2550 AP_THM_TAC THEN AP_TERM_TAC THEN 2551 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 2552 EXTENSION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, IN_INTER, IN_DIFF] THEN 2553 METIS_TAC[] 2554 ) THEN 2555 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2556 2557 SUBGOAL_TAC `(!e. 2558 ~(e IN IMAGE (\s. P_PROP (f' s)) (POW A.S)) \/ 2559 ~P_SEM 2560 (Z UNION 2561 (i DIFF 2562 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S)))) e) = 2563 (Z INTER IMAGE f' (POW A.S) = EMPTY)` THEN1 ( 2564 SIMP_TAC std_ss [IN_IMAGE, GSYM LEFT_FORALL_OR_THM, P_SEM_THM, IN_POW, IN_UNION, EXTENSION, IN_INTER, IN_IMAGE, NOT_IN_EMPTY, IN_DIFF] THEN 2565 METIS_TAC[] 2566 ) THEN 2567 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2568 2569 EQ_TAC THENL [ 2570 REPEAT STRIP_TAC THEN 2571 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN 2572 GEN_TAC THEN 2573 SUBGOAL_TAC `Z = Z INTER (IMAGE f (POW A.S))` THEN1 ( 2574 SIMP_ALL_TAC std_ss [EXTENSION, SUBSET_DEF, IN_INTER, NOT_IN_EMPTY, IN_UNION] THEN 2575 METIS_TAC[] 2576 ) THEN 2577 ONCE_ASM_REWRITE_TAC [] THEN WEAKEN_HD_TAC THEN 2578 SIMP_TAC std_ss [IN_INTER] THEN 2579 BOOL_EQ_STRIP_TAC THEN 2580 SIMP_ALL_TAC std_ss [IN_IMAGE, IN_POW] THEN 2581 METIS_TAC[], 2582 2583 2584 SIMP_TAC std_ss [] THEN 2585 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2586 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_INTER, NOT_IN_EMPTY] THEN 2587 REPEAT STRIP_TAC THENL [ 2588 ASM_SIMP_TAC std_ss [] THEN 2589 BOOL_EQ_STRIP_TAC THEN 2590 SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2591 PROVE_TAC[], 2592 2593 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM] THEN 2594 METIS_TAC[] 2595 ] 2596 ], 2597 2598 2599 2600 ASM_SIMP_TAC std_ss [IS_TRANSITION_def, symbolic_semi_automaton_REWRITES, 2601 XP_SEM_THM, INPUT_RUN_STATE_UNION_def, XP_NEXT_FORALL_SEM, 2602 SET_TO_LIST_INV, XP_SEM___XP_NEXT, VAR_RENAMING_HASHTABLE_SEM, 2603 XP_CURRENT_EXISTS_SEM, XP_SEM___XP_CURRENT, XP_BIGOR_SEM, 2604 MEM_SET_TO_LIST, FINITE_POW_IFF, IMAGE_FINITE] THEN 2605 2606 SUBGOAL_TAC `!l' Z i. 2607 (Z SUBSET IMAGE f (POW A.S) UNION IMAGE f' (POW A.S)) ==> ((Z UNION 2608 (i DIFF 2609 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) DIFF 2610 A.S UNION l') INTER A.S = (l' INTER A.S))` THEN1 ( 2611 UNDISCH_NO_TAC 4 (*DISJOINT IMAGE IMAGE*) THEN 2612 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, SUBSET_DEF, 2613 GSYM SUBSET_COMPL_DISJOINT, IN_COMPL] THEN 2614 METIS_TAC[] 2615 ) THEN 2616 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2617 2618 SUBGOAL_TAC `!l' Z i. (Z SUBSET IMAGE f (POW A.S) UNION IMAGE f' (POW A.S)) ==> (( 2619 (f (l' INTER A.S) IN 2620 Z UNION 2621 (i DIFF 2622 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) DIFF 2623 A.S UNION l') = (f (l' INTER A.S) IN (Z UNION (l' DIFF A.S)))) /\ 2624 2625 ((f' (l' INTER A.S) IN 2626 Z UNION 2627 (i DIFF 2628 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))) DIFF 2629 A.S UNION l') = (f' (l' INTER A.S) IN (Z UNION (l' DIFF A.S)))))` THEN1 ( 2630 2631 SIMP_ALL_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 2632 UNION_SUBSET] THEN 2633 UNDISCH_NO_TAC 5 (*DISJOINT IMAGE f' IV*) THEN 2634 UNDISCH_NO_TAC 5 (*DISJOINT IMAGE f IV*) THEN 2635 UNDISCH_NO_TAC 10 (*A.S SUBSET IV*) THEN 2636 REPEAT WEAKEN_HD_TAC THEN 2637 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, SUBSET_DEF, 2638 GSYM SUBSET_COMPL_DISJOINT, IN_COMPL, IN_IMAGE, IN_POW] THEN 2639 METIS_TAC[INTER_SUBSET, SUBSET_DEF] 2640 ) THEN 2641 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2642 2643 SUBGOAL_TAC `(!e. 2644 ~(e IN IMAGE (\s. XP_PROP (f' s)) (POW A.S)) \/ 2645 ~XP_SEM e 2646 (S1 UNION 2647 (i1 DIFF 2648 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))), 2649 S2 UNION 2650 (i2 DIFF 2651 (IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))))) = 2652 (S1 INTER IMAGE f' (POW A.S) = EMPTY)` THEN1 ( 2653 SIMP_TAC std_ss [IN_IMAGE, GSYM LEFT_FORALL_OR_THM, XP_SEM_THM, IN_POW, IN_UNION, EXTENSION, IN_INTER, IN_IMAGE, NOT_IN_EMPTY, IN_DIFF] THEN 2654 METIS_TAC[] 2655 ) THEN 2656 POP_NO_ASSUM 0 (fn thm => 2657 let 2658 val thm2 = ONCE_REWRITE_RULE [prove (``(A = B) = (~A = ~B)``, PROVE_TAC[])] thm 2659 val thm2 = CONV_RULE (LHS_CONV (SIMP_CONV std_ss [])) thm2 2660 in 2661 ASSUME_TAC thm THEN ASSUME_TAC thm2 2662 end) THEN 2663 ASM_SIMP_TAC std_ss [] THEN NTAC 2 WEAKEN_HD_TAC THEN 2664 2665 SUBGOAL_TAC `!i1 i2 l' l''. XP_SEM A.R 2666 (S1 UNION 2667 (i1 DIFF 2668 (IMAGE f (POW A.S) UNION 2669 IMAGE f' (POW A.S))) DIFF A.S UNION l'', 2670 S2 UNION 2671 (i2 DIFF 2672 (IMAGE f (POW A.S) UNION 2673 IMAGE f' (POW A.S))) DIFF A.S UNION l') = 2674 2675 (XP_SEM A.R (l'' UNION (i1 DIFF A.S), l' UNION (i2 DIFF A.S)))` THEN1 ( 2676 REPEAT GEN_TAC THEN 2677 ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN 2678 MATCH_MP_TAC (prove (``(s1 = s1') /\ (s2 = s2') ==> (XP_SEM xp (s1, s2) = XP_SEM xp (s1', s2'))``, PROVE_TAC[])) THEN 2679 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, 2680 EXTENSION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, IN_INTER, IN_DIFF, XP_USED_VARS_def] THEN 2681 METIS_TAC[] 2682 ) THEN 2683 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2684 2685 2686 SUBGOAL_TAC `!i2 l'. (P_SEM 2687 (S2 UNION 2688 (i2 DIFF 2689 (IMAGE f (POW A.S) UNION 2690 IMAGE f' (POW A.S))) DIFF A.S UNION l') pS) = 2691 2692 (P_SEM l' pS)` THEN1 ( 2693 REPEAT GEN_TAC THEN 2694 ONCE_REWRITE_TAC[P_USED_VARS_INTER_THM] THEN 2695 AP_THM_TAC THEN AP_TERM_TAC THEN 2696 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, 2697 EXTENSION, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, IN_INTER, IN_DIFF, XP_USED_VARS_def] THEN 2698 METIS_TAC[] 2699 ) THEN 2700 ASM_SIMP_TAC std_ss [IN_ABS] THEN WEAKEN_HD_TAC THEN 2701 2702 SUBGOAL_TAC `!l'. l' SUBSET A.S ==> 2703 (((l' INTER A.S = l') /\ (l' DIFF A.S = EMPTY)) /\ 2704 (((f l' IN IMAGE f (POW A.S)) /\ (f' l' IN IMAGE f' (POW A.S))) /\ 2705 (~(f' l' IN IMAGE f (POW A.S)) /\ ~(f l' IN IMAGE f' (POW A.S)))))` THEN1 ( 2706 GEN_TAC THEN NTAC 2 STRIP_TAC THENL [ 2707 METIS_TAC [SUBSET_INTER_ABSORPTION, DIFF_SUBSET_EMPTY], 2708 2709 2710 LEFT_CONJ_TAC THENL [ 2711 SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2712 PROVE_TAC[], 2713 2714 PROVE_TAC[DISJOINT_DISJ_THM] 2715 ] 2716 ] 2717 ) THEN 2718 2719 EQ_TAC THENL [ 2720 ASM_SIMP_TAC std_ss [EXTENSION, IN_UNION, GSPECIFICATION] THEN 2721 DISCH_TAC THEN GEN_TAC THEN 2722 Cases_on `~(x IN IMAGE f (POW A.S) UNION IMAGE f' (POW A.S))` THEN1 ( 2723 SIMP_ALL_TAC std_ss [IN_UNION, SUBSET_DEF] THEN 2724 ASM_REWRITE_TAC[] THEN 2725 METIS_TAC[] 2726 ) THEN 2727 UNDISCH_HD_TAC THEN 2728 SIMP_TAC std_ss [IN_UNION] THEN 2729 STRIP_TAC THENL [ 2730 `~(x IN IMAGE f' (POW A.S))` by PROVE_TAC[DISJOINT_DISJ_THM] THEN 2731 FULL_SIMP_TAC std_ss [] THEN 2732 SIMP_ALL_TAC std_ss [IN_IMAGE, IN_POW] THEN 2733 Q_SPEC_NO_ASSUM 5 `x'` THEN 2734 UNDISCH_HD_TAC THEN 2735 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY] THEN 2736 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2737 METIS_TAC[NOT_IN_EMPTY], 2738 2739 2740 `~(x IN IMAGE f (POW A.S))` by PROVE_TAC[DISJOINT_DISJ_THM] THEN 2741 FULL_SIMP_TAC std_ss [] THEN 2742 SIMP_ALL_TAC std_ss [IN_IMAGE, IN_POW] THEN 2743 Q_SPEC_NO_ASSUM 3 `x'` THEN 2744 UNDISCH_HD_TAC THEN 2745 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY] THEN 2746 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2747 METIS_TAC[NOT_IN_EMPTY] 2748 ], 2749 2750 2751 2752 ASM_SIMP_TAC std_ss [UNION_EMPTY, GSPECIFICATION, IN_UNION, NOT_IN_EMPTY] THEN 2753 REPEAT STRIP_TAC THENL [ 2754 SUBGOAL_TAC `f l' IN IMAGE f (POW A.S)` THEN1 ( 2755 SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2756 PROVE_TAC[] 2757 ) THEN 2758 `~(f l' IN IMAGE f' (POW A.S))` by PROVE_TAC [DISJOINT_DISJ_THM] THEN 2759 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY, IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM, 2760 GSYM LEFT_EXISTS_AND_THM, IN_POW] THEN 2761 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2762 Q_TAC EXISTS_TAC `x` THEN 2763 ASM_SIMP_TAC std_ss [] THEN 2764 METIS_TAC[], 2765 2766 Q_TAC EXISTS_TAC `l''` THEN 2767 ASM_SIMP_TAC std_ss [] THEN 2768 PROVE_TAC[SUBSET_INTER_ABSORPTION], 2769 2770 PROVE_TAC[DIFF_SUBSET_EMPTY, NOT_IN_EMPTY] 2771 ], 2772 2773 2774 2775 Cases_on `(S1 INTER IMAGE f' (POW A.S) = {})` THENL [ 2776 ASM_SIMP_TAC std_ss [IN_IMAGE, IN_POW, UNION_EMPTY, IN_UNION, GSPECIFICATION] THEN 2777 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2778 Q_TAC EXISTS_TAC `x` THEN 2779 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY] THEN 2780 METIS_TAC[], 2781 2782 Q_TAC EXISTS_TAC `f l''` THEN 2783 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY] THEN 2784 METIS_TAC[], 2785 2786 PROVE_TAC[NOT_IN_EMPTY] 2787 ], 2788 2789 2790 ASM_REWRITE_TAC[IN_IMAGE, IN_POW] THEN 2791 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2792 Q_TAC EXISTS_TAC `x` THEN 2793 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY] THEN 2794 METIS_TAC[], 2795 2796 Q_TAC EXISTS_TAC `f' l''` THEN 2797 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY] THEN 2798 METIS_TAC[], 2799 2800 PROVE_TAC[NOT_IN_EMPTY] 2801 ] 2802 ] 2803 ] 2804 ] 2805]); 2806 2807 2808val SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS = 2809 store_thm ( 2810 "SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS", 2811 ``!A f f' p. (FINITE A.S /\ (P_USED_VARS p SUBSET 2812 SEMI_AUTOMATON_USED_VARS A) /\ 2813 DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A) /\ 2814 DISJOINT (IMAGE f' (POW A.S)) (SEMI_AUTOMATON_USED_VARS A)) ==> 2815 (SEMI_AUTOMATON_USED_INPUT_VARS 2816 (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A f f' p) = 2817 SEMI_AUTOMATON_USED_INPUT_VARS A)``, 2818 2819 REPEAT GEN_TAC THEN 2820 ASM_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 2821 SEMI_AUTOMATON_USED_INPUT_VARS_def, 2822 symbolic_semi_automaton_REWRITES, 2823 P_USED_VARS_EVAL, XP_USED_VARS_EVAL, 2824 XP_COND_def, P_BIGOR___P_USED_VARS, 2825 P_FORALL___P_USED_VARS, VAR_RENAMING_HASHTABLE_def, 2826 XP_FORALL___XP_USED_VARS, 2827 XP_EXISTS___XP_USED_VARS, 2828 XP_USED_VARS_def, 2829 XP_USED_VARS_EVAL, 2830 XP_BIGOR___XP_USED_VARS, 2831 SET_TO_LIST_INV, UNION_EMPTY, 2832 P_PROP_SET_MODEL___P_USED_VARS] THEN 2833 2834 ONCE_REWRITE_TAC[EXTENSION] THEN 2835 REPEAT STRIP_TAC THEN 2836 2837 ASM_SIMP_TAC std_ss [IN_UNION, IN_DIFF, 2838 IN_LIST_BIGUNION, MEM_MAP, GSYM LEFT_EXISTS_AND_THM, 2839 MEM_SET_TO_LIST, FINITE_POW_IFF, IMAGE_FINITE, 2840 IN_IMAGE, P_USED_VARS_EVAL, IN_SING, 2841 XP_USED_VARS_EVAL, 2842 IN_POW, 2843 P_PROP_SET_MODEL___P_USED_VARS, NOT_IN_EMPTY] THEN 2844 2845 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, IN_POW, 2846 IN_IMAGE, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, 2847 XP_USED_VARS_def] THEN 2848 2849 EQ_TAC THEN REPEAT STRIP_TAC THEN 2850 METIS_TAC[SUBSET_DEF, IN_UNION]); 2851 2852 2853 2854 2855val SYMBOLIC___NDET_FG___TO___DET_FG___CONCRETE_THM = 2856 store_simp_thm ("SYMBOLIC___NDET_FG___TO___DET_FG___CONCRETE_THM", 2857 2858``!A p f f' A' p'. 2859 (FINITE A.S /\ 2860 (P_USED_VARS p SUBSET A.S) /\ 2861 (A' = SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A f f' p) /\ 2862 (p' = (P_BIGOR (SET_TO_LIST 2863 (IMAGE (\s. P_PROP (f' s)) (POW A.S))))) /\ 2864 INJ f (POW A.S) UNIV /\ 2865 INJ f' (POW A.S) UNIV /\ 2866 DISJOINT (IMAGE f (POW A.S)) (SEMI_AUTOMATON_USED_VARS A) /\ 2867 DISJOINT (IMAGE f' (POW A.S)) (SEMI_AUTOMATON_USED_VARS A) /\ 2868 DISJOINT (IMAGE f (POW A.S)) (IMAGE f' (POW A.S))) ==> 2869 2870((!i. 2871(A_SEM i (A_NDET (A, ACCEPT_COND_FG p)) = 2872A_SEM i (A_NDET (A', ACCEPT_COND_FG p')))) /\ 2873IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A')``, 2874 2875 2876 2877REPEAT GEN_TAC THEN STRIP_TAC THEN 2878 2879SUBGOAL_TAC `?inv_f. !x. (x IN POW A.S) ==> (inv_f (f x) = x)` THEN1 ( 2880 PROVE_TAC[INJ_INVERSE] 2881) THEN 2882SUBGOAL_TAC `?inv_f'. !x. (x IN POW A.S) ==> (inv_f' (f' x) = x)` THEN1 ( 2883 PROVE_TAC[INJ_INVERSE] 2884) THEN 2885`?g. g = \x. if (x IN IMAGE f (POW A.S)) then inv_f x else inv_f' x` by METIS_TAC[] THEN 2886 2887REPEAT STRIP_TAC THENL [ 2888 2889 MATCH_MP_TAC SYMBOLIC___NDET_FG___TO___DET_FG___THM THEN 2890 2891 Q_TAC EXISTS_TAC `SEMI_AUTOMATON_USED_VARS A` THEN 2892 Q_TAC EXISTS_TAC `f` THEN 2893 Q_TAC EXISTS_TAC `f'` THEN 2894 Q_TAC EXISTS_TAC `g` THEN 2895 Q_TAC EXISTS_TAC `\s. s SUBSET A.S /\ P_SEM s p` THEN 2896 2897 2898 ASM_REWRITE_TAC[] THEN 2899 REPEAT STRIP_TAC THENL [ 2900 ASM_SIMP_TAC std_ss [P_USED_VARS_EVAL, P_BIGOR___P_USED_VARS, 2901 SUBSET_DEF, SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 2902 symbolic_semi_automaton_REWRITES, IN_LIST_BIGUNION, MEM_MAP, 2903 GSYM LEFT_EXISTS_AND_THM, 2904 MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_POW_IFF, 2905 IN_IMAGE, IN_SING, IN_UNION] THEN 2906 PROVE_TAC[], 2907 2908 2909 MATCH_MP_TAC SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS THEN 2910 ASM_REWRITE_TAC[] THEN 2911 REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN 2912 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 2913 2914 2915 MATCH_MP_TAC SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_THM THEN 2916 ASM_SIMP_TAC std_ss [SUBSET_REFL] THEN 2917 SIMP_ALL_TAC std_ss [IN_POW, GSYM FORALL_AND_THM, 2918 GSYM IMP_CONJ_THM] THEN 2919 GEN_TAC THEN STRIP_TAC THEN 2920 2921 SUBGOAL_TAC `f z IN IMAGE f (POW A.S) /\ 2922 f' z IN IMAGE f' (POW A.S)` THEN1 ( 2923 ASM_SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2924 PROVE_TAC[] 2925 ) THEN 2926 SUBGOAL_TAC `~(f' z IN IMAGE f (POW A.S))` THEN1 ( 2927 PROVE_TAC[DISJOINT_DISJ_THM] 2928 ) THEN 2929 ASM_SIMP_TAC std_ss [], 2930 2931 2932 ASM_SIMP_TAC std_ss [P_SEM_THM, P_BIGOR_SEM, MEM_SET_TO_LIST, 2933 IMAGE_FINITE, FINITE_POW_IFF, IN_IMAGE, GSYM LEFT_EXISTS_AND_THM] THEN 2934 SIMP_TAC std_ss [EXTENSION, NOT_IN_EMPTY, IN_INTER, IN_IMAGE] THEN 2935 PROVE_TAC[] 2936 ], 2937 2938 2939 2940 2941 MATCH_MP_TAC SYMBOLIC_BREAKPOINT_CONSTRUCTION___IS_DET_TOTAL THEN 2942 Q_TAC EXISTS_TAC `A` THEN 2943 Q_TAC EXISTS_TAC `SEMI_AUTOMATON_USED_VARS A` THEN 2944 Q_TAC EXISTS_TAC `f` THEN 2945 Q_TAC EXISTS_TAC `f'` THEN 2946 Q_TAC EXISTS_TAC `g` THEN 2947 Q_TAC EXISTS_TAC `\s. s SUBSET A.S /\ P_SEM s p` THEN 2948 2949 MATCH_MP_TAC SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_THM THEN 2950 ASM_SIMP_TAC std_ss [SUBSET_REFL] THEN 2951 SIMP_ALL_TAC std_ss [IN_POW, GSYM FORALL_AND_THM, 2952 GSYM IMP_CONJ_THM] THEN 2953 GEN_TAC THEN STRIP_TAC THEN 2954 2955 SUBGOAL_TAC `f z IN IMAGE f (POW A.S) /\ 2956 f' z IN IMAGE f' (POW A.S)` THEN1 ( 2957 ASM_SIMP_TAC std_ss [IN_IMAGE, IN_POW] THEN 2958 PROVE_TAC[] 2959 ) THEN 2960 SUBGOAL_TAC `~(f' z IN IMAGE f (POW A.S))` THEN1 ( 2961 PROVE_TAC[DISJOINT_DISJ_THM] 2962 ) THEN 2963 ASM_SIMP_TAC std_ss [] 2964]); 2965 2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980val KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_def = 2981 Define `KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE (ks:('a, 'b) kripke_structure) f = 2982 symbolic_kripke_structure 2983 (P_BIGOR (SET_TO_LIST ((IMAGE (\s. P_PROP_SET_MODEL (f s) (BIGUNION (IMAGE f ks.S))) ks.S0)))) 2984 2985 (XP_AND( 2986 XP_CURRENT(P_BIGAND (SET_TO_LIST (IMAGE 2987 (\s. P_IMPL(P_PROP_SET_MODEL (f s) (BIGUNION (IMAGE f ks.S)), P_PROP_SET_MODEL (ks.L s) (ks.P) )) ks.S))), 2988 2989 XP_BIGOR (SET_TO_LIST ((IMAGE (\(s1, s2). XP_AND(XP_CURRENT (P_PROP_SET_MODEL (f s1) (BIGUNION (IMAGE f ks.S))), XP_NEXT (P_PROP_SET_MODEL (f s2) (BIGUNION (IMAGE f ks.S))))) ks.R)))))`; 2990 2991 2992val KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_THM = 2993 store_thm ( 2994 "KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_THM", 2995 2996 ``!K S f. 2997 2998 IS_WELL_FORMED_KRIPKE_STRUCTURE K /\ 2999 (S = (BIGUNION (IMAGE f K.S))) /\ 3000 INJ f K.S UNIV /\ 3001 (!s. s IN K.S ==> FINITE (f s)) /\ 3002 DISJOINT S K.P ==> 3003 3004 !p. IS_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE K p = 3005 ((!n. p n IN K.S) /\ IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE 3006 (KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE K f) 3007 (\n. f (p n) UNION K.L (p n)))``, 3008 3009REWRITE_TAC [IS_WELL_FORMED_KRIPKE_STRUCTURE_def] THEN 3010REPEAT STRIP_TAC THEN 3011`FINITE K.S0` by PROVE_TAC[SUBSET_FINITE] THEN 3012`FINITE K.R` by PROVE_TAC[SUBSET_FINITE, FINITE_CROSS] THEN 3013SUBGOAL_TAC `FINITE (BIGUNION (IMAGE f K.S))` THEN1 ( 3014 MATCH_MP_TAC FINITE_BIGUNION THEN 3015 ASM_SIMP_TAC std_ss [IMAGE_FINITE, IN_IMAGE] THEN 3016 PROVE_TAC[] 3017) THEN 3018ASM_SIMP_TAC std_ss [IS_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE_def, 3019 IS_PATH_THROUGH_KRIPKE_STRUCTURE_def, 3020 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 3021 KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_def, 3022 symbolic_kripke_structure_REWRITES, 3023 XP_SEM_THM, XP_SEM___XP_CURRENT, 3024 P_BIGAND_SEM, MEM_SET_TO_LIST, 3025 IMAGE_FINITE, IN_IMAGE, 3026 GSYM LEFT_FORALL_IMP_THM, 3027 P_SEM_THM, 3028 P_PROP_SET_MODEL_SEM, 3029 P_BIGOR_SEM, GSYM LEFT_EXISTS_AND_THM, 3030 XP_BIGOR_SEM, 3031 prove (``(?x:('b # 'b). P x) = ?s1 s2. P (s1, s2)``, 3032 METIS_TAC[PAIR]), 3033 XP_SEM___XP_NEXT] THEN 3034 3035SUBGOAL_TAC `!n s. (s IN K.S /\ (p n) IN K.S) ==> (((f (p n) UNION (K.L (p n))) INTER BIGUNION (IMAGE f K.S) = 3036 f s INTER BIGUNION (IMAGE f K.S)) = (s = p n))` THEN1 ( 3037 REPEAT STRIP_TAC THEN 3038 SUBGOAL_TAC `(f s INTER BIGUNION (IMAGE f K.S)) = f s` THEN1 ( 3039 ONCE_REWRITE_TAC[EXTENSION] THEN 3040 SIMP_TAC std_ss [IN_UNION, IN_INTER, IN_BIGUNION, IN_IMAGE, 3041 GSYM RIGHT_EXISTS_AND_THM] THEN 3042 METIS_TAC[] 3043 ) THEN 3044 SUBGOAL_TAC `(f (p n) UNION K.L (p n)) INTER BIGUNION (IMAGE f K.S) = f (p n)` THEN1 ( 3045 UNDISCH_NO_TAC 6 (*DISJOING S IMAGE g*) THEN 3046 ONCE_REWRITE_TAC[EXTENSION] THEN 3047 ASM_SIMP_TAC std_ss [IN_UNION, IN_INTER, DISJOINT_DISJ_THM, 3048 GSYM RIGHT_EXISTS_AND_THM, IN_BIGUNION, 3049 IN_IMAGE] THEN 3050 METIS_TAC[SUBSET_DEF] 3051 ) THEN 3052 ASM_REWRITE_TAC[] THEN 3053 3054 METIS_TAC[INJ_DEF] 3055) THEN 3056 3057EQ_TAC THENL [ 3058 STRIP_TAC THEN 3059 `!n. p n IN K.S` by 3060 METIS_TAC[SUBSET_DEF, IN_CROSS, FST, SND] THEN 3061 REPEAT STRIP_TAC THENL [ 3062 ASM_REWRITE_TAC[], 3063 3064 UNDISCH_HD_TAC THEN 3065 ASM_SIMP_TAC std_ss [] THEN 3066 STRIP_TAC THEN 3067 3068 ONCE_REWRITE_TAC [EXTENSION] THEN GEN_TAC THEN 3069 SIMP_TAC std_ss [IN_INTER, IN_UNION] THEN 3070 REPEAT BOOL_EQ_STRIP_TAC THEN 3071 CCONTR_TAC THEN 3072 REMAINS_TAC `x IN S` THEN1 METIS_TAC[DISJOINT_DISJ_THM] THEN 3073 ASM_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM] THEN 3074 PROVE_TAC[], 3075 3076 3077 Q_TAC EXISTS_TAC `p n` THEN 3078 Q_TAC EXISTS_TAC `p (SUC n)` THEN 3079 ASM_SIMP_TAC std_ss [], 3080 3081 Q_TAC EXISTS_TAC `p 0` THEN 3082 ASM_SIMP_TAC std_ss [] 3083 ], 3084 3085 3086 SIMP_TAC std_ss [FORALL_AND_THM] THEN 3087 REPEAT STRIP_TAC THENL [ 3088 Q_SPEC_NO_ASSUM 2 `n` THEN 3089 CLEAN_ASSUMPTIONS_TAC THEN 3090 `s1 IN K.S /\ s2 IN K.S` by METIS_TAC[IN_CROSS, SUBSET_DEF, FST, SND] THEN 3091 METIS_TAC[], 3092 3093 METIS_TAC[SUBSET_DEF] 3094 ] 3095]); 3096 3097 3098 3099 3100 3101 3102val KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE___TRACE_OF_INITIAL_PATH = 3103 store_thm ( 3104 "KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE___TRACE_OF_INITIAL_PATH", 3105 3106 ``!K S f. 3107 3108 IS_WELL_FORMED_KRIPKE_STRUCTURE K /\ 3109 (S = (BIGUNION (IMAGE f K.S))) /\ 3110 INJ f K.S UNIV /\ 3111 (!s. s IN K.S ==> FINITE (f s)) /\ 3112 DISJOINT S K.P ==> 3113 3114 !p. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE 3115 (KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE K f) p ==> 3116 3117 IS_TRACE_OF_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE K 3118 (PATH_RESTRICT p K.P)``, 3119 3120REPEAT GEN_TAC THEN STRIP_TAC THEN 3121ASM_SIMP_TAC std_ss [IS_TRACE_OF_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE_def] THEN 3122 3123ASSUME_TAC (SIMP_RULE std_ss [] KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_THM) THEN 3124Q_SPECL_NO_ASSUM 0 [`K`, `f`] THEN 3125PROVE_CONDITION_NO_ASSUM 0 THEN1 PROVE_TAC[] THEN 3126ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 3127 3128SIMP_ALL_TAC std_ss [IS_WELL_FORMED_KRIPKE_STRUCTURE_def] THEN 3129`FINITE K.S0` by PROVE_TAC[SUBSET_FINITE] THEN 3130`FINITE K.R` by PROVE_TAC[SUBSET_FINITE, FINITE_CROSS] THEN 3131SUBGOAL_TAC `FINITE (BIGUNION (IMAGE f K.S))` THEN1 ( 3132 MATCH_MP_TAC FINITE_BIGUNION THEN 3133 ASM_SIMP_TAC std_ss [IMAGE_FINITE, IN_IMAGE] THEN 3134 PROVE_TAC[] 3135) THEN 3136 3137 3138ASM_SIMP_TAC std_ss [TRACE_OF_PATH_THROUGH_KRIPKE_STRUCTURE_def, 3139 KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_def, 3140 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 3141 symbolic_kripke_structure_REWRITES, 3142 XP_SEM_THM, P_SEM_THM, P_BIGOR_SEM, 3143 MEM_SET_TO_LIST, IMAGE_FINITE, 3144 IN_IMAGE, GSYM LEFT_EXISTS_AND_THM, 3145 XP_SEM___XP_CURRENT, XP_BIGOR_SEM, 3146 prove (``(?x:('b # 'b). P x) = ?s1 s2. P (s1, s2)``, 3147 METIS_TAC[PAIR]), 3148 P_BIGAND_SEM, 3149 GSYM LEFT_FORALL_IMP_THM, XP_SEM___XP_NEXT, 3150 P_PROP_SET_MODEL_SEM 3151 ] THEN 3152 3153 3154 3155REWRITE_TAC [IS_WELL_FORMED_KRIPKE_STRUCTURE_def] THEN 3156REPEAT STRIP_TAC THEN 3157rename1 `s IN K.S0` THEN 3158`FINITE K.S0` by PROVE_TAC[SUBSET_FINITE] THEN 3159`FINITE K.R` by PROVE_TAC[SUBSET_FINITE, FINITE_CROSS] THEN 3160SUBGOAL_TAC `FINITE (BIGUNION (IMAGE f K.S))` THEN1 ( 3161 MATCH_MP_TAC FINITE_BIGUNION THEN 3162 ASM_SIMP_TAC std_ss [IMAGE_FINITE, IN_IMAGE] THEN 3163 PROVE_TAC[] 3164) THEN 3165 3166 3167SUBGOAL_TAC `!s. s IN K.S ==> ((f s INTER BIGUNION (IMAGE f K.S)) = f s)` THEN1 ( 3168 ONCE_REWRITE_TAC[EXTENSION] THEN 3169 SIMP_TAC std_ss [IN_UNION, IN_INTER, IN_BIGUNION, IN_IMAGE, 3170 GSYM RIGHT_EXISTS_AND_THM] THEN 3171 METIS_TAC[] 3172) THEN 3173 3174SUBGOAL_TAC `!s'. s' IN K.S ==> ((f s' UNION (K.L s')) INTER BIGUNION (IMAGE f K.S) = f s')` THEN1 ( 3175 REPEAT STRIP_TAC THEN 3176 UNDISCH_NO_TAC 8 (*DISJOING S K.P*) THEN 3177 ONCE_REWRITE_TAC[EXTENSION] THEN 3178 ASM_SIMP_TAC std_ss [IN_UNION, IN_INTER, DISJOINT_DISJ_THM, 3179 GSYM RIGHT_EXISTS_AND_THM, IN_BIGUNION, 3180 IN_IMAGE] THEN 3181 METIS_TAC[SUBSET_DEF] 3182) THEN 3183 3184SUBGOAL_TAC `!s s'. (s IN K.S /\ s' IN K.S) ==> (((f s' UNION (K.L s')) INTER BIGUNION (IMAGE f K.S) = 3185 f s INTER BIGUNION (IMAGE f K.S)) = (s = s'))` THEN1 ( 3186 REPEAT STRIP_TAC THEN 3187 ASM_SIMP_TAC std_ss [] THEN 3188 METIS_TAC[INJ_DEF] 3189) THEN 3190 3191SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN 3192REPEAT STRIP_TAC THEN 3193`?w'. w' = (CHOOSEN_PATH {s} (\s1 sn x. x IN K.S /\ (((f x) INTER BIGUNION (IMAGE f K.S)) = ((p sn) INTER BIGUNION (IMAGE f K.S)))))` by METIS_TAC[] THEN 3194 3195Q_TAC EXISTS_TAC `w'` THEN 3196 3197 3198SUBGOAL_TAC `(!n. w' n IN K.S /\ 3199 (((p n) INTER BIGUNION (IMAGE f K.S)) = (f (w' n))))` THEN1 ( 3200 ASM_REWRITE_TAC[] THEN 3201 Cases_on `n` THENL [ 3202 SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_SING] THEN 3203 METIS_TAC[SUBSET_DEF], 3204 3205 3206 SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_ABS] THEN 3207 SELECT_ELIM_TAC THEN 3208 REPEAT STRIP_TAC THENL [ 3209 Q_SPEC_NO_ASSUM 7 `n'` (*K.R def*) THEN 3210 CLEAN_ASSUMPTIONS_TAC THEN 3211 Q_TAC EXISTS_TAC `s2` THEN 3212 ASM_REWRITE_TAC[] THEN 3213 METIS_TAC[SUBSET_DEF, IN_CROSS, SND], 3214 3215 ASM_REWRITE_TAC[], 3216 3217 METIS_TAC[] 3218 ] 3219 ] 3220) THEN 3221 3222GSYM_NO_TAC 1 (*Def w'*) THEN 3223ASM_SIMP_TAC std_ss [] THEN 3224REPEAT STRIP_TAC THENL [ 3225 UNDISCH_NO_TAC 12 (*DISJOINT S K.P*) THEN 3226 ASM_REWRITE_TAC[] THEN 3227 `w' n IN K.S` by PROVE_TAC[] THEN 3228 UNDISCH_HD_TAC THEN 3229 REPEAT WEAKEN_HD_TAC THEN 3230 3231 SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_BIGUNION, IN_IMAGE, 3232 EXTENSION, IN_INTER, IN_UNION] THEN 3233 METIS_TAC[], 3234 3235 3236 3237 Q_TAC EXISTS_TAC `w' n` THEN 3238 Q_TAC EXISTS_TAC `w' (SUC n)` THEN 3239 ASM_SIMP_TAC std_ss [] THEN 3240 3241 Q_SPEC_NO_ASSUM 8 `n` THEN 3242 CLEAN_ASSUMPTIONS_TAC THEN 3243 `s1 IN K.S /\ s2 IN K.S` by METIS_TAC[SUBSET_DEF, IN_CROSS, FST, SND] THEN 3244 NTAC 3 (UNDISCH_NO_TAC 2) THEN 3245 ASM_SIMP_TAC std_ss [] THEN 3246 METIS_TAC[INJ_DEF], 3247 3248 3249 Q_TAC EXISTS_TAC `w' 0` THEN 3250 GSYM_NO_TAC 0 (*Def w'*) THEN 3251 ONCE_ASM_REWRITE_TAC[] THEN 3252 GSYM_NO_TAC 0 (*Def w'*) THEN 3253 ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_SING] THEN 3254 METIS_TAC[SUBSET_DEF], 3255 3256 3257 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 3258 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 3259 Q_SPECL_NO_ASSUM 7 [`x`, `w' x`] THEN 3260 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 3261 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN 3262 ASM_REWRITE_TAC[GSYM SUBSET_INTER_ABSORPTION] THEN 3263 METIS_TAC[] 3264]); 3265 3266 3267 3268val UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES_ARE_ULTIMATIVELY_PERIODIC = 3269 store_thm ( 3270 "UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES_ARE_ULTIMATIVELY_PERIODIC", 3271 3272 ``!i S M. ((FINITE S /\ IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M i) /\ 3273 (!i'. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M i' ==> (PATH_RESTRICT i' S = PATH_RESTRICT i S))) ==> 3274 (IS_ULTIMATIVELY_PERIODIC_PATH (PATH_RESTRICT i S))``, 3275 3276 3277 3278SIMP_TAC std_ss [PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES] THEN 3279REPEAT STRIP_TAC THEN 3280ASSUME_TAC (INST_TYPE [alpha |-> alpha-->bool] INF_ELEMENTS_OF_PATH_NOT_EMPTY) THEN 3281Q_SPEC_NO_ASSUM 0 `POW (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)` THEN 3282PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3283 SIMP_TAC std_ss [FINITE_POW_IFF, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 3284 FINITE_UNION, FINITE___P_USED_VARS, FINITE___XP_USED_VARS] 3285) THEN 3286Q_SPEC_NO_ASSUM 0 `PATH_RESTRICT i (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)` THEN 3287PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3288 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, IN_POW, INTER_SUBSET] 3289) THEN 3290 3291 3292SIMP_ALL_TAC std_ss [GSYM MEMBER_NOT_EMPTY, 3293 INF_ELEMENTS_OF_PATH_def, GSPECIFICATION] THEN 3294 3295SUBGOAL_TAC `?m0. (PATH_RESTRICT i (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M) m0 = x)` THEN1 ( 3296 Q_SPEC_NO_ASSUM 0 `0:num` THEN 3297 PROVE_TAC[] 3298) THEN 3299 3300SUBGOAL_TAC `?m1. (m1 > m0) /\ 3301 (PATH_RESTRICT i (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M) m1 = x)` THEN1 ( 3302 METIS_TAC[] 3303) THEN 3304 3305`?i'. i' = CUT_PATH_PERIODICALLY (PATH_RESTRICT i (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)) m0 (m1 - m0)` by METIS_TAC[] THEN 3306 3307Q_SPEC_NO_ASSUM 5 `i'` THEN 3308PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3309 ASM_SIMP_TAC std_ss [] THEN 3310 REPEAT STRIP_TAC THENL [ 3311 SIMP_TAC std_ss [CUT_PATH_PERIODICALLY_def, PATH_RESTRICT_def, PATH_MAP_def, SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def] THEN 3312 Cases_on `SUC n < m0` THENL [ 3313 ASM_SIMP_TAC arith_ss [] THEN 3314 PROVE_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, SUBSET_UNION], 3315 3316 3317 Cases_on `SUC n = m0` THENL [ 3318 ASM_SIMP_TAC arith_ss [] THEN 3319 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, SUBSET_UNION], 3320 3321 3322 `~(n < m0)` by DECIDE_TAC THEN 3323 NTAC 2 (WEAKEN_NO_TAC 1) THEN 3324 ASM_SIMP_TAC arith_ss [] THEN 3325 3326 Cases_on `~(1 < m1 - m0)` THEN1 ( 3327 `m1 - m0 = 1` by DECIDE_TAC THEN 3328 ASM_SIMP_TAC std_ss [MOD_1] THEN 3329 SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, 3330 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def] THEN 3331 `m1 = SUC m0` by DECIDE_TAC THEN 3332 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, SUBSET_UNION] 3333 ) THEN 3334 3335 Q.ABBREV_TAC `m' = m1 - m0` THEN 3336 SUBGOAL_TAC `(SUC n - m0) MOD m' = (1 + (n - m0) MOD m') MOD m'` THEN1 ( 3337 SUBGOAL_TAC `1 MOD m' = 1` THEN1 ( 3338 MATCH_RIGHT_EQ_MP_TAC X_MOD_Y_EQ_X THEN 3339 DECIDE_TAC 3340 ) THEN 3341 GSYM_NO_TAC 0 THEN ONCE_ASM_REWRITE_TAC [] THEN WEAKEN_HD_TAC THEN 3342 3343 ASM_SIMP_TAC arith_ss [MOD_PLUS] THEN 3344 AP_THM_TAC THEN AP_TERM_TAC THEN 3345 DECIDE_TAC 3346 ) THEN 3347 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 3348 Q.ABBREV_TAC `r = (n - m0) MOD m'` THEN 3349 Cases_on `1 + r < m'` THENL [ 3350 ASM_SIMP_TAC arith_ss [] THEN 3351 `m0 + (r + 1) = SUC (m0 + r)` by DECIDE_TAC THEN 3352 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, SUBSET_UNION], 3353 3354 SUBGOAL_TAC `1 + r = m'` THEN1 ( 3355 `0 < m'` by DECIDE_TAC THEN 3356 `r < m'` by METIS_TAC [DIVISION] THEN 3357 DECIDE_TAC 3358 ) THEN 3359 ASM_SIMP_TAC arith_ss [] THEN 3360 3361 SUBGOAL_TAC `m0 + r = PRE m1` THEN1 ( 3362 `r = PRE m'` by DECIDE_TAC THEN 3363 Q.UNABBREV_TAC `m'` THEN 3364 DECIDE_TAC 3365 ) THEN 3366 `SUC (PRE m1) = m1` by DECIDE_TAC THEN 3367 SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, 3368 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def] THEN 3369 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, SUBSET_UNION] 3370 ] 3371 ] 3372 ], 3373 3374 `0 < (m1 - m0) + m0` by DECIDE_TAC THEN 3375 ASM_SIMP_TAC std_ss [CUT_PATH_PERIODICALLY___BEGINNING] THEN 3376 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, 3377 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def] THEN 3378 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM, SUBSET_UNION] 3379 ] 3380) THEN 3381 3382GSYM_NO_TAC 0 THEN 3383ASM_REWRITE_TAC[PATH_RESTRICT___CUT_PATH_PERIODICALLY, 3384 IS_ULTIMATIVELY_PERIODIC_PATH_def] THEN 3385Q_TAC EXISTS_TAC `m0` THEN 3386Q_TAC EXISTS_TAC `(m1 - m0)` THEN 3387ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___IS_ULTIMATIVELY_PERIODIC] 3388) 3389 3390 3391val ULTIMALTIVELY_PERIODIC_PATH_CORRESPONDING_TO_UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES = 3392 store_thm ( 3393 "ULTIMALTIVELY_PERIODIC_PATH_CORRESPONDING_TO_UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES", 3394 3395``!i S. (FINITE (S:'a set) /\ INFINITE (UNIV:'a set) /\ 3396 (IS_ULTIMATIVELY_PERIODIC_PATH i)) ==> 3397 3398 (?M. 3399 (?i'. (IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M i')) /\ 3400 (!i'. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M i' ==> (PATH_RESTRICT i' S = PATH_RESTRICT i S)))``, 3401 3402REPEAT STRIP_TAC THEN 3403ASSUME_TAC (INST_TYPE [beta |-> alpha] DET_TOTAL_KRIPKE_STRUCTURES_THM) THEN 3404PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 3405Q_SPECL_NO_ASSUM 0 [`S`, `PATH_RESTRICT i S`] THEN 3406POP_NO_ASSUM 0 (fn thm => ASSUME_TAC (fst (EQ_IMP_RULE thm))) THEN 3407PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3408 REPEAT STRIP_TAC THENL [ 3409 SIMP_ALL_TAC std_ss [IS_ULTIMATIVELY_PERIODIC_PATH_def, 3410 IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE_def] THEN 3411 Q_TAC EXISTS_TAC `n0` THEN 3412 Q_TAC EXISTS_TAC `n` THEN 3413 ASM_REWRITE_TAC[] THEN 3414 REPEAT STRIP_TAC THEN 3415 RES_TAC THEN 3416 ASM_SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def], 3417 3418 ASM_REWRITE_TAC[], 3419 3420 ASM_SIMP_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, 3421 INTER_SUBSET] 3422 ] 3423) THEN 3424CLEAN_ASSUMPTIONS_TAC THEN 3425GSYM_NO_TAC 1 (*M.P = S*) THEN 3426FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 3427 3428SUBGOAL_TAC `?f. INJ f M.S UNIV /\ DISJOINT (IMAGE f M.S) M.P` THEN1 ( 3429 MATCH_MP_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, 3430 AND_IMP_INTRO] FINITE_INJ_EXISTS) THEN 3431 SIMP_ALL_TAC std_ss [IS_WELL_FORMED_KRIPKE_STRUCTURE_def] THEN 3432 ASM_REWRITE_TAC[] 3433) THEN 3434 3435ASSUME_TAC (SIMP_RULE std_ss [] ((INST_TYPE [beta |-> alpha, gamma |-> alpha] KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE_THM))) THEN 3436Q_SPECL_NO_ASSUM 0 [`M`, `\x. {f x}`] THEN 3437 3438PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3439 ASM_SIMP_TAC std_ss [FINITE_SING, INJ_DEF, IN_UNIV, EQUAL_SING] THEN 3440 UNDISCH_HD_TAC (*DISJ IMAGE f M.P*) THEN 3441 UNDISCH_HD_TAC (*INJ f*) THEN 3442 SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_BIGUNION, IN_IMAGE, 3443 GSYM RIGHT_FORALL_OR_THM, IN_SING, INJ_DEF] 3444) THEN 3445 3446SIMP_ALL_TAC std_ss [IMAGE_ID, UNION_SING] THEN 3447Q_TAC EXISTS_TAC `KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE M 3448 (\x. {f x})` THEN 3449REPEAT STRIP_TAC THENL [ 3450 UNDISCH_NO_TAC 4 (*IS_TRACE_OF_INITIAL_PATH*) THEN 3451 ASM_SIMP_TAC std_ss [IS_TRACE_OF_INITIAL_PATH_THROUGH_KRIPKE_STRUCTURE_def] THEN 3452 METIS_TAC[], 3453 3454 ASSUME_TAC (SIMP_RULE std_ss [] (INST_TYPE [beta |-> alpha] 3455 KRIPKE_STRUCTURE___TO___SYMBOLIC_KRIPKE_STRUCTURE___TRACE_OF_INITIAL_PATH)) THEN 3456 Q_SPECL_NO_ASSUM 0 [`M`, `(\x. {f x})`] THEN 3457 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3458 ASM_SIMP_TAC std_ss [FINITE_SING, INJ_DEF, IN_UNIV, EQUAL_SING] THEN 3459 UNDISCH_NO_TAC 2 (*DISJ IMAGE f M.P*) THEN 3460 UNDISCH_NO_TAC 2 (*INJ f*) THEN 3461 SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_BIGUNION, IN_IMAGE, 3462 GSYM RIGHT_FORALL_OR_THM, IN_SING, INJ_DEF] 3463 ) THEN 3464 METIS_TAC[] 3465]); 3466 3467 3468 3469 3470val SYMBOLIC___UNIV_G___TO___DET_GF___EXISTS_THM = 3471 store_thm ( 3472 "SYMBOLIC___UNIV_G___TO___DET_GF___EXISTS_THM", 3473 3474 ``!S A (p:'a prop_logic). (INFINITE (UNIV:'a set) /\ FINITE S /\ FINITE A.S) ==> 3475 3476?A' p'. ((IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A') /\ 3477 (DISJOINT A'.S S) /\ FINITE A'.S /\ 3478 (P_USED_VARS p' SUBSET A'.S) /\ 3479 (!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = 3480 A_SEM i (A_UNIV (A',ACCEPT_COND_GF p'))))``, 3481 3482 3483REPEAT STRIP_TAC THEN 3484SUBGOAL_TAC `!A p i. (A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = 3485 ~A_SEM i (A_NDET (A,ACCEPT_COND_F (P_NOT p)))) /\ 3486 (A_SEM i (A_UNIV (A,ACCEPT_COND_GF p)) = 3487 ~A_SEM i (A_NDET (A,ACCEPT_COND_FG (P_NOT p))))` THEN1 ( 3488 SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_FG_def, ACCEPT_COND_GF_def, 3489 ACCEPT_COND_F_def, ACCEPT_COND_G_def, ACCEPT_COND_SEM_def, 3490 ACCEPT_COND_SEM_TIME_def, ACCEPT_F_def, P_SEM_THM] THEN 3491 METIS_TAC[] 3492) THEN 3493ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 3494 3495SUBGOAL_TAC `?x. ~(x IN SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p)` THEN1 ( 3496 REMAINS_TAC `FINITE (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p)` THEN1 ( 3497 METIS_TAC[IN_INFINITE_NOT_FINITE, IN_UNIV] 3498 ) THEN 3499 ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, FINITE_UNION, 3500 FINITE___P_USED_VARS, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS] 3501) THEN 3502 3503ASSUME_TAC (REWRITE_RULE [AUTOMATON_EQUIV_def] A_SEM___NDET_F___TO___NDET_FG) THEN 3504Q_SPECL_NO_ASSUM 0 [`A`, `P_NOT p`, `x`] THEN 3505PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[P_USED_VARS_def] THEN 3506ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 3507 3508Q.ABBREV_TAC `B = (symbolic_semi_automaton (x INSERT A.S) 3509 (P_AND (P_EQUIV (P_PROP x,P_NOT p),A.S0)) 3510 (XP_AND 3511 (XP_EQUIV 3512 (XP_NEXT_PROP x, 3513 XP_OR (XP_PROP x,XP_NEXT (P_NOT p))),A.R)))` THEN 3514SUBGOAL_TAC `?f. INJ f (POW B.S) UNIV /\ DISJOINT (IMAGE f (POW B.S)) (SEMI_AUTOMATON_USED_VARS B UNION S)` THEN1 ( 3515 MATCH_MP_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, 3516 AND_IMP_INTRO] FINITE_INJ_EXISTS) THEN 3517 Q.UNABBREV_TAC `B` THEN 3518 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, 3519 FINITE_POW_IFF, FINITE_INSERT, SEMI_AUTOMATON_USED_VARS_def, 3520 FINITE_UNION, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS] 3521) THEN 3522 3523SUBGOAL_TAC `?f'. INJ f' (POW B.S) UNIV /\ DISJOINT (IMAGE f' (POW B.S)) (SEMI_AUTOMATON_USED_VARS B UNION (IMAGE f (POW B.S)) UNION S)` THEN1 ( 3524 MATCH_MP_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, 3525 AND_IMP_INTRO] FINITE_INJ_EXISTS) THEN 3526 Q.UNABBREV_TAC `B` THEN 3527 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, 3528 FINITE_POW_IFF, FINITE_INSERT, SEMI_AUTOMATON_USED_VARS_def, 3529 FINITE_UNION, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, 3530 IMAGE_FINITE] 3531) THEN 3532 3533 3534ASSUME_TAC SYMBOLIC___NDET_FG___TO___DET_FG___CONCRETE_THM THEN 3535Q_SPECL_NO_ASSUM 0 [`B`, `P_PROP x`, `f`, `f'`] THEN 3536PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3537 FULL_SIMP_TAC std_ss [DISJOINT_UNION_BOTH, DISJOINT_SYM] THEN 3538 Q.UNABBREV_TAC `B` THEN 3539 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, FINITE_INSERT, 3540 P_USED_VARS_def, SUBSET_DEF, IN_INSERT, NOT_IN_EMPTY] 3541) THEN 3542CLEAN_ASSUMPTIONS_TAC THEN 3543 3544Q_TAC EXISTS_TAC `SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON B f f' (P_PROP x)` THEN 3545Q_TAC EXISTS_TAC `P_NOT (P_BIGOR (SET_TO_LIST (IMAGE (\s. P_PROP (f' s)) (POW B.S))))` THEN 3546 3547ASM_SIMP_TAC std_ss [] THEN 3548REPEAT STRIP_TAC THENL [ 3549 FULL_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 3550 symbolic_semi_automaton_REWRITES, DISJOINT_UNION_BOTH, DISJOINT_SYM], 3551 3552 Q.UNABBREV_TAC `B` THEN 3553 FULL_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 3554 symbolic_semi_automaton_REWRITES, IMAGE_FINITE, FINITE_UNION, FINITE_POW_IFF, FINITE_INSERT], 3555 3556 Q.UNABBREV_TAC `B` THEN 3557 ASM_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 3558 symbolic_semi_automaton_REWRITES, 3559 P_BIGOR___P_USED_VARS, SUBSET_DEF, IN_LIST_BIGUNION, IN_UNION, 3560 MEM_MAP, MEM_SET_TO_LIST, FINITE_POW_IFF, FINITE_INSERT, 3561 IMAGE_FINITE, GSYM LEFT_EXISTS_AND_THM, IN_IMAGE, P_USED_VARS_def, 3562 IN_SING] THEN 3563 METIS_TAC[], 3564 3565 ASM_SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_FG_def, ACCEPT_COND_SEM_def, 3566 ACCEPT_COND_SEM_TIME_def, ACCEPT_F_def, P_SEM_def] 3567]) 3568 3569 3570 3571 3572val TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_PRODUCT_THM = 3573 store_thm 3574 ("TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_PRODUCT_THM", 3575 3576``!A B i w ac . (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ 3577 (DISJOINT B.S (SEMI_AUTOMATON_USED_VARS A)) /\ 3578 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w) ==> 3579 3580 (A_SEM i (A_UNIV (PRODUCT_SEMI_AUTOMATON A B, ac)) = 3581 A_SEM (INPUT_RUN_PATH_UNION A i w) (A_UNIV (B, ac)))``, 3582 3583 3584REPEAT STRIP_TAC THEN 3585SIMP_TAC std_ss [A_SEM_THM] THEN 3586SUBGOAL_TAC ` 3587 !w'. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (PRODUCT_SEMI_AUTOMATON A B) i w' = 3588 (PATH_SUBSET w' (A.S UNION B.S) /\ (PATH_RESTRICT w' A.S = w) /\ 3589 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON B (INPUT_RUN_PATH_UNION A i w) (PATH_RESTRICT w' B.S)))` THEN1 ( 3590 3591 SUBGOAL_TAC `!x. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i x ==> (x = w)` THEN1 ( 3592 METIS_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] 3593 ) THEN 3594 GEN_TAC THEN 3595 NTAC 2 UNDISCH_HD_TAC THEN 3596 REWRITE_TAC [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, PRODUCT_SEMI_AUTOMATON_REWRITES, P_SEM_THM, IS_TRANSITION_def, 3597 INPUT_RUN_STATE_UNION_def, INPUT_RUN_PATH_UNION_def] THEN 3598 REPEAT STRIP_TAC THEN 3599 SIMP_ALL_TAC std_ss [XP_SEM_THM, P_SEM_THM, FORALL_AND_THM] THEN 3600 REPEAT BOOL_EQ_STRIP_TAC THEN 3601 SUBGOAL_TAC `P_SEM (w' 0 UNION (i 0 DIFF (A.S UNION B.S))) A.S0 = 3602 P_SEM ((PATH_RESTRICT w' A.S) 0 UNION (i 0 DIFF A.S)) A.S0` THEN1 ( 3603 ONCE_REWRITE_TAC[P_USED_VARS_INTER_THM] THEN 3604 AP_THM_TAC THEN AP_TERM_TAC THEN 3605 UNDISCH_NO_TAC 5 (*DISJOINT B.S *)THEN 3606 UNDISCH_HD_TAC (*w' n SUBSET *) THEN 3607 REPEAT WEAKEN_HD_TAC THEN 3608 SIMP_TAC std_ss [DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, EXTENSION, PATH_RESTRICT_def, IN_INTER, PATH_MAP_def, IN_DIFF, SUBSET_DEF] THEN 3609 METIS_TAC[] 3610 ) THEN 3611 3612 SUBGOAL_TAC `!n. XP_SEM A.R (w' n UNION (i n DIFF (A.S UNION B.S)), 3613 w' (SUC n) UNION (i (SUC n) DIFF (A.S UNION B.S))) = 3614 XP_SEM A.R ((PATH_RESTRICT w' A.S) n UNION (i n DIFF A.S), (PATH_RESTRICT w' A.S) (SUC n) UNION (i (SUC n) DIFF A.S)) ` THEN1 ( 3615 GEN_TAC THEN 3616 ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN 3617 AP_TERM_TAC THEN 3618 UNDISCH_NO_TAC 6 (*DISJOINT B.S *)THEN 3619 UNDISCH_NO_TAC 1 (*w' n SUBSET *) THEN 3620 REPEAT WEAKEN_HD_TAC THEN 3621 SIMP_TAC std_ss [DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, EXTENSION, PATH_RESTRICT_def, IN_INTER, PATH_MAP_def, IN_DIFF, SUBSET_DEF, 3622 XP_USED_VARS_def] THEN 3623 METIS_TAC[] 3624 ) THEN 3625 ASM_REWRITE_TAC[] THEN NTAC 2 WEAKEN_HD_TAC THEN 3626 3627 EQ_TAC THENL [ 3628 STRIP_TAC THEN 3629 Q_SPEC_NO_ASSUM 5 `PATH_RESTRICT w' A.S` THEN 3630 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3631 ASM_SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET] 3632 ) THEN 3633 ASM_REWRITE_TAC[] THEN 3634 3635 SUBGOAL_TAC `!n. (PATH_RESTRICT w' B.S n UNION (w n UNION (i n DIFF A.S) DIFF B.S)) = (w' n UNION (i n DIFF (A.S UNION B.S)))` THEN1 ( 3636 GSYM_NO_TAC 0 THEN 3637 UNDISCH_NO_TAC 5 (*PATH_SUBSET w' n*) THEN 3638 UNDISCH_NO_TAC 8 (*DISJOINT B.S*) THEN 3639 ASM_REWRITE_TAC[] THEN 3640 REPEAT WEAKEN_HD_TAC THEN 3641 3642 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, DISJOINT_DISJ_THM, 3643 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, SUBSET_DEF, IN_UNION, 3644 EXTENSION, IN_INTER, IN_DIFF] THEN 3645 METIS_TAC[] 3646 ) THEN 3647 ASM_SIMP_TAC std_ss [] THEN 3648 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET], 3649 3650 3651 STRIP_TAC THEN 3652 ASM_REWRITE_TAC[] THEN 3653 3654 SUBGOAL_TAC `!n. (PATH_RESTRICT w' B.S n UNION (w n UNION (i n DIFF A.S) DIFF B.S)) = (w' n UNION (i n DIFF (A.S UNION B.S)))` THEN1 ( 3655 GSYM_NO_TAC 3 (*w = PATH_RESTRICT*) THEN 3656 UNDISCH_NO_TAC 4 (*PATH_SUBSET w' n*) THEN 3657 UNDISCH_NO_TAC 8 (*DISJOINT B.S*) THEN 3658 ASM_REWRITE_TAC[] THEN 3659 REPEAT WEAKEN_HD_TAC THEN 3660 3661 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, DISJOINT_DISJ_THM, 3662 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, SUBSET_DEF, IN_UNION, 3663 EXTENSION, IN_INTER, IN_DIFF] THEN 3664 METIS_TAC[] 3665 ) THEN 3666 METIS_TAC[] 3667 ] 3668) THEN 3669ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 3670 3671EQ_TAC THENL [ 3672 REPEAT STRIP_TAC THEN 3673 `PATH_SUBSET w A.S /\ PATH_SUBSET w' B.S` by METIS_TAC[IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 3674 SUBGOAL_TAC `!x. ~(x IN A.S) \/ ~(x IN B.S)` THEN1 ( 3675 FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION] THEN 3676 METIS_TAC[] 3677 ) THEN 3678 3679 Q_SPEC_NO_ASSUM 4 `PATH_UNION w w'` THEN 3680 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 3681 REPEAT STRIP_TAC THENL [ 3682 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, PATH_SUBSET_def, PATH_UNION_def, IN_UNION] THEN 3683 METIS_TAC[], 3684 3685 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 3686 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, PATH_RESTRICT_def, PATH_UNION_def, IN_UNION, PATH_MAP_def, EXTENSION, IN_INTER] THEN 3687 METIS_TAC[], 3688 3689 REMAINS_TAC `(PATH_RESTRICT (PATH_UNION w w') B.S) = w'` THEN1 ( 3690 ASM_REWRITE_TAC[] 3691 ) THEN 3692 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 3693 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, PATH_RESTRICT_def, PATH_UNION_def, IN_UNION, PATH_MAP_def, EXTENSION, IN_INTER] THEN 3694 METIS_TAC[] 3695 ] 3696 ) THEN 3697 3698 UNDISCH_HD_TAC THEN 3699 IMP_TO_EQ_TAC THEN 3700 AP_THM_TAC THEN AP_TERM_TAC THEN 3701 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 3702 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, 3703 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3704 PRODUCT_SEMI_AUTOMATON_REWRITES, PATH_UNION_def, EXTENSION, 3705 IN_UNION, IN_DIFF] THEN 3706 METIS_TAC[], 3707 3708 3709 3710 REPEAT STRIP_TAC THEN 3711 Q_SPEC_NO_ASSUM 3 `PATH_RESTRICT w' B.S` THEN 3712 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 3713 UNDISCH_HD_TAC THEN 3714 IMP_TO_EQ_TAC THEN 3715 AP_THM_TAC THEN AP_TERM_TAC THEN 3716 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 3717 3718 GSYM_NO_TAC 1 (*Def w*) THEN 3719 UNDISCH_NO_TAC 2 (*PATH_SUBSET w'*) THEN 3720 ASM_REWRITE_TAC[] THEN 3721 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, 3722 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3723 PRODUCT_SEMI_AUTOMATON_REWRITES, PATH_UNION_def, EXTENSION, 3724 IN_UNION, IN_DIFF, PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 3725 METIS_TAC[] 3726]); 3727 3728 3729val _ = export_theory(); 3730