examples/sigma/liftScript.sml

36 val obj   =  ty_antiq( ==`:obj1`== );
285     ���!o1:^obj o2 s1 s2.
532     ���(!t:^obj xs ys.
554     ���(!t:^obj x y.
569     ���((!x d.       ~(ALPHA_obj (OVAR1 x)       (OBJ1 d        : ^obj))) /\
570          (!x a l.     ~(ALPHA_obj (OVAR1 x)       (INVOKE1 a l   : ^obj))) /\
571          (!x a l m.   ~(ALPHA_obj (OVAR1 x)       (UPDATE1 a l m : ^obj))) /\
572          (!d a l.     ~(ALPHA_obj (OBJ1 d)        (INVOKE1 a l   : ^obj))) /\
573          (!d a l m.   ~(ALPHA_obj (OBJ1 d)        (UPDATE1 a l m : ^obj))) /\
574          (!a l b s m. ~(ALPHA_obj (INVOKE1 a l)   (UPDATE1 b s m : ^obj))) /\
575          (!d x.       ~(ALPHA_obj (OBJ1 d)        (OVAR1 x       : ^obj))) /\
576          (!a l x.     ~(ALPHA_obj (INVOKE1 a l)   (OVAR1 x       : ^obj))) /\
577          (!a l m x.   ~(ALPHA_obj (UPDATE1 a l m) (OVAR1 x       : ^obj))) /\
578          (!a l d.     ~(ALPHA_obj (INVOKE1 a l)   (OBJ1 d        : ^obj))) /\
579          (!a l m d.   ~(ALPHA_obj (UPDATE1 a l m) (OBJ1 d        : ^obj))) /\
580          (!a l m b s. ~(ALPHA_obj (UPDATE1 a l m) (INVOKE1 b s   : ^obj))))
588     ���(!a:^obj. (?x. ALPHA_obj a (OVAR1 x)) \/
652 (* !(var : var->'a) obj inv upd cns nil par sgm.                       *)
658 (*       (!d.     ho (OBJ1 d) = obj (hd d)) /\                         *)
684     `(hom_o (OVAR1 x) var obj nvk upd cns nil par sgm = (var x):'a) /\
685      (hom_o (OBJ1 d) var obj nvk upd cns nil par sgm =
686          obj (hom_d d var obj nvk upd cns nil par sgm) d) /\
687      (hom_o (INVOKE1 a l) var obj nvk upd cns nil par sgm =
688          nvk (hom_o a var obj nvk upd cns nil par sgm) a l) /\
689      (hom_o (UPDATE1 a l m) var obj nvk upd cns nil par sgm =
690          upd (hom_o a var obj nvk upd cns nil par sgm)
691             (hom_m m var obj nvk upd cns nil par sgm) a l m) /\
692      (hom_d (e::d) var obj nvk upd cns nil par sgm =
693          cns (hom_e e var obj nvk upd cns nil par sgm)
694              (hom_d d var obj nvk upd cns nil par sgm) e d) /\
695      (hom_d ([]) var obj nvk upd cns nil par sgm = nil:'b) /\
696      (hom_e (l,m) var obj nvk upd cns nil par sgm =
697          (par (hom_m m var obj nvk upd cns nil par sgm) l m):'c) /\
698      (hom_m (SIGMA1 x a) var obj nvk upd cns nil par sgm =
699          (sgm (\y. hom_o (a <[ [x, OVAR1 y]) var obj nvk upd cns nil par sgm)
800     ���!(var :var -> 'a) obj nvk upd cns (nil:'b)
802          respects($= ===> ALPHA_dict ===> $=) obj /\
810          (!t:^obj u. (HEIGHT_obj1 t <= n) /\ ALPHA_obj t u ==>
811              (hom_o t var obj nvk upd cns nil par sgm =
812               hom_o u var obj nvk upd cns nil par sgm)) /\
814              (hom_d t var obj nvk upd cns nil par sgm =
815               hom_d u var obj nvk upd cns nil par sgm)) /\
817              (hom_e t var obj nvk upd cns nil par sgm =
818               hom_e u var obj nvk upd cns nil par sgm)) /\
820              (hom_m t var obj nvk upd cns nil par sgm =
821               hom_m u var obj nvk upd cns nil par sgm))���),
866     ���!(var :var -> 'a) obj nvk upd cns (nil:'b)
868           respects($= ===> ALPHA_dict ===> $=) obj /\
876                      (\a. hom_o a var obj nvk upd cns nil par sgm) /\
878                      (\d. hom_d d var obj nvk upd cns nil par sgm) /\
880                      (\e. hom_e e var obj nvk upd cns nil par sgm) /\
882                      (\m. hom_m m var obj nvk upd cns nil par sgm)���),
908     ���!(var :var -> 'a) obj nvk upd cns (nil:'b)
910           respects($= ===> ALPHA_dict ===> $=) obj /\
923            (!d.     hom_o (OBJ1 d) = obj (hom_d d) d) /\
936            ���((\t:^obj.    hom_o t (var:var->'a) obj nvk upd cns
938                 (\t:^dict.   hom_d t var obj nvk upd cns nil par sgm),
939                 (\t:^entry.  hom_e t var obj nvk upd cns nil par sgm),
940                 (\t:^method. hom_m t var obj nvk upd cns nil par sgm))���
952          (var :var -> 'a) obj nvk upd cns (nil:'b)
963             (!d.     hom_o1 (OBJ1 d) = obj (hom_d1 d) d) /\
973             (!d.     hom_o2 (OBJ1 d) = obj (hom_d2 d) d) /\
1013          (var :var -> 'a) obj nvk upd cns (nil:'b)
1024             (!d.     hom_o1 (OBJ1 d) = obj (hom_d1 d) d) /\
1034             (!d.     hom_o2 (OBJ1 d) = obj (hom_d2 d) d) /\
1062     ���!(var :var -> 'a) obj nvk upd cns (nil:'b)
1075             (!d.     hom_o1 (OBJ1 d) = obj (hom_d1 d) d) /\
1085             (!d.     hom_o2 (OBJ1 d) = obj (hom_d2 d) d) /\
1175          (obj :: respects($= ===> ALPHA_dict ===> $=))
1190             (!d.     hom_o (OBJ1 d) = obj (hom_d d) d) /\
1304                func= ���OVAR1 :var->^obj���, fixity=NONE
1307                func= ���OBJ1 :^dict -> ^obj���, fixity=NONE},
1309                func= ���INVOKE1 :^obj -> string -> ^obj���, fixity=NONE},
1311                func= ���UPDATE1 :^obj -> string -> ^method -> ^obj���,
1314                func= ���SIGMA1 :var -> ^obj -> ^method���, fixity=NONE},
1316                func= ���ABS1 :(var -> ^obj) -> ^method���, fixity=NONE},
1318                func= ���HEIGHT_obj1 :^obj -> num���, fixity=NONE},
1326                func= ���FV_obj1 :^obj -> var -> bool���, fixity=NONE},
1334                func= ���SUB1 :^subs -> var -> ^obj���, fixity=NONE},
1339                func= ���SUB1o :^obj -> ^subs -> ^obj���,
1545     {types = [{name = "obj",    equiv = ALPHA_obj_EQUIV},
1626 val subs  =  ty_antiq( ==`:(var # obj) list`== );
1627 val obj   =  ty_antiq( ==`:obj`== );
1889     ���!y x1 (t1:^obj) x2 t2 s.
1922                         ���x:var���,���a:obj���]
1944                         ���x:var���,���a:obj���]
2071     THEN EXISTS_TAC ���MAP (\a:obj. a <[ [x,OVAR z]) os���
2072     THEN MP_TAC (SPECL [���os:obj list���,z,���x:var���]
2135     THEN DEP_ONCE_REWRITE_TAC[SPECL [���a:obj���,
2160                         ���x:var���,���a:obj���]
2168     THEN EXISTS_TAC ���o':obj���
2193     THEN EXISTS_TAC ���o':obj���