factor_1 Theory

The theory here is developed constructively. Some theorems computable content is `useful': e.g. mfact_exists. An instantiation of this theorem is posint_is_ufm, which has as extract, a theorem to compute prime factorisations. Other theorems have computational content which is for most purposes uninteresting. e.g. look at theorem unique_mfact.

The theorem unique_mfact nicely demonstrates rewriting with equivalence relations of differing strengths: e.g. permr and permr_upto.

Summary of Definitions

Typed Definitions

mdivides *2

rev_mdivides *1

munit *1

mpdivides *1

massoc *1

mprime *1

mprime_ty *1

mreducible *1

matomic *1

matom_ty *1

permr_massoc *1

uni_sat_upto *1

exists_uni_upto *1

permr_massoc_rel *1

is_ufm *1

posint_mul_mon *11

Main Theorems

mdivides_id *3

mdivides_refl *3

mdivides_trans *6

mdivides_preorder *4

mdivides_cancel *6

munit_char *4

munit_of_op *9

non_munit_diff_imp_mpdivides *10

mdivides_weakening *2

massoc_equiv_rel *4

massoc_weakening *6

massoc_inversion *5

massoc_transitivity *5

grp_op_ap2_functionality_wrt_massoc *5

grp_op_ap2_functionality_wrt_mdivides *4

massoc_functionality_wrt_massoc *3

massoc_cancel *3

massoc_imp_unit_diff *14

sq_stable__mprime *5

mproper_div_cond *9

mreducible_elim *16

mdivisor_of_atom_is_assoc *11

mcomp_imp_not_unit *15

mprime_imp_matomic *20

mprime_divs_list_el *17

permr_massoc_weakening *4

permr_massoc_functionality *5

cons_functionality_wrt_permr_massoc *4

mfact_exists *18

mfact_exists_a *7

unique_mfact *34

exists_uni_upto_char *5

ufm_char *12

posint_cancel *7

posint_munit_elim *5

posint_well_fnd *11

posint_reduc_dec *12

posint_unit_dec *2

posint_div_dec *1

posint_atom_imp_prime *1

posint_fact_exists *30

posint_is_ufm *6