Ignore:
Timestamp:
Sep 14, 2011, 4:04:53 PM (9 years ago)
Author:
mulligan
Message:

getting rid of typeclass-like records in favour of file-level axioms. much too heavyweight to use effectively

File:
1 edited

Legend:

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

    r1208 r1210  
    55include "utilities/adt/ordering.ma".
    66
    7 record set_adt
    8   (elt_type: Type[0]) (order: ordered elt_type): Type[1] ≝
    9 {
    10   set        : Type[0] → Type[0];
    11  
    12   set_empty  : set elt_type;
    13   set_size   : set elt_type → nat;
    14  
    15   set_to_list: set elt_type → list elt_type;
    16  
    17   set_insert : elt_type → set elt_type → set elt_type;
    18   set_remove : elt_type → set elt_type → set elt_type;
    19  
    20   set_member : elt_type → set elt_type → bool;
    21  
    22   set_forall : (elt_type → bool) → set elt_type → bool;
    23   set_exists : (elt_type → bool) → set elt_type → bool;
    24   set_filter : (elt_type → bool) → set elt_type → set elt_type;
    25  
    26   set_equal  : set elt_type → set elt_type → bool;
    27  
    28   set_map    : ∀a: Type[0]. (elt_type → a) → set elt_type → set a;
    29   set_fold   : ∀a: Type[0]. (elt_type → a → a) → set elt_type  → a → a
    30 }.
     7axiom set: Type[0] → Type[0].
     8axiom set_empty: ∀elt_type. set elt_type.
     9
     10axiom set_size: ∀elt_type. set elt_type → nat.
     11axiom set_to_list: ∀elt_type. set elt_type → list elt_type.
     12axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
     13axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
     14axiom set_member: ∀elt_type. elt_type → set elt_type → bool.
     15axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
     16axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
     17axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
     18axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.
     19axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
     20axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
    3121
    3222definition set_is_empty ≝
    3323  λelt_type: Type[0].
    34   λorder   : ordered elt_type.
    35   λset_adt : set_adt elt_type order.
    36   λset     : set elt_type order set_adt elt_type.
    37     set_size … set = 0.
     24  λset: set elt_type.
     25    set_size elt_type set = 0.
    3826
    3927definition set_singleton ≝
    4028  λelt_type: Type[0].
    41   λorder   : ordered elt_type.
    42   λset_adt : set_adt elt_type order.
    4329  λelt     : elt_type.
    44     set_insert … elt (set_empty elt_type order set_adt).
     30    set_insert elt_type elt (set_empty elt_type).
    4531
    4632definition set_from_list ≝
    4733  λelt_type: Type[0].
    48   λorder   : ordered elt_type.
    49   λset_adt : set_adt elt_type order.
    5034  λthe_list: list elt_type.
    51     foldr … (set_insert elt_type order set_adt) (set_empty …) the_list.
     35    foldr … (set_insert elt_type) (set_empty elt_type) the_list.
    5236
    5337definition set_split ≝
    5438  λelt_type: Type[0].
    55   λorder   : ordered elt_type.
    56   λset_adt : set_adt elt_type order.
    5739  λpred    : elt_type → bool.
    58   λthe_set : set elt_type order set_adt elt_type.
    59   let left  ≝ set_filter elt_type order set_adt pred the_set in
     40  λthe_set : set elt_type.
     41  let left  ≝ set_filter elt_type pred the_set in
    6042  let npred ≝ λx. ¬ (pred x) in
    61   let right ≝ set_filter elt_type order set_adt npred the_set in
     43  let right ≝ set_filter elt_type npred the_set in
    6244    〈left, right〉.
    6345
    6446definition set_subset ≝
    6547  λelt_type: Type[0].
    66   λorder   : ordered elt_type.
    67   λset_adt : set_adt elt_type order.
    68   λleft    : set elt_type order set_adt elt_type.
    69   λright   : set elt_type order set_adt elt_type.
    70     set_forall … (λelt. set_member … elt right) left.
     48  λleft    : set elt_type.
     49  λright   : set elt_type.
     50    set_forall elt_type (λelt. set_member elt_type elt right) left.
    7151
    7252definition set_subseteq ≝
    7353  λelt_type: Type[0].
    74   λorder   : ordered elt_type.
    75   λset_adt : set_adt elt_type order.
    76   λleft    : set elt_type order set_adt elt_type.
    77   λright   : set elt_type order set_adt elt_type.
    78     set_equal … left right ∧ (set_subset elt_type order set_adt left right).
     54  λleft    : set elt_type.
     55  λright   : set elt_type.
     56    set_equal elt_type left right ∧ (set_subset elt_type left right).
    7957
    8058definition set_union ≝
    8159  λelt_type: Type[0].
    82   λorder   : ordered elt_type.
    83   λset_adt : set_adt elt_type order.
    84   λleft    : set elt_type order set_adt elt_type.
    85   λright   : set elt_type order set_adt elt_type.
    86     set_fold … (set_insert elt_type order set_adt) left right.
     60  λleft    : set elt_type.
     61  λright   : set elt_type.
     62    set_fold elt_type (set elt_type) (set_insert elt_type) left right.
    8763
    8864definition set_intersection ≝
    8965  λelt_type: Type[0].
    90   λelt_type: Type[0].
    91   λorder   : ordered elt_type.
    92   λset_adt : set_adt elt_type order.
    93   λleft    : set elt_type order set_adt elt_type.
    94   λright   : set elt_type order set_adt elt_type.
    95     set_filter … (λelt. set_member … elt right) left.
     66  λleft    : set elt_type.
     67  λright   : set elt_type.
     68    set_filter elt_type (λelt. set_member elt_type elt right) left.
Note: See TracChangeset for help on using the changeset viewer.