Axioms for the theory of proveit.core_expr_types.lambda_maps

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 Function, Lambda, Conditional, Composition
from proveit import i, a, b, c, f, g, m, x, y, z, B, Q, fx, fy, gy, gz
from proveit.core_expr_types import (
    a_1_to_i, b_1_to_i, c_1_to_i, 
    f__a_1_to_i, g__a_1_to_i, f__b_1_to_i, g__c_1_to_i,
    A_1_to_m)
#from proveit.core_expr_types.tuples import f_x
from proveit.logic import Implies, Forall, Equals
from proveit.numbers import NaturalPos

%begin axioms

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

A Lambda map is as a Lambda map does. Thus, Lambda maps are defined to be equal if they preform the same transformation under the pertinent conditions. This is similar to the proveit.logic.equality.substitution axiom except that the substitution is performed within a Lambda map which requires a special rule due to scoping restriction.

lambda_substitution = \
    Forall(i, Forall((f, g), 
                     Implies(Forall(a_1_to_i, 
                                    Equals(f__a_1_to_i, 
                                           g__a_1_to_i)),
                             Equals(Lambda(b_1_to_i, f__b_1_to_i),
                                    Lambda(c_1_to_i, g__c_1_to_i)) \
                                      .with_wrap_after_operator()).with_wrap_after_operator()),
          domain=NaturalPos)

lambda_substitution:

The unary composition of a single map is just that map.

unary_composition = \
    Forall((f, g), Equals(Composition(Lambda(x, fx)),
                          Lambda(y, fy)))

unary_composition:

Define a binary composition.

binary_composition = \
    Forall((f, g), Equals(Composition(Lambda(x, fx), Lambda(y, gy)),
                          Lambda(z, Function(f, gz))))

binary_composition:

Define an n-ary composition.

multi_composition_def = \
    Forall(m, Forall((A_1_to_m, B), 
                     Equals(Composition(A_1_to_m, B), 
                            Composition(Composition(A_1_to_m), B)).with_wrap_after_operator()),
           domain=NaturalPos)

multi_composition_def:

%end axioms

These axioms may now be imported from the theory package: proveit.core_expr_types.lambda_maps