examples/sigma/semanticsScript.sml

285     THEN MP_TAC (SPECL [���l:^dict���,���OBJ l���,���lb:string���]
293     ���!d l x L. ((invoke (OBJ d) l) <[ [x,L]) =
294                     invoke ((OBJ d) <[ [x,L]) l���,
375     ���!d lb mth x L. ((update (OBJ d) lb mth) <[ [x,L]) =
376                       update ((OBJ d) <[ [x,L]) lb (mth <[ [x,L])���,
392 (*        INVOKE (OBJ d) l   or   UPDATE (OBJ d) l m                     *)
404       (^SIGMA_R (INVOKE (OBJ d) l) (invoke (OBJ d) l))      /\
408     (^SIGMA_R (UPDATE (OBJ d) l m) (update (OBJ d) l m))
469                    (?d. (o1 = OBJ d) /\ (o2 = invoke o1 l))) /\
471                    (?d. (o1 = OBJ d) /\ (o2 = update o1 l m))) /\
473         (!d o2. SIGMA_R (OBJ d) o2 = F)���,
564                 (^REDL_obj (OBJ d1) (OBJ d2)))                          /\
609      (^REDL_obj (INVOKE (OBJ d1) l) (invoke (OBJ d2) l)))             /\
614    (^REDL_obj (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)))
643          (!d1 d2. P_1 d1 d2 ==> P_0 (OBJ d1) (OBJ d2)) /\
649            P_1 d1 d2 ==> P_0 (INVOKE (OBJ d1) l) (invoke (OBJ d2) l)) /\
652            P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
768          (!d1 d2. P_1 d1 d2 ==> P_0 (OBJ d1) (OBJ d2)) /\
774            P_1 d1 d2 ==> P_0 (INVOKE (OBJ d1) l) (invoke (OBJ d2) l)) /\
777            P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
811          (!d1 d2. P_1 d1 d2 /\ REDL_dict d1 d2 ==> P_0 (OBJ d1) (OBJ d2)) /\
820            P_0 (INVOKE (OBJ d1) l) (invoke (OBJ d2) l)) /\
823            P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
942          (!d1 d2. P_1 d1 d2 /\ REDL_dict d1 d2 ==> P_0 (OBJ d1) (OBJ d2)) /\
951            P_0 (INVOKE (OBJ d1) l) (invoke (OBJ d2) l)) /\
954            P_0 (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2)) /\
1015         THEN EXISTS_TAC ���FV_obj (OBJ d2)���
1019         THEN EXISTS_TAC ���FV_obj (OBJ d2) UNION FV_method m2���
1258             (!d l. (OBJ d = M) ==>
1305           REDL_obj (OBJ D) M' ==>
1307                 REDL_obj (invoke (OBJ D) l) (invoke M' l))) /\
1332           (!d N N' l. (OBJ d = M) /\ REDL_method N N' ==>
1356                 REDL_obj (update (OBJ D) l N) (update (OBJ D) l N')) /\
1371             (!d N N' l. (OBJ d = M) /\ REDL_method N N' ==>
1414           REDL_obj (OBJ D) M' ==>
1416                 REDL_obj (update (OBJ D) l N) (update M' l N'))) /\
1433           REDL_obj (OBJ d) o1 ==> (?d2. o1 = OBJ d2)���,
1450           REDL_obj (OBJ d1) (OBJ d2) ==> REDL_dict d1 d2���,
1483           REDL_obj (OBJ d1) o2 ==>
1484           (?d2. (o2 = (OBJ d2)) /\ REDL_dict d1 d2)) /\
1488            (?d1 d2. (o1 = OBJ d1) /\
1489                     (o2 = (invoke (OBJ d2) l)) /\
1496            (?d1 d2 m2. (o1 = OBJ d1) /\
1497                     (o2 = (update (OBJ d2) l m2)) /\
1652         THEN EXISTS_TAC ���OBJ d4���
1661             UNDISCH_THEN ���o1 = OBJ d1��� REWRITE_ALL_THM
1670             THEN EXISTS_TAC ���invoke (OBJ d2') l���
1680             UNDISCH_THEN ���o1 = OBJ d1��� REWRITE_ALL_THM
1689             THEN EXISTS_TAC ���update (OBJ d2') l m4���
1699             THEN EXISTS_TAC ���invoke (OBJ d4) l���
1702             UNDISCH_THEN ���OBJ d1 = OBJ d1'���
1706             THEN EXISTS_TAC ���invoke (OBJ d4) l���
1716             THEN EXISTS_TAC ���update (OBJ d4) l m4���
1719             UNDISCH_THEN ���OBJ d1 = OBJ d1'���
1723             THEN EXISTS_TAC ���update (OBJ d4) l m4���
1907           RED1_obj SIGMA_R (INVOKE (OBJ d) l) (invoke (OBJ d) l)) /\
1909           RED1_obj SIGMA_R (UPDATE (OBJ d) l m) (update (OBJ d) l m))���,
1919           RED_obj SIGMA_R (INVOKE (OBJ d1) l) (invoke (OBJ d2) l)) /\
1923           RED_obj SIGMA_R (UPDATE (OBJ d1) l m1) (update (OBJ d2) l m2))
1928         THEN EXISTS_TAC ���INVOKE (OBJ d2) l���
1940         THEN EXISTS_TAC ���UPDATE (OBJ d2) l m2���
1946             THEN EXISTS_TAC ���UPDATE (OBJ d2) l m1���