Nuprl - Definition Cascade for w-es

WhoCites Definitions mb event system 6 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

	Who Cites w-es?

w-es	Def ES(the_w;p) Def == <E Def == ,product-deq(Id;;IdDeq;NatDeq) Def == ,(i,x. vartype(i;x)) Def == ,(i,a. V(i;locl(a))) Def == ,the_w.M Def == , Def == ,(e.loc(e)) Def == ,(e.kind(e)) Def == ,(e.val(e)) Def == ,(x,e. (x when e)) Def == ,(x,e. (x after e)) Def == ,(l,e. sends(l;e)) Def == ,(e.sender(e)) Def == ,(e.index(e)) Def == ,(e.first(e)) Def == ,(e.pred(e)) Def == ,(e,e'. e <c e') Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p) Def == ,>

w-causl	Def e <c e' == e e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^+ e'

w-pred	Def pred(e) Def == if isnull(a(loc(e);time(e)-1)) pred(<loc(e),time(e)-1>) Def == else <loc(e),time(e)-1> fi Def (recursive)

w-first	Def first(e) Def == if time(e)=0 true Def == i; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>) Def == else false fi Def (recursive)

w-index	Def index(e) Def == \|\|rcvs(lnk(kind(e));time(e))\|\|-\|\|snds(lnk(kind(e));time(sender(e)))\|\|

w-sender	Def sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>

w-sends	Def sends(l;e) == onlnk(l;m(loc(e);time(e)))

w-after	Def (x after e) == s(1of(e);2of(e)+1).x

w-when	Def (x when e) == s(1of(e);2of(e)).x

w-eval	Def val(e) == val(act(e))

w-ekind	Def kind(e) == kind(act(e))

w-locl	Def e <loc e' == loc(e) = loc(e') Id & time(e)<time(e')

w-loc	Def loc(e) == 1of(e)

w-M	Def w.M == 1of(2of(2of(w)))

locl	Def locl(a) == inr(a)

	Thm* a:Id. locl(a) Knd

w-V	Def V(i;k) == kindcase(k;a.1of(2of(w))(i,a);l,tg.1of(2of(2of(w)))(l,tg))

w-vartype	Def vartype(i;x) == w.T(i,x)

w-match	Def match(l;t;t') Def == (\|\|snds(l;t)\|\|\|\|rcvs(l;t')\|\|) Def == (\|\|rcvs(l;t')\|\|<\|\|snds(l;t)\|\|+\|\|onlnk(l;m(source(l);t))\|\|)

w-snds	Def snds(l;t) == concat(map(t1.m(l;t1);upto(t)))

w-rcvs	Def rcvs(l;t) == filter(a.isrcv(l;a);map(t1.a(destination(l);t1);upto(t)))

w-ml	Def m(l;t) == onlnk(l;m(source(l);t))

w-onlnk	Def onlnk(l;mss) == filter(ms.mlnk(ms) = l;mss)

w-isrcvl	Def isrcv(l;a) == isnull(a)isrcv(kind(a))lnk(kind(a)) = l

eq_lnk	Def a = b == eqof(IdLnkDeq)(a,b)

	Thm* a,b:IdLnk. a = b

idlnk-deq	Def IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))

id-deq	Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq)

nat-deq	Def NatDeq == <a,b. a=b,nat_DASH_deq_DASH_aux{1:l}>

w-E	Def E == {p:(Id)\| isnull(a(1of(p);2of(p))) }

Id	Def Id == Atom

	Thm* Id Type

nat	Def == {i:\| 0i }

	Thm* Type

product-deq	Def product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>

isrcv	Def isrcv(k) == isl(k)

	Thm* k:Knd. isrcv(k)

