Selected Objects
| THM | implies_functionality_2 | (P1   P2)  (Q1 Q2) ((P1 Q1) (P2 Q2)) |
| THM | map_map_sq |  as:A List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as) |
| def | ts | ts() == Label+Label+Label+Label+Label |
| THM | ts_sq | SQType(ts()) |
| def | ts_var | ts_var(x) == inl(x) |
| def | case_ts_var | Case ts_var(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z)) |
| def | ts_pvar | ts_pvar(x) == inr(inl(x)) |
| def | case_ts_pvar | Case ts_pvar(x) = > body(x) cont(x1,z)
== ( x1.inr(x2) = >
(x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x1]) |
| def | ts_op | ts_op(x) == inr(inr(inl(x))) |
| def | case_ts_op | Case ts_op(x) = > body(x) cont(x1,z)
== (x1.inr(x2) = >
(x1.inr(x2) = >
(x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x1]) |
| def | ts_fvar | ts_fvar(x) == inr(inr(inr(inl(x)))) |
| def | case_ts_fvar | Case ts_fvar(x) = > body(x) cont(x1,z)
== (x1.inr(x2) = >
(x1.inr(x2) = >
(x1.inr(x2) = >
(x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x1]) |
| def | ts_trace | ts_trace(x) == inr(inr(inr(inr(x)))) |
| def | case_ts_trace | Case ts_trace(x) = > body(x) cont(x1,z)
== (x1.inr(x2) = >
(x1.inr(x2) = >
(x1.inr(x2) = >
(x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x2 / tl(x1)])
cont
(hd(x1)
,z))
([x1]) |
| def | ts_case | ts_case(x)
var(a)= > v(a)
var'(b)= > p(b)
opr(f)= > op(f)
fvar(x)= > f(x)
trace(P)= > t(P)
end_ts_case
== Case(x)
Case ts_var(a) = >
v(a)
Case ts_pvar(b) = >
p(b)
Case ts_op(f) = >
op(f)
Case ts_fvar(x) = >
f(x)
Case ts_trace(P) = >
t(P)
Default = >  |
| def | ts_eq | (a=b)
== ts_case(a)
var(v)= > ts_case(b)
var(v')= > v = v'
var'(x)= > false
opr(x)= > false
fvar(x)= > false
trace(x)= > false
end_ts_case
var'(p)= > ts_case(b)
var(x)= > false
var'(p')= > p = p'
opr(x)= > false
fvar(x)= > false
trace(x)= > false
end_ts_case
opr(op)= > ts_case(b)
var(x)= > false
var'(x)= > false
opr(op')= > op = op'
fvar(x)= > false
trace(x)= > false
end_ts_case
fvar(f)= > ts_case(b)
var(x)= > false
var'(x)= > false
opr(x)= > false
fvar(f')= > f = f'
trace(x)= > false
end_ts_case
trace(P)= > ts_case(b)
var(x)= > false
var'(x)= > false
opr(x)= > false
fvar(x)= > false
trace(P')= > P = P'
end_ts_case
end_ts_case |
| THM | assert_ts_eq | a,b:ts(). (a=b) a = b |
| def | term | Term == Tree(ts()) |
| THM | term_sq2 | SQType(Term) |
| def | tvar | l == tree_leaf(ts_var(l)) |
| def | tfvar | l == tree_leaf(ts_fvar(l)) |
| def | ttrace | trace(l) == tree_leaf(ts_trace(l)) |
| def | tpvar | l' == tree_leaf(ts_pvar(l)) |
| def | topr | f == tree_leaf(ts_op(f)) |
| def | tapp | t1 t2 == tree_node( < t1, t2 > ) |
| def | term_iterate | term_iterate(v;
p;
op;
f;
tr;
a;
t)
== t_iterate(x.ts_case(x)
var(a)= > v(a)
var'(b)= > p(b)
opr(c)= > op(c)
fvar(d)= > f(d)
trace(P)= > tr(P)
end_ts_case ;a;t) |
| def | st | SimpleType == Tree(Label+Unit) |
| THM | st_sq | SQType(SimpleType) |
| def | st_eq | (rec) st_eq(s1;s2)
== Case(s1)
Case a;b = >
Case(s2)
Case a';b' = >
st_eq(a;a') st_eq(b;b')
Default = > false
Case tree_leaf(x) = >
Case(s2)
Case a';b' = >
false
Case tree_leaf(y) = >
InjCase(x; x'. InjCase(y; y'. x' = y'; b. false); a. InjCase(y; y'. false; b. true))
Default = > false
Default = > false |
| def | typ | t == tree_leaf(inl(t)) |
| def | st_top | tTop == tree_leaf(inr()) |
| def | arrow | a  b == tree_node( < a, b > ) |
| THM | assert_st_eq | s1,s2:SimpleType. st_eq(s1;s2) s1 = s2 |
| def | sig_fun | t.fun == 1of(t) |
| def | sig_rel | t.rel == 2of(t) |
| def | dec_lbl | t.lbl == 1of(t) |
| def | dec_typ | t.typ == 2of(t) |
| def | mk_dec | mk_dec(lbl, typ) == < lbl,typ > |
| def | case_mk_dec | Case lbl : typ = > body(lbl;typ)(x,z) == x/x2,x1. body(x2;x1) |
| def | smt_lbl | t.lbl == 1of(t) |
| def | smt_term | t.term == 1of(2of(t)) |
| def | smt_typ | t.typ == 2of(2of(t)) |
| def | mk_smt | mk_smt(lbl, term, typ) == < lbl,term,typ > |
| def | relname_eq | relname_eq(x) == inl(x) |
| def | case_relname_eq | Case eq(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z)) |
| def | relname_other | relname_other(x) == inr(x) |
| def | case_relname_other | Case x = > body(x) cont(x1,z) == (x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1]) |
| def | rel_name | t.name == 1of(t) |
| def | rel_args | t.args == 2of(t) |
| def | mk_rel | mk_rel(name, args) == < name,args > |
| def | eff_kind | t.kind == 1of(t) |
| def | eff_typ | t.typ == 1of(2of(2of(t))) |
| def | eff_smt | t.smt == 2of(2of(2of(t))) |
| def | frame_var | t.var == 1of(t) |
| def | frame_typ | t.typ == 1of(2of(t)) |
| def | frame_acts | t.acts == 2of(2of(t)) |
| def | pre_kind | t.kind == 1of(t) |
| def | pre_rel | t.rel == 2of(2of(t)) |
| def | ioa_ds | t.ds == 1of(t) |
| def | ioa_da | t.da == 1of(2of(t)) |
| def | ioa_init | t.init == 1of(2of(2of(t))) |
| def | ioa_pre | t.pre == 1of(2of(2of(2of(t)))) |
| def | ioa_eff | t.eff == 1of(2of(2of(2of(2of(t))))) |
| def | ioa_frame | t.frame == 2of(2of(2of(2of(2of(t))))) |
| def | mk_ioa | mk_ioa(ds, da, init, pre, eff, frame) == < ds,da,init,pre,eff,frame > |
| def | ioa_all | ioa_all(I; i.A(i))
== mk_ioa( i:I. A(i).ds,
i:I. A(i).da,
i:I. A(i).init,
i:I. A(i).pre,
i:I. A(i).eff,
i:I. A(i).frame) |
| def | tc1 | tc1(r;de)
== Case(r.name)
Case eq(Q) = >
||r.args|| = 2
Case R = >
||de.rel(R)|| = ||r.args||  
Default = > False |
| def | rel_arg_typ | rel_arg_typ(rn;i;de) == Case(rn) Case eq(Q) = > Q Case R = > (de.rel(R))[i] Default = > False |
| def | trace_env | trace_env(d) == (( d) List) (LabelLabel ) |
| def | trace_env_trace | t.trace == 1of(t) |
| def | trace_env_proj | t.proj == 2of(t) |
| def | mk_trace_env | mk_trace_env(trace, proj) == < trace,proj > |
| def | tproj | tre.P == tre.trace | tre.proj(P) |
| def | niltrace | niltrace() == mk_trace_env(nil, P,k. false) |
| def | tappend | tappend(tr;a) == mk_trace_env(tr.trace @ [a], tr.proj) |
| def | term_mng | [[t]] e s a tr
== iterate(statevar x- > s.x
statevar x'- > s.x
funsymbol f- > e.f
freevar x- > a
trace(P)- > tr.P
x(y)- > x(y)
over t) |
| THM | term_mng_nil | u:Term, te:(LabelLabel), e,s,a:Top. [[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace() |
| def | st_lift | st_lift(rho)(x) == InjCase(x; x'. rho(x'); a. Top) |
| def | pred | Fmla == Collection(rel()) |
| def | pred_and | P Q == P + Q |
| def | pred_rel | r == < r > |
| def | apply_alist | apply_alist(as;l;d) == 2of((first p as s.t. 1of(p) = l else < l,d > )) |
| THM | apply_alist_property | as:(LabelT) List, d:T, x:Label. (apply_alist(as;x;d) 2of(unzip(as)))  apply_alist(as;x;d) = d |
| THM | apply_alist_nil | d:Top, l:Label. apply_alist(nil;l;d) ~ d |
| THM | apply_alist_cons | as:(LabelT) List, p:(LabelT), l:Label, d:T.
apply_alist([p / as];l;d) ~ if 1of(p) = l 2of(p) else apply_alist(as;l;d) fi |
| def | term_vars | term_vars(t)
== iterate(statevar v- > [v]
statevar v'- > [v]
funsymbol f- > nil
freevar f- > nil
trace(P)- > nil
x(y)- > x @ y
over t) |
| THM | apply_alist_member | as:(LabelT) List, d:T, x:Label. (x 1of(unzip(as))) ( < x,apply_alist(as;x;d) > as) |
| THM | apply_alist_member2 | as:(LabelT) List, d1,d2:T, x:Label.
(x 1of(unzip(as))) apply_alist(as;x;d1) = apply_alist(as;x;d2) |
| THM | apply_alist_non_member | as:(LabelT) List, d:T, x:Label.  (x 1of(unzip(as))) apply_alist(as;x;d) = d |