Changeset 2732


Ignore:
Timestamp:
Feb 25, 2013, 11:03:20 PM (6 years ago)
Author:
sacerdot
Message:

Unused code removed.

Location:
src/utilities/adt
Files:
3 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/adt/set_adt.ma

    r1599 r2732  
    1212axiom set_empty: ∀elt_type. set elt_type.
    1313
    14 axiom set_size: ∀elt_type. set elt_type → nat.
    15 axiom set_to_list: ∀elt_type. set elt_type → list elt_type.
    16 axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
    17 axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
    18 axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
    19 axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    20 axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    21 axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
    22 axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
    23 axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
    2414axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
    2515  set elt_type → set elt_type → bool.
    2616
    27 (* XXX: define in terms of primitives *)
    28 axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type.
     17axiom set_subset: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
     18 set elt_type → set elt_type → bool.
    2919
    30 definition set_is_empty ≝
    31   λelt_type: Type[0].
    32   λset: set elt_type.
    33     eq_nat (set_size elt_type set) 0.
     20axiom set_singleton: ∀elt_type: Type[0]. elt_type → set elt_type.
    3421
    35 definition set_singleton ≝
    36   λelt_type: Type[0].
    37   λelt     : elt_type.
    38     set_insert elt_type elt (set_empty elt_type).
     22axiom set_union: ∀elt_type: Type[0]. elt_type → elt_type → elt_type.
    3923
    40 definition set_from_list ≝
    41   λelt_type: Type[0].
    42   λthe_list: list elt_type.
    43     foldr … (set_insert elt_type) (set_empty elt_type) the_list.
     24axiom set_diff: ∀elt_type: Type[0]. elt_type → elt_type → elt_type.
    4425
    45 definition set_split ≝
    46   λelt_type: Type[0].
    47   λpred    : elt_type → bool.
    48   λthe_set : set elt_type.
    49   let left  ≝ set_filter elt_type pred the_set in
    50   let npred ≝ λx. ¬ (pred x) in
    51   let right ≝ set_filter elt_type npred the_set in
    52     〈left, right〉.
     26axiom set_from_list: ∀elt_type: Type[0]. list elt_type → set elt_type.
    5327
    54 definition set_subset ≝
    55   λelt_type: Type[0].
    56   λeq      : elt_type → elt_type → bool.
    57   λleft    : set elt_type.
    58   λright   : set elt_type.
    59     set_forall elt_type (λelt. set_member elt_type eq elt right) left.
    60 
    61 definition set_subseteq ≝
    62   λelt_type: Type[0].
    63   λeq      : elt_type → elt_type → bool.
    64   λleft    : set elt_type.
    65   λright   : set elt_type.
    66     set_equal elt_type eq left right ∧ (set_subset elt_type eq left right).
    67 
    68 definition set_union ≝
    69   λelt_type: Type[0].
    70   λleft    : set elt_type.
    71   λright   : set elt_type.
    72     set_fold elt_type (set elt_type) (set_insert elt_type) left right.
    73 
    74 definition set_intersection ≝
    75   λelt_type: Type[0].
    76   λeq      : elt_type → elt_type → bool.
    77   λleft    : set elt_type.
    78   λright   : set elt_type.
    79     set_filter elt_type (λelt. set_member elt_type eq elt right) left.
     28axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
Note: See TracChangeset for help on using the changeset viewer.