prod-deq	Def prod-deq(A;B;a;b) Def == (A,B,a,b,p,q. q/q1,q2. Def == (p/p1,p2. Def == (b/eq,b1. Def == (a/e1,a1. Def == ((%1.%1 Def == ((%1.(<%.<(%1.%1(p1,q1)/%4,%5. %4((%1.%1)((%1.``)(``))))(a1) Def == ((%1.(<%.,(%1.%1(p2,q2)/%4,%5. %4((%1.%1)((%1.``)(``))))(b1)> Def == ((%1.(,%.%/%1,%2. ``>)) Def == (((%1.%1.2) Def == ((((%1.%1 Def == ((((%1.(<p1,p2> = <q1,q2> AB Def == ((((%1.,<p1,p2> = <q1,q2> AB Def == ((((%1.,((e1(p1,q1))(eq(p2,q2))) Def == ((((%1.,(e1(p1,q1)) & (eq(p2,q2)) Def == ((((%1.,(%1.%1)((%1.<%2.%2,%2.%2>)(``)) Def == ((((%1.,(%1.%1) Def == ((((%1.,((%1.%1(e1(p1,q1),eq(p2,q2))) Def == ((((%1.,((p,q. InjCase(q; x. InjCase(p Def == ((((%1.,((p,q. InjCase(q; x. InjCase; x. <%.<``,``>,%.``> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. <%.<any(%),``> Def == ((((%1.,((p,q. InjCase(q; x. InjCase; y. ,%.%/%1,%2. any(%1)>) Def == ((((%1.,((p,q. ; y. Def == ((((%1.,((p,q. InjCase(p Def == ((((%1.,((p,q. InjCase; x. <%.<`*`,any(%)>,%.%/%1,%2. any(%2)> Def == ((((%1.,((p,q. InjCase; y. <%.<any(%),any(%)> Def == ((((%1.,((p,q. InjCase; y. ,%.%/%1,%2. any(%2)>)))))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%5 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%6((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. <%2.,%3.(%)> Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%5 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(((((((%)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.<%3.(%1) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%6 Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((((%4.%4) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%4.%4/%5,%6. Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%5((%4.%4)((%4.%4)(%3)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(((((((%1)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.((((%2)))) Def == ((((P1,P2,Q1,Q2,%,%1. ,%2.,%3.(%)>>)))) Def == (A Def == ,B Def == ,a Def == ,b)

assert	Def b == if b True else False fi

	Thm* b:. b Prop

rel_plus	Def R^+(x,y) == n:. x R^n y

	Thm* T:Type, R:(TTType). R^+ TTType

w-time	Def time(e) == 2of(e)

w-act	Def act(e) == a(1of(e);2of(e))

w-a	Def a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t)

w-isnull	Def isnull(a) == isl(a)

rel_exp	Def R^n == if n=0 x,y. x = y T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)

	Thm* n:, T:Type, R:(TTProp). R^n TTProp

upto	Def upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi (recursive)

	Thm* n:. upto(n) n List

eq_int	Def i=j == if i=j true ; false fi

	Thm* i,j:. (i=j)

kindcase	Def kindcase(k;a.f(a);l,t.g(l;t)) Def == if islocal(k) f(act(k)) else g(lnk(k);tag(k)) fi

	Thm* B:Type, k:Knd, f:(IdB), g:(IdLnkIdB). Thm* kindcase(k;a.f(a);l,t.g(l,t)) B

lnk	Def lnk(k) == 1of(outl(k))

	Thm* k:Knd. isrcv(k) lnk(k) IdLnk

length	Def \|\|as\|\| == Case of as; nil 0 ; a.as' \|\|as'\|\|+1 (recursive)

	Thm* A:Type, l:A List. \|\|l\|\|

	Thm* \|\|nil\|\|

mu	Def mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi (recursive)

	Thm* f:(). (n:. f(n)) mu(f)

lsrc	Def source(l) == 1of(l)

	Thm* l:IdLnk. source(l) Id

w-m	Def m(i;t) == 1of(2of(2of(2of(2of(2of(w))))))(i,t)

w-s	Def s(i;t).x == 1of(2of(2of(2of(w))))(i,t,x)

w-val	Def val(a) == 2of(outr(a))

proddeq	Def proddeq(a;b)(p,q) == (1of(a)(1of(p),1of(q)))(1of(b)(2of(p),2of(q)))

	Thm* A,B:Type, a:EqDecider(A), b:EqDecider(B). proddeq(a;b) ABAB

ldst	Def destination(l) == 1of(2of(l))

	Thm* l:IdLnk. destination(l) Id

tagof	Def tag(k) == 2of(outl(k))

	Thm* k:Knd. isrcv(k) tag(k) Id

pi2	Def 2of(t) == t.2

	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))

w-kind	Def kind(a) == 1of(outr(a))

w-T	Def w.T == 1of(w)

mlnk	Def mlnk(m) == 1of(m)

	Thm* M:(IdLnkIdType), m:Msg(M). mlnk(m) IdLnk

	Thm* the_es:ES, m:Msg. mlnk(m) IdLnk

eqof	Def eqof(d) == 1of(d)

	Thm* T:Type, d:EqDecider(T). eqof(d) TT

pi1	Def 1of(t) == t.1

	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

atom-deq	Def AtomDeq == <a,b. a=bAtom,atom_DASH_deq_DASH_aux{1:l}>

le	Def AB == B<A

	Thm* i,j:. (ij) Prop

not	Def A == A False

	Thm* A:Prop. (A) Prop

islocal	Def islocal(k) == isl(k)

	Thm* k:Knd. islocal(k)

isl	Def isl(x) == InjCase(x; y. true; z. false)

	Thm* A,B:Type, x:A+B. isl(x)

nat_plus	Def == {i:\| 0<i }

	Thm* Type

outl	Def outl(x) == InjCase(x; y. y; z. "???")

	Thm* A,B:Type, x:A+B. isl(x) outl(x) A

map	Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] Def (recursive)

	Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List

	Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List

concat	Def concat(ll) == reduce(l,l'. l @ l';nil;ll)

	Thm* T:Type, ll:(T List) List. concat(ll) T List

filter	Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l)

	Thm* T:Type, P:(T), l:T List. filter(P;l) T List

le_int	Def ij == j<i

	Thm* i,j:. (ij)

lt_int	Def i<j == if i<j true ; false fi

	Thm* i,j:. (i<j)

band	Def pq == if p q else false fi

	Thm* p,q:. (pq)

actof	Def act(k) == outr(k)

	Thm* k:Knd. islocal(k) act(k) Id

outr	Def outr(x) == InjCase(x; y. "???"; z. z)

	Thm* A,B:Type, x:A+B. isl(x) outr(x) B

eq_atom	Def x=yAtom == if x=yAtomtrue; false fi

	Thm* x,y:Atom. x=yAtom

append	Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)

	Thm* T:Type, as,bs:T List. (as @ bs) T List

reduce	Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) Def (recursive)

	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B

bnot	Def b == if b false else true fi

	Thm* b:. b