Source code for proveit.numbers.numerals.binaries.binary_sequence

from proveit import (Literal, ExprRange, equality_prover)
from proveit.logic import is_irreducible_value
from proveit.numbers.numerals.numeral import NumeralSequence
from .bit import BITS

[docs]class BinarySequence(NumeralSequence): # operator of the BinarySequence operation. _operator_ = Literal(string_format='Binary', theory=__file__) def __init__(self, *bits, styles=None): NumeralSequence.__init__(self, BinarySequence._operator_, *bits, styles=styles) self.bits = bits for bit in self.bits: if is_irreducible_value(bit) and bit not in BITS: raise Exception( 'A BinarySequence may only be composed of bits')
[docs] @equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): """ If the BinarySequence contains an ExprRange representing a repeated digit, expand it appropriately. """ if self.bits.is_single(): return self.single_digit_reduction() for digit in self.digits: if isinstance(digit, ExprRange): # if at least one digit is an ExprRange, we can try to # reduce it to an ExprTuple return self.digit_repetition_reduction()
[docs] def as_int(self): if all(bit in BITS for bit in self.bits): return int(self.formatted('string')) raise ValueError("Cannot convert %s to an integer; the bits " "are not all irreducible values")
def _prefix(self, format_type): if format_type == 'string': return 'b' # prefix to indicate a binary representation elif format_type == 'latex': return r'\texttt{b}' else: raise ValueError("'format_type', %s, not recognized"%format_type) """ @relation_prover def deduce_in_number_set(self, number_set, **defaults_config): from proveit.numbers import Natural, NaturalPos from proveit.logic import InSet if number_set == Natural: return self.deduce_in_natural() elif number_set == NaturalPos: return self.deduce_in_natural_pos() else: try: # Do this to avoid infinite recursion -- if # we already know this numeral is in NaturalPos # we should know how to prove that it is in any # number set that contains the natural numbers. if self.as_int() > 0: InSet(self, NaturalPos).prove(automation=False) else: InSet(self, Natural).prove(automation=False) except BaseException: # Try to prove that it is in the given number # set after proving that the numeral is in # the Natural set and the NaturalPos set. self.deduce_in_natural() if self.as_int() > 0: self.deduce_in_natural_pos() return InSet(self, number_set).conclude() @relation_prover def deduce_in_natural(self, **defaults_config): from . import deci_sequence_is_nat return deci_sequence_is_nat.instantiate( {n: self.operands.num_elements(), a: self.digits}) # if Numeral._inNaturalStmts is None: # from proveit.numbers.number_sets.integers import zero_in_nats # from proveit.numbers.numerals.decimals import nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9 # Numeral._inNaturalStmts = {0: zero_in_nats, 1: nat1, 2: nat2, 3: nat3, 4: nat4, 5: nat5, 6: nat6, 7: nat7, # 8: nat8, 9: nat9} # return Numeral._inNaturalStmts[self.n] @relation_prover def deduce_in_natural_pos(self, **defaults_config): from . import deci_sequence_is_nat_pos return deci_sequence_is_nat_pos.instantiate( {n: self.operands.num_elements(), a: self.digits}) # from proveit import ProofFailure # if Numeral._inNaturalPosStmts is None: # from proveit.numbers.numerals.decimals import posnat1, posnat2, posnat3, posnat4, posnat5 # from proveit.numbers.numerals.decimals import posnat6, posnat7, posnat8, posnat9 # Numeral._inNaturalPosStmts = {1: posnat1, 2: posnat2, 3: posnat3, 4: posnat4, 5: posnat5, 6: posnat6, # 7: posnat7, 8: posnat8, 9: posnat9} # if self.n <= 0: # raise ProofFailure(self, [], # "Cannot prove %d in NaturalPos" % self.n) # return Numeral._inNaturalPosStmts[self.n] """
[docs] @equality_prover('single_bit_reduced', 'single_bit_reduce') def single_bit_reduction(self, **defaults_config): from . import single_bit_reduction if not self.bits.is_single(): raise ValueError("single_digit_reduction is only applicable " "when there is a single digit in the " "BinarySequence; not satisfied by %s"%self) return single_bit_reduction.instantiate({n:self.digits[0]})