src/deep_embeddings/symbolic_semi_automatonScript.sml

91 (* (s1,i1) is the current state, (s2,i2) is the next state *)
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)`;
120       (!s1 i1 i2. EXISTS_AT_MOST_ONE s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`;
128       (!s1 i1 i2. ?s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`;
140        (!s1 i1 i2. ?!s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))
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
288       (SKOLEM_CONV ``!s1 i1 i2. ?s2. s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2``)
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)
302  >> EXISTS_TAC ``\s1 i1 i2. @s2. (s2 SUBSET A.S /\ IS_TRANSITION A s1 i1 s2 i2)``
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)
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 []
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`
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
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)
1006  >> REMAINS_TAC `s2 UNION (i2 DIFF A.S) = s2 INTER A.S UNION (i2 UNION s2 DIFF A.S)`
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)