Definition: bag
bag(T) == as,bs:T List//permutation(T;as;bs)
Lemma: bag_wf
∀[T:Type]. (bag(T) ∈ Type)
Lemma: bag-valueall-type
∀[T:Type]. valueall-type(bag(T)) supposing valueall-type(T)
Lemma: bag-value-type
∀[T:Type]. value-type(bag(T))
Lemma: list-subtype-bag
∀[A,B:Type]. (A List) ⊆r bag(B) supposing A ⊆r B
Lemma: bag-subtype-fset
∀[A:Type]. (bag(A) ⊆r fset(A))
Lemma: bag-subtype-list
∀T:Type. (bag(T) ⊆r (Top List))
Lemma: bag-equality
∀[A,B:Type]. ∀[f,g:bag(A) ⟶ bag(B)]. ∀[b:bag(A)]. (f[b] = g[b] ∈ bag(B)) supposing ∀[b:A List]. (f[b] = g[b] ∈ bag(B))
Lemma: bag_to_squash_list
∀[T:Type]. ∀[b:bag(T)]. (↓∃L:T List. (b = L ∈ bag(T)))
Lemma: respects-equality-bag
∀[A,B:Type]. respects-equality(bag(A);bag(B)) supposing respects-equality(A;B)
Lemma: respects-equality-list-bag
∀[A,B:Type]. respects-equality(A List;bag(B)) supposing respects-equality(A;B)
Definition: eval_bag
eval_bag(b) == eval_list(b)
Lemma: eval_bag_wf
∀[T:Type]. ∀[b:bag(T)]. (eval_bag(b) ∈ bag(T))
Definition: mk_bag
mk_bag(L) == L
Lemma: mk_bag_wf
∀[T:Type]. ∀[L:T List]. (mk_bag(L) ∈ bag(T))
Definition: empty-bag
{} == []
Lemma: empty-bag_wf
∀[T:Type]. ({} ∈ bag(T))
Lemma: empty-bag-wf-list-test
∀[T:Type]. ({} ∈ T List)
Lemma: equal-empty-bag
∀[T:Type]. ∀x:bag(T). ((x = {} ∈ bag(T)) ⇒ (x ~ {}))
Lemma: bag-void-sq-empty
∀[T:Type]. ∀x:bag(T). x ~ {} supposing ¬T
Definition: single-bag
{x} == [x]
Lemma: single-bag_wf
∀T:Type. ∀x:T. ({x} ∈ bag(T))
Definition: cons-bag
x.b == [x / b]
Lemma: cons-bag_wf
∀[T:Type]. ∀[x:T]. ∀[b:bag(T)]. (x.b ∈ bag(T))
Lemma: cons_bag_empty_lemma
∀x:Top. (x.{} ~ {x})
Lemma: reverse-bag
∀[T:Type]. ∀[b:bag(T)]. (rev(b) = b ∈ bag(T))
Definition: bag-upto
bag-upto(n) == upto(n)
Lemma: bag-upto_wf
∀[n:ℤ]. (bag-upto(n) ∈ bag(ℤ))
Definition: bag-map
bag-map(f;bs) == map(f;bs)
Lemma: bag-map_wf
∀[B,A:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)]. (bag-map(f;bs) ∈ bag(B))
Lemma: bag_map_empty_lemma
∀f:Top. (bag-map(f;{}) ~ {})
Lemma: bag_map_single_lemma
∀x,f:Top. (bag-map(f;{x}) ~ {f x})
Lemma: subtype_rel_bag
∀[B,A:Type]. bag(A) ⊆r bag(B) supposing A ⊆r B
Definition: bag-append
as + bs == as @ bs
Lemma: bag-append_wf
∀[T:Type]. ∀[as,bs:bag(T)]. (as + bs ∈ bag(T))
Lemma: bag-append-comm
∀[T:Type]. ∀[as,bs:bag(T)]. ((as + bs) = (bs + as) ∈ bag(T))
Lemma: bag-append-assoc
∀[as,bs,cs:Top]. ((as + bs) + cs ~ as + bs + cs)
Lemma: bag-append-assoc2
∀[as,bs,cs:Top]. (as + bs + cs ~ (as + bs) + cs)
Lemma: bag-append-assoc-comm
∀[T:Type]. ∀[as,bs,cs:bag(T)]. ((as + bs + cs) = (bs + as + cs) ∈ bag(T))
Lemma: bag-append-comm-assoc
∀[T:Type]. ∀[as,bs,cs:bag(T)]. ((as + bs + cs) = ((as + cs) + bs) ∈ bag(T))
Lemma: bag-append-empty
∀[as:Top List]. (as + {} ~ as)
Lemma: bag-append-cancel
∀[T:Type]. ∀[as,bs,cs:bag(T)]. uiff((as + bs) = (as + cs) ∈ bag(T);bs = cs ∈ bag(T))
Lemma: empty_bag_append_lemma
∀b:Top. ({} + b ~ b)
Lemma: cons_bag_append_lemma
∀b2,b1,x:Top. (x.b1 + b2 ~ x.b1 + b2)
Lemma: bag-empty-append
∀[as:Top]. ({} + as ~ as)
Lemma: bag-append-ident
∀[T:Type]. ∀[as:bag(T)]. (((as + {}) = as ∈ bag(T)) ∧ (({} + as) = as ∈ bag(T)))
Lemma: bag-append-eq-empty
∀[T:Type]. ∀[b1,b2:bag(T)]. uiff((b1 + b2) = {} ∈ bag(T);(b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T)))
Lemma: bag-append-ac
∀[T:Type]. ∀[as,bs,cs:bag(T)]. ((as + bs + cs) = (bs + as + cs) ∈ bag(T))
Lemma: cons-bag-as-append
∀[x,b:Top]. (x.b ~ {x} + b)
Lemma: bag-function
∀[T,A:Type]. ∀[f:(T List) ⟶ bag(A)].
f ∈ bag(T) ⟶ bag(A) supposing ∀as,bs:T List. (f[as @ bs] = (f[as] + f[bs]) ∈ bag(A))
Definition: bag-product
bs × cs == rec-case(bs) of [] => {} | b::as => r.bag-map(λx.<b, x>;cs) + r
Lemma: bag-product_wf
∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. (as × bs ∈ bag(A × B))
Lemma: bag-product-empty
∀[bs:Top]. ({} × bs ~ {})
Lemma: bag-product-single
∀[bs:Top List]. ∀[a:Top]. ({a} × bs ~ bag-map(λx.<a, x>;bs))
Lemma: bag-product-append
∀[as,bs,cs:Top List]. (as + bs × cs ~ as × cs + bs × cs)
Definition: bag-filter
[x∈b|p[x]] == filter(λx.p[x];b)
Lemma: bag-filter_wf
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. ([x∈bs|p[x]] ∈ bag({x:T| ↑p[x]} ))
Lemma: bag-filter-wf3
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. ([x∈bs|p[x]] ∈ bag(T))
Lemma: bag-filter-is-nil
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. ([x∈bs|p[x]] ~ []) supposing ∀x:T. (¬↑p[x])
Lemma: bag-filter-trivial
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. ([x∈bs|p[x]] = bs ∈ bag(T)) supposing ∀x:T. (↑p[x])
Lemma: bag-filter-append
∀[p,as,bs:Top]. ([x∈as + bs|p[x]] ~ [x∈as|p[x]] + [x∈bs|p[x]])
Lemma: bag-filter-filter
∀[p,q,bs:Top]. ([x∈[x∈bs|p[x]]|q[x]] ~ [x∈bs|p[x] ∧b q[x]])
Lemma: bag-filter-filter2
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[q:{x:T| ↑p[x]} ⟶ 𝔹]. ∀[bs:bag(T)].
([x∈[x∈bs|p[x]]|q[x]] = [x∈bs|p[x] ∧b q[x]] ∈ bag({x:T| ↑(p[x] ∧b q[x])} ))
Lemma: bag-filter-singleton
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[v:T]. ([x∈{v}|p[x]] ~ if p[v] then {v} else {} fi )
Lemma: bag-filter-split
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. (([x∈bs|p[x]] + [x∈bs|¬bp[x]]) = bs ∈ bag(T))
Lemma: bag-filter-map
∀[f,p,as:Top]. ([x∈bag-map(f;as)|p[x]] ~ bag-map(f;[x∈as|p[f x]]))
Lemma: bag-filter-map2
∀[T,A:Type]. ∀[f:A ⟶ T]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(A)].
([x∈bag-map(f;as)|p[x]] = bag-map(f;[x∈as|p[f x]]) ∈ bag({x:T| ↑p[x]} ))
Lemma: bag_filter_empty_lemma
∀p:Top. ([x∈{}|p[x]] ~ {})
Lemma: bag_filter_cons_lemma
∀p,v,u:Top. ([x∈u.v|p[x]] ~ if p[u] then u.[x∈v|p[x]] else [x∈v|p[x]] fi )
Lemma: test-bag-filter-empty
∀[p:Top]. ([b∈{}|p[b]] ~ {})
Lemma: bag-split
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(T)]. (as = ([x∈as|p[x]] + [x∈as|¬bp[x]]) ∈ bag(T))
Lemma: bag-map-null
∀f,bs:Top. (null(bag-map(f;bs)) ~ null(bs))
Definition: bag-mapfilter
bag-mapfilter(f;P;bs) == bag-map(f;[x∈bs|P x])
Lemma: bag-mapfilter_wf
∀[T,A:Type]. ∀P:T ⟶ 𝔹. ∀f:{x:T| ↑(P x)} ⟶ A. ∀bs:bag(T). (bag-mapfilter(f;P;bs) ∈ bag(A))
Lemma: bag-mapfilter-null
∀P,f,bs:Top. (null(bag-mapfilter(f;P;bs)) ~ null([x∈bs|P x]))
Lemma: bag-mapfilter-empty
∀P,f:Top. (bag-mapfilter(f;P;{}) ~ {})
Definition: bag-null
bag-null(bs) == null(bs)
Lemma: bag-null_wf
∀T:Type. ∀bs:bag(T). (bag-null(bs) ∈ 𝔹)
Lemma: bag_null_empty_lemma
bag-null({}) ~ tt
Lemma: bag_null_cons_lemma
∀v,u:Top. (bag-null(u.v) ~ ff)
Lemma: bag-null-append
∀[T:Type]. ∀[as,bs:bag(T)]. bag-null(as + bs) = bag-null(as) ∧b bag-null(bs)
Lemma: assert-bag-null
∀[T:Type]. ∀[bs:bag(T)]. uiff(↑bag-null(bs);bs = {} ∈ bag(T))
Lemma: null-bag-mapfilter
∀P,f,bs:Top. (bag-null(bag-mapfilter(f;P;bs)) ~ bag-null([x∈bs|P x]))
Lemma: bag-map-equal
∀[T,A:Type].
∀f,g:T ⟶ A. ∀P:T ⟶ 𝔹.
((∀x:T. ((¬↑(P x)) ⇒ ((f x) = (g x) ∈ A)))
⇒ (∀as:bag(T). ((↑null([x∈as|P x])) ⇒ (bag-map(f;as) = bag-map(g;as) ∈ bag(A)))))
Lemma: null-bag-filter-map
∀[T,A:Type]. ∀[f:A ⟶ T]. ∀[p:T ⟶ 𝔹]. ∀[as:bag(A)]. null([x∈bag-map(f;as)|p[x]]) = null([x∈as|p[f x]])
Definition: bag-size
#(bs) == ||bs||
Lemma: bag-size_wf
∀[C:Type]. ∀[bs:bag(C)]. (#(bs) ∈ ℕ)
Lemma: bag_size_single_lemma
∀x:Top. (#({x}) ~ 1)
Lemma: bag_size_cons_lemma
∀b,x:Top. (#(x.b) ~ #(b) + 1)
Lemma: bag-size-map
∀[bs,f:Top]. (#(bag-map(f;bs)) ~ #(bs))
Lemma: bag-size-append
∀[as,bs:Top]. (#(as + bs) ~ #(as) + #(bs))
Lemma: bag-size-cons
∀[b:bag(Top)]. ∀[x:Top]. (#(x.b) ~ 1 + #(b))
Lemma: bag-size-zero
∀[C:Type]. ∀[bs:bag(C)]. bs ~ {} supposing #(bs) ≤ 0
Lemma: bag_size_empty_lemma
#({}) ~ 0
Lemma: bag-size-is-zero
∀[C:Type]. ∀[bs:bag(C)]. bs ~ {} supposing #(bs) = 0 ∈ ℤ
Lemma: bag-size-bound
∀[T:Type]. ∀[as,bs:bag(T)]. ∀[n:ℕ]. #(as + bs) - n < #(bs) supposing #(as) < n
Lemma: null-bag
∀[T:Type]. ∀[x:bag(T)]. uiff(↑null(x);x = {} ∈ bag(T))
Lemma: assert-bag-null-sq
∀bs:bag(Top). ((↑bag-null(bs)) ⇒ (bs ~ {}))
Lemma: smallbag-subtype-list
∀T:Type. ({b:bag(T)| #(b) < 2} ⊆r {b:T List| ||b|| < 2} )
Lemma: bag-cases
∀[T:Type]. ∀bs:bag(T). ((bs = {} ∈ bag(T)) ∨ (↓∃x:T. ∃bs':bag(T). (bs = ({x} + bs') ∈ bag(T))))
Lemma: null-bag-size
∀[T:Type]. ∀[x:bag(T)]. (bag-null(x) ~ (#(x) =z 0))
Lemma: bag-map-append
∀[as:bag(Top)]. ∀[bs,f:Top]. (bag-map(f;as + bs) ~ bag-map(f;as) + bag-map(f;bs))
Lemma: bag-map-cons
∀[b,x,f:Top]. (bag-map(f;x.b) ~ f x.bag-map(f;b))
Lemma: bag-map-single
∀[x,f:Top]. (bag-map(f;{x}) ~ {f x})
Lemma: bag-map-map
∀[as,f,g:Top]. (bag-map(f;bag-map(g;as)) ~ bag-map(f o g;as))
Lemma: bag-map-filter
∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].
∀[L:bag(T)]. (bag-map(f;[x∈L|P[x]]) = [x∈bag-map(f;L)|Q[x]] ∈ bag(A)) supposing ∀x:T. Q[f x] = P[x]
Lemma: bag-map-trivial
∀[A:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ A]. bag-map(f;as) = as ∈ bag(A) supposing ∀x:A. ((f x) = x ∈ A)
Lemma: bag-mapfilter-append
∀[T:Type]. ∀[a:bag(T)]. ∀[b:bag(Top)]. ∀[f:Top]. ∀[P:T ⟶ 𝔹].
(bag-mapfilter(f;P;a + b) ~ bag-mapfilter(f;P;a) + bag-mapfilter(f;P;b))
Lemma: bag-mapfilter-map
∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:B ⟶ 𝔹]. ∀[f:{x:B| ↑P[x]} ⟶ C]. ∀[g:A ⟶ B].
(bag-mapfilter(f;P;bag-map(g;b)) = bag-mapfilter(f o g;P o g;b) ∈ bag(C))
Lemma: bag-map-mapfilter
∀[b,P,f,g:Top]. (bag-map(g;bag-mapfilter(f;P;b)) ~ bag-mapfilter(g o f;P;b))
Lemma: bag-mapfilter-mapfilter
∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]} ⟶ B]. ∀[Q:B ⟶ 𝔹]. ∀[g:{x:B| ↑Q[x]} ⟶ C].
(bag-mapfilter(g;Q;bag-mapfilter(f;P;b)) = bag-mapfilter(g o f;λx.(P[x] ∧b Q[f[x]]);b) ∈ bag(C))
Definition: bagp
T Bag+ == {b:bag(T)| 0 < #(b)}
Lemma: bagp_wf
∀[T:Type]. (T Bag+ ∈ Type)
Lemma: bagp_properties
∀[T:Type]. ∀[b:T Bag+]. (#(b) ≥ 1 )
Definition: bag-val
bag-val(zero;+) == λb.accumulate (with value v and list item x): v + xover list: bwith starting value: zero)
Lemma: bag-val_wf
∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T]. (Comm(T;+) ⇒ Assoc(T;+) ⇒ Ident(T;+;zero) ⇒ (bag-val(zero;+) ∈ bag(T) ⟶ T))
Lemma: bag-val-empty
∀[+,zero:Top]. (bag-val(zero;+) {} ~ zero)
Lemma: bag-val-append
∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].
(Comm(T;+)
⇒ Assoc(T;+)
⇒ Ident(T;+;zero)
⇒ (∀[as,bs:bag(T)]. ((bag-val(zero;+) (as + bs)) = ((bag-val(zero;+) as) + (bag-val(zero;+) bs)) ∈ T)))
Definition: bag-union
bag-union(bbs) == concat(bbs)
Lemma: bag-union_wf
∀[T:Type]. ∀[bbs:bag(bag(T))]. (bag-union(bbs) ∈ bag(T))
Lemma: bag_union_empty_lemma
bag-union({}) ~ {}
Lemma: bag_union_cons_lemma
∀v,u:Top. (bag-union(u.v) ~ u + bag-union(v))
Lemma: bag-union-bagp
∀[T:Type]. ∀[bbs:bag(bag(T))]. (0 < #([b∈bbs|0 <z #(b)]) ⇒ (bag-union(bbs) ∈ T Bag+))
Lemma: bag-induction
∀[T:Type]. ∀[P:bag(T) ⟶ ℙ]. ((∀x:T. P[[x]]) ⇒ (∀bs:bag({b:bag(T)| P[b]} ). P[bag-union(bs)]) ⇒ (∀b:bag(T). P[b]))
Lemma: bag-filter-union
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bbs:bag(bag(T))].
([x∈bag-union(bbs)|p[x]] = bag-union(bag-map(λb.[x∈b|p[x]];bbs)) ∈ bag({x:T| ↑p[x]} ))
Lemma: bag-filter-union2
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bbs:bag(bag(T))]. ([x∈bag-union(bbs)|p[x]] = bag-union(bag-map(λb.[x∈b|p[x]];bbs)) ∈ bag(T))
Lemma: bag-map-union
∀[T,S:Type]. ∀[f:T ⟶ bag(S)]. ∀[bbs:bag(bag(T))].
(bag-map(f;bag-union(bbs)) = bag-union(bag-map(λb.bag-map(f;b);bbs)) ∈ bag(bag(S)))
Lemma: bag-append-union
∀[T:Type]. ∀as,bs:bag(bag(T)). (bag-union(as + bs) = (bag-union(as) + bag-union(bs)) ∈ bag(T))
Lemma: bag-union-single
∀x:Top List. (bag-union({x}) ~ x)
Lemma: bag-append-is-single
∀[T:Type]. ∀[x:T].
∀as,bs:bag(T).
↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T))) ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T)))
supposing (as + bs) = {x} ∈ bag(T)
Lemma: bag-append-is-single-iff
∀[T:Type]. ∀[x:T].
∀as,bs:bag(T).
uiff((as + bs) = {x} ∈ bag(T);↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))
∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))))
Lemma: bag-append-is-single-iff2
∀[T:Type]. ∀[x:T].
∀as,bs:bag(T).
uiff({x} = (as + bs) ∈ bag(T);↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))
∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))))
Lemma: bag-append-is-empty
∀[T:Type]. ∀as,bs:bag(T). uiff((as + bs) = {} ∈ bag(T);(as = {} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))
Lemma: bag-union-is-single-if
∀[T:Type]. ∀[x:T]. ∀bbs:bag(bag(T)). bag-union(bbs) = {x} ∈ bag(T) supposing bbs = {{x}} ∈ bag(bag(T))
Lemma: bag-union-is-single
∀[T:Type]. ∀[x:T].
∀bbs:bag(bag(T))
uiff(bag-union(bbs) = {x} ∈ bag(T);↓∃bbs':bag(bag(T))
((bbs = {x}.bbs' ∈ bag(bag(T))) ∧ (bag-union(bbs') = {} ∈ bag(T))))
Lemma: bag-union-cons
∀[b,a:Top]. (bag-union(a.b) ~ a + bag-union(b))
Lemma: bag-union-append
∀[A:Type]. ∀[b1,b2:bag(bag(A))]. (bag-union(b1 + b2) = (bag-union(b1) + bag-union(b2)) ∈ bag(A))
Lemma: non-empty-bag-union-of-list
∀[T:Type]. ∀L:bag(T) List. (0 < #(bag-union(L)) ⇐⇒ (∃b∈L. 0 < #(b)))
Lemma: non-empty-bag-mapfilter-union-of-list
∀[T:Type]
∀P:T ⟶ 𝔹. ∀f:T ⟶ Top. ∀L:bag(T) List. (0 < #(bag-mapfilter(f;λx.P[x];bag-union(L))) ⇐⇒ (∃b∈L. 0 < #([x∈b|P[x]])))
Definition: bag-combine
⋃x∈bs.f[x] == bag-union(bag-map(λx.f[x];bs))
Lemma: bag-combine_wf
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)]. (⋃x∈bs.f[x] ∈ bag(B))
Lemma: bag_combine_empty_lemma
∀f:Top. (⋃x∈{}.f[x] ~ {})
Lemma: strict4-bag-combine
strict4(λx,y,z,w. ⋃b∈x.y[b])
Lemma: bag-combine-assoc
∀[f,g:Top]. ∀[bs:bag(Top)]. (⋃y∈⋃x∈bs.f[x].g[y] ~ ⋃x∈bs.⋃y∈f[x].g[y])
Lemma: bag-combine-unit-left
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[a:A]. (⋃x∈[a].f[x] ~ f[a])
Lemma: bag-combine-unit-left-top
∀[f,a:Top]. (⋃x∈[a].f[x] ~ f[a] + {})
Lemma: bag-combine-single-left
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[a:A]. (⋃x∈{a}.f[x] ~ f[a])
Lemma: bag-combine-empty-left
∀[f:Top]. (⋃x∈{}.f[x] ~ {})
Lemma: bag-combine-empty-right
∀[T:Type]. ∀[bs:bag(T)]. (⋃x∈bs.{} ~ {})
Lemma: bag-combine-unit-right
∀[A:Type]. ∀[bs:bag(A)]. (⋃x∈bs.[x] ~ bs)
Lemma: bag-combine-single-right
∀[A:Type]. ∀[bs:bag(A)]. (⋃x∈bs.{x} ~ bs)
Lemma: bag-combine-single-right-as-map
∀[bs,f:Top]. (⋃x∈bs.{f[x]} ~ bag-map(λx.f[x];bs))
Lemma: bag-combine-append-left
∀[A,B:Type]. ∀[ba,bb:bag(A)]. ∀[f:A ⟶ bag(B)]. (⋃x∈ba + bb.f[x] = (⋃x∈ba.f[x] + ⋃x∈bb.f[x]) ∈ bag(B))
Lemma: bag-combine-append-right
∀[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)]. (⋃x∈ba.F[x] + G[x] = (⋃x∈ba.F[x] + ⋃x∈ba.G[x]) ∈ bag(B))
Lemma: bag-combine-cons-left
∀[b,a,f:Top]. (⋃x∈a.b.f[x] ~ f[a] + ⋃x∈b.f[x])
Lemma: bag-combine-com
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[ba:bag(A)]. ∀[bb:bag(B)]. (⋃a∈ba.⋃b∈bb.f[a;b] = ⋃b∈bb.⋃a∈ba.f[a;b] ∈ bag(C))
Lemma: bag-combine-filter
∀[A,B:Type]. ∀[p:A ⟶ 𝔹]. ∀[f:{a:A| ↑p[a]} ⟶ bag(B)]. ∀[ba:bag(A)].
(⋃a∈[a∈ba|p[a]].f[a] = ⋃a∈ba.if p[a] then f[a] else {} fi ∈ bag(B))
Lemma: bag-map-combine
∀[A,B,C:Type]. ∀[g:A ⟶ bag(B)]. ∀[f:B ⟶ C]. ∀[bs:bag(A)]. (bag-map(f;⋃x∈bs.g[x]) = ⋃x∈bs.bag-map(f;g[x]) ∈ bag(C))
Lemma: bag-combine-map
∀[A,B,C:Type]. ∀[g:B ⟶ bag(C)]. ∀[f:A ⟶ B]. ∀[bs:bag(A)]. (⋃x∈bag-map(f;bs).g[x] = ⋃x∈bs.g[f x] ∈ bag(C))
Lemma: bag-combine-is-single-if
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[bs:bag(A)]. ∀[x:B].
⋃x∈bs.f[x] = {x} ∈ bag(B) supposing ↓∃y:A. ((bs = {y} ∈ bag(A)) ∧ (f[y] = {x} ∈ bag(B)))
Lemma: bag-combine-combine
∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)]. (⋃x∈⋃y∈b.f[y].g[x] = ⋃x∈b.⋃y∈f[x].g[y] ∈ bag(C))
Lemma: bag-map-union2
∀[A,B:Type]. ∀[g:A ⟶ B]. ∀[x:bag(bag(A))]. (bag-map(g;bag-union(x)) = bag-union(bag-map(λz.bag-map(g;z);x)) ∈ bag(B))
Lemma: bag-union-as-combine
∀[A:Type]. ∀[x:bag(bag(A))]. (bag-union(x) = ⋃b∈x.b ∈ bag(A))
Lemma: bag-union-union-as-combine
∀[X:Type]. ∀[x:bag(bag(bag(X)))]. (bag-union(bag-union(x)) = ⋃z∈x.bag-union(z) ∈ bag(X))
Definition: bag-monad
BagMonad == mk_monad(λT.bag(T);λx.{x};λba,f. ⋃x∈ba.f x)
Lemma: bag-monad_wf
BagMonad ∈ Monad
Lemma: bag-combine-mapfilter
∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]} ⟶ B]. ∀[g:B ⟶ bag(C)].
(⋃x∈bag-mapfilter(f;P;b).g[x] = ⋃x∈b.if P[x] then g[f[x]] else {} fi ∈ bag(C))
Lemma: bag-combine-is-map
∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ B]. (⋃x∈b.{f[x]} = bag-map(f;b) ∈ bag(B))
Definition: bag-sum
bag-sum(ba;x.f[x]) == accumulate (with value s and list item x): f[x] + sover list: bawith starting value: 0)
Lemma: bag-sum_wf
∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)]. (bag-sum(ba;x.f[x]) ∈ ℤ)
Lemma: bag-sum_wf_nat
∀[A:Type]. ∀[f:A ⟶ ℕ]. ∀[ba:bag(A)]. (bag-sum(ba;x.f[x]) ∈ ℕ)
Lemma: bag-sum-nonneg
∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)]. 0 ≤ bag-sum(ba;x.f[x]) supposing ∀x:A. (0 ≤ f[x])
Lemma: bag-combine-size
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[ba:bag(A)]. (#(⋃a∈ba.f[a]) = bag-sum(ba;a.#(f[a])) ∈ ℕ)
Lemma: bag-combine-size-bound
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[L:A List]. ∀[a:A]. #(f[a]) ≤ #(⋃a∈L.f[a]) supposing (a ∈ L)
Definition: bag-reduce
bag-reduce(x,y.f[x; y];zero;bs) == reduce(λx,y. f[x; y];zero;bs)
Lemma: bag-reduce_wf
∀[T:Type]. ∀[zero:T]. ∀[f:T ⟶ T ⟶ T].
(∀[bs:bag(T)]. (bag-reduce(x,y.f[x;y];zero;bs) ∈ T)) supposing (Assoc(T;λx,y. f[x;y]) and Comm(T;λx,y. f[x;y]))
Definition: bag-accum
bag-accum(v,x.f[v; x];init;bs) ==
accumulate (with value v and list item x):
f[v; x]
over list:
bs
with starting value:
init)
Lemma: bag-accum_wf
∀[T,S:Type]. ∀[init:S]. ∀[f:S ⟶ T ⟶ S]. ∀[bs:bag(T)].
bag-accum(v,x.f[v;x];init;bs) ∈ S supposing ∀v:S. ∀x,y:T. (f[f[v;y];x] = f[f[v;x];y] ∈ S)
Lemma: bag-accum-map
∀[L,y,f,g:Top]. (bag-accum(x,a.f[x;a];y;bag-map(g;L)) ~ bag-accum(x,a.f[x;g a];y;L))
Lemma: bag-accum-single
∀[init,f,x:Top]. (bag-accum(v,x.f[v;x];init;{x}) ~ f[init;x])
Lemma: bag-map-as-accum
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[bs:bag(A)]. (bag-map(f;bs) = bag-accum(b,x.f[x].b;{};bs) ∈ bag(B))
Lemma: bag-combine-as-accum
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[bs:bag(A)]. (⋃b∈bs.f[b] = bag-accum(c,b.f[b] + c;{};bs) ∈ bag(B))
Lemma: sum-as-bag-accum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. (Σ(f[x] | x < n) ~ bag-accum(x,y.x + y;0;[x∈bag-map(λx.f[x];upto(n))|¬b(x =z 0)]))
Lemma: bag-filter-as-accum
∀[A:Type]. ∀[p:A ⟶ 𝔹]. ∀[bs:bag(A)].
([x∈bs|p[x]] = bag-accum(b,x.if p[x] then x.b else b fi ;{};bs) ∈ bag({x:A| ↑p[x]} ))
Definition: bag-maximal?
bag-maximal?(bg;x;R) == bag-accum(b,y.b ∧b R[x;y];tt;bg)
Lemma: bag-maximal?_wf
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T]. (bag-maximal?(b;x;R) ∈ 𝔹)
Lemma: bag-maximal?-single
∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[v,x:T]. uiff(↑bag-maximal?({v};x;R);↑(R x v))
Lemma: bag-maximal?-append
∀[T:Type]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[b1,b2:bag(T)]. ∀[x:T].
uiff(↑bag-maximal?(b1 + b2;x;R);(↑bag-maximal?(b1;x;R)) ∧ (↑bag-maximal?(b2;x;R)))
Lemma: bag-maximal?-cons
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,v:T]. uiff(↑bag-maximal?(v.b;x;R);(↑bag-maximal?(b;x;R)) ∧ (↑(R x v)))
Definition: bag-maximals
bag-maximals(bg;R) == [x∈bg|bag-maximal?(bg;x;R)]
Lemma: bag-maximals_wf
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. (bag-maximals(b;R) ∈ bag(T))
Definition: imax-bag
imax-bag(bs) == imax-list(bs)
Lemma: imax-bag_wf
∀[bs:bag(ℤ)]. imax-bag(bs) ∈ ℤ supposing 0 < #(bs)
Definition: bag-summation
Σ(x∈b). f[x] == bag-accum(c,x.add f[x] c;zero;b)
Lemma: bag-summation_wf
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[f:T ⟶ R]. ∀[b:bag(T)].
Σ(x∈b). f[x] ∈ R supposing Assoc(R;add) ∧ Comm(R;add)
Lemma: bag-summation-empty
∀[add,zero,f:Top]. (Σ(x∈{}). f[x] ~ zero)
Lemma: bag-summation-append
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T:Type]. ∀[f:T ⟶ R]. ∀[b,c:bag(T)]. (Σ(x∈b + c). f[x] = (Σ(x∈b). f[x] add Σ(x∈c). f[x]) ∈ R)
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-single-sq
∀[add,zero,f,a:Top]. (Σ(x∈{a}). f[x] ~ add f[a] zero)
Lemma: bag-summation-single
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T:Type]. ∀[f:T ⟶ R]. ∀[a:T]. (Σ(x∈{a}). f[x] = f[a] ∈ R) supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-cons
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T:Type]. ∀[f:T ⟶ R]. ∀[b:bag(T)]. ∀[a:T]. (Σ(x∈a.b). f[x] = (f[a] add Σ(x∈b). f[x]) ∈ R)
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-linear
∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].
∀a:R. (Σ(x∈b). a mul (f[x] add g[x]) = (a mul (Σ(x∈b). f[x] add Σ(x∈b). g[x])) ∈ R)
supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
Lemma: bag-summation-add
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[f,g:T ⟶ R]. ∀[b:bag(T)].
Σ(x∈b). f[x] add g[x] = (Σ(x∈b). f[x] add Σ(x∈b). g[x]) ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-linear-right
∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].
∀a:R. (Σ(x∈b). (f[x] add g[x]) mul a = ((Σ(x∈b). f[x] add Σ(x∈b). g[x]) mul a) ∈ R)
supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
Lemma: bag-summation-zero
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)].
Σ(x∈b). zero = zero ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-linear1
∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
∀a:R. (Σ(x∈b). a mul f[x] = (a mul Σ(x∈b). f[x]) ∈ R)
supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
Lemma: bag-summation-constant
∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀a:|r|. (Σ(x∈b). a = (#(b) ⋅r a) ∈ |r|)
Lemma: bag-summation-minus
∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|]. (Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|)
Lemma: bag-summation-linear1-right
∀[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
∀a:R. (Σ(x∈b). f[x] mul a = (Σ(x∈b). f[x] mul a) ∈ R)
supposing (∃minus:R ⟶ R. IsGroup(R;add;zero;minus)) ∧ Comm(R;add) ∧ BiLinear(R;add;mul)
Lemma: bag-summation-ring-linear1
∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|].
∀a:|r|. ((Σ(x∈b). f[x] * a = (Σ(x∈b). f[x] * a) ∈ |r|) ∧ (Σ(x∈b). a * f[x] = (a * Σ(x∈b). f[x]) ∈ |r|))
Lemma: bag-summation-map
∀[add,zero:Top]. ∀[b:Top List]. ∀[f,g:Top]. (Σ(x∈bag-map(g;b)). f[x] ~ Σ(x∈b). f[g x])
Lemma: bag-summation-reindex
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[h:A ⟶ T]. ∀[f:T ⟶ R].
∀[b:bag(T)]. (Σ(x∈b). f[x] = Σ(x∈bag-map(g;b)). f[h x] ∈ R) supposing ∀x:T. (x = (h (g x)) ∈ T)
supposing Comm(R;add) ∧ Assoc(R;add)
Lemma: bag-summation-split
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹]. ∀[f:T ⟶ R].
Σ(x∈b). f[x] = (Σ(x∈[x∈b|p[x]]). f[x] add Σ(x∈[x∈b|¬bp[x]]). f[x]) ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-product
∀[r:Rng]. ∀[A,B:Type]. ∀[f:A ⟶ |r|]. ∀[c:bag(B)]. ∀[g:B ⟶ |r|]. ∀[b:bag(A)].
((Σ(x∈b). f[x] * Σ(y∈c). g[y]) = Σ(p∈b × c). f[fst(p)] * g[snd(p)] ∈ |r|)
Lemma: bag-summation-hom
∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].
∀[A:Type]. ∀[g:A ⟶ |r|]. ∀[b:bag(A)]. (Σ(x∈b). f[g[x]] = f[Σ(x∈b). g[x]] ∈ |s|) supposing rng_hom_p(r;s;f)
Lemma: bag-double-summation1
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ bag(A[x])]. ∀[h:x:T ⟶ A[x] ⟶ R]. ∀[b:bag(T)].
(Σ(x∈b). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ R)
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-double-summation
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T,A,B:Type]. ∀[f:T ⟶ bag(A)]. ∀[g:T ⟶ B]. ∀[h:B ⟶ A ⟶ R]. ∀[b:bag(T)].
(Σ(x∈b). Σ(y∈f[x]). h[g[x];y] = Σ(p∈⋃x∈b.bag-map(λy.<g[x], y>;f[x])). h[fst(p);snd(p)] ∈ R)
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-double-summation2
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T,A:Type]. ∀[f:T ⟶ bag(A)]. ∀[h:T ⟶ A ⟶ R]. ∀[b:bag(T)].
(Σ(x∈b). Σ(y∈f[x]). h[x;y] = Σ(p∈⋃x∈b.bag-map(λy.<x, y>;f[x])). h[fst(p);snd(p)] ∈ R)
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Definition: bag-product
Πx ∈ b. f[x] == Σ(x∈b). f[x]
Lemma: bag-product_wf
∀[T,R:Type]. ∀[mul:R ⟶ R ⟶ R]. ∀[one:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
Πx ∈ b. f[x] ∈ R supposing Assoc(R;mul) ∧ Comm(R;mul)
Definition: int-bag-product
Π(b) == Πx ∈ b. x
Lemma: int-bag-product_wf
∀[b:bag(ℤ)]. (Π(b) ∈ ℤ)
Lemma: int-bag-product-append
∀[b1,b2:bag(ℤ)]. (Π(b1 + b2) ~ Π(b1) * Π(b2))
Definition: int-bag-sum
Σ(b) == Σ(x∈b). x
Lemma: int-bag-sum_wf
∀[b:bag(ℤ)]. (Σ(b) ∈ ℤ)
Lemma: int-bag-sum-append
∀[b1,b2:bag(ℤ)]. (Σ(b1 + b2) ~ Σ(b1) + Σ(b2))
Definition: bag-no-repeats
bag-no-repeats(T;bs) == ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ no_repeats(T;L))
Lemma: bag-no-repeats_wf
∀[T:Type]. ∀[bs:bag(T)]. (bag-no-repeats(T;bs) ∈ ℙ)
Lemma: sq_stable__bag-no-repeats
∀[T:Type]. ∀[bs:bag(T)]. SqStable(bag-no-repeats(T;bs))
Lemma: bag-single-no-repeats
∀[T:Type]. ∀[x:T]. bag-no-repeats(T;{x})
Lemma: empty-bag-no-repeats
∀[T:Type]. bag-no-repeats(T;{})
Lemma: bag-map-no-repeats
∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[bs:bag(T1)].
uiff(bag-no-repeats(T2;bag-map(f;bs));bag-no-repeats(T1;bs)) supposing Inj(T1;T2;f)
Lemma: bag-filter-no-repeats
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. bag-no-repeats(T;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)
Definition: bag-rep
bag-rep(n;x) == primrec(n;{};λi,r. x.r)
Lemma: bag-rep_wf
∀[T:Type]. ∀[n:ℕ]. ∀[x:T]. (bag-rep(n;x) ∈ T List)
Lemma: bag-size-rep
∀[n:ℕ]. ∀[x:Top]. (#(bag-rep(n;x)) ~ n)
Lemma: bag-null-rep
∀[n:ℕ]. ∀[x:Top]. (bag-null(bag-rep(n;x)) ~ (n =z 0))
Lemma: bag-rep-add
∀x:Top. ∀n,m:ℕ. (bag-rep(n + m;x) ~ bag-rep(n;x) + bag-rep(m;x))
Lemma: empty-bag-union
∀T:Type. ∀bs:bag(bag(T)). ((bag-union(bs) = {} ∈ bag(T)) ⇒ (bs ~ bag-rep(#(bs);{})))
Definition: bag-all
bag-all(x.p[x];bs) == bag-reduce(x,y.x ∧b y;tt;bag-map(λx.p[x];bs))
Lemma: bag-all_wf
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. (bag-all(x.p[x];bs) ∈ 𝔹)
Definition: bag_all
bag_all(b;f) == bag-accum(a,x.a ∧b f[x];tt;b)
Lemma: bag_all_wf
∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[b:bag(T)]. (bag_all(b;f) ∈ 𝔹)
Lemma: bag_all-empty
∀[f:Top]. (bag_all({};f) ~ tt)
Lemma: bag_all-cons
∀[T:Type]. ∀[x:T]. ∀[b:bag(T)]. ∀[f:T ⟶ 𝔹]. (bag_all(x.b;f) ~ (f x) ∧b bag_all(b;f))
Lemma: bag_all-map
∀[b,f,g:Top]. (bag_all(bag-map(g;b);f) ~ bag_all(b;f o g))
Definition: bag-only
only(bs) == hd(bs)
Lemma: bag-only_wf
∀[T:Type]. ∀[bs:bag(T)]. only(bs) ∈ T supposing #(bs) = 1 ∈ ℤ
Lemma: bag_only_single_lemma
∀x:Top. (only({x}) ~ x)
Lemma: bag-size-one
∀[T:Type]. ∀[bs:bag(T)]. bs ~ {only(bs)} supposing #(bs) = 1 ∈ ℤ
Lemma: subtype-bag-only
∀[T:Type]. ∀[bs:bag(T)]. bs ∈ bag({x:T| x = only(bs) ∈ T} ) supposing #(bs) = 1 ∈ ℤ
Lemma: subtype-bag-empty
∀[T:Type]. ∀[bs:bag(T)]. bs ∈ bag(Void) supposing #(bs) = 0 ∈ ℤ
Lemma: only-bag-map
∀[f:Top]. ∀[T:Type]. ∀[b:bag(T)]. only(bag-map(f;b)) ~ f only(b) supposing #(b) = 1 ∈ ℤ
Lemma: equal-bag-size-le1
∀[T:Type]. ∀[as,bs:bag(T)].
uiff(as = bs ∈ bag(T);(as = {} ∈ bag(T) ⇐⇒ bs = {} ∈ bag(T))
∧ ((#(as) = 1 ∈ ℤ) ⇒ (#(bs) = 1 ∈ ℤ) ⇒ (only(as) = only(bs) ∈ T)))
supposing (#(as) ≤ 1) ∧ (#(bs) ≤ 1)
Definition: bag-merge
bag-merge(as;bs) == bag-map(λx.(inl x);as) + bag-map(λx.(inr x );bs)
Lemma: bag-merge_wf
∀A,B:Type. ∀as:bag(A). ∀bs:bag(B). (bag-merge(as;bs) ∈ bag(A + B))
Definition: bag-separate
bag-separate(bs) == <bag-mapfilter(λt.outl(t);λt.isl(t);bs), bag-mapfilter(λt.outr(t);λt.(¬bisl(t));bs)>
Lemma: bag-separate_wf
∀[A,B:Type]. ∀[bs:bag(A + B)]. (bag-separate(bs) ∈ bag(A) × bag(B))
Lemma: bag-separate-merge
∀[as,bs:Top List]. (bag-separate(bag-merge(as;bs)) ~ <as, bs>)
Definition: sub-bag
sub-bag(T;as;bs) == ∃cs:bag(T). (bs = (as + cs) ∈ bag(T))
Lemma: sub-bag_wf
∀[T:Type]. ∀[as,bs:bag(T)]. (sub-bag(T;as;bs) ∈ ℙ)
Lemma: sub-bag_weakening
∀[T:Type]. ∀[as,bs:bag(T)]. ((as = bs ∈ bag(T)) ⇒ sub-bag(T;as;bs))
Lemma: sub-bag_transitivity
∀[T:Type]. ∀[as,bs,cs:bag(T)]. (sub-bag(T;as;bs) ⇒ sub-bag(T;bs;cs) ⇒ sub-bag(T;as;cs))
Lemma: sub-bag_antisymmetry
∀[T:Type]. ∀[as,bs:bag(T)]. (as = bs ∈ bag(T)) supposing (sub-bag(T;as;bs) and sub-bag(T;bs;as))
Lemma: sub-bag-rep
∀[T:Type]. ∀x:T. ∀n,m:ℕ. uiff(sub-bag(T;bag-rep(n;x);bag-rep(m;x));n ≤ m)
Lemma: sub-bag-combine
∀[T,U:Type]. ∀f:T ⟶ bag(U). ∀b1,b2:bag(T). (sub-bag(T;b1;b2) ⇒ sub-bag(U;⋃x∈b1.f[x];⋃x∈b2.f[x]))
Lemma: sub-bag-append-trivial1
∀[T:Type]. ∀[b,x:bag(T)]. ∀y:bag(T). (sub-bag(T;b;x) ⇒ sub-bag(T;b;x + y))
Lemma: sub-bag-append-trivial2
∀[T:Type]. ∀[b,y:bag(T)]. ∀x:bag(T). (sub-bag(T;b;y) ⇒ sub-bag(T;b;x + y))
Lemma: sub-bag-append-left
∀[T:Type]. ∀b1,b2,b:bag(T). (sub-bag(T;b1 + b2;b) ⇒ sub-bag(T;b1;b))
Lemma: sub-bag-append-left2
∀[T:Type]. ∀b1,b2,b:bag(T). (sub-bag(T;b1 + b2;b) ⇒ sub-bag(T;b2;b))
Lemma: sub-bag-cancel-right
∀[T:Type]. ∀b1,b2,b:bag(T). (sub-bag(T;b1 + b;b2 + b) ⇐⇒ sub-bag(T;b1;b2))
Lemma: sub-bag-equal
∀[T:Type]. ∀[b1,b2:bag(T)]. (b1 = b2 ∈ bag(T)) supposing (sub-bag(T;b1;b2) and sub-bag(T;b2;b1))
Lemma: empty-sub-bag
∀T:Type. ∀b:bag(T). sub-bag(T;{};b)
Lemma: sub-bag-empty
∀[T:Type]. ∀[b:bag(T)]. uiff(sub-bag(T;b;{});b = {} ∈ bag(T))
Definition: maximal-sub-bag
maximal-sub-bag(T;m;b;s.P[s]) == (∀s:bag(T). (sub-bag(T;s;b) ⇒ P[s] ⇒ sub-bag(T;s;m))) ∧ P[m]
Lemma: maximal-sub-bag_wf
∀[T:Type]. ∀[b,m:bag(T)]. ∀[P:bag(T) ⟶ ℙ]. (maximal-sub-bag(T;m;b;s.P[s]) ∈ ℙ)
Definition: bag-member
x ↓∈ bs == ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ (x ∈ L))
Lemma: bag-member_wf
∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. (x ↓∈ bs ∈ ℙ)
Lemma: squash-bag-member
∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. uiff(↓x ↓∈ bs;x ↓∈ bs)
Lemma: sq_stable__bag-member
∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. SqStable(x ↓∈ bs)
Lemma: bag-member-subtype
∀[A,B:Type]. ∀b:bag(A). ∀x:A. (x ↓∈ b ⇒ x ↓∈ b) supposing A ⊆r B
Lemma: bag-member-strong-subtype
∀[A,B:Type]. ∀b:bag(A). ∀x:B. (x ↓∈ b ⇒ (x ∈ A)) supposing strong-subtype(A;B)
Lemma: bag-member-empty
∀[T:Type]. ∀[x:T]. False supposing x ↓∈ {}
Lemma: bag-member-empty-iff
∀[T:Type]. ∀[x:T]. uiff(x ↓∈ {};False)
Lemma: bag-member-empty-weak
∀[T:Type]. ∀[x:T]. (x ↓∈ {} ⇐⇒ False)
Lemma: empty-bag-iff-no-member
∀[T:Type]. ∀[bs:bag(T)]. uiff(bs = {} ∈ bag(T);∀x:T. (¬x ↓∈ bs))
Lemma: bag-member-iff-size
∀[T:Type]. ∀[bs:bag(T)]. uiff(↓∃x:T. x ↓∈ bs;0 < #(bs))
Lemma: empty-bag-iff-size
∀[T:Type]. ∀[bs:bag(T)]. uiff(bs = {} ∈ bag(T);#(bs) ≤ 0)
Lemma: non-empty-bag-implies-non-void
∀[T:Type]. ∀[bs:bag(T)]. ((¬(bs = {} ∈ bag(T))) ⇒ (↓T))
Lemma: bag-member-single
∀[T:Type]. ∀[x,y:T]. uiff(x ↓∈ {y};x = y ∈ T)
Lemma: single-bags-equal
∀[T:Type]. ∀[x,y:T]. uiff({x} = {y} ∈ bag(T);x = y ∈ T)
Lemma: bag-member-single-weak
∀[T:Type]. ∀[x,y:T]. (x ↓∈ {y} ⇐⇒ x = y ∈ T)
Lemma: bag-member-list
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀x:T. ∀L:T List. (x ↓∈ L ⇐⇒ (x ∈ L))))
Lemma: l_member-bag-member
∀[T:Type]. ∀x:T. ∀L:T List. (x ↓∈ L ⇐⇒ ↓(x ∈ L))
Lemma: bag-member-iff-hd
∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T]. uiff(x ↓∈ bs;↓∃L:T List. (bs = [x / L] ∈ bag(T)))
Lemma: bag-member-append
∀[T:Type]. ∀x:T. ∀as,bs:bag(T). (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
Lemma: bag-member-iff
∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T]. uiff(x ↓∈ bs;↓∃as:bag(T). (bs = ({x} + as) ∈ bag(T)))
Lemma: bag-in-subtype
∀[A,B:Type]. ∀[b:bag(B)]. b ∈ bag(A) supposing ∀x:B. (x ↓∈ b ⇒ (x ∈ A)) supposing strong-subtype(A;B)
Lemma: bag-in-subtype2
∀[A,B:Type]. ∀[b:bag(B)]. b ∈ bag(A) supposing ∀x:B. (x ↓∈ b ⇒ (∃a:bag(A). x ↓∈ a)) supposing strong-subtype(A;B)
Lemma: bag-member-combine
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[b:B]. uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x]))
Lemma: bag-member-select
∀[A:Type]. ∀[L:A List]. ∀[i:ℕ||L||]. L[i] ↓∈ L
Lemma: bag-map-list-map
∀[T,U:Type]. ∀L1:T List. ∀L2:U List. ∀f:T ⟶ U. ((L2 = map(f;L1) ∈ bag(U)) ⇒ (∃L:U List. (L = map(f;L1) ∈ (U List))))
Lemma: bag-member-cons
∀[T:Type]. ∀[x,u:T]. ∀[v:bag(T)]. uiff(x ↓∈ u.v;(x = u ∈ T) ↓∨ x ↓∈ v)
Lemma: bag-member-map
∀[T,U:Type]. ∀x:U. ∀f:T ⟶ U. ∀bs:bag(T). uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
Lemma: bag-member-filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:T]. ∀[bs:bag(T)]. uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs ∧ (↑P[x]))
Lemma: bag-member-filter-set
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:{x:T| ↑P[x]} ]. ∀[bs:bag(T)]. uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs)
Lemma: bag-member-mapfilter
∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:U]. ∀[bs:bag(T)]. ∀[f:{x:T| ↑(P x)} ⟶ U].
uiff(x ↓∈ bag-mapfilter(f;P;bs);↓∃v:{x:T| ↑(P x)} . (v ↓∈ bs ∧ (x = (f v) ∈ U)))
Lemma: bag-member-union
∀[T:Type]. ∀[x:T]. ∀[bbs:bag(bag(T))]. uiff(x ↓∈ bag-union(bbs);↓∃b:bag(T). (x ↓∈ b ∧ b ↓∈ bbs))
Lemma: bag-member-list-member
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀L:T List. ∀b:bag(T). ∀x:T. ((L = b ∈ bag(T)) ⇒ x ↓∈ b ⇒ (x ∈ L))))
Lemma: bag-member-from-upto
∀[n,m,x:ℤ]. uiff(x ↓∈ [n, m);(n ≤ x) ∧ x < m)
Lemma: bag-member-ifthenelse
∀[T:Type]. ∀[as,bs:bag(T)]. ∀[x:T]. ∀b:𝔹. uiff(x ↓∈ if b then as else bs fi ;if b then x ↓∈ as else x ↓∈ bs fi )
Lemma: bag-member-not-bag-null
∀[T:Type]. ∀[bs:bag(T)]. uiff(↓∃x:T. x ↓∈ bs;¬↑bag-null(bs))
Lemma: bag-member-product
∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[p:A × B]. uiff(p ↓∈ as × bs;fst(p) ↓∈ as ∧ snd(p) ↓∈ bs)
Lemma: bag-member-spread
∀[P:Top × Top]. ∀[C,p,T:Top]. (p ↓∈ let x,y = P in C[x;y] ~ let x,y = P in p ↓∈ C[x;y])
Lemma: bag-member-spread-to-pi
∀[P:Top × Top]. ∀[C,p,T:Top]. (p ↓∈ let x,y = P in C[x;y] ~ p ↓∈ C[fst(P);snd(P)])
Lemma: bag-member-evidence
∀[T:Type]. ∀[b:bag(T)]. ∀[x:T]. Ax ∈ x ↓∈ b supposing x ↓∈ b
Lemma: list-member-bag-member
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ x ↓∈ L)
Lemma: bag-member-sq-list-member
∀[T:Type]. ∀L:T List. ∀x:T. ↓(x ∈ L) supposing x ↓∈ L
Lemma: bag-member-iff-sq-list-member
∀[T:Type]. ∀L:T List. ∀x:T. uiff(x ↓∈ L;↓(x ∈ L))
Lemma: not-list-member-not-bag-member
∀[T:Type]. ∀[L:T List]. ∀[x:T]. ((¬(x ∈ L)) ⇒ (¬x ↓∈ L))
Lemma: int-bag-product-positive
∀[b:bag(ℤ)]. 0 < Π(b) supposing ∀[x:ℤ]. (x ↓∈ b ⇒ 0 < x)
Lemma: map-member-wf
∀[A,B:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)} ⟶ B]. (map(f;L) ∈ B List)
Lemma: bag-combine-null
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[b:bag(A)]. uiff(↑bag-null(⋃x∈b.f[x]);∀x:A. (x ↓∈ b ⇒ (↑bag-null(f[x]))))
Lemma: bag-combine-size-bound2
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[L:bag(A)]. ∀[a:A]. #(f[a]) ≤ #(⋃a∈L.f[a]) supposing a ↓∈ L
Lemma: bag-size-bag-member
∀[T:Type]. ∀[bs:bag(T)]. (0 < #(bs) ⇐⇒ ↓∃b:T. b ↓∈ bs)
Lemma: bag-member-size
∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T]. 0 < #(bs) supposing x ↓∈ bs
Lemma: sub-bag-union-of-list
∀[T:Type]. ∀[x:bag(T)]. ∀bs:bag(T) List. ((x ∈ bs) ⇒ sub-bag(T;x;bag-union(bs)))
Lemma: member-bag-rep
∀[T:Type]. ∀[n:ℕ]. ∀[x,y:T]. y = x ∈ T supposing y ↓∈ bag-rep(n;x)
Lemma: select-bag-rep
∀[T:Type]. ∀[n:ℕ]. ∀[x:T]. ∀[i:ℕn]. (bag-rep(n;x)[i] = x ∈ T)
Lemma: assert-bag_all
∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[b:bag(T)]. (∀x:T. (x ↓∈ b ⇒ (↑f[x])) ⇐⇒ ↑bag_all(b;f))
Lemma: bag-null-bag-union
∀[T:Type]. ∀[bbs:bag(bag(T))]. ↑bag-null(bag-union(bbs)) supposing ∀bs:bag(T). (bs ↓∈ bbs ⇒ (↑bag-null(bs)))
Lemma: bag-null-filter
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[b:bag(T)]. uiff(↑bag-null([x∈b|p[x]]);∀x:T. (x ↓∈ b ⇒ (¬↑p[x])))
Definition: b_all
b_all(T;b;x.P[x]) == ∀x:T. (x ↓∈ b ⇒ P[x])
Lemma: b_all_wf
∀[T:Type]. ∀[b:bag(T)]. ∀[P:T ⟶ ℙ]. (b_all(T;b;x.P[x]) ∈ ℙ)
Lemma: b_all-wf2
∀[T:Type]. ∀[b:bag(T)]. ∀[P:{x:T| x ↓∈ b} ⟶ ℙ]. (b_all(T;b;x.P[x]) ∈ ℙ)
Lemma: b_all-map
∀[A,B:Type].
∀f:A ⟶ B. ∀b:bag(A). ∀P:B ⟶ ℙ. ((∀b:B. SqStable(P[b])) ⇒ (b_all(B;bag-map(f;b);x.P[x]) ⇐⇒ b_all(A;b;x.P[f x])))
Lemma: b_all-inst
∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B. (x ↓∈ b ⇒ b_all(B;b;x.P[x]) ⇒ P[x])
Lemma: b_all-cons
∀[B:Type]. ∀b:bag(B). ∀P:B ⟶ ℙ. ∀x:B. ((∀b:B. SqStable(P[b])) ⇒ (b_all(B;x.b;x.P[x]) ⇐⇒ P[x] ∧ b_all(B;b;x.P[x])))
Lemma: b_all-squash-exists-bag
∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].
↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ b_all(A × B;bs;x.let a,b = x in ↓P[a;b]))
supposing b_all(A;as;x.↓∃y:B. P[x;y])
Lemma: b_all-squash-exists-bag2
∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].
↓∃bs:bag(A × B). ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ b_all(A × B;bs;x.↓P[fst(x);snd(x)]))
supposing b_all(A;as;x.↓∃y:B. P[x;y])
Lemma: b_all-squash-exists-list
∀[A,B:Type]. ∀[as:bag(A)]. ∀[P:A ⟶ B ⟶ ℙ].
↓∃bs:(A × B) List. ((bag-map(λx.(fst(x));bs) = as ∈ bag(A)) ∧ (∀x∈bs.↓P[fst(x);snd(x)]))
supposing b_all(A;as;x.↓∃y:B. P[x;y])
Lemma: l_all-squash-exists-list
∀[A,B:Type]. ∀[as:A List]. ∀[P:A ⟶ B ⟶ ℙ].
↓∃bs:(A × B) List. ((map(λx.(fst(x));bs) = as ∈ (A List)) ∧ (∀x∈bs.↓P[fst(x);snd(x)])) supposing (∀x∈as.↓∃y:B. P[x;y])
Lemma: l_all_implies_b_all
∀[A:Type]. ∀as:A List. ∀P:A ⟶ ℙ. ((∀x,y:A. Dec(x = y ∈ A)) ⇒ (∀x∈as.P[x]) ⇒ b_all(A;as;x.P[x]))
Definition: bag-inject
bag-inject(A;b;B;f) == Inj({x:A| x ↓∈ b} ;B;f)
Lemma: bag-inject_wf
∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ B]. (bag-inject(A;b;B;f) ∈ ℙ)
Definition: similar-bags
similar-bags(A;as;bs) == ∀a:A. (a ↓∈ as ∧ 0 < #(bs) ⇐⇒ a ↓∈ bs ∧ 0 < #(as))
Lemma: similar-bags_wf
∀[A:Type]. ∀[as,bs:bag(A)]. (similar-bags(A;as;bs) ∈ ℙ)
Definition: single-valued-bag
single-valued-bag(b;T) == ∀x,y:T. (x ↓∈ b ⇒ y ↓∈ b ⇒ (x = y ∈ T))
Lemma: single-valued-bag_wf
∀[T:Type]. ∀[b:bag(T)]. (single-valued-bag(b;T) ∈ ℙ)
Lemma: single-valued-bag-hd
∀[T:Type]. ∀[b:bag(T)]. (hd(b) ∈ T) supposing (0 < #(b) and single-valued-bag(b;T))
Lemma: single-valued-bag-if-le1
∀[T:Type]. ∀[b:bag(T)]. single-valued-bag(b;T) supposing #(b) ≤ 1
Lemma: single-valued-bag-single
∀[T:Type]. ∀[b:T]. single-valued-bag({b};T)
Lemma: single-valued-bag-empty
∀[T:Type]. single-valued-bag({};T)
Lemma: single-valued-bag-combine
∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ bag(B)].
(single-valued-bag(⋃x∈as.f[x];B)) supposing ((∀a:A. single-valued-bag(f[a];B)) and single-valued-bag(as;A))
Lemma: single-valued-bag-append
∀[A:Type]. ∀[as,bs:bag(A)].
(single-valued-bag(as + bs;A)) supposing
(similar-bags(A;as;bs) and
single-valued-bag(as;A) and
single-valued-bag(bs;A))
Lemma: single-valued-bag-map
∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ B]. single-valued-bag(bag-map(f;as);B) supposing single-valued-bag(as;A)
Lemma: single-valued-bag-list
∀[T:Type]. ∀[L:T List]. single-valued-list(L;T) supposing single-valued-bag(L;T)
Lemma: single-valued-bag-is-rep
∀[A:Type]. ∀[as:bag(A)]. ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
Definition: sv-bag-only
sv-bag-only(b) == hd(b)
Lemma: sv-bag-only_wf
∀[T:Type]. ∀[b:bag(T)]. (sv-bag-only(b) ∈ T) supposing (0 < #(b) and single-valued-bag(b;T))
Lemma: bag-member-sv-bag-only
∀[T:Type]. ∀[b:bag(T)]. (sv-bag-only(b) ↓∈ b) supposing (0 < #(b) and single-valued-bag(b;T))
Lemma: bag-member-implies-hd-append
∀[T:Type]. ∀[x:T]. ∀[b:bag(T)]. ↓∃c:bag(T). (b = ({x} + c) ∈ bag(T)) supposing x ↓∈ b
Lemma: sv-bag-only-single
∀[x:Top]. (sv-bag-only({x}) ~ x)
Lemma: sv_bag_only_single_lemma
∀x:Top. (sv-bag-only({x}) ~ x)
Lemma: sv-bag-only-append
∀[A:Type]. ∀[as,bs:bag(A)].
(sv-bag-only(as + bs) = sv-bag-only(as) ∈ A) supposing
(similar-bags(A;as;bs) and
0 < #(as) and
single-valued-bag(as;A) and
single-valued-bag(bs;A))
Lemma: sv-bag-only-combine
∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)].
(sv-bag-only(⋃x∈b.f[x]) = sv-bag-only(f[sv-bag-only(b)]) ∈ B) supposing
((∀a:A. 0 < #(f[a])) and
(∀a:A. single-valued-bag(f[a];B)) and
0 < #(b) and
single-valued-bag(b;A))
Lemma: sv-bag-only-map
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].
(sv-bag-only(bag-map(f;b)) = f[sv-bag-only(b)] ∈ B) supposing (0 < #(b) and single-valued-bag(b;A))
Lemma: sv-bag-only-map2
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)].
(sv-bag-only(bag-map(f;b)) = (f sv-bag-only(b)) ∈ B) supposing (0 < #(b) and single-valued-bag(b;A))
Definition: bag-disjoint
bag-disjoint(T;as;bs) == ∀x:T. (¬(x ↓∈ as ∧ x ↓∈ bs))
Lemma: bag-disjoint_wf
∀[T:Type]. ∀[as,bs:bag(T)]. (bag-disjoint(T;as;bs) ∈ ℙ)
Lemma: bag-combine-eq-right
∀[A,B:Type]. ∀[b:bag(A)]. ∀[f1,f2:A ⟶ bag(B)].
⋃x∈b.f1[x] = ⋃x∈b.f2[x] ∈ bag(B) supposing ∀x:{x:A| x ↓∈ b} . (f1[x] = f2[x] ∈ bag(B))
Lemma: bag-filter-empty
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)]. ∀x:T. (x ↓∈ b ⇒ (¬↑P[x])) supposing ↑bag-null([x∈b|P[x]])
Lemma: bag-filter-empty-iff
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)]. uiff(∀x:T. (x ↓∈ b ⇒ (¬↑P[x]));↑bag-null([x∈b|P[x]]))
Lemma: bag-filter-is-empty
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)]. uiff(∀x:T. (x ↓∈ b ⇒ (¬↑P[x]));[x∈b|P[x]] = {} ∈ bag(T))
Lemma: bag-filter-trivial2
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. [x∈bs|p[x]] = bs ∈ bag(T) supposing ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
Lemma: bag-filter-equal
∀[T:Type]. ∀[p1,p2:T ⟶ 𝔹]. ∀[b:bag(T)]. uiff([x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T);∀x:T. (x ↓∈ b ⇒ (↑p1[x] ⇐⇒ ↑p2[x])))
Lemma: sub-bag-member
∀[T:Type]. ∀[b1,b2:bag(T)]. ∀[x:T]. (x ↓∈ b2) supposing (sub-bag(T;b1;b2) and x ↓∈ b1)
Lemma: sub-bag-filter
∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b,c:bag(T). (sub-bag(T;b;[x∈c|p[x]]) ⇐⇒ sub-bag(T;b;c) ∧ (∀x:T. (x ↓∈ b ⇒ (↑p[x]))))
Lemma: bag-filter-is-sub-bag
∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b:bag(T). sub-bag(T;[x∈b|p[x]];b)
Lemma: sub-bag-filter2
∀T:Type. ∀p1,p2:T ⟶ 𝔹. ∀b,c:bag(T).
(sub-bag(T;b;[x∈c|p1[x]]) ⇒ sub-bag(T;b;[x∈c|p2[x]]) ⇒ sub-bag(T;b;[x∈c|p1[x] ∧b p2[x]]))
Lemma: sub-bag-filter3
∀T:Type. ∀p:T ⟶ 𝔹. ∀b,c:bag(T). (sub-bag(T;b;c) ⇒ sub-bag(T;[x∈b|p[x]];[x∈c|p[x]]))
Lemma: single-valued-sub-bag
∀[T:Type]. ∀[as,bs:bag(T)]. (single-valued-bag(bs;T) ⇒ sub-bag(T;as;bs) ⇒ single-valued-bag(as;T))
Lemma: bag-subtype
∀[A:Type]. ∀b:bag(A). (b ∈ bag({x:A| x ↓∈ b} ))
Lemma: bag-subtype2
∀[A:Type]. ∀P:A ⟶ ℙ. ∀b:bag({x:A| P[x]} ). ∀x:{x:A| P[x]} . (x ↓∈ b ⇐⇒ x ↓∈ b)
Lemma: bag-member-subtype-2
∀[A:Type]. ∀b:bag(A). ∀x:A. (x ↓∈ b ⇒ x ↓∈ b)
Lemma: strong-subtype-bag
∀[A,B:Type]. strong-subtype(bag(A);bag(B)) supposing strong-subtype(A;B)
Definition: bag-to-list
bag-to-list(cmp;b) == comparison-sort(cmp;b)
Lemma: bag-to-list_wf
∀[T:Type]
∀[b:bag(T)]. ∀[cmp:comparison({x:T| x ↓∈ b} )].
bag-to-list(cmp;b) ∈ T List supposing ∀x,y:{x:T| x ↓∈ b} . (((cmp x y) = 0 ∈ ℤ) ⇒ (x = y ∈ T))
supposing valueall-type(T)
Lemma: sub-bag-of-bag-rep
∀[T:Type]. ∀x:T. ∀n:ℕ. ∀[b:bag(T)]. b = bag-rep(#(b);x) ∈ bag(T) supposing sub-bag(T;b;bag-rep(n;x))
Lemma: bag-append-equal-bag-rep
∀[T:Type]. ∀[x:T]. ∀[n:ℕ]. ∀[a,b:bag(T)].
uiff((a + b) = bag-rep(n;x) ∈ bag(T);(n = (#(a) + #(b)) ∈ ℤ)
∧ (a = bag-rep(#(a);x) ∈ bag(T))
∧ (b = bag-rep(#(b);x) ∈ bag(T)))
Lemma: bag-no-repeats-subtype
∀[T,A:Type]. ∀[bs:bag(A)]. (bag-no-repeats(A;bs)) supposing (bag-no-repeats(T;bs) and strong-subtype(A;T))
Lemma: bag-filter-no-repeats2
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. bag-no-repeats({x:T| ↑p[x]} ;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)
Lemma: bag-combine-eq-out
∀[A,B,C:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[f:A ⟶ bag(C)]. ∀[g:B ⟶ bag(C)]. ∀[h:A ⟶ B].
(⋃a∈as.f[a] = ⋃b∈bs.g[b] ∈ bag(C)) supposing
((∀a:A. (a ↓∈ as ⇒ (g[h[a]] = f[a] ∈ bag(C)))) and
(bs = bag-map(h;as) ∈ bag(B)))
Lemma: bag-map-member-wf
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:{a:A| a ↓∈ bs} ⟶ B]. (bag-map(f;bs) ∈ bag(B))
Lemma: bag-combine-member-wf
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:{a:A| a ↓∈ bs} ⟶ bag(B)]. (⋃x∈bs.f[x] ∈ bag(B))
Lemma: bag-filter-wf2
∀[T:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs} ⟶ 𝔹]. ([x∈bs|p[x]] ∈ bag({x:{b:T| b ↓∈ bs} | ↑p[x]} ))
Lemma: bag-mapfilter-wf2
∀[T,A:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs} ⟶ 𝔹]. ∀[f:{x:{b:T| b ↓∈ bs} | ↑p[x]} ⟶ A].
(bag-mapfilter(f;p;bs) ∈ bag(A))
Lemma: bag-member-map2
∀[T,U:Type]. ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs} ⟶ U. uiff(x ↓∈ bag-map(f;bs);↓∃v:{v:T| v ↓∈ bs} . (x = (f v) ∈ U))
Lemma: bag-member-map3
∀[T,U:Type]. ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs} ⟶ U. uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
Lemma: bag-member-filter-implies1
∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs} ⟶ 𝔹]. x ↓∈ [x∈bs|P[x]] supposing x ↓∈ bs ∧ (↑P[x])
Lemma: bag-member-filter-implies2
∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs} ⟶ 𝔹]. x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]
Lemma: bag-member-filter2
∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs} ⟶ 𝔹]. uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs ∧ (↑P[x]))
Lemma: single-valued-bag-filter
∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b} ⟶ 𝔹].
single-valued-bag([x∈b|p[x]];A) supposing ∀x,y:A. (x ↓∈ b ⇒ y ↓∈ b ⇒ (↑p[x]) ⇒ (↑p[y]) ⇒ (x = y ∈ A))
Lemma: bag-eq-subtype1
∀[A:Type]. ∀[B:A ⟶ ℙ]. ∀[d1,d2:bag({a:A| B[a]} )]. d1 = d2 ∈ bag({a:A| B[a]} ) supposing d1 = d2 ∈ bag(A)
Lemma: bag-eq-subtype
∀[A:Type]. ∀[d1,d2:bag(A)]. d1 = d2 ∈ bag({a:A| a ↓∈ d1} ) supposing d1 = d2 ∈ bag(A)
Lemma: sv-bag-only-filter
∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b} ⟶ 𝔹].
∀x:A. (sv-bag-only([x∈b|p[x]]) = x ∈ A) supposing ((↑p[x]) and x ↓∈ b and (∀y:A. (y ↓∈ b ⇒ (↑p[y]) ⇒ (y = x ∈ A))))
Lemma: bag-member-map3-deq
∀[T,U:Type].
∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs} ⟶ U.
(Inj({v:T| v ↓∈ bs} ;U;f) ⇒ (∀x,y:U. Dec(x = y ∈ U)) ⇒ uiff(x ↓∈ bag-map(f;bs);∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))\000C)
Lemma: b_all-map2
∀[A,B:Type].
∀b:bag(A). ∀f:{a:A| a ↓∈ b} ⟶ B. ∀P:B ⟶ ℙ.
((∀b:B. SqStable(P[b])) ⇒ (b_all(B;bag-map(f;b);x.P[x]) ⇐⇒ b_all(A;b;x.P[f x])))
Definition: bag-combine-restrict
bag-combine-restrict(b;x.f[x]) == ⋃x∈b.f[x]
Lemma: bag-combine-restrict_wf
∀[A,B:Type]. ∀[b:bag(A)]. ∀[f:{a:A| a ↓∈ b} ⟶ bag(B)]. (bag-combine-restrict(b;x.f[x]) ∈ bag(B))
Lemma: bag-only_wf2
∀[T:Type]. ∀[b:bag(T)]. only(b) ∈ T supposing single-valued-bag(b;T) ∧ 0 < #(b)
Lemma: bag-filter-combine
∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[f:U ⟶ bag(T)]. ∀[b:bag(U)]. ([x∈⋃z∈b.f[z]|P[x]] = ⋃z∈b.[x∈f[z]|P[x]] ∈ bag(T))
Lemma: bag-filter-combine2
∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[f:U ⟶ bag(T)]. ∀[b:bag(U)]. ([x∈⋃z∈b.f[z]|P[x]] = ⋃z∈b.[x∈f[z]|P[x]] ∈ bag({x:T| ↑P[x]} ))
Lemma: bag-mapfilter-combine
∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[P:B ⟶ 𝔹]. ∀[g:{x:B| ↑P[x]} ⟶ C].
(bag-mapfilter(g;P;⋃x∈b.f[x]) = ⋃x∈b.bag-mapfilter(g;P;f[x]) ∈ bag(C))
Definition: bag-mapfilter-fast
bag-mapfilter-fast(f;P;bs) == bag-accum(b,x.if P[x] then f[x].b else b fi ;{};bs)
Lemma: bag-mapfilter-fast_wf
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]} ⟶ B]. (bag-mapfilter-fast(f;P;bs) ∈ bag(B))
Lemma: bag-mapfilter-fast-eq
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]} ⟶ B].
(bag-mapfilter-fast(f;P;bs) = bag-mapfilter(f;P;bs) ∈ bag(B))
Lemma: bag-mapfilter-fast-eq2
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]} ⟶ B].
(bag-mapfilter(f;P;bs) = bag-mapfilter-fast(f;P;bs) ∈ bag(B))
Lemma: bag-mapfilter-fast-map
∀[bs:bag(Top)]. ∀[P,f,g:Top]. (bag-mapfilter-fast(f;P;bag-map(g;bs)) ~ bag-mapfilter-fast(f o g;P o g;bs))
Lemma: bag-maximals-not-max
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].
(¬↑(R x y)) supposing
(y ↓∈ bag-maximals(b;R) and
x ↓∈ bag-maximals(b;R) and
(∀x,y:T. ((↑(R x y)) ⇒ (↑(R y x)) ⇒ (x = y ∈ T))) and
(∀x:T. (¬↑(R x x))))
Lemma: bag-maximal?-max
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T]. (↑(R x y)) supposing ((↑bag-maximal?(b;x;R)) and y ↓∈ b)
Lemma: bag-maximal?-iff
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x:T]. uiff(↑bag-maximal?(b;x;R);∀y:T. (y ↓∈ b ⇒ (↑(R x y))))
Lemma: bag-maximals-max
∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T]. (↑(R x y)) supposing (x ↓∈ bag-maximals(b;R) and y ↓∈ b)
Lemma: imax-bag-ub
∀[bs:bag(ℤ)]. ∀[x:ℤ]. (x ↓∈ bs ⇒ (x ≤ imax-bag(bs)))
Lemma: imax-bag-lb
∀[bs:bag(ℤ)]. (0 < #(bs) ⇒ imax-bag(bs) ↓∈ bs)
Definition: bag-max
bag-max(f;bs) == imax-bag(bag-map(f;bs))
Lemma: bag-max_wf
∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)]. bag-max(f;bs) ∈ ℤ supposing 0 < #(bs)
Lemma: bag-max-ub
∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)]. ∀[x:A]. (f x) ≤ bag-max(f;bs) supposing x ↓∈ bs
Lemma: bag-max-lb
∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[bs:bag(A)]. bag-max(f;bs) ↓∈ bag-map(f;bs) supposing 0 < #(bs)
Lemma: bag-append-no-repeats1
∀[T:Type]. ∀[as,bs:bag(T)].
bag-no-repeats(T;as + bs) supposing bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀z:T. (z ↓∈ as ⇒ (¬z ↓∈ bs)))
Lemma: bag-append-no-repeats
∀[T:Type]. ∀[as,bs:bag(T)].
uiff(bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀z:T. (z ↓∈ as ⇒ (¬z ↓∈ bs)));bag-no-repeats(T;as + bs))
Lemma: bag-product-no-repeats
∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)].
bag-no-repeats(A × B;as × bs) supposing bag-no-repeats(A;as) ∧ bag-no-repeats(B;bs)
Lemma: bag-no-repeats-implies-disjoint
∀[T:Type]. ∀[as,bs:bag(T)]. bag-disjoint(T;as;bs) supposing bag-no-repeats(T;as + bs)
Lemma: bag-settype
∀[T:Type]. ∀[bs:bag(T)]. ∀[P:T ⟶ ℙ]. bs ∈ bag({x:T| P[x]} ) supposing ∀x:T. (x ↓∈ bs ⇒ P[x])
Lemma: bag-filter-same
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)]. [x∈bs|p[x]] = bs ∈ bag(T) supposing ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
Lemma: bag-extensionality-no-repeats
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀[as,bs:bag(T)].
uiff(as = bs ∈ bag(T);∀x:T. uiff(x ↓∈ as;x ↓∈ bs)) supposing bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs)))
Lemma: bag-extensionality1
∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].
∀[as,bs:bag(T)]. uiff(as = bs ∈ bag(T);∀x:T. (#([y∈as|eq x y]) = #([y∈bs|eq x y]) ∈ ℤ))
supposing ∀[x,y:T]. (↑(eq x y) ⇐⇒ x = y ∈ T)
Lemma: bag-intersection
∀[A:Type]. ∀[as,as',bs,bs':bag(A)].
(↓∃x:A. (x ↓∈ as ∧ x ↓∈ bs)) supposing (#(as') < #(as) and #(bs') < #(bs) and ((as + as') = (bs + bs') ∈ bag(A)))
Definition: bag-splits
bag-splits(b) == rec-case(b) of [] => {<{}, {}>} | a::as => r.bag-map(λp.<{a} + (fst(p)), snd(p)>;r) + bag-map(λp.<fst(\000Cp), {a} + (snd(p))>;r)
Lemma: bag-splits_wf_list
∀T:Type. ∀b:T List. (bag-splits(b) ∈ (bag(T) × bag(T)) List)
Lemma: bag-splits-permutation1
∀T:Type. ∀L:T List. ∀a,b:T. permutation(bag(T) × bag(T);bag-splits([a; [b / L]]);bag-splits([b; [a / L]]))
Lemma: bag-splits-permutation
∀T:Type. ∀L1,L2:T List. (permutation(T;L1;L2) ⇒ permutation(bag(T) × bag(T);bag-splits(L1);bag-splits(L2)))
Lemma: bag-splits_wf
∀T:Type. ∀b:bag(T). (bag-splits(b) ∈ bag(bag(T) × bag(T)))
Lemma: bag-member-splits
∀[T:Type]. ∀[as,bs,cs:bag(T)]. uiff(<as, bs> ↓∈ bag-splits(cs);(as + bs) = cs ∈ bag(T))
Definition: bag-decomp
bag-decomp(bs) == map(λn.remove-nth(n;bs);upto(||bs||))
Lemma: bag-decomp_wf
∀[T:Type]. ∀[bs:bag(T)]. (bag-decomp(bs) ∈ bag(T × bag(T)))
Lemma: bag-member-decomp
∀[T:Type]. ∀[bs:bag(T)]. ∀[x:T]. ∀[b:bag(T)]. uiff(<x, b> ↓∈ bag-decomp(bs);({x} + b) = bs ∈ bag(T))
Lemma: bag-decomp_wf2
∀[T:Type]. ∀[bs:bag(T)]. (bag-decomp(bs) ∈ bag({p:T × bag(T)| bs = ({fst(p)} + (snd(p))) ∈ bag(T)} ))
Lemma: no_repeats-bag
∀[T:Type]. ∀[as,bs:T List]. (no_repeats(T;as)) supposing (no_repeats(T;bs) and (as = bs ∈ bag(T)))
Lemma: bag-no-repeats-settype
∀[T:Type]. ∀[bs:bag(T)]. uiff(bag-no-repeats({x:T| x ↓∈ bs} ;bs);bag-no-repeats(T;bs)) supposing ∀x,y:T. Dec(x = y ∈ T\000C)
Lemma: bag-no-repeats-le-bag-size
∀[T:Type]. ∀[locs,b:bag(T)]. #(b) ≤ #(locs) supposing bag-no-repeats(T;b) ∧ (∀x:T. (x ↓∈ b ⇒ x ↓∈ locs))
Lemma: bag-no-repeats-single
∀[T:Type]. ∀[x:T]. bag-no-repeats(T;{x})
Lemma: bag-no-repeats-append
∀[T:Type]. ∀[as,bs:bag(T)].
uiff(bag-no-repeats(T;as + bs);bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀x:T. (x ↓∈ as ⇒ (¬x ↓∈ bs))))
Lemma: bag-no-repeats-cons
∀[T:Type]. ∀[b:bag(T)]. ∀[x:T]. uiff(bag-no-repeats(T;x.b);bag-no-repeats(T;b) ∧ (¬x ↓∈ b))
Lemma: bag-no-repeats-list
∀[T:Type]. ∀[L:T List]. uiff(bag-no-repeats(T;L);no_repeats(T;L))
Lemma: bag-no-repeats-filter
∀[T:Type]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹]. bag-no-repeats(T;[x∈b|p[x]]) supposing bag-no-repeats(T;b)
Lemma: remove-repeats-wf-bag
∀[T:Type]. ∀eq:EqDecider(T). ∀bs:bag(T). (remove-repeats(eq;bs) ∈ bag(T))
Lemma: bag-summation-equal
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f,g:T ⟶ R].
Σ(x∈b). f[x] = Σ(x∈b). g[x] ∈ R supposing (∀x:T. (x ↓∈ b ⇒ (f[x] = g[x] ∈ R))) ∧ IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-equal2
∀[T:Type]. ∀[r:Rng]. ∀[f,g:T ⟶ |r|]. ∀[b,c:bag(T)].
Σ(x∈b). f[x] = Σ(x∈c). g[x] ∈ |r| supposing (∀x:T. (x ↓∈ b ⇒ (f[x] = g[x] ∈ |r|))) ∧ (b = c ∈ bag(T))
Lemma: bag-summation-is-zero
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
Σ(x∈b). f[x] = zero ∈ R supposing (∀x:T. (x ↓∈ b ⇒ (f[x] = zero ∈ R))) ∧ IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-single-non-zero
∀[T,R:Type]. ∀[eq:EqDecider(T)]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
∀z:T. Σ(x∈b). f[x] = Σ(x∈[x∈b|eq x z]). f[x] ∈ R supposing ∀x:T. (x ↓∈ b ⇒ ((x = z ∈ T) ∨ (f[x] = zero ∈ R)))
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-single-non-zero-no-repeats
∀[T,R:Type]. ∀[eq:EqDecider(T)]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
∀z:T
(Σ(x∈b). f[x] = f[z] ∈ R) supposing
((bag-no-repeats(T;b) ∧ z ↓∈ b) and
(∀x:T. (x ↓∈ b ⇒ ((x = z ∈ T) ∨ (f[x] = zero ∈ R)))))
supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-filter
∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹]. ∀[f:T ⟶ R].
Σ(x∈[x∈b|p[x]]). f[x] = Σ(x∈b). if p[x] then f[x] else zero fi ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Lemma: bag-summation-from-upto
∀[a,b:ℤ]. ∀[f:{a..b-} ⟶ ℤ]. (Σ(i∈[a, b)). f[i] = Σ(f[j + a] | j < b - a) ∈ ℤ)
Lemma: bag-summation-partition
∀[A:Type]
∀[R,T:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[case:T ⟶ A ⟶ 𝔹]. ∀[f:T ⟶ R]. ∀[c:bag(A)].
Σ(x∈b). f[x] = Σ(z∈c). Σ(x∈[x∈b|case[x;z]]). f[x] ∈ R
supposing (IsMonoid(R;add;zero) ∧ Comm(R;add))
∧ (∀x:{x:T| x ↓∈ b} . (∃z:A [(z ↓∈ c ∧ (↑case[x;z]))]))
∧ bag-no-repeats(A;c)
∧ (∀z1,z2:A. ∀x:T. ((↑case[x;z1]) ⇒ (↑case[x;z2]) ⇒ (z1 = z2 ∈ A)))
supposing ∀x,y:A. Dec(x = y ∈ A)
Lemma: bag-summation_functionality_wrt_le_1
∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:T ⟶ ℤ]. Σ(x∈b). f[x] ≤ Σ(x∈b). g[x] supposing ∀x:T. (f[x] ≤ g[x])
Lemma: bag-summation_functionality_wrt_le
∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b} ⟶ ℤ].
Σ(x∈b). f[x] ≤ Σ(x∈b). g[x] supposing ∀x:T. (x ↓∈ b ⇒ (f[x] ≤ g[x]))
Lemma: bag-summation-equal-implies-all-equal-1
∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:T ⟶ ℤ].
(∀x:T. (x ↓∈ b ⇒ (f[x] = g[x] ∈ ℤ))) supposing ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and (∀x:T. (x ↓∈ b ⇒ (f[x] ≤ g[x]))))
Lemma: bag-summation-equal-implies-all-equal
∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b} ⟶ ℤ].
(∀x:T. (x ↓∈ b ⇒ (f[x] = g[x] ∈ ℤ))) supposing ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and (∀x:T. (x ↓∈ b ⇒ (f[x] ≤ g[x]))))
Definition: strict-bag-function
strict-bag-function(G;L;B;S) == ∀x:tuple-type(map(λT.bag(T);L)). ((∀i∈S.x.i = {} ∈ bag(L[i])) ⇒ ((G x) = {} ∈ bag(B)))
Lemma: strict-bag-function_wf
∀[L:Type List]. ∀[B:Type]. ∀[G:tuple-type(map(λT.bag(T);L)) ⟶ bag(B)]. ∀[S:ℕ||L|| List].
(strict-bag-function(G;L;B;S) ∈ ℙ)
Lemma: bag-from-member-function
∀[T:Type]
∀bs:bag(T). ∀P,Q:T ⟶ ℙ.
((∀i:T. Dec(Q[i]))
⇒ (∀i:T. (i ↓∈ bs ⇒ Q[i] ⇒ P[i]))
⇒ (∃b:bag(T). ((∀i:T. (i ↓∈ bs ⇒ Q[i] ⇒ i ↓∈ b)) ∧ (∀i:T. (i ↓∈ b ⇒ P[i])))))
Lemma: bag-from-member-function-exists
∀[T,A:Type].
∀bs:bag(T). ∀P:T ⟶ A ⟶ ℙ.
((∀x,y:A. Dec(x = y ∈ A))
⇒ (∀x,y:T. Dec(x = y ∈ T))
⇒ (∀i:T. (i ↓∈ bs ⇒ (∃a:A. P[i;a])))
⇒ (∃b:bag(T × A). ((∀i:T. (i ↓∈ bs ⇒ i ↓∈ bag-map(λx.(fst(x));b))) ∧ (∀x:T × A. (x ↓∈ b ⇒ P[fst(x);snd(x)])))))
Definition: lifting-gen-list-rev
lifting-gen-list-rev(n;bags) ==
fix((λlifting-gen-list-rev,m,g. if (n =z m) then {g} else ⋃x∈bags m.lifting-gen-list-rev (m + 1) (g x) fi ))
Lemma: lifting-gen-list-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].
(lifting-gen-list-rev(n;bags) m g ∈ bag(B))
Lemma: temp-lifting-gen-list-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));B)].
(lifting-gen-list-rev(n;bags) m g ∈ bag(B))
Definition: lifting-gen-rev
lifting-gen-rev(n;f;bags) == lifting-gen-list-rev(n;bags) 0 f
Lemma: lifting-gen-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;B)]. (lifting-gen-rev(n;f;bags) ∈ bag(B))
Definition: lifting-gen
lifting-gen(n;f) == λbags.lifting-gen-rev(n;f;bags)
Lemma: lifting-gen_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;B)]. (lifting-gen(n;f) ∈ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))
Lemma: lifting-gen-strict
∀[n:ℕ]. ∀[f:Top]. ∀[a:k:ℕn ⟶ bag(Top)]. lifting-gen(n;f) a ~ {} supposing ∃k:ℕn. (↑bag-null(a k))
Definition: lifting1
lifting1(f;b) == lifting-gen-rev(1;f;λx.b)
Lemma: lifting1_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[b:bag(A)]. (lifting1(f;b) ∈ bag(B))
Definition: lifting2
lifting2(f;abag;bbag) == lifting-gen-rev(2;f;λx.[abag; bbag][x])
Lemma: lifting2_wf
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[abag:bag(A)]. ∀[bbag:bag(B)]. (lifting2(f;abag;bbag) ∈ bag(C))
Definition: lifting-0
lifting-0(b) == lifting-gen-rev(0;b;λn.[][n])
Lemma: lifting-0_wf
∀[B:Type]. ∀[b:B]. (lifting-0(b) ∈ bag(B))
Definition: lifting-1
lifting-1(f) == λb.lifting1(f;b)
Lemma: lifting-1_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. (lifting-1(f) ∈ bag(A) ⟶ bag(B))
Lemma: lifting-1-strict
∀[f:Top]. (lifting-1(f) {} ~ {})
Definition: lifting-2
lifting-2(f) == λa,b. lifting2(f;a;b)
Lemma: lifting-2_wf
∀[C,B,A:Type]. ∀[f:A ⟶ B ⟶ C]. (lifting-2(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C))
Lemma: lifting-2-strict
∀[f:Top]. ∀[b:bag(Top)]. ((lifting-2(f) {} b ~ {}) ∧ (lifting-2(f) b {} ~ {}))
Definition: lifting-3
lifting-3(f) == λa,b,c. lifting-gen-rev(3;f;λn.[a; b; c][n])
Lemma: lifting-3_wf
∀[A,B,C,D:Type]. ∀[f:A ⟶ B ⟶ C ⟶ D]. (lifting-3(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))
Lemma: lifting-3-strict
∀[f:Top]. ∀[b:bag(Top)].
∀b':bag(Top). ((lifting-3(f) {} b b' ~ {}) ∧ (lifting-3(f) b {} b' ~ {}) ∧ (lifting-3(f) b b' {} ~ {}))
Definition: uncurry-gen
uncurry-gen(n) == fix((λrec,m,g. if (m =z n) then g else rec (m + 1) (λx.(g x (x m))) fi ))
Lemma: uncurry-gen_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[g:(k:ℕn ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].
(uncurry-gen(n) m g ∈ (k:ℕn ⟶ (A k)) ⟶ B)
Lemma: uncurry-gen_wf2
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type].
∀[g:(k:{q..n-} ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].
(uncurry-gen(n) m g ∈ (k:{q..n-} ⟶ (A k)) ⟶ B)
Definition: uncurry-rev
uncurry-rev(n;f) == uncurry-gen(n) 0 (λx.f)
Lemma: uncurry-rev_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;B)]. (uncurry-rev(n;f) ∈ (k:ℕn ⟶ (A k)) ⟶ B)
Definition: apply_gen
apply_gen(n;lst) == fix((λrec,m,g. if (m =z n) then g else rec (m + 1) (g (lst m)) fi ))
Lemma: apply_gen_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n - m;λx.(A (x + m));B)]. ∀[lst:k:{m..n-} ⟶ (A k)].
(apply_gen(n;lst) m f ∈ B)
Lemma: apply_gen_wf2
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n - q;λx.(A (x + q));B)].
∀[lst:k:{q..n-} ⟶ (A k)].
(apply_gen(m;lst) q f ∈ funtype(n - m;λx.(A (x + m));B))
Lemma: apply_uncurry
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[lst:k:{q..n-} ⟶ (A k)].
∀[f:(k:{q..n-} ⟶ (A k)) ⟶ funtype(n - m;λx.(A (x + m));B)].
((uncurry-gen(n) m f lst) = (apply_gen(n;lst) m (f lst)) ∈ B)
Lemma: apply_larger_list
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[lst:k:{q..n-} ⟶ (A k)]. ∀[r:ℕm]. ∀[a:A r].
∀[f:funtype(n - m;λx.(A (x + m));B)].
((apply_gen(n;λx.if (x =z r) then a else lst x fi ) m f) = (apply_gen(n;lst) m f) ∈ B)
Lemma: lifting-member
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n - m;λx.(A (x + m));B)]. ∀[b:B].
(b ↓∈ lifting-gen-list-rev(n;bags) m f
⇐⇒ ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) m (λx.f) lst) = b ∈ B)))
Lemma: lifting-member-simple
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;B)]. ∀[b:B].
(b ↓∈ lifting-gen-rev(n;f;bags)
⇐⇒ ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ ((uncurry-rev(n;f) lst) = b ∈ B)))
Lemma: bag-member-lifting-2
∀[C,B,A:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[c:C].
uiff(c ↓∈ lifting-2(f) as bs;↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c = (f a b) ∈ C)))
Definition: concat-lifting-list
concat-lifting-list(n;bags) == λm,g. bag-union(lifting-gen-list-rev(n;bags) m g)
Lemma: concat-lifting-list_wf
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - m;λx.(A (x + m));bag(B))].
(concat-lifting-list(n;bags) m g ∈ bag(B))
Lemma: concat-lifting-list-member
∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n - m;λx.(A (x + m));bag(B))].
∀[b:B].
(b ↓∈ concat-lifting-list(n;bags) m f
⇐⇒ ↓∃lst:k:{m..n-} ⟶ (A k). ((∀[k:{m..n-}]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-gen(n) m (λx.f) lst))
Definition: concat-lifting
concat-lifting(n;f;bags) == concat-lifting-list(n;bags) 0 f
Lemma: concat-lifting_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;bag(B))].
(concat-lifting(n;f;bags) ∈ bag(B))
Lemma: concat-lifting-member
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[f:funtype(n;A;bag(B))]. ∀[b:B].
(b ↓∈ concat-lifting(n;f;bags) ⇐⇒ ↓∃lst:k:ℕn ⟶ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-rev(n;f) lst))
Lemma: concat-lifting-strict
∀[n:ℕ]. ∀[bags:k:ℕn ⟶ bag(Top)]. ∀[f:Top]. concat-lifting(n;f;bags) ~ {} supposing ∃k:ℕn. ((bags k) = {} ∈ bag(Top))
Definition: concat-lifting-gen
concat-lifting-gen(n;f) == λbags.concat-lifting(n;f;bags)
Lemma: concat-lifting-gen_wf
∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;bag(B))]. (concat-lifting-gen(n;f) ∈ (k:ℕn ⟶ bag(A k)) ⟶ bag(B))
Definition: concat-lifting1
concat-lifting1(f;bag) == concat-lifting(1;f;λx.bag)
Lemma: concat-lifting1_wf
∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[b:bag(A)]. (concat-lifting1(f;b) ∈ bag(B))
Definition: concat-lifting2
concat-lifting2(f;abag;bbag) == concat-lifting(2;f;λn.[abag; bbag][n])
Lemma: concat-lifting2_wf
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[abag:bag(A)]. ∀[bbag:bag(B)]. (concat-lifting2(f;abag;bbag) ∈ bag(C))
Definition: concat-lifting-0
concat-lifting-0(f) == concat-lifting(0;f;λn.[][n])
Lemma: concat-lifting-0_wf
∀[B:Type]. ∀[f:bag(B)]. (concat-lifting-0(f) ∈ bag(B))
Definition: concat-lifting-1
f@ == λb.concat-lifting1(f;b)
Lemma: concat-lifting-1_wf
∀[B,A:Type]. ∀[f:A ⟶ bag(B)]. (f@ ∈ bag(A) ⟶ bag(B))
Lemma: concat-lifting-1-strict
∀[f:Top]. (f@ {} ~ {})
Definition: concat-lifting-2
f@ == λa,b. concat-lifting2(f;a;b)
Lemma: concat-lifting-2_wf
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. (f@ ∈ bag(A) ⟶ bag(B) ⟶ bag(C))
Lemma: concat-lifting-2-strict
∀[f:Top]. ∀[b:bag(Top)]. ((f@ {} b ~ {}) ∧ (f@ b {} ~ {}))
Definition: concat-lifting-3
concat-lifting-3(f) == λa,b,c. concat-lifting(3;f;λn.[a; b; c][n])
Lemma: concat-lifting-3_wf
∀[A,B,C,D:Type]. ∀[f:A ⟶ B ⟶ C ⟶ bag(D)]. (concat-lifting-3(f) ∈ bag(A) ⟶ bag(B) ⟶ bag(C) ⟶ bag(D))
Lemma: concat-lifting-3-strict
∀[f:Top]. ∀[b:bag(Top)].
∀b':bag(Top)
((concat-lifting-3(f) {} b b' ~ {}) ∧ (concat-lifting-3(f) b {} b' ~ {}) ∧ (concat-lifting-3(f) b b' {} ~ {}))
Lemma: bag-map-append-empty
∀[f,b:Top]. (bag-map(f;b) + {} ~ bag-map(f;b))
Lemma: bag-combine-append-empty
∀[f,bs:Top]. (⋃x∈bs.f[x] @ [] ~ ⋃x∈bs.f[x])
Lemma: bag-combine-bag-append-empty
∀[f,bs:Top]. (⋃x∈bs.f[x] + [] ~ ⋃x∈bs.f[x])
Definition: bag-monoid
bag-monoid(T) == <bag(T), λx,y. tt, λx,y. tt, λx,y. (x + y), {}, λx.x>
Lemma: bag-monoid_wf
∀[T:Type]. (bag-monoid(T) ∈ AbMon)
Lemma: single-bag-append-nil
∀[a:Top]. ([a] + [] ~ [a])
Lemma: spread-bag-append
∀[x,F,L:Top]. (let a,b = x in F[a;b] + L ~ let a,b = x in F[a;b] + L)
Lemma: callbyvalueall-single-bag-combine1
∀[F,a,as:Top]. (let x ⟵ [a] in let y ⟵ ⋃z∈x.map(z;as) in F[y] ~ let x ⟵ a in let y ⟵ map(x;as) in F[y])
Lemma: callbyvalueall-single-bag-combine2
∀[F,G,a:Top]. (let x ⟵ [a] in let y ⟵ ⋃z∈x.G[z] in F[y] ~ let x ⟵ a in let y ⟵ G[x] @ [] in F[y])
Lemma: callbyvalueall-single-bag-combine3
∀[F,G,a,b:Top].
(let x ⟵ [a]
in let z ⟵ b
in let y ⟵ ⋃v∈x.G[z;v]
in F[z;y] ~ let x ⟵ a
in let z ⟵ b
in let y ⟵ G[z;x] @ []
in F[z;y])
Lemma: callbyvalueall-single-bag-combine4
∀[F,a:Top]. (let x ⟵ [a] in F[x] ~ let x ⟵ a in F[[x]])
Lemma: lifting-bag-combine-decide
∀[a,F,G,f:Top].
(⋃b∈case a of inl(x) => F[x] | inr(x) => G[x].f[b] ~ case a of inl(x) => ⋃b∈F[x].f[b] | inr(x) => ⋃b∈G[x].f[b])
Lemma: lifting-bag-combine-decide-name_eq
∀[a,b,F,G,f:Top].
(⋃b∈case name_eq(a;b) of inl(x) => F[x] | inr(x) => G[x].f[b] ~ case name_eq(a;b)
of inl(x) =>
⋃b∈F[x].f[b]
| inr(x) =>
⋃b∈G[x].f[b])
Definition: bag-admissable
bag-admissable(T;as,bs.R[as; bs]) == (∀bs:bag(T). R[{}; bs]) ∧ (∀as,bs,cs:bag(T). (R[as; bs] ⇒ R[as + cs; bs + cs]))
Lemma: bag-admissable_wf
∀[T:Type]. ∀[R:bag(T) ⟶ bag(T) ⟶ ℙ]. (bag-admissable(T;as,bs.R[as;bs]) ∈ ℙ)
Lemma: sub-bag-admissable
∀[T:Type]. ∀[R:bag(T) ⟶ bag(T) ⟶ ℙ].
(bag-admissable(T;as,bs.R[as;bs]) ⇒ (∀as,bs:bag(T). (sub-bag(T;as;bs) ⇒ R[as;bs])))
Lemma: sub-bag-singleton-left
∀[T:Type]. ∀[b:bag(T)]. ∀[x:T]. x ↓∈ b supposing sub-bag(T;{x};b)
Lemma: sub-bag-map-equal
∀[T,U:Type]. ∀[b1,b2:bag(T)]. ∀[f:T ⟶ U].
(b1 = b2 ∈ bag(T)) supposing (sub-bag(T;b2;b1) and sub-bag(U;bag-map(f;b1);bag-map(f;b2)))
Lemma: sub-bag-mapfilter-implies
∀[A,B:Type].
∀as:bag(A). ∀bs:bag(B). ∀f:A ⟶ B. ∀P:A ⟶ 𝔹. (sub-bag(B;bag-map(f;as);bs) ⇒ sub-bag(B;bag-mapfilter(f;P;as);bs))
Lemma: sub-bag-size
∀[T:Type]. ∀[a,b:bag(T)]. #(a) ≤ #(b) supposing sub-bag(T;a;b)
Definition: bag-order
bag-order(T) ==
{cmp:bag(T) ⟶ bag(T) ⟶ ℤ|
(∀as,bs:bag(T). (((cmp as bs) = 0 ∈ ℤ ⇐⇒ as = bs ∈ bag(T)) ∧ (cmp as bs < 0 ⇐⇒ (cmp bs as) > 0)))
∧ Linorder(bag(T);as,bs.(cmp as bs) ≤ 0)}
Lemma: bag-order_wf
∀T:Type. (bag-order(T) ∈ Type)
Definition: unordered-combination
UnorderedCombination(n;T) == {b:bag(T)| bag-no-repeats(T;b) ∧ (#(b) = n ∈ ℤ)}
Lemma: unordered-combination_wf
∀[T:Type]. ∀[n:ℕ]. (UnorderedCombination(n;T) ∈ Type)
Lemma: unordered-combination_functionality
∀[A,B:Type]. ∀n,m:ℕ. (A ~ B ⇒ UnorderedCombination(n;A) ~ UnorderedCombination(m;B) supposing n = m ∈ ℤ)
Lemma: subtype_rel_unordered-combination
∀[A,B:Type]. ∀n:ℕ. UnorderedCombination(n;A) ⊆r UnorderedCombination(n;B) supposing strong-subtype(A;B)
Definition: bag-incomparable
bag-incomparable(T;R;b) == ∀x,y:T. (x ↓∈ b ⇒ y ↓∈ b ⇒ (¬(x R y)))
Lemma: bag-incomparable_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[b:bag(T)]. (bag-incomparable(T;R;b) ∈ ℙ)
Definition: bag-covers
bag-covers(T;R;cvr;b) == ∀x:T. (x ↓∈ b ⇒ (x ↓∈ cvr ∨ (∃y:T. (y ↓∈ cvr ∧ (x R y)))))
Lemma: bag-covers_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[cvr,b:bag(T)]. (bag-covers(T;R;cvr;b) ∈ ℙ)
Definition: bag-cover
bag-cover(T;R;mx;b) == sub-bag(T;mx;b) ∧ bag-covers(T;R;mx;b) ∧ bag-incomparable(T;R;mx)
Lemma: bag-cover_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[cvr,b:bag(T)]. (bag-cover(T;R;cvr;b) ∈ ℙ)
Definition: monad-from
monad-from(Mnd) ==
mk-monad(functor(ob(T) = M-map(Mnd) T;
arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));
λx.M-return(Mnd);
λx,z. (M-bind(Mnd) z (λx.x)))
Lemma: monad-from_wf
∀[Mnd:Monad]. (monad-from(Mnd) ∈ Monad(TypeCat))
Definition: bag-cat-monad
bag-cat-monad() == mk-monad(functor(ob(x) = bag(x);arrow(x,y,f) = λz.bag-map(f;z));x |→ λz.{z};x |→ λz.bag-union(z))
Lemma: bag-cat-monad_wf
bag-cat-monad() ∈ Monad(TypeCat)
Definition: bag-bind
bag-bind(bs;f) == bag-union(bag-map(f;bs))
Lemma: bag-bind_wf
∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)]. (bag-bind(bs;f) ∈ bag(B))
Lemma: bag-bind-assoc
∀[A,B,C:Type]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)]. ∀[bs:bag(A)].
(bag-bind(bag-bind(bs;f);g) = bag-bind(bs;λa.bag-bind(f a;g)) ∈ bag(C))
Lemma: bag-bind-empty-right
∀A:Type. ∀ba:bag(A). (bag-bind(ba;λa.{}) ~ {})
Lemma: bag-bind-append
∀[A,B:Type]. ∀[ba,bb:bag(A)]. ∀[f:A ⟶ bag(B)]. (bag-bind(ba + bb;f) = (bag-bind(ba;f) + bag-bind(bb;f)) ∈ bag(B))
Lemma: bag-bind-append2
∀[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)].
(bag-bind(ba;λa.((F a) + (G a))) = (bag-bind(ba;F) + bag-bind(ba;G)) ∈ bag(B))
Lemma: bag-bind-com
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[ba:bag(A)]. ∀[bb:bag(B)].
(bag-bind(ba;λa.bag-bind(bb;λb.f[a;b])) = bag-bind(bb;λb.bag-bind(ba;λa.f[a;b])) ∈ bag(C))
Lemma: bag-bind-filter
∀[A,B:Type]. ∀[p:A ⟶ 𝔹]. ∀[f:{a:A| ↑p[a]} ⟶ bag(B)]. ∀[ba:bag(A)].
(bag-bind([a∈ba|p[a]];λa.f[a]) = bag-bind(ba;λa.if p[a] then f[a] else {} fi ) ∈ bag(B))
Home
Index