Axioms for the theory of proveit.logic.sets.enumeration

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import n, x
from proveit.logic import Forall, Equals, InSet, Set, EmptySet
from proveit.core_expr_types import y_1_to_n
from proveit.logic.sets import x_equals_any_y
from proveit.numbers import Natural
%begin axioms

Defining axioms for theory 'proveit.logic.sets.enumeration'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Membership in an enumeration is the same as being equal to any of the contents of the enumeration:

enum_set_def = Forall(n, Forall((x, y_1_to_n), 
                              Equals(InSet(x, Set(y_1_to_n)), 
                                     x_equals_any_y).with_wrapping_at(2)),
                   domain=Natural)

enum_set_def:

Define the empty set as an enumerated set with no elements.

empty_set_def = Equals(EmptySet, Set())

empty_set_def:

#
# might need an axiom here:
# if 2 enum sets are SetEquiv then they are equal
# see some hard-copy notes/comments from project meeting 2/07/2020

%end axioms

These axioms may now be imported from the theory package: proveit.logic.sets.enumeration