Specification bag-union

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   bag-basic
with
   functions 
       { . } : A → Bag[A];
       . -- . : Bag[A] × A → Bag[A] prio 9 left;
       . ∪ . : Bag[A] × Bag[A] → Bag[A];
       . \ . : Bag[A] × Bag[A] → Bag[A];
       # . : Bag[A] → Nat;
       . map ( . ) : Bag[A] × (A → B) → Bag[B];
       . filter ( . ) : Bag[A] × (A → Bool) → Bag[A];
   
   predicates 
       . ∈ . : A × Bag[A];
       . ⊆ . : Bag[A] × Bag[A];
       . forall ( . ) : Bag[A] × (A → Bool);
       . exists ( . ) : Bag[A] × (A → Bool);
   
   variables 
       bag : Bag[A];
       a : A;
       b : A;
       p : A → Bool;
   
   axioms 
      forall-base: ∅.forall(p);
      used for: s, ls;
      
      forall-rec: (bag ++ a).forall(p) ↔ p(a) ∧ bag.forall(p);
      used for: s, ls;
      
      exists-base: ¬ ∅.exists(p);
      used for: s, ls;
      
      exists-rec: (bag ++ a).exists(p) ↔ p(a) ∨ bag.exists(p);
      used for: s, ls;
      
      filter-empty: ∅.filter(p) = ∅;
      used for: s, ls;
      
      filter-add: (bag ++ a).filter(p) = (p(a) ⊃ bag.filter(p) ++ a;bag.filter(p));
      used for: s, ls;
      
      map-base: ∅.map(f) = ∅;
      used for: s, ls;
      
      map-rec: (bag ++ a).map(f) ≠ bag.map(f) ++ f(a);
      used for: s, ls;
      
      size-empty: # ∅ = 0;
      used for: s, ls;
      
      size-rec: #(bag ++ a) = # bag + 1;
      used for: s, ls;
      
      del-empty: ∅ -- a = ∅;
      used for: s, ls;
      
      del-rec: (bag ++ a) -- b = (a = b ⊃ bag;(bag -- b) ++ a);
      used for: s, ls;
      
      union-empty: ∅ ∪ bag = bag;
      used for: s, ls;
      
      union-rec: (bag0 ++ a) ∪ bag1 = (bag0 ∪ bag1) ++ a;
      used for: s, ls;
      
      diff-empty: bag0 \ ∅ = bag0;
      used for: s, ls;
      
      diff-rec: bag0 \ (bag1 ++ a) = (bag0 -- a) \ bag1;
      used for: ls;
      
      one: {a}  = ∅ ++ a;
      used for: s, ls;
      
      in: a ∈ bag ↔ bag.count(a) ≠ 0;
      used for: s, ls;
      
      count-subset: bag0 ⊆ bag1 ↔ (∀ a. bag0.count(a) ≤ bag1.count(a));
      used for: ls;
   
   
end enrich