1(* -*- Mode: holscript; -*- ***************************************************) 2(* *) 3(* Symbolic representation of non-deterministic semi-automata *) 4(* *) 5(******************************************************************************) 6 7open HolKernel Parse boolLib bossLib; 8 9open infinite_pathTheory pred_setTheory listTheory pairTheory xprop_logicTheory 10 containerTheory prop_logicTheory set_lemmataTheory prim_recTheory; 11 12open term_grammar tuerk_tacticsLib temporal_deep_mixedTheory; 13 14open Sanity; 15 16val _ = hide "S"; 17val _ = hide "K"; 18val _ = hide "I"; 19 20val _ = new_theory "symbolic_semi_automaton"; 21val _ = ParseExtras.temp_loose_equality() 22 23(* Different with symbolic_kripke_structure, which does not have concepts of 24 input and state variables, i.e. there's no "S" component (state variables). 25 26 `symbolic_semi_automaton` is used in LTL to Omega automata translation, where 27 variables used in LTL formula are treated as input variables. (ltl2omega.sml) 28 29 It's "semi" because there's no final states or fair states specified (yet). 30 *) 31Datatype : 32 symbolic_semi_automaton = 33 <| S: 'var set; (* set of all (used) state variables *) 34 S0: 'var prop_logic; (* initial states *) 35 R: 'var xprop_logic (* transition relation, current state # input # next state *) 36 |> 37End 38 39(* used input vars = all used vars in (S0,R) - all state vars (S) *) 40val SEMI_AUTOMATON_USED_INPUT_VARS_def = Define 41 `SEMI_AUTOMATON_USED_INPUT_VARS A = (P_USED_VARS A.S0 UNION XP_USED_VARS A.R) DIFF A.S`; 42 43val SEMI_AUTOMATON_USED_VARS_def = Define 44 `SEMI_AUTOMATON_USED_VARS A = (SEMI_AUTOMATON_USED_INPUT_VARS A) UNION A.S`; 45 46(* all used vars = all used vars in (S0,R) + all state vars (S) *) 47Theorem SEMI_AUTOMATON_USED_VARS___DIRECT_DEF : 48 !A. SEMI_AUTOMATON_USED_VARS A = P_USED_VARS A.S0 UNION XP_USED_VARS A.R UNION A.S 49Proof 50 SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, EXTENSION, IN_UNION, 51 IN_DIFF, SEMI_AUTOMATON_USED_INPUT_VARS_def] 52 >> PROVE_TAC [] 53QED 54 55val SEMI_AUTOMATON_VAR_RENAMING_def = Define 56 `SEMI_AUTOMATON_VAR_RENAMING (f:'a->'b) (symbolic_semi_automaton S S0 R) = 57 (symbolic_semi_automaton (IMAGE f S) (P_VAR_RENAMING f S0) (XP_VAR_RENAMING f R))`; 58 59Theorem SEMI_AUTOMATON_VAR_RENAMING_REWRITES : 60 !A f. ((SEMI_AUTOMATON_VAR_RENAMING f A).S = IMAGE f A.S) /\ 61 ((SEMI_AUTOMATON_VAR_RENAMING f A).S0 = P_VAR_RENAMING f A.S0) /\ 62 ((SEMI_AUTOMATON_VAR_RENAMING f A).R = XP_VAR_RENAMING f A.R) 63Proof 64 Cases_on `A` >> EVAL_TAC >> PROVE_TAC [] 65QED 66 67val symbolic_semi_automaton_S = DB.fetch "-" "symbolic_semi_automaton_S"; 68val symbolic_semi_automaton_S0 = DB.fetch "-" "symbolic_semi_automaton_S0"; 69val symbolic_semi_automaton_R = DB.fetch "-" "symbolic_semi_automaton_R"; 70val symbolic_semi_automaton_11 = DB.fetch "-" "symbolic_semi_automaton_11"; 71 72Theorem symbolic_semi_automaton_REWRITES = LIST_CONJ 73 [symbolic_semi_automaton_S, symbolic_semi_automaton_S0, 74 symbolic_semi_automaton_R, symbolic_semi_automaton_11]; 75 76(*============================================================================= 77= Semantics 78=============================================================================*) 79 80(*****************************************************************************) 81(* symbolic representation of non deterministic semi automata *) 82(*****************************************************************************) 83 84(* `A` is used only to filter out all state variables in `i` *) 85val INPUT_RUN_STATE_UNION_def = Define 86 `INPUT_RUN_STATE_UNION A i s = s UNION (i DIFF A.S)`; 87 88val INPUT_RUN_PATH_UNION_def = Define 89 `INPUT_RUN_PATH_UNION A i w = \n. INPUT_RUN_STATE_UNION A (i n) (w n)`; 90 91(* (s1,i1) is the current state, (s2,i2) is the next state *) 92val IS_TRANSITION_def = Define 93 `IS_TRANSITION A s1 i1 s2 i2 = 94 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 s1, INPUT_RUN_STATE_UNION A i2 s2)`; 95 96(*****************************************************************************) 97(* RUN A i w is true iff w is a run of i through A *) 98(*****************************************************************************) 99val IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def = Define 100 `IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w = 101 (PATH_SUBSET w A.S /\ 102 P_SEM (INPUT_RUN_PATH_UNION A i w 0) A.S0 /\ 103 !n. IS_TRANSITION A (w n) (i n) (w (SUC n)) (i (SUC n)))`; 104 105(*============================================================================= 106= Syntactic Sugar and elementary lemmata 107=============================================================================*) 108 109(* cf. boolTheory.EXISTS_DEF (at least one), EXISTS_UNIQUE_DEF (exactly one) *) 110val EXISTS_AT_MOST_ONE_def = Define 111 `EXISTS_AT_MOST_ONE = \P:'a->bool. !x y. P x /\ P y ==> (x=y)`; 112val _ = set_fixity "EXISTS_AT_MOST_ONE" Binder; 113 114(* Deterministric: for each input trace there's at most one "compatible" trace 115 satisfying initial state and transition relation. 116 *) 117val IS_DET_SYMBOLIC_SEMI_AUTOMATON_def = Define 118 `IS_DET_SYMBOLIC_SEMI_AUTOMATON A = 119 (!i. EXISTS_AT_MOST_ONE s. ((s SUBSET A.S) /\ (P_SEM (INPUT_RUN_STATE_UNION A i s) A.S0))) /\ 120 (!s1 i1 i2. EXISTS_AT_MOST_ONE s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`; 121 122(* Total: for each input trace there's at least one "compatible" trace, i.e. 123 no deadlock for whatever inputs. 124 *) 125val IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON_def = Define 126 `IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A = 127 (!i. ?s. ((s SUBSET A.S) /\ (P_SEM (INPUT_RUN_STATE_UNION A i s) A.S0))) /\ 128 (!s1 i1 i2. ?s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`; 129 130val IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_def = Define 131 `IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A = 132 IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ IS_DET_SYMBOLIC_SEMI_AUTOMATON A`; 133 134(* Total+deterministric: for each input trace there's exactly one "compatible" trace 135 satisfying initial state and transition relation. 136 *) 137Theorem IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_THM : 138 !A. IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A = 139 (!i. ?!s. ((s SUBSET A.S) /\ (P_SEM (INPUT_RUN_STATE_UNION A i s) A.S0))) /\ 140 (!s1 i1 i2. ?!s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2)) 141Proof 142 GEN_TAC 143 >> SIMP_TAC std_ss [IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_def, 144 IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON_def, 145 IS_DET_SYMBOLIC_SEMI_AUTOMATON_def, EXISTS_AT_MOST_ONE_def] 146 >> PROVE_TAC [] 147QED 148 149(* A semi-automaton without some syntactic sugar, i.e. w/o input variables *) 150val IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON_def = Define 151 `IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON A = 152 (P_USED_VARS A.S0 SUBSET A.S /\ XP_USED_X_VARS A.R SUBSET A.S)`; 153 154(* In "simple" symbolic runs of semi-automaton, the input state (i n) is only 155 used in the current part of relation. 156 *) 157val IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_def = Define 158 `IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON A i w = 159 (PATH_SUBSET w A.S /\ P_SEM (w 0) A.S0 /\ 160 !n. XP_SEM A.R ((w n) UNION (i n DIFF A.S), (w (SUC n))))`; 161 162(* In case of simple symbolic semi-automaton, the normal symbolic run is 163 also the "simple" symbolic run. 164 *) 165Theorem IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_THM : 166 !A. IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON A ==> 167 !i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w = 168 IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON A i w 169Proof 170 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 171 IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_def, 172 IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON_def, 173 IS_TRANSITION_def, 174 INPUT_RUN_PATH_UNION_def, 175 INPUT_RUN_STATE_UNION_def, 176 PATH_SUBSET_def] 177 >> rpt STRIP_TAC 178 >> BOOL_EQ_STRIP_TAC 179 >> SUBGOAL_TAC `!n. (w n UNION (i n DIFF A.S)) INTER A.S = w n` 180 >- (SIMP_ALL_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, IN_DIFF, SUBSET_DEF] \\ 181 METIS_TAC []) 182 >> PROVE_TAC [P_USED_VARS_INTER_SUBSET_THM, XP_USED_VARS_INTER_SUBSET_THM] 183QED 184 185(* A = f(A'), a simplification of A' (mostly the input variables) *) 186val IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def = Define 187 `IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON A A' f = 188 (!i. i IN SEMI_AUTOMATON_USED_INPUT_VARS A' ==> 189 f i NOTIN (A'.S UNION SEMI_AUTOMATON_USED_INPUT_VARS A' UNION 190 IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A' DIFF {i}))) /\ 191 (A = symbolic_semi_automaton 192 (A'.S UNION (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A'))) 193 (P_VAR_RENAMING (\x. if (x IN A'.S) then x else f x) A'.S0) 194 (XP_AND((XP_VAR_RENAMING (\x. if (x IN A'.S) then x else f x) A'.R), 195 XP_BIGAND (SET_TO_LIST (IMAGE (\i. XP_EQUIV(XP_PROP (f i), XP_PROP i)) 196 (SEMI_AUTOMATON_USED_INPUT_VARS A'))))))`; 197(* product = synchoronous composition *) 198val PRODUCT_SEMI_AUTOMATON_def = Define 199 `PRODUCT_SEMI_AUTOMATON (symbolic_semi_automaton S_1 S0_1 R_1) 200 (symbolic_semi_automaton S_2 S0_2 R_2) = 201 symbolic_semi_automaton (S_1 UNION S_2) (P_AND(S0_1, S0_2)) (XP_AND(R_1, R_2))`; 202 203Theorem PRODUCT_SEMI_AUTOMATON_THM : 204 !A B C. (PRODUCT_SEMI_AUTOMATON A B = C) <=> (C.S = (A.S UNION B.S)) /\ 205 (C.S0 = (P_AND(A.S0, B.S0))) /\ 206 (C.R = (XP_AND(A.R, B.R))) 207Proof 208 Cases_on `A` >> Cases_on `B` >> Cases_on `C` 209 >> EVAL_TAC >> PROVE_TAC [] 210QED 211 212Theorem PRODUCT_SEMI_AUTOMATON_REWRITES : 213 !A B. ((PRODUCT_SEMI_AUTOMATON A B).S = (A.S UNION B.S)) /\ 214 ((PRODUCT_SEMI_AUTOMATON A B).S0 = (P_AND(A.S0,B.S0))) /\ 215 ((PRODUCT_SEMI_AUTOMATON A B).R = (XP_AND(A.R, B.R))) 216Proof 217 PROVE_TAC [PRODUCT_SEMI_AUTOMATON_THM] 218QED 219 220(* empty semi automaton (accepting all input traces) *) 221val ID_SEMI_AUTOMATON_def = Define 222 `ID_SEMI_AUTOMATON = symbolic_semi_automaton EMPTY P_TRUE XP_TRUE`; 223 224Theorem ID_SEMI_AUTOMATON_RUN : 225 !i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON ID_SEMI_AUTOMATON i w <=> (w = EMPTY_PATH) 226Proof 227 EVAL_TAC >> PROVE_TAC [SUBSET_EMPTY] 228QED 229 230Theorem ID_SEMI_AUTOMATON_REWRITES : 231 (ID_SEMI_AUTOMATON.S = EMPTY) /\ 232 (ID_SEMI_AUTOMATON.S0 = P_TRUE) /\ 233 (ID_SEMI_AUTOMATON.R = XP_TRUE) 234Proof 235 EVAL_TAC 236QED 237 238Theorem SYMBOLIC_SEMI_AUTOMATON___REWRITE : 239 !A. symbolic_semi_automaton A.S A.S0 A.R = A 240Proof 241 Cases_on `A` >> EVAL_TAC 242QED 243 244Theorem FINITE___SEMI_AUTOMATON_USED_INPUT_VARS : 245 !A. FINITE (SEMI_AUTOMATON_USED_INPUT_VARS A) 246Proof 247 Cases_on `A` 248 >> REWRITE_TAC [SEMI_AUTOMATON_USED_INPUT_VARS_def] 249 >> METIS_TAC [FINITE___P_USED_VARS, FINITE___XP_USED_VARS, FINITE_UNION, FINITE_DIFF] 250QED 251 252Theorem SEMI_AUTOMATON_VAR_RENAMING___USED_VARS : 253 !A f. SEMI_AUTOMATON_USED_VARS (SEMI_AUTOMATON_VAR_RENAMING f A) = 254 IMAGE f (SEMI_AUTOMATON_USED_VARS A) 255Proof 256 Cases_on `A` 257 >> REWRITE_TAC [SEMI_AUTOMATON_USED_VARS_def, SEMI_AUTOMATON_USED_INPUT_VARS_def, 258 SEMI_AUTOMATON_VAR_RENAMING_def, 259 symbolic_semi_automaton_REWRITES] 260 >> SIMP_TAC std_ss [DIFF_UNION_ELIM] 261 >> REWRITE_TAC [IMAGE_UNION, P_VAR_RENAMING___USED_VARS, XP_VAR_RENAMING___USED_VARS] 262QED 263 264Theorem SEMI_AUTOMATON_VAR_RENAMING___USED_INPUT_VARS : 265 !A f. INJ f (SEMI_AUTOMATON_USED_VARS A) UNIV ==> 266 (SEMI_AUTOMATON_USED_INPUT_VARS (SEMI_AUTOMATON_VAR_RENAMING f A) = 267 (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A))) 268Proof 269 Cases_on `A` 270 >> REWRITE_TAC [SEMI_AUTOMATON_USED_INPUT_VARS_def, SEMI_AUTOMATON_VAR_RENAMING_def, 271 SEMI_AUTOMATON_USED_VARS_def, DIFF_UNION_ELIM, 272 symbolic_semi_automaton_REWRITES, 273 P_VAR_RENAMING___USED_VARS, XP_VAR_RENAMING___USED_VARS] 274 >> METIS_TAC [IMAGE_UNION, IMAGE_DIFF] 275QED 276 277(* for total automata (at least one next state), there exist a transition function 278 which picks one next state given the last state and inputs. 279 *) 280Theorem TOTAL_SYMBOLIC_SEMI_AUTOMATON_TRANS_FUNC : 281 !A. IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A ==> 282 ?R_FUNC. !s1 s2 i1 i2. (R_FUNC s1 i1 i2 = s2) ==> 283 s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2 284Proof 285 SIMP_TAC std_ss [IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON_def] 286 >> rpt STRIP_TAC 287 >> ASSUME_TAC 288 (SKOLEM_CONV ``!s1 i1 i2. ?s2. s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2``) 289 >> PROVE_TAC [] 290QED 291 292(* for deterministic automata (at most one next state), there exists a transition 293 function such that, if a transition exists, it picks that exact next state. 294 *) 295Theorem DET_SYMBOLIC_SEMI_AUTOMATON_TRANS_FUNC : 296 !A. IS_DET_SYMBOLIC_SEMI_AUTOMATON A ==> 297 ?R_FUNC. !s1 s2 i1 i2. s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2 ==> 298 (R_FUNC s1 i1 i2 = s2) 299Proof 300 SIMP_TAC std_ss [IS_DET_SYMBOLIC_SEMI_AUTOMATON_def, EXISTS_AT_MOST_ONE_def] 301 >> rpt STRIP_TAC 302 >> EXISTS_TAC ``\s1 i1 i2. @s2. (s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2)`` 303 >> SIMP_TAC std_ss [] 304 >> rpt STRIP_TAC 305 >> SELECT_ELIM_TAC 306 >> METIS_TAC [] 307QED 308 309(* `==>` becomes `<=>` if the deterministic automata is also total *) 310Theorem TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_TRANS_FUNC : 311 !A. IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A ==> 312 ?R_FUNC. !s1 s2 i1 i2. s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2 <=> 313 (R_FUNC s1 i1 i2 = s2) 314Proof 315 SIMP_TAC std_ss [IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_THM] 316 >> rpt STRIP_TAC 317 >> ASSUME_TAC 318 (SKOLEM_CONV ``!s1 i1 i2. ?s2. s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2``) 319 >> `?f. !s1 i1 i2. (f s1 i1 i2) SUBSET A.S /\ 320 IS_TRANSITION A s1 i1 (f s1 i1 i2) i2` by PROVE_TAC [] 321 >> EXISTS_TAC ``f:'a set -> 'a set -> 'a set -> 'a set`` 322 >> METIS_TAC [] 323QED 324 325Theorem DET_SYMBOLIC_SEMI_AUTOMATON_EXISTS_AT_MOST_ONE_RUN : 326 !A i. IS_DET_SYMBOLIC_SEMI_AUTOMATON A ==> 327 EXISTS_AT_MOST_ONE w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w 328Proof 329 SIMP_TAC std_ss [IS_DET_SYMBOLIC_SEMI_AUTOMATON_def, EXISTS_AT_MOST_ONE_def, 330 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 331 PATH_SUBSET_def, INPUT_RUN_PATH_UNION_def] 332 >> rpt STRIP_TAC 333 >> ONCE_REWRITE_TAC [FUN_EQ_THM] 334 >> Induct_on `x'` 335 >> PROVE_TAC [] 336QED 337 338Theorem TOTAL_SYMBOLIC_SEMI_AUTOMATON_EXISTS_RUN : 339 !A i. IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A ==> 340 ?w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w 341Proof 342 SIMP_TAC std_ss [IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON_def, EXISTS_AT_MOST_ONE_def, 343 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 344 PATH_SUBSET_def, INPUT_RUN_PATH_UNION_def] 345 >> rpt STRIP_TAC 346 >> `?R_FUNC. !s1 s2 i1 i2. (s2 = R_FUNC s1 i1 i2) ==> 347 s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2` 348 by METIS_TAC [DET_SYMBOLIC_SEMI_AUTOMATON_TRANS_FUNC] 349 >> `?s. s SUBSET A.S /\ P_SEM (INPUT_RUN_STATE_UNION A (i 0) s) A.S0` by PROVE_TAC [] 350 >> `?f:num -> 'a set -> 'a set. f= (\n s. R_FUNC s (i n) (i (SUC n)))` by METIS_TAC [] 351 >> `?t. (t 0 = s) /\ !n. t (SUC n) = f n (t n)` by METIS_TAC [num_Axiom] 352 >> EXISTS_TAC ``t:num->'a set`` 353 >> rpt STRIP_TAC 354 >| [ Cases_on `n` >> PROVE_TAC [], 355 ASM_SIMP_TAC std_ss [], 356 METIS_TAC[] ] 357QED 358 359Theorem TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN : 360 !A i. IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A ==> 361 ?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w 362Proof 363 SIMP_TAC std_ss [IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_def, EXISTS_UNIQUE_DEF] 364 >> rpt STRIP_TAC 365 >| [ PROVE_TAC [TOTAL_SYMBOLIC_SEMI_AUTOMATON_EXISTS_RUN], 366 METIS_TAC [DET_SYMBOLIC_SEMI_AUTOMATON_EXISTS_AT_MOST_ONE_RUN, 367 EXISTS_AT_MOST_ONE_def] ] 368QED 369 370Theorem PRODUCT_SEMI_AUTOMATON_COMM_RUN : 371 !A B v w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (PRODUCT_SEMI_AUTOMATON A B) v w = 372 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (PRODUCT_SEMI_AUTOMATON B A) v w 373Proof 374 Cases_on `A` >> Cases_on `B` 375 >> SIMP_TAC std_ss [PRODUCT_SEMI_AUTOMATON_def, 376 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, PATH_SUBSET_def, 377 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 378 symbolic_semi_automaton_REWRITES, 379 UNION_COMM, P_SEM_def, IS_TRANSITION_def, XP_SEM_def] 380 >> PROVE_TAC [] 381QED 382 383(* symbolic run of product semi-automaton requires disjointness of all vars *) 384Theorem PRODUCT_SEMI_AUTOMATON_RUN : 385 !A1 A2. DISJOINT A1.S A2.S /\ 386 DISJOINT A1.S (SEMI_AUTOMATON_USED_INPUT_VARS A2) /\ 387 DISJOINT A2.S (SEMI_AUTOMATON_USED_INPUT_VARS A1) ==> 388 !i w1 w2. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A1 i w1 /\ 389 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A2 i w2 ==> 390 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON 391 (PRODUCT_SEMI_AUTOMATON A1 A2) i (PATH_UNION w1 w2) 392Proof 393 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 394 SEMI_AUTOMATON_USED_INPUT_VARS_def, 395 INPUT_RUN_PATH_UNION_def, PATH_UNION_def, 396 INPUT_RUN_STATE_UNION_def, PRODUCT_SEMI_AUTOMATON_REWRITES] 397 >> rpt (rpt GEN_TAC >> DISCH_THEN STRIP_ASSUME_TAC) 398 >> SUBGOAL_TAC 399 `!n. ((w1 n UNION w2 n UNION (i n DIFF (A1.S UNION A2.S))) INTER (COMPL A2.S) = 400 (w1 n UNION (i n DIFF A1.S)) INTER (COMPL A2.S)) /\ 401 ((w1 n UNION w2 n UNION (i n DIFF (A1.S UNION A2.S))) INTER (COMPL A1.S) = 402 (w2 n UNION (i n DIFF A2.S)) INTER (COMPL A1.S))` 403 >- (SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] \\ 404 FULL_SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 405 IN_UNION, IN_DIFF, PATH_SUBSET_def] \\ 406 rpt STRIP_TAC >> rpt BOOL_EQ_STRIP_TAC >> PROVE_TAC []) 407 >> rpt STRIP_TAC 408 >| [ (* goal 1 (of 3) *) 409 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, PRODUCT_SEMI_AUTOMATON_REWRITES, 410 UNION_SUBSET] \\ 411 PROVE_TAC [SUBSET_UNION, SUBSET_TRANS], 412 (* goal 2 (of 3) *) 413 SIMP_TAC std_ss [P_SEM_def] THEN 414 SUBGOAL_TAC `(P_USED_VARS A1.S0) SUBSET (COMPL A2.S) /\ 415 (P_USED_VARS A2.S0) SUBSET (COMPL A1.S)` 416 >- (FULL_SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, 417 SUBSET_DEF, IN_COMPL, IN_UNION, IN_DIFF] \\ 418 PROVE_TAC []) \\ 419 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 420 (* goal 3 (of 3) *) 421 FULL_SIMP_TAC std_ss [IS_TRANSITION_def, PRODUCT_SEMI_AUTOMATON_REWRITES, XP_SEM_def, 422 INPUT_RUN_STATE_UNION_def] \\ 423 SUBGOAL_TAC `(XP_USED_VARS A1.R SUBSET COMPL A2.S) /\ 424 (XP_USED_VARS A2.R SUBSET COMPL A1.S)` 425 >- (FULL_SIMP_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 426 IN_UNION, IN_DIFF, XP_USED_VARS_def] \\ 427 PROVE_TAC []) \\ 428 PROVE_TAC [XP_USED_VARS_INTER_SUBSET_BOTH_THM] ] 429QED 430 431(* symbolic run of product semi-automaton implies run of the 1st semi-automaton *) 432Theorem PRODUCT_SEMI_AUTOMATON_RUN2___FIRST : 433 !A1 A2. DISJOINT A1.S A2.S /\ 434 DISJOINT A2.S (SEMI_AUTOMATON_USED_INPUT_VARS A1) ==> 435 !i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (PRODUCT_SEMI_AUTOMATON A1 A2) i w ==> 436 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A1 i (PATH_RESTRICT w A1.S) 437Proof 438 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 439 IS_TRANSITION_def, FORALL_AND_THM, 440 PRODUCT_SEMI_AUTOMATON_REWRITES, P_SEM_def, XP_SEM_def] 441 >> rpt ((rpt GEN_TAC) THEN (DISCH_THEN STRIP_ASSUME_TAC)) 442 >> SUBGOAL_TAC 443 `!n. (INPUT_RUN_STATE_UNION A1 (i n) (PATH_RESTRICT w A1.S n)) INTER (COMPL A2.S) = 444 (INPUT_RUN_STATE_UNION (PRODUCT_SEMI_AUTOMATON A1 A2) (i n) (w n)) INTER (COMPL A2.S)` 445 >- (SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, EXTENSION, IN_INTER, IN_COMPL, IN_UNION, 446 PRODUCT_SEMI_AUTOMATON_REWRITES, IN_DIFF, PATH_RESTRICT_def, PATH_MAP_def] \\ 447 rpt GEN_TAC >> rpt BOOL_EQ_STRIP_TAC \\ 448 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, GSYM SUBSET_COMPL_DISJOINT, 449 SUBSET_DEF, IN_UNION, IN_COMPL] \\ 450 PROVE_TAC []) 451 >> rpt STRIP_TAC 452 >| [ SIMP_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET], 453 SUBGOAL_TAC `P_USED_VARS A1.S0 SUBSET COMPL A2.S` 454 >- (FULL_SIMP_TAC std_ss [PATH_SUBSET_def, GSYM SUBSET_COMPL_DISJOINT, 455 SUBSET_DEF, IN_UNION, IN_COMPL, 456 SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_UNION, IN_DIFF] \\ 457 PROVE_TAC []) \\ 458 PROVE_TAC [P_USED_VARS_INTER_SUBSET_THM], 459 SUBGOAL_TAC `XP_USED_VARS A1.R SUBSET COMPL A2.S` 460 >- (FULL_SIMP_TAC std_ss [PATH_SUBSET_def, GSYM SUBSET_COMPL_DISJOINT, 461 SUBSET_DEF, IN_UNION, IN_COMPL, 462 SEMI_AUTOMATON_USED_INPUT_VARS_def, 463 IN_UNION, IN_DIFF, XP_USED_VARS_def] \\ 464 PROVE_TAC []) \\ 465 PROVE_TAC [XP_USED_VARS_INTER_SUBSET_BOTH_THM] ] 466QED 467 468(* symbolic run of product semi-automaton implies run of the 2nd semi-automaton *) 469Theorem PRODUCT_SEMI_AUTOMATON_RUN2___SECOND : 470 !A1 A2. DISJOINT A1.S A2.S /\ 471 DISJOINT A1.S (SEMI_AUTOMATON_USED_INPUT_VARS A2) ==> 472 !i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (PRODUCT_SEMI_AUTOMATON A1 A2) i w ==> 473 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A2 i (PATH_RESTRICT w A2.S) 474Proof 475 PROVE_TAC [PRODUCT_SEMI_AUTOMATON_RUN2___FIRST, DISJOINT_SYM, 476 PRODUCT_SEMI_AUTOMATON_COMM_RUN] 477QED 478 479(* symbolic run restricted to a superset of input vars is still a symbolic run *) 480Theorem SEMI_AUTOMATON_USED_INPUT_VARS_INTER_SUBSET_THM : 481 !A S. (SEMI_AUTOMATON_USED_INPUT_VARS A) SUBSET S ==> 482 !i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w = 483 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A (PATH_RESTRICT i S) w 484Proof 485 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 486 IS_TRANSITION_def, INPUT_RUN_PATH_UNION_def, 487 SEMI_AUTOMATON_USED_INPUT_VARS_def, DIFF_SUBSET_ELIM, UNION_SUBSET] 488 >> rpt STRIP_TAC 489 >> rpt CONJ_EQ_STRIP_TAC 490 >> SUBGOAL_TAC 491 `!n. (INPUT_RUN_STATE_UNION A (i n) (w n)) INTER (S UNION A.S) = 492 (INPUT_RUN_STATE_UNION A (PATH_RESTRICT i S n) (w n)) INTER (S UNION A.S)` 493 >- (SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, EXTENSION, IN_INTER, 494 IN_UNION, IN_DIFF, PATH_RESTRICT_def, PATH_MAP_def] \\ 495 rpt GEN_TAC \\ 496 rpt BOOL_EQ_STRIP_TAC >> PROVE_TAC []) 497 >> BINOP_TAC 498 >| [ PROVE_TAC [P_USED_VARS_INTER_SUBSET_THM], 499 PROVE_TAC [XP_USED_VARS_INTER_SUBSET_BOTH_THM] ] 500QED 501 502(* special case: symbolic run restricted to input vars is still a symbolic run *) 503Theorem SEMI_AUTOMATON_USED_INPUT_VARS_INTER_THM : 504 !A i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w = 505 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A 506 (PATH_RESTRICT i (SEMI_AUTOMATON_USED_INPUT_VARS A)) w 507Proof 508 METIS_TAC [SEMI_AUTOMATON_USED_INPUT_VARS_INTER_SUBSET_THM, SUBSET_REFL] 509QED 510 511(* A = f(A') *) 512Theorem IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUN_INPUT_VARS : 513 !A A' f w i. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON A A' f /\ 514 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> 515 !i'. i' IN SEMI_AUTOMATON_USED_INPUT_VARS A' ==> !n. i' IN i n <=> f i' IN w n 516Proof 517 SIMP_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, 518 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 519 IS_TRANSITION_def, INPUT_RUN_STATE_UNION_def, 520 INPUT_RUN_PATH_UNION_def, 521 symbolic_semi_automaton_REWRITES, 522 XP_SEM_THM, FORALL_AND_THM, 523 XP_BIGAND_SEM, IMAGE_FINITE, 524 FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, 525 MEM_SET_TO_LIST, IN_IMAGE, IN_UNION, 526 GSYM LEFT_FORALL_IMP_THM, IN_DIFF, IN_SING] 527 >> rpt STRIP_TAC 528 >> SPECL_NO_ASSUM 1 [``n:num``, ``i':'a``] 529 >> UNDISCH_HD_TAC 530 >> ASM_SIMP_TAC std_ss [] 531 >> SUBGOAL_TAC `~(f i' IN i n /\ 532 !x. f i' <> f x \/ x NOTIN SEMI_AUTOMATON_USED_INPUT_VARS A')` 533 >- METIS_TAC [] 534 >> SUBGOAL_TAC `~(i' IN w n) /\ 535 (i' NOTIN A'.S /\ 536 !x. i' <> f x \/ x NOTIN SEMI_AUTOMATON_USED_INPUT_VARS A')` 537 >- (WEAKEN_HD_TAC \\ 538 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, 539 PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_IMAGE] \\ 540 METIS_TAC []) 541 >> ASM_SIMP_TAC std_ss [] 542QED 543 544Theorem IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS : 545 !A A' f. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON A A' f ==> 546 IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON A /\ 547 !w i. PATH_SUBSET w A'.S ==> 548 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i 549 (\n. w n UNION 550 IMAGE f (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) = 551 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i w) 552Proof 553 rpt GEN_TAC >> DISCH_TAC 554 >> LEFT_CONJ_TAC 555 >| [ FULL_SIMP_TAC std_ss 556 [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, 557 IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON_def, 558 IN_UNION, IN_IMAGE, 559 symbolic_semi_automaton_REWRITES, 560 P_VAR_RENAMING___USED_VARS, SUBSET_DEF, 561 XP_VAR_RENAMING___USED_X_VARS, 562 XP_BIGAND___XP_USED_VARS, 563 XP_USED_VARS_EVAL, MEM_MAP, 564 IN_LIST_BIGUNION, 565 IMAGE_FINITE, 566 FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, 567 MEM_SET_TO_LIST, 568 GSYM LEFT_EXISTS_AND_THM, GSYM EXISTS_OR_THM, 569 GSYM LEFT_FORALL_IMP_THM, 570 NOT_IN_EMPTY] \\ 571 rpt STRIP_TAC >| (* 2 subgoals *) 572 [ Cases_on `x' IN A'.S` THEN 573 ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_INPUT_VARS_def, 574 IN_UNION, IN_DIFF] THEN 575 PROVE_TAC [], 576 577 Cases_on `i IN A'.S` \\ 578 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_INPUT_VARS_def, 579 IN_UNION, IN_DIFF, XP_USED_VARS_def] \\ 580 PROVE_TAC [] ], 581 582 ASM_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_THM] THEN 583 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 584 IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_def] THEN 585 rpt STRIP_TAC THEN 586 FULL_SIMP_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, 587 symbolic_semi_automaton_REWRITES, XP_SEM_THM, 588 FORALL_AND_THM] THEN 589 MATCH_MP_TAC (prove(``!A A' B B' C. ((C /\ D) /\ ((A /\ B) = (A'/\ B'))) ==> 590 ((C /\ A /\ B /\ D) = (A' /\ B'))``, METIS_TAC[])) THEN 591 rpt STRIP_TAC THENL [ 592 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_UNION] THEN 593 rpt STRIP_TAC THENL [ 594 METIS_TAC[], 595 METIS_TAC[IMAGE_INTER, SUBSET_DEF, IN_INTER] 596 ], 597 598 FULL_SIMP_TAC std_ss [XP_BIGAND_SEM, 599 FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, 600 MEM_SET_TO_LIST, IMAGE_FINITE, IN_IMAGE, 601 GSYM LEFT_FORALL_IMP_THM, XP_SEM_THM, 602 IN_UNION, IN_INTER, IN_DIFF, IN_SING, 603 PATH_SUBSET_def, SUBSET_DEF, 604 SEMI_AUTOMATON_USED_INPUT_VARS_def 605 ] THEN 606 METIS_TAC[], 607 608 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, 609 INPUT_RUN_STATE_UNION_def, 610 IS_TRANSITION_def] THEN 611 `?f'. (\x. (if x IN A'.S then x else f x)) = f'` by METIS_TAC[] THEN 612 SUBGOAL_TAC `!n. (w n UNION IMAGE f (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) = 613 IMAGE f' (w n UNION (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A'))` THEN1 ( 614 ASM_SIMP_TAC std_ss [EXTENSION, IN_UNION, IMAGE_UNION] THEN 615 rpt STRIP_TAC THEN 616 BINOP_TAC THENL [ 617 GSYM_NO_TAC 1 (*Def f'*) THEN 618 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_IMAGE] THEN 619 METIS_TAC[], 620 621 SIMP_TAC std_ss [IN_IMAGE, IN_INTER, 622 SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_UNION, IN_DIFF] THEN 623 EXISTS_EQ_STRIP_TAC THEN 624 rpt BOOL_EQ_STRIP_TAC THEN 625 METIS_TAC[] 626 ] 627 ) THEN 628 SUBGOAL_TAC `INJ f' (SEMI_AUTOMATON_USED_VARS A') UNIV` THEN1 ( 629 SIMP_ALL_TAC std_ss [INJ_DEF, IN_UNIV, SEMI_AUTOMATON_USED_VARS_def, 630 SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_UNION, IN_DIFF, IN_IMAGE, IN_SING] THEN 631 METIS_TAC[] 632 ) THEN 633 634 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF] THEN 635 BINOP_TAC THENL [ 636 SUBGOAL_TAC `P_SEM (IMAGE f' (w 0 UNION i 0 INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) 637 (P_VAR_RENAMING f' A'.S0) = P_SEM (w 0 UNION i 0 INTER SEMI_AUTOMATON_USED_INPUT_VARS A') A'.S0` THEN1 ( 638 SUBGOAL_TAC `(w 0 UNION i 0 INTER SEMI_AUTOMATON_USED_INPUT_VARS A') UNION (P_USED_VARS A'.S0) SUBSET 639 (SEMI_AUTOMATON_USED_VARS A')` THEN1 ( 640 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, SUBSET_DEF, IN_UNION, 641 IN_INTER, SEMI_AUTOMATON_USED_INPUT_VARS_def, 642 IN_DIFF, PATH_SUBSET_def] THEN 643 METIS_TAC[] 644 ) THEN 645 METIS_TAC[INJ_SUBSET_DOMAIN, P_SEM___VAR_RENAMING] 646 ) THEN 647 FULL_SIMP_TAC std_ss [] THEN 648 ONCE_REWRITE_TAC [P_USED_VARS_INTER_THM] THEN 649 MK_COMB_TAC THEN SIMP_TAC std_ss [] THEN 650 MK_COMB_TAC THEN SIMP_TAC std_ss [] THEN 651 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 652 SEMI_AUTOMATON_USED_INPUT_VARS_def] THEN 653 METIS_TAC[], 654 655 ASM_SIMP_TAC std_ss [] THEN 656 FORALL_EQ_STRIP_TAC THEN 657 SUBGOAL_TAC `XP_SEM (XP_VAR_RENAMING f' A'.R) 658 (IMAGE f' 659 (w n UNION i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A') UNION 660 (i n DIFF (A'.S UNION IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A'))), 661 IMAGE f' 662 (w (SUC n) UNION 663 i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) = 664 XP_SEM (XP_VAR_RENAMING f' A'.R) 665 (IMAGE f' 666 (w n UNION i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A'), 667 IMAGE f' 668 (w (SUC n) UNION 669 i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A'))` THEN1 ( 670 SUBGOAL_TAC `XP_USED_CURRENT_VARS (XP_VAR_RENAMING f' A'.R) SUBSET 671 (A'.S UNION IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A'))` THEN1 ( 672 SIMP_TAC std_ss [XP_VAR_RENAMING___USED_CURRENT_VARS, 673 SUBSET_DEF, IN_UNION, 674 SEMI_AUTOMATON_USED_INPUT_VARS_def, 675 IN_IMAGE, IN_DIFF, IN_UNION, 676 XP_USED_VARS_def] THEN 677 METIS_TAC[] 678 ) THEN 679 SUBGOAL_TAC `!S1 S2 S3 S4. (S1 UNION (S2 DIFF S3)) INTER S3 = 680 (S1 INTER S3)` THEN1 ( 681 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] THEN 682 PROVE_TAC[] 683 ) THEN 684 METIS_TAC[XP_USED_VARS_INTER_SUBSET_THM] 685 ) THEN 686 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 687 688 SUBGOAL_TAC ` XP_SEM (XP_VAR_RENAMING f' A'.R) 689 (IMAGE f' (w n UNION i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A'), 690 IMAGE f' (w (SUC n) UNION i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) = 691 XP_SEM A'.R 692 (w n UNION i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A', 693 w (SUC n) UNION i (SUC n) INTER SEMI_AUTOMATON_USED_INPUT_VARS A')` THEN1 ( 694 MATCH_MP_TAC (GSYM XP_SEM___VAR_RENAMING) THEN 695 UNDISCH_HD_TAC (*INJ f'*) THEN 696 SIMP_TAC std_ss [] THEN 697 MATCH_MP_TAC (REWRITE_RULE [ 698 prove (``!t1 t2 t3. (t1 /\ t2 ==> t3) = (t2 ==> t1 ==> t3)``, PROVE_TAC[])] INJ_SUBSET_DOMAIN) THEN 699 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTER, SEMI_AUTOMATON_USED_VARS_def, 700 PATH_SUBSET_def, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF] THEN 701 METIS_TAC[] 702 ) THEN 703 704 FULL_SIMP_TAC std_ss [] THEN 705 ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN 706 MK_COMB_TAC THEN SIMP_TAC std_ss [PAIR_EQ] THEN 707 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 708 SEMI_AUTOMATON_USED_INPUT_VARS_def, 709 XP_USED_VARS_def] THEN 710 METIS_TAC[] 711 ] 712 ] 713 ] 714QED 715 716val IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS2 = 717 store_thm 718 ("IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS2", 719 720 ``!A A' f. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON A A' f ==> 721 !w i. ((IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w) = 722 (PATH_SUBSET w (A'.S UNION IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A')) /\ 723 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A' i (PATH_RESTRICT w A'.S) /\ 724 (!i'. (i' IN SEMI_AUTOMATON_USED_INPUT_VARS A') ==> 725 (!n. (i' IN i n) = (f i' IN w n)))))``, 726 727 rpt STRIP_TAC THEN EQ_TAC THENL [ 728 STRIP_TAC THEN LEFT_CONJ_TAC THENL [ 729 SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def, 730 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 731 UNDISCH_HD_TAC (*PATH_SUBSET w A.S*) THEN 732 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES], 733 734 735 REVERSE RIGHT_CONJ_TAC THEN1 ( 736 METIS_TAC[IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUN_INPUT_VARS] 737 ) THEN 738 739 MP_TAC (Q.SPECL [`A`, `A'`, `f`] (GSYM IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS)) THEN 740 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 741 Q.PAT_X_ASSUM `!w i. _` (MP_TAC o Q.SPECL [`PATH_RESTRICT w A'.S`, `i`]) THEN 742 ASM_SIMP_TAC std_ss [PATH_SUBSET_RESTRICT] THEN 743 DISCH_THEN (K ALL_TAC) THEN 744 745 746 `(\n. PATH_RESTRICT w A'.S n UNION 747 IMAGE f (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) = w` suffices_by 748 (DISCH_TAC >> ASM_REWRITE_TAC[]) THEN 749 750 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 751 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 752 753 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, IN_UNION, IN_IMAGE, 754 SUBSET_DEF, PATH_MAP_def, IN_INTER] THEN 755 METIS_TAC[] 756 ], 757 758 759 STRIP_TAC THEN 760 ASSUME_TAC (GSYM IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS) THEN 761 Q_SPECL_NO_ASSUM 0 [`A`, `A'`, `f`] THEN 762 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 763 CLEAN_ASSUMPTIONS_TAC THEN 764 Q_SPECL_NO_ASSUM 1 [`PATH_RESTRICT w A'.S`, `i`] THEN 765 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET, PATH_SUBSET_def] THEN 766 767 REMAINS_TAC `(\n. 768 PATH_RESTRICT w A'.S n UNION 769 IMAGE f (i n INTER SEMI_AUTOMATON_USED_INPUT_VARS A')) = w` THEN1 ( 770 FULL_SIMP_TAC std_ss [] 771 ) THEN 772 773 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN 774 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 775 776 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, IN_UNION, IN_IMAGE, 777 SUBSET_DEF, PATH_MAP_def, IN_INTER] THEN 778 METIS_TAC[] 779 ]); 780 781Theorem INPUT_RUN_PATH_UNION___SPLIT : 782 !A p. INPUT_RUN_PATH_UNION A p (PATH_RESTRICT p A.S) = p 783Proof 784 rpt GEN_TAC 785 >> ONCE_REWRITE_TAC [FUN_EQ_THM] 786 >> SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 787 PATH_RESTRICT_def, EXTENSION, IN_UNION, PATH_MAP_def, 788 IN_INTER, IN_DIFF] 789 >> PROVE_TAC [] 790QED 791 792Theorem INPUT_RUN_STATE_UNION___SPLIT : 793 !A s. INPUT_RUN_STATE_UNION A s (s INTER A.S) = s 794Proof 795 rpt GEN_TAC 796 >> SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, PATH_RESTRICT_def, EXTENSION, 797 IN_UNION, PATH_MAP_def, IN_INTER, IN_DIFF] 798 >> PROVE_TAC [] 799QED 800 801Theorem IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___SPLIT : 802 !S S0 R i w. 803 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 R) i w <=> 804 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 XP_TRUE) i w /\ 805 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S P_TRUE R) i w 806Proof 807 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 808 symbolic_semi_automaton_REWRITES, P_SEM_def, 809 IS_TRANSITION_def, XP_SEM_def, 810 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def] 811 >> PROVE_TAC [] 812QED 813 814Theorem IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___R_AND_SPLIT : 815 !S S0 R1 R2 i w. 816 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 (XP_AND(R1, R2))) i w <=> 817 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 R1) i w /\ 818 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 R2) i w 819Proof 820 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 821 symbolic_semi_automaton_REWRITES, P_SEM_def, IS_TRANSITION_def, 822 XP_SEM_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def] 823 >> PROVE_TAC [] 824QED 825 826Theorem IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___R_AND_SPLIT_MINIMAL : 827 !S S0 R1 R2 i w. 828 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 (XP_AND(R1, R2))) i w <=> 829 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0 XP_TRUE) i w /\ 830 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S P_TRUE R1) i w /\ 831 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S P_TRUE R2) i w 832Proof 833 METIS_TAC [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___R_AND_SPLIT, 834 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___SPLIT] 835QED 836 837Theorem IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___S0_AND_SPLIT : 838 !S S0_1 S0_2 R i w. 839 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S (P_AND(S0_1, S0_2)) R) i w 840 <=> 841 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0_1 R) i w /\ 842 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0_2 R) i w 843Proof 844 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 845 symbolic_semi_automaton_REWRITES, P_SEM_def, IS_TRANSITION_def, 846 XP_SEM_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def] 847 >> METIS_TAC [] 848QED 849 850Theorem IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___S0_AND_SPLIT_MINIMAL : 851 !S S0_1 S0_2 R i w. 852 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S (P_AND(S0_1, S0_2)) R) i w 853 <=> 854 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S P_TRUE R) i w /\ 855 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0_1 XP_TRUE) i w /\ 856 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S S0_2 XP_TRUE) i w 857Proof 858 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 859 symbolic_semi_automaton_REWRITES, P_SEM_def, IS_TRANSITION_def, 860 XP_SEM_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def] 861 >> METIS_TAC [] 862QED 863 864Theorem IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON___S_EXTENSION : 865 !S1 S2 S' S0 R i w. 866 (S2 = S1 UNION S') /\ DISJOINT S' (P_USED_VARS S0 UNION XP_USED_VARS R) /\ 867 PATH_SUBSET w S2 ==> 868 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S2 S0 R) i w <=> 869 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (symbolic_semi_automaton S1 S0 R) i 870 (PATH_RESTRICT w S1)) 871Proof 872 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 873 symbolic_semi_automaton_REWRITES, IS_TRANSITION_def, 874 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 875 PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET, 876 DISJOINT_UNION_BOTH, GSYM SUBSET_COMPL_DISJOINT, UNION_SUBSET] 877 >> rpt STRIP_TAC 878 >> SUBGOAL_TAC `!n. (w n UNION (i n DIFF (S1 UNION S'))) INTER COMPL S' = 879 (w n INTER S1 UNION (i n DIFF S1)) INTER COMPL S'` 880 >- (FULL_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_COMPL, IN_UNION, IN_DIFF, SUBSET_DEF] \\ 881 rpt STRIP_TAC \\ 882 rpt BOOL_EQ_STRIP_TAC >> PROVE_TAC []) 883 >> PROVE_TAC [P_USED_VARS_INTER_SUBSET_THM, XP_USED_VARS_INTER_SUBSET_BOTH_THM] 884QED 885 886Theorem SEMI_AUTOMATON___VAR_RENAMING : 887 !A v f w. INJ f ((PATH_USED_VARS v) UNION (PATH_USED_VARS w) UNION (SEMI_AUTOMATON_USED_VARS A)) 888 UNIV ==> 889 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A v w = 890 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON 891 (SEMI_AUTOMATON_VAR_RENAMING f A) (PATH_VAR_RENAMING f v) (PATH_VAR_RENAMING f w)) 892Proof 893 Cases_on `A` 894 >> FULL_SIMP_TAC std_ss 895 [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, IS_TRANSITION_def, 896 INPUT_RUN_PATH_UNION_def, PATH_VAR_RENAMING_def, PATH_MAP_def, 897 symbolic_semi_automaton_REWRITES, 898 SEMI_AUTOMATON_VAR_RENAMING_def, INPUT_RUN_STATE_UNION_def, 899 PATH_SUBSET_def, PATH_USED_VARS_def, SEMI_AUTOMATON_USED_VARS_def, 900 INJ_DEF, IN_UNIV, IN_UNION, IN_BIGUNION, GSPECIFICATION, 901 SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, GSYM RIGHT_EXISTS_AND_THM, 902 GSYM EXISTS_OR_THM] 903 >> rpt STRIP_TAC 904 >> BINOP_TAC >| [ ALL_TAC, BINOP_TAC ] 905 >| [ (* goal 1 (of 3) *) 906 FORALL_EQ_STRIP_TAC THEN 907 SIMP_TAC std_ss [IMAGE_DEF, SUBSET_DEF, GSPECIFICATION] THEN 908 METIS_TAC[], 909 (* goal 2 (of 3) *) 910 SUBGOAL_TAC `INJ f' (v 0 UNION f) UNIV /\ 911 INJ f' ((w 0 UNION (v 0 DIFF f)) UNION (P_USED_VARS p)) UNIV` 912 >- (SIMP_TAC std_ss [INJ_DEF, IN_UNIV, IN_UNION, IN_DIFF] \\ 913 METIS_TAC []) \\ 914 FULL_SIMP_TAC std_ss [GSYM IMAGE_DIFF, GSYM IMAGE_UNION] \\ 915 PROVE_TAC[P_SEM___VAR_RENAMING], 916 (* goal 3 (of 3) *) 917 FORALL_EQ_STRIP_TAC \\ 918 SUBGOAL_TAC `!n. INJ f' (v n UNION f) UNIV /\ 919 INJ f' ((w n UNION (v n DIFF f)) UNION 920 (w (SUC n) UNION (v (SUC n) DIFF f)) UNION 921 (XP_USED_VARS x)) UNIV` 922 >- (SIMP_TAC std_ss [INJ_DEF, IN_UNIV, IN_UNION, IN_DIFF] \\ 923 METIS_TAC []) \\ 924 FULL_SIMP_TAC std_ss [GSYM IMAGE_DIFF, GSYM IMAGE_UNION] \\ 925 METIS_TAC [XP_SEM___VAR_RENAMING] ] 926QED 927 928Theorem SEMI_AUTOMATON___STATE_VAR_RENAMING : 929 !A f. (INJ f UNIV UNIV) /\ (!x. x IN (SEMI_AUTOMATON_USED_INPUT_VARS A) ==> (f x = x)) ==> 930 !i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w = 931 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (SEMI_AUTOMATON_VAR_RENAMING f A) 932 i (PATH_VAR_RENAMING f w) 933Proof 934 rpt STRIP_TAC 935 >> SUBGOAL_TAC 936 `((PATH_RESTRICT i (SEMI_AUTOMATON_USED_INPUT_VARS A)) = 937 (PATH_RESTRICT (PATH_VAR_RENAMING f i) (SEMI_AUTOMATON_USED_INPUT_VARS A))) /\ 938 (SEMI_AUTOMATON_USED_INPUT_VARS (SEMI_AUTOMATON_VAR_RENAMING f A) = 939 SEMI_AUTOMATON_USED_INPUT_VARS A)` 940 >- (Cases_on `A` THEN 941 SIMP_ALL_TAC std_ss 942 [PATH_RESTRICT_def, PATH_MAP_def, SEMI_AUTOMATON_USED_INPUT_VARS_def, 943 SEMI_AUTOMATON_VAR_RENAMING_def, 944 symbolic_semi_automaton_REWRITES, 945 P_VAR_RENAMING___USED_VARS, EXTENSION, IN_UNION, IN_DIFF, 946 IN_IMAGE, XP_VAR_RENAMING___USED_VARS, INJ_DEF, IN_UNIV] \\ 947 rpt STRIP_TAC >| 948 [ ONCE_REWRITE_TAC [FUN_EQ_THM] \\ 949 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, PATH_VAR_RENAMING_def, 950 PATH_MAP_def, IN_IMAGE] \\ 951 rpt GEN_TAC >> rpt BOOL_EQ_STRIP_TAC >> PROVE_TAC [], 952 PROVE_TAC [] ]) 953 >> METIS_TAC [SEMI_AUTOMATON___VAR_RENAMING, INJ_SUBSET_DOMAIN, SUBSET_UNIV, 954 SEMI_AUTOMATON_USED_INPUT_VARS_INTER_THM] 955QED 956 957Theorem P_SEM_AUTOMATON_RUN___STATE_VAR_RENAMING : 958 !A p f. INJ f UNIV UNIV /\ 959 (!x. x IN (SEMI_AUTOMATON_USED_INPUT_VARS A UNION (P_USED_VARS p DIFF A.S)) ==> (f x = x)) ==> 960 !i w t. (P_SEM (INPUT_RUN_PATH_UNION A i w t) p = 961 P_SEM (INPUT_RUN_PATH_UNION (SEMI_AUTOMATON_VAR_RENAMING f A) i 962 (PATH_VAR_RENAMING f w) t) 963 (P_VAR_RENAMING f p)) 964Proof 965 rpt STRIP_TAC 966 >> SIMP_ASSUMPTIONS_TAC std_ss [IN_UNION, IN_DIFF] 967 >> `P_SEM (INPUT_RUN_PATH_UNION A i w t) p = 968 P_SEM (IMAGE f (INPUT_RUN_PATH_UNION A i w t)) (P_VAR_RENAMING f p)` 969 by METIS_TAC [P_SEM___VAR_RENAMING, INJ_SUBSET_DOMAIN, SUBSET_UNIV] 970 >> ASM_REWRITE_TAC [] 971 >> `P_USED_VARS (P_VAR_RENAMING f p) = IMAGE f (P_USED_VARS p)` 972 by METIS_TAC [P_VAR_RENAMING___USED_VARS] 973 >> SUBGOAL_TAC `(IMAGE f (INPUT_RUN_PATH_UNION A i w t)) INTER (P_USED_VARS (P_VAR_RENAMING f p)) = 974 (INPUT_RUN_PATH_UNION (SEMI_AUTOMATON_VAR_RENAMING f A) i 975 (PATH_VAR_RENAMING f w) t) INTER 976 (P_USED_VARS (P_VAR_RENAMING f p))` 977 >- (ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_IMAGE] \\ 978 GEN_TAC >> CONJ_EQ_STRIP_TAC \\ 979 Cases_on `A` \\ 980 SIMP_ALL_TAC std_ss [IN_IMAGE, SEMI_AUTOMATON_VAR_RENAMING_def, 981 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 982 PATH_VAR_RENAMING_def, symbolic_semi_automaton_REWRITES, 983 PATH_MAP_def, IN_UNION, IN_DIFF, INJ_DEF, IN_UNIV] \\ 984 METIS_TAC []) 985 >> PROVE_TAC [P_USED_VARS_INTER_THM] 986QED 987 988Theorem TRANSITION_CURRENT_STATE_CLEANING : 989 !A s1 i1 s2 i2. IS_TRANSITION A s1 i1 s2 i2 = 990 IS_TRANSITION A (s1 INTER A.S) (i1 UNION s1) s2 i2 991Proof 992 SIMP_TAC std_ss [IS_TRANSITION_def, INPUT_RUN_STATE_UNION_def] 993 >> rpt STRIP_TAC 994 >> REMAINS_TAC `s1 UNION (i1 DIFF A.S) = s1 INTER A.S UNION (i1 UNION s1 DIFF A.S)` 995 >- ASM_REWRITE_TAC [] 996 >> SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] 997 >> PROVE_TAC [] 998QED 999 1000Theorem TRANSITION_NEXT_STATE_CLEANING : 1001 !A s1 i1 s2 i2. IS_TRANSITION A s1 i1 s2 i2 = 1002 IS_TRANSITION A s1 i1 (s2 INTER A.S) (i2 UNION s2) 1003Proof 1004 SIMP_TAC std_ss [IS_TRANSITION_def, INPUT_RUN_STATE_UNION_def] 1005 >> rpt STRIP_TAC 1006 >> REMAINS_TAC `s2 UNION (i2 DIFF A.S) = s2 INTER A.S UNION (i2 UNION s2 DIFF A.S)` 1007 >- ASM_REWRITE_TAC [] 1008 >> SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] 1009 >> PROVE_TAC [] 1010QED 1011 1012Theorem TRANSITION_STATE_CLEANING : 1013 !A s1 i1 s2 i2. IS_TRANSITION A s1 i1 s2 i2 = 1014 IS_TRANSITION A (s1 INTER A.S) (i1 UNION s1) (s2 INTER A.S) (i2 UNION s2) 1015Proof 1016 PROVE_TAC [TRANSITION_CURRENT_STATE_CLEANING, 1017 TRANSITION_NEXT_STATE_CLEANING] 1018QED 1019 1020val _ = export_theory (); 1021