Theory

class proveit.Theory(path='.', active_folder=None, owns_active_folder=False)

Bases: object

A Theory object provides an interface into the __pv_it database for access to the common expressions, axioms, theorems and associated proofs of a Prove-It theory. You can also store miscellaneous expressions (and their latex/png representations) generated in test/demonstration notebooks within the theory directory. These may be garbage collected via the ‘clean’ method; anything that is not associated with a common expression, axiom, theorem, or theorem proof will be garbage collected.

Attributes Summary

default
special_expr_kind_to_module_name
storages

Methods Summary

append_sub_theory_name(self, sub_theory_name)
clean_active_folder(self[, clear])	Clean the corresponding __pv_it directory of any stored expressions or proofs that have a reference count of zero.
contains_any_expression(self)	Return True if this theory and all of its sub-theories contain no expressions.
expression_notebook(expr[, …])	Return the path of the expression notebook, creating it if it does not already exist.
extract_markdowntitle_of_notebook(nb_str[, …])	Given a Prove-It notebook as a string, extract the title displayed at the top of the first markdown cell.
find_axiom(full_name)	Given the full name of an axiom that includes the theory name, return the Axiom obtained the proper Theory.
find_theorem(full_name)	Given the full name of an theorem that includes the theory name, return the Theorem obtained the proper Theory.
generate_all_contained_axioms(self)	Yield each of the axioms contained both at the local level of this theory and recursively through contained theorys.
generate_local_axioms(self)	Yield each of the axioms contained at the local level of this theory.
generate_sub_theories(self)	Yield the Theory objects for the sub-theories.
get_axiom(self, name)	Return the Axiom of the given name in this theory.
get_axiom_names(self)	Return the names of the axioms in this Theory.
get_common_expr(self, name)	Return the Expression of the common expression in this theory with the given name.
get_common_expression_names(self)	Return the names of the common expression in this Theory.
get_expression_axiom_and_theorem_names(self)	Return the names of the common expressions, axioms, theorems in this Theory.
get_expression_axiom_or_theorem_kind(self, name)	Return ‘common’, ‘axiom’, or ‘theorem’ if the given name is the name of a common expression, axiom, or theorem of this Theory respectively.
get_path(self)	Return the directory associated with the theory
get_show_proof(self, proof_id[, folder])	Return the _ShowProof representing the proof with the given id (hash string) for display purposes.
get_stored_axiom(fullname)
get_stored_expr(self, expr_id[, folder])	Return the stored Expression with the given id (hash string).
get_stored_judgment_or_proof(self, storage_id)	Return the stored Judgment or Proof with the given id (hash string).
get_stored_stmt(fullname, kind)
get_stored_theorem(fullname)
get_sub_theory_names(self)
get_theorem(self, name)	Return the Theorem of the given name in this theory.
get_theorem_names(self)	Return the names of the theorems in this Theory.
get_theory(theory_name)	Return the Theory with the given name.
is_root(self)	Return True iff this Theory is a “root” Theory (no parent directory with an __init__.py file).
links(self[, from_directory])
proof_notebook(self, proof)	Return the “basic” proof notebook corresponding to the given proof_id.
reference_hyperlinked_objects(self, name[, …])	Reference displayed expressions, recorded under the given name in the __pv_it directory.
set_active_folder(self, active_folder[, …])
set_sub_theory_names(self, sub_theory_names)
stash_extraneous_thm_proof_notebooks(self)	For any proof notebooks for theorem names not included in the theory, stash them or remove them if they are generic notebooks.
stored_common_expr_dependencies(self)	Return the stored set of theory names of common expressions referenced by the common expressions of this theory.
thm_proof_notebook(self, theorem_name, expr)	Return the path of the proof notebook for a theorem with the given name and expression, creating it if it does not already exist.
update_proving_name_if_needed(filename, …)	Check if the notebook stored in ‘filename’ has the correct name following %proving.
update_title_if_needed(filename, generic_nb_str)	Check if the notebook stored in ‘filename’ has the same markdown title as the generic version.

Attributes Documentation

default = None

special_expr_kind_to_module_name = {'axiom': '_axioms_', 'common': '_common_', 'theorem': '_theorems_'}

storages = {'c:\\users\\wwitzel\\prove-it\\packages\\proveit': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\_core_\\expression\\composite': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\_core_\\expression\\conditional': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\_core_\\expression\\label': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\_core_\\expression\\lambda_expr': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\_core_\\expression\\operation': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\abstract_algebra': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\abstract_algebra\\fields': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\abstract_algebra\\groups': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\abstract_algebra\\rings': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\core_expr_types': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\core_expr_types\\tuples': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\conjunction': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\disjunction': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\implication': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\negation': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\quantification': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\quantification\\existence': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\booleans\\quantification\\universality': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\classes': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\classes\\membership': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\equality': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\cardinality': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\cartesian_products': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\comprehension': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\disjointness': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\enumeration': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\equivalence': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\functions': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\functions\\bijections': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\functions\\images': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\functions\\injections': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\functions\\surjections': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\inclusion': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\intersection': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\membership': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\power_set': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\subtraction': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\logic\\sets\\unification': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\absolute_value': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\addition': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\divisibility': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\division': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\exponentiation': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\functions': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\integration': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\logarithms': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\modular': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\multiplication': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\negation': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\number_sets': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\number_sets\\complex_numbers': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\number_sets\\integers': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\number_sets\\natural_numbers': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\number_sets\\rational_numbers': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\number_sets\\real_numbers': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\numerals': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\numerals\\binaries': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\numerals\\decimals': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\ordering': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\product': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\rounding': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\numbers\\summation': <proveit._core_._theory_storage.TheoryStorage object>, 'c:\\users\\wwitzel\\prove-it\\packages\\proveit\\physics': <proveit._core_._theory_storage.TheoryStorage object>}

Methods Documentation

append_sub_theory_name(self, sub_theory_name)

clean_active_folder(self, clear=False)

Clean the corresponding __pv_it directory of any stored expressions or proofs that have a reference count of zero.

contains_any_expression(self)

Return True if this theory and all of its sub-theories contain no expressions.

static expression_notebook(expr, name_kind_theory=None, complete_special_expr_notebook=False)

Return the path of the expression notebook, creating it if it does not already exist. If ‘name_kind_theory’ is provided, it should be the (name, kind, theory) for a special expression that may or may not be complete/official (%end_[common/axioms/theorems] has not been called yet in the special expressions notebook).

static extract_markdowntitle_of_notebook(nb_str, replace_str=None)

Given a Prove-It notebook as a string, extract the title displayed at the top of the first markdown cell. If a ‘replace_str’ is given, then replace this title with the given replacement string and also return this replacement.

static find_axiom(full_name)

Given the full name of an axiom that includes the theory name, return the Axiom obtained the proper Theory.

static find_theorem(full_name)

Given the full name of an theorem that includes the theory name, return the Theorem obtained the proper Theory.

generate_all_contained_axioms(self)

Yield each of the axioms contained both at the local level of this theory and recursively through contained theorys.

generate_local_axioms(self)

Yield each of the axioms contained at the local level of this theory.

generate_sub_theories(self)

Yield the Theory objects for the sub-theories.

get_axiom(self, name)

Return the Axiom of the given name in this theory.

get_axiom_names(self)

Return the names of the axioms in this Theory.

get_common_expr(self, name)

Return the Expression of the common expression in this theory with the given name.

get_common_expression_names(self)

Return the names of the common expression in this Theory.

get_expression_axiom_and_theorem_names(self)

Return the names of the common expressions, axioms, theorems in this Theory.

get_expression_axiom_or_theorem_kind(self, name)

Return ‘common’, ‘axiom’, or ‘theorem’ if the given name is the name of a common expression, axiom, or theorem of this Theory respectively.

get_path(self)

Return the directory associated with the theory

get_show_proof(self, proof_id, folder=None)

Return the _ShowProof representing the proof with the given id (hash string) for display purposes. Use the “active folder” as the default folder.

static get_stored_axiom(fullname)

get_stored_expr(self, expr_id, folder=None)

Return the stored Expression with the given id (hash string). Use the “active folder” as the default folder.

get_stored_judgment_or_proof(self, storage_id, folder=None)

Return the stored Judgment or Proof with the given id (hash string). Use the “active folder” as the default folder.

static get_stored_stmt(fullname, kind)

static get_stored_theorem(fullname)

get_sub_theory_names(self)

get_theorem(self, name)

Return the Theorem of the given name in this theory.

get_theorem_names(self)

Return the names of the theorems in this Theory.

static get_theory(theory_name)

Return the Theory with the given name.

is_root(self)

Return True iff this Theory is a “root” Theory (no parent directory with an __init__.py file).

links(self, from_directory='.')

proof_notebook(self, proof)

Return the “basic” proof notebook corresponding to the given proof_id. Note, this is different than a “theorem” proof notebook which generates the proof. This just shows the proof as Prove-It stores it.

reference_hyperlinked_objects(self, name, clear=False)

Reference displayed expressions, recorded under the given name in the __pv_it directory. If the same name is reused, any expressions that are not displayed this time that were displayed last time will be unreferenced. If clear is True, remove all of the references and the file that stores these references.

set_active_folder(self, active_folder, owns_active_folder=False)

set_sub_theory_names(self, sub_theory_names)

stash_extraneous_thm_proof_notebooks(self)

For any proof notebooks for theorem names not included in the theory, stash them or remove them if they are generic notebooks.

stored_common_expr_dependencies(self)

Return the stored set of theory names of common expressions referenced by the common expressions of this theory.

thm_proof_notebook(self, theorem_name, expr, num_duplicates=0)

Return the path of the proof notebook for a theorem with the given name and expression, creating it if it does not already exist. num_duplicates is the number of previous instances of the expression that we have encountered.

static update_proving_name_if_needed(filename, theorem_name)

Check if the notebook stored in ‘filename’ has the correct name following %proving. If not, fix it. Return the possibly updated notebook string, or None if it file was not in an expected format to be able to extract the title.

static update_title_if_needed(filename, generic_nb_str)

Check if the notebook stored in ‘filename’ has the same markdown title as the generic version. If not, update it to the generic version. Return the possibly updated notebook string, or None if it file was not in an expected format to be able to extract the title.