Origin Definitions Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb_event_system_3
Nuprl Section: mb_event_system_3

Selected Objects
defes-ble es-ble{i:l}(es;e;e')
== InjCase(decidable__es_DASH_le{1:l, i:l}(es,e',e); x. true, false)
THMassert-es-ble es:ES, e,e':E. es-ble{i:l}(es;e;e')  e  e' 
defes-mtag mtag(m) == mtag(m)
defes-before before(e) == if first(e) nil else before(pred(e)) @ [pred(e)] fi  (recursive)
THMmember-es-before the_es:ES, e',e:E. (e  before(e'))  (e <loc e')
defes-interval [e, e'] == filter(ev.es-ble{i:l}(es;e;ev);before(e') @ [e'])
THMmember-es-interval es:ES, e,e',ev:E. (ev  [e, e'])  e  ev  & ev  e' 
defes-tg-sends sends(l,tg,e) == filter(m.mtag(m) = tg;sends(l;e))
THMes-after-pred es:ES, x:Id, e:E.
first(e)  (x after pred(e)) = (x when e)  vartype(loc(e);x)
defalle-at e@i.P(e) == e:E. loc(e) = i  Id  P(e)
defalle-at1 @i always.P(v) == e@i.P((x when e))
THMalle-at-iff es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop).
e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e)
THMes-invariant1 es:ES, i,x:Id, T:Type, I:(TProp).
(vartype(i;x) r T) & e@i.first(e)  I((x when e))

e@i.I((x when e))  I((x after e))  @i always.I(x)
defexistse-at e@i.P(e) == e:E. loc(e) = i  Id & P(e)
THMchange-lemma es:ES, x,i:Id, T:Type.
(x,y:T. Dec(x = y  T))

(vartype(i;x) r T)

(e',e:E.
(e  e' 
(
(loc(e') = i  Id
(
((x after e') = (x when e)  T
(
((ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T))
THMes-first-exists es:ES, e':E. e:E. first(e) & e  e' 
THMchange-since-init es:ES, x,i:Id, T:Type, c:T.
(x,y:T. Dec(x = y  T))

(vartype(i;x) r T)

(e:E. loc(e) = i  Id  first(e)  (x when e) = c  T)

(e':E. 
(loc(e') = i  Id
(
((x after e') = c  T  (ev:E. ev  e'  & (x after ev) = (x when ev)  T))
THMes-rcv-kind es:ES, l:IdLnk, tg:Id, e:E.
isrcv(e)  lnk(e) = l  tag(e) = tg  kind(e) = rcv(l; tg)
THMes-kind-rcv es:ES, l:IdLnk, tg:Id, e:E.
kind(e) = rcv(l; tg)

isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)
defaction action(dec) == Unit+(k:Knddec(k))
defw-action-dec w-action-dec(TA;M;i)(k)
== kindcase(k;a.TA(i,a);l,tg.if destination(l) = i M(l,tg) else Void fi)
defworld World
== T:IdIdType
== TA:IdIdType
== M:IdLnkIdType
== (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i)))
== (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top
defw-T w.T == 1of(w)
defw-TA w.TA == 1of(2of(w))
defw-M w.M == 1of(2of(2of(w)))
defw-vartype vartype(i;x) == w.T(i,x)
defw-action Action(i) == action(w-action-dec(w.TA;w.M;i))
defw-isnull isnull(a) == isl(a)
defw-kind kind(a) == 1of(outr(a))
defw-valtype valtype(i;a) == kindcase(kind(a);a.w.TA(i,a);l,tg.w.M(l,tg))
defw-val val(a) == 2of(outr(a))
defw-isrcvl isrcv(l;a) == isnull(a)isrcv(kind(a))lnk(kind(a)) = l
THMassert-w-isrcvl the_w:World, l:IdLnk, i:Id, a:Action(i).
isrcv(l;a)  isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l
defw-Msg Msg == Msg(w.M)
defw-s s(i;t).x == 1of(2of(2of(2of(w))))(i,t,x)
defw-a a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t)
defw-m m(i;t) == 1of(2of(2of(2of(2of(2of(w))))))(i,t)
defw-onlnk onlnk(l;mss) == filter(ms.mlnk(ms) = l;mss)
THMw-onlnk-m w:World, t:, l:IdLnk, i:Id. ||onlnk(l;m(i;t))||  
defw-withlnk withlnk(l;mss) == mapfilter(ms.2of(ms);ms.mlnk(ms) = l;mss)
defw-tagged w-tagged(tg; mss) == filter(ms.mtag(ms) = tg;mss)
defw-ml m(l;t) == onlnk(l;m(source(l);t))
defw-snds snds(l;t) == concat(map(t1.m(l;t1);upto(t)))
defw-rcvs rcvs(l;t) == filter(a.isrcv(l;a);map(t1.a(destination(l);t1);upto(t)))
defw-queue queue(l;t) == nth_tl(||rcvs(l;t)||;snds(l;t))
defw-msg msg(a) == msg(lnk(kind(a));tag(kind(a));val(a))
deffair-fifo FairFifo
== (i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List)
== & (i:Id, t:.
== & (isnull(a(i;t))
== & (
== & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x)) & m(i;t) = nil  Msg List)
== & (i:Id, t:, l:IdLnk.
== & (isrcv(l;a(i;t))
== & (
== & (destination(l) = i
== & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg)
== & (l:IdLnk, t:.
== & (t':. 
== & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)
defw-E E == {p:(Id)| isnull(a(1of(p);2of(p))) }
defw-eq-E p = q == 1of(p) = 1of(q)(2of(p)=2of(q))
THMassert-w-eq-E the_w:World, e,e':E. e = e'  e = e'
THMassert-w-eq-E-iff the_w:World, e,e':E. e = e'  e = e'
defw-loc loc(e) == 1of(e)
defw-act act(e) == a(1of(e);2of(e))
THMw-act-not-null the_w:World, e:E. isnull(act(e))
defw-ekind kind(e) == kind(act(e))
defw-V V(i;k) == kindcase(k;a.1of(2of(w))(i,a);l,tg.1of(2of(2of(w)))(l,tg))
defw-eval val(e) == val(act(e))
defw-time time(e) == 2of(e)
defw-when (x when e) == s(1of(e);2of(e)).x
defw-after (x after e) == s(1of(e);2of(e)+1).x
defw-initially (x initially i) == s(i;0).x
defw-first first(e)
== if time(e)=0 true
== i; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>)
== else false fi
(recursive)
THMw-first-aux the_w:World, i:Id, t:. first(<i,t>)  
THMassert-w-first the_w:World, e:E. first(e)  (t':. t'<time(e)  isnull(a(loc(e);t')))
THMw-loc-time the_w:World, e:E. <loc(e),time(e)> ~ e
defw-pred pred(e)
== if isnull(a(loc(e);time(e)-1)) pred(<loc(e),time(e)-1>)
== else <loc(e),time(e)-1> fi
(recursive)
THMw-pred-aux the_w:World, t:, i:Id. first(<i,t>)  pred(<i,t>)  E
defw-locl e <loc e' == loc(e) = loc(e')  Id & time(e)<time(e')
defw-sends sends(l;e) == onlnk(l;m(loc(e);time(e)))
defw-match match(l;t;t')
== (||snds(l;t)||||rcvs(l;t')||)
== (||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||)
THMassert-w-match the_w:World, l:IdLnk, t,t':.
match(l;t;t')

||snds(l;t)||||rcvs(l;t')||
& ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||
THMw-match-exists the_w:World, e:E.
FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))
THMbetter-w-match-exists the_w:World, e:E.
FairFifo

isrcv(kind(e))

(t:time(e). 
(match(lnk(kind(e));t;time(e))
(& onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
(& -||snds(lnk(kind(e));t)||)]
(& =
(& msg(a(loc(e);time(e)))
(&  Msg)
THMw-match-unique the_w:World, e:E, t,t':.
FairFifo

isrcv(kind(e))

match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'
THMw-match-property the_w:World, e:E, t:.
FairFifo

isrcv(kind(e))

match(lnk(kind(e));t;time(e))

onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
-||snds(lnk(kind(e));t)||)]
=
msg(a(loc(e);time(e)))
 Msg
defw-sender sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>
defw-index index(e)
== ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));time(sender(e)))||
defw-causl e <c e' == e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^+ e'
THMw-causl-time the_w:World, e,e':E. FairFifo  e <c e'  time(e)<time(e')
THMw-locl-iff the_w:World, e,e':E. FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e')
THMworld-event-system the_w:World. 
FairFifo

ESAxioms{i:l}
ESAxioms(E;
ESAxioms((i,x. vartype(i;x));
ESAxioms(the_w.M;
ESAxioms((e.loc(e));
ESAxioms((e.kind(e));
ESAxioms((e.val(e));
ESAxioms((x,e. (x when e));
ESAxioms((x,e. (x after e));
ESAxioms((l,e. sends(l;e));
ESAxioms((e.sender(e));
ESAxioms((e.index(e));
ESAxioms((e.first(e));
ESAxioms((e.pred(e));
ESAxioms((e,e'. e <c e'))
defw-es ES(the_w;p)
== <E
== ,product-deq(Id;;IdDeq;NatDeq)
== ,(i,x. vartype(i;x))
== ,(i,a. V(i;locl(a)))
== ,the_w.M
== ,
== ,(e.loc(e))
== ,(e.kind(e))
== ,(e.val(e))
== ,(x,e. (x when e))
== ,(x,e. (x after e))
== ,(l,e. sends(l;e))
== ,(e.sender(e))
== ,(e.index(e))
== ,(e.first(e))
== ,(e.pred(e))
== ,(e,e'. e <c e')
== ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p)
== ,>
THMes-valtype-w-valtype i:Id, w:World, p:FairFifo, t:.
isnull(a(i;t))  (valtype(<i,t>) ~ valtype(i;a(i;t)))
deffpf a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
THMsubtype-fpf2 B1,B2:(AType). (a:A. B1(a) r B2(a))  (a:A fp-> B1(a) r a:A fp-> B2(a))
THMsubtype-fpf3 B1:(A1Type), B2:(A2Type).
strong-subtype(A1;A2)

(a:A1. B1(a) r B2(a))  (a:A1 fp-> B1(a) r a:A2 fp-> B2(a))
deffpf-dom x  dom(f) == deq-member(eq;x;1of(f))
THMfpf-dom_functionality B:(AType), eq1,eq2:EqDecider(A), f:a:A fp-> B(a), x:A.
x  dom(f) = x  dom(f)  
THMfpf-dom_functionality2 eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x  dom(f)  x  dom(f)
THMfpf-dom-type eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
strong-subtype(X;Y)  x  dom(f)  x  X
THMfpf-dom-type2 eq:EqDecider(Y), f:x:X fp-> Top, x:Y.
strong-subtype(X;Y)  x  dom(f)  x  X
deffpf-empty == <nil,x.>
deffpf-is-empty fpf-is-empty(f) == ||1of(f)||=0
THMassert-fpf-is-empty B:(AType), f:x:A fp-> B(x). fpf-is-empty(f)  f =   x:A fp-> B(x)
deffpf-ap f(x) == 2of(f)(x)
deffpf-cap f(x)?z == if x  dom(f) f(x) else z fi
deffpf-val z != f(x) ==> P(a;z) == x  dom(f)  P(x;f(x))
deffpf-sub f  g == x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)
THMfpf-empty-sub B,eq,g:Top.   g
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections EventSystems Doc