Structure monoidTheory
signature monoidTheory =
sig
type thm = Thm.thm
(* Definitions *)
val AbelianMonoid_def : thm
val FiniteAbelianMonoid_def : thm
val FiniteMonoid_def : thm
val GPROD_SET_def : thm
val Invertibles_def : thm
val MonoidAuto_def : thm
val MonoidEndo_def : thm
val MonoidHomo_def : thm
val MonoidIso_def : thm
val Monoid_def : thm
val Submonoid_def : thm
val WeakHomo_def : thm
val WeakIso_def : thm
val addition_monoid_def : thm
val extend_def : thm
val homo_monoid_def : thm
val image_op_def : thm
val lists_def : thm
val monoid_TY_DEF : thm
val monoid_case_def : thm
val monoid_exp_def : thm
val monoid_inj_image_def : thm
val monoid_intersect_def : thm
val monoid_inv_def : thm
val monoid_invertibles_def : thm
val monoid_size_def : thm
val multiplication_monoid_def : thm
val order_def : thm
val orders_def : thm
val period_def : thm
val plus_mod_def : thm
val power_monoid_def : thm
val recordtype_monoid_seldef_carrier_def : thm
val recordtype_monoid_seldef_carrier_fupd_def : thm
val recordtype_monoid_seldef_id_def : thm
val recordtype_monoid_seldef_id_fupd_def : thm
val recordtype_monoid_seldef_op_def : thm
val recordtype_monoid_seldef_op_fupd_def : thm
val set_inter_def : thm
val set_union_def : thm
val submonoid_big_intersect_def : thm
val submonoid_def : thm
val times_mod_def : thm
val trivial_monoid_def : thm
(* Theorems *)
val COMMUTING_GITBAG_INSERT : thm
val COMMUTING_GITSET_INSERT : thm
val COMMUTING_GITSET_RECURSES : thm
val COMMUTING_GITSET_REDUCTION : thm
val EXISTS_monoid : thm
val FORALL_monoid : thm
val FiniteAbelianMonoid_def_alt : thm
val GBAG_IMAGE_FILTER : thm
val GBAG_IMAGE_PARTITION : thm
val GBAG_INSERT : thm
val GBAG_PARTITION : thm
val GBAG_UNION : thm
val GBAG_in_carrier : thm
val GITBAG_BAG_IMAGE_op : thm
val GITBAG_CONG : thm
val GITBAG_EMPTY : thm
val GITBAG_GBAG : thm
val GITBAG_INSERT : thm
val GITBAG_INSERT_THM : thm
val GITBAG_THM : thm
val GITBAG_UNION : thm
val GITBAG_in_carrier : thm
val GITBAG_same_op : thm
val GITSET_EMPTY : thm
val GITSET_INSERT : thm
val GITSET_PROPERTY : thm
val GITSET_THM : thm
val GPROD_SET_EMPTY : thm
val GPROD_SET_PROPERTY : thm
val GPROD_SET_SING : thm
val GPROD_SET_THM : thm
val IMP_GBAG_EQ_EXP : thm
val IMP_GBAG_EQ_ID : thm
val Invertibles_carrier : thm
val Invertibles_order : thm
val Invertibles_property : thm
val Invertibles_subset : thm
val MonoidHomo_GBAG : thm
val SUBSET_COMMUTING_ITBAG_INSERT : thm
val abelian_monoid_op_closure_comm_assoc_fun : thm
val abelian_monoid_order_common : thm
val abelian_monoid_order_common_coprime : thm
val abelian_monoid_order_lcm : thm
val addition_monoid_abelian_monoid : thm
val addition_monoid_monoid : thm
val addition_monoid_property : thm
val datatype_monoid : thm
val extend_carrier : thm
val extend_id : thm
val extend_is_monoid : thm
val extend_op : thm
val finite_monoid_exp_not_distinct : thm
val homo_monoid_I : thm
val homo_monoid_abelian_monoid : thm
val homo_monoid_assoc : thm
val homo_monoid_by_inj : thm
val homo_monoid_closure : thm
val homo_monoid_comm : thm
val homo_monoid_element : thm
val homo_monoid_id : thm
val homo_monoid_id_property : thm
val homo_monoid_monoid : thm
val homo_monoid_op_inj : thm
val homo_monoid_property : thm
val image_op_inj : thm
val lists_monoid : thm
val maximal_order_alt : thm
val monoid_11 : thm
val monoid_Axiom : thm
val monoid_accessors : thm
val monoid_accfupds : thm
val monoid_assoc : thm
val monoid_auto_I : thm
val monoid_auto_bij : thm
val monoid_auto_compose : thm
val monoid_auto_element : thm
val monoid_auto_exp : thm
val monoid_auto_id : thm
val monoid_auto_linv_auto : thm
val monoid_auto_order : thm
val monoid_carrier_nonempty : thm
val monoid_case_cong : thm
val monoid_case_eq : thm
val monoid_comm_exp : thm
val monoid_comm_exp_exp : thm
val monoid_comm_op_exp : thm
val monoid_component_equality : thm
val monoid_exp_0 : thm
val monoid_exp_1 : thm
val monoid_exp_SUC : thm
val monoid_exp_add : thm
val monoid_exp_comm : thm
val monoid_exp_element : thm
val monoid_exp_mod_order : thm
val monoid_exp_mult : thm
val monoid_exp_mult_comm : thm
val monoid_exp_suc : thm
val monoid_fn_updates : thm
val monoid_fupdcanon : thm
val monoid_fupdcanon_comp : thm
val monoid_fupdfupds : thm
val monoid_fupdfupds_comp : thm
val monoid_homo_I_refl : thm
val monoid_homo_compose : thm
val monoid_homo_cong : thm
val monoid_homo_element : thm
val monoid_homo_exp : thm
val monoid_homo_id : thm
val monoid_homo_sym : thm
val monoid_homo_sym_any : thm
val monoid_homo_trans : thm
val monoid_id : thm
val monoid_id_element : thm
val monoid_id_exp : thm
val monoid_id_id : thm
val monoid_id_invertible : thm
val monoid_id_unique : thm
val monoid_induction : thm
val monoid_inj_image_abelian_monoid : thm
val monoid_inj_image_monoid : thm
val monoid_inj_image_monoid_homo : thm
val monoid_intersect_element : thm
val monoid_intersect_id : thm
val monoid_intersect_property : thm
val monoid_inv_def_alt : thm
val monoid_inv_element : thm
val monoid_inv_from_invertibles : thm
val monoid_inv_invertible : thm
val monoid_inv_op_invertible : thm
val monoid_invertibles_element : thm
val monoid_invertibles_is_monoid : thm
val monoid_iso_I_refl : thm
val monoid_iso_bij : thm
val monoid_iso_card_eq : thm
val monoid_iso_compose : thm
val monoid_iso_element : thm
val monoid_iso_eq_id : thm
val monoid_iso_exp : thm
val monoid_iso_id : thm
val monoid_iso_linv_iso : thm
val monoid_iso_monoid : thm
val monoid_iso_order : thm
val monoid_iso_property : thm
val monoid_iso_sym : thm
val monoid_iso_trans : thm
val monoid_lid : thm
val monoid_lid_unique : thm
val monoid_literal_11 : thm
val monoid_literal_nchotomy : thm
val monoid_nchotomy : thm
val monoid_op_element : thm
val monoid_order_cofactor : thm
val monoid_order_common : thm
val monoid_order_common_coprime : thm
val monoid_order_condition : thm
val monoid_order_divides_exp : thm
val monoid_order_divides_maximal : thm
val monoid_order_divisor : thm
val monoid_order_eq_1 : thm
val monoid_order_id : thm
val monoid_order_nonzero : thm
val monoid_order_power : thm
val monoid_order_power_coprime : thm
val monoid_order_power_eq_0 : thm
val monoid_order_power_eqn : thm
val monoid_rid : thm
val monoid_rid_unique : thm
val monoid_updates_eq_literal : thm
val monoid_weak_iso_id : thm
val multiplication_monoid_abelian_monoid : thm
val multiplication_monoid_monoid : thm
val multiplication_monoid_property : thm
val order_alt : thm
val order_eq_0 : thm
val order_minimal : thm
val order_period : thm
val order_property : thm
val order_thm : thm
val orders_element : thm
val orders_eq_1 : thm
val orders_finite : thm
val orders_subset : thm
val plus_mod_abelian_monoid : thm
val plus_mod_exp : thm
val plus_mod_finite : thm
val plus_mod_finite_abelian_monoid : thm
val plus_mod_finite_monoid : thm
val plus_mod_monoid : thm
val plus_mod_property : thm
val power_monoid_abelian_monoid : thm
val power_monoid_monoid : thm
val power_monoid_property : thm
val power_to_addition_homo : thm
val power_to_addition_iso : thm
val set_inter_abelian_monoid : thm
val set_inter_monoid : thm
val set_union_abelian_monoid : thm
val set_union_monoid : thm
val submonoid_I_antisym : thm
val submonoid_alt : thm
val submonoid_antisymmetric : thm
val submonoid_big_intersect_element : thm
val submonoid_big_intersect_has_id : thm
val submonoid_big_intersect_monoid : thm
val submonoid_big_intersect_op_element : thm
val submonoid_big_intersect_property : thm
val submonoid_big_intersect_submonoid : thm
val submonoid_big_intersect_subset : thm
val submonoid_carrier_antisym : thm
val submonoid_carrier_subset : thm
val submonoid_element : thm
val submonoid_eqn : thm
val submonoid_exp : thm
val submonoid_homo_homo : thm
val submonoid_homomorphism : thm
val submonoid_id : thm
val submonoid_intersect_monoid : thm
val submonoid_intersect_property : thm
val submonoid_intersect_submonoid : thm
val submonoid_monoid : thm
val submonoid_op : thm
val submonoid_order : thm
val submonoid_order_eqn : thm
val submonoid_property : thm
val submonoid_refl : thm
val submonoid_reflexive : thm
val submonoid_subset : thm
val submonoid_trans : thm
val submonoid_transitive : thm
val times_mod_abelian_monoid : thm
val times_mod_eval : thm
val times_mod_exp : thm
val times_mod_finite : thm
val times_mod_finite_abelian_monoid : thm
val times_mod_finite_monoid : thm
val times_mod_monoid : thm
val times_mod_property : thm
val trivial_monoid : thm
(*
[bag] Parent theory of "monoid"
[prime] Parent theory of "monoid"
[AbelianMonoid_def] Definition
⊢ ∀g. AbelianMonoid g ⇔
Monoid g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x
[FiniteAbelianMonoid_def] Definition
⊢ ∀g. FiniteAbelianMonoid g ⇔ AbelianMonoid g ∧ FINITE G
[FiniteMonoid_def] Definition
⊢ ∀g. FiniteMonoid g ⇔ Monoid g ∧ FINITE G
[GPROD_SET_def] Definition
⊢ ∀g s. GPROD_SET g s = GITSET g s #e
[Invertibles_def] Definition
⊢ ∀g. Invertibles g = <|carrier := G*; op := $*; id := #e|>
[MonoidAuto_def] Definition
⊢ ∀f g. MonoidAuto f g ⇔ MonoidIso f g g
[MonoidEndo_def] Definition
⊢ ∀f g. MonoidEndo f g ⇔ MonoidHomo f g g
[MonoidHomo_def] Definition
⊢ ∀f g h.
MonoidHomo f g h ⇔
(∀x. x ∈ G ⇒ f x ∈ h.carrier) ∧
(∀x y. x ∈ G ∧ y ∈ G ⇒ f (x * y) = h.op (f x) (f y)) ∧
f #e = h.id
[MonoidIso_def] Definition
⊢ ∀f g h. MonoidIso f g h ⇔ MonoidHomo f g h ∧ BIJ f G h.carrier
[Monoid_def] Definition
⊢ ∀g. Monoid g ⇔
(∀x y. x ∈ G ∧ y ∈ G ⇒ x * y ∈ G) ∧
(∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * y * z = x * (y * z)) ∧
#e ∈ G ∧ ∀x. x ∈ G ⇒ #e * x = x ∧ x * #e = x
[Submonoid_def] Definition
⊢ ∀h g. h << g ⇔ Monoid h ∧ Monoid g ∧ H ⊆ G ∧ $o = $* ∧ #i = #e
[WeakHomo_def] Definition
⊢ ∀f g h.
WeakHomo f g h ⇔
(∀x. x ∈ G ⇒ f x ∈ h.carrier) ∧
∀x y. x ∈ G ∧ y ∈ G ⇒ f (x * y) = h.op (f x) (f y)
[WeakIso_def] Definition
⊢ ∀f g h. WeakIso f g h ⇔ WeakHomo f g h ∧ BIJ f G h.carrier
[addition_monoid_def] Definition
⊢ addition_monoid = <|carrier := 𝕌(:num); op := $+; id := 0|>
[extend_def] Definition
⊢ ∀m. extend m =
<|carrier := 𝕌(:α); id := m.id;
op :=
(λx y.
if x ∈ m.carrier then
if y ∈ m.carrier then m.op x y else y
else x)|>
[homo_monoid_def] Definition
⊢ ∀g f.
homo_monoid g f =
<|carrier := IMAGE f G; op := image_op g f; id := f #e|>
[image_op_def] Definition
⊢ ∀g f x y.
image_op g f x y =
f (CHOICE (preimage f G x) * CHOICE (preimage f G y))
[lists_def] Definition
⊢ lists = <|carrier := 𝕌(:α list); id := []; op := $++ |>
[monoid_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('monoid').
(∀a0'.
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR 0 (a0,a1,a2)
(λn. ind_type$BOTTOM)) a0 a1 a2) ⇒
$var$('monoid') a0') ⇒
$var$('monoid') a0') rep
[monoid_case_def] Definition
⊢ ∀a0 a1 a2 f. monoid_CASE (monoid a0 a1 a2) f = f a0 a1 a2
[monoid_exp_def] Definition
⊢ ∀g x n. x ** n = FUNPOW ($* x) n #e
[monoid_inj_image_def] Definition
⊢ ∀g f.
monoid_inj_image g f =
<|carrier := IMAGE f G;
op := (let t = LINV f G in λx y. f (t x * t y)); id := f #e|>
[monoid_intersect_def] Definition
⊢ ∀g h. (g mINTER h) = <|carrier := G ∩ H; op := $*; id := #e|>
[monoid_inv_def] Definition
⊢ ∀g x. Monoid g ∧ x ∈ G* ⇒ |/ x ∈ G ∧ x * |/ x = #e ∧ |/ x * x = #e
[monoid_invertibles_def] Definition
⊢ ∀g. G* = {x | x ∈ G ∧ ∃y. y ∈ G ∧ x * y = #e ∧ y * x = #e}
[monoid_size_def] Definition
⊢ ∀f a0 a1 a2. monoid_size f (monoid a0 a1 a2) = 1 + f a2
[multiplication_monoid_def] Definition
⊢ multiplication_monoid = <|carrier := 𝕌(:num); op := $*; id := 1|>
[order_def] Definition
⊢ ∀g x.
ord x = case OLEAST k. period g x k of NONE => 0 | SOME k => k
[orders_def] Definition
⊢ ∀g n. orders g n = {x | x ∈ G ∧ ord x = n}
[period_def] Definition
⊢ ∀g x k. period g x k ⇔ 0 < k ∧ x ** k = #e
[plus_mod_def] Definition
⊢ ∀n. plus_mod n =
<|carrier := count n; id := 0; op := (λi j. (i + j) MOD n)|>
[power_monoid_def] Definition
⊢ ∀b. power_monoid b =
<|carrier := {b ** j | j ∈ 𝕌(:num)}; op := $*; id := 1|>
[recordtype_monoid_seldef_carrier_def] Definition
⊢ ∀f f0 a. (monoid f f0 a).carrier = f
[recordtype_monoid_seldef_carrier_fupd_def] Definition
⊢ ∀f1 f f0 a.
monoid f f0 a with carrier updated_by f1 = monoid (f1 f) f0 a
[recordtype_monoid_seldef_id_def] Definition
⊢ ∀f f0 a. (monoid f f0 a).id = a
[recordtype_monoid_seldef_id_fupd_def] Definition
⊢ ∀f1 f f0 a.
monoid f f0 a with id updated_by f1 = monoid f f0 (f1 a)
[recordtype_monoid_seldef_op_def] Definition
⊢ ∀f f0 a. (monoid f f0 a).op = f0
[recordtype_monoid_seldef_op_fupd_def] Definition
⊢ ∀f1 f f0 a.
monoid f f0 a with op updated_by f1 = monoid f (f1 f0) a
[set_inter_def] Definition
⊢ set_inter = <|carrier := 𝕌(:α -> bool); id := 𝕌(:α); op := $INTER|>
[set_union_def] Definition
⊢ set_union = <|carrier := 𝕌(:α -> bool); id := ∅; op := $UNION|>
[submonoid_big_intersect_def] Definition
⊢ ∀g. smbINTER g =
<|carrier := BIGINTER (IMAGE (λh. H) {h | h << g}); op := $*;
id := #e|>
[submonoid_def] Definition
⊢ ∀h g. submonoid h g ⇔ MonoidHomo I h g
[times_mod_def] Definition
⊢ ∀n. times_mod n =
<|carrier := count n; id := if n = 1 then 0 else 1;
op := (λi j. (i * j) MOD n)|>
[trivial_monoid_def] Definition
⊢ ∀e. trivial_monoid e = <|carrier := {e}; id := e; op := (λx y. e)|>
[COMMUTING_GITBAG_INSERT] Theorem
⊢ ∀g b.
AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ⇒
∀x a::G. GITBAG g (BAG_INSERT x b) a = GITBAG g b (x * a)
[COMMUTING_GITSET_INSERT] Theorem
⊢ ∀g s.
AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
∀b x::G. GITSET g (x INSERT s) b = GITSET g (s DELETE x) (x * b)
[COMMUTING_GITSET_RECURSES] Theorem
⊢ ∀g s.
AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
∀b x::G. GITSET g (x INSERT s) b = x * GITSET g (s DELETE x) b
[COMMUTING_GITSET_REDUCTION] Theorem
⊢ ∀g s.
AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
∀b x::G. GITSET g s (x * b) = x * GITSET g s b
[EXISTS_monoid] Theorem
⊢ ∀P. (∃m. P m) ⇔ ∃f0 f a. P <|carrier := f0; op := f; id := a|>
[FORALL_monoid] Theorem
⊢ ∀P. (∀m. P m) ⇔ ∀f0 f a. P <|carrier := f0; op := f; id := a|>
[FiniteAbelianMonoid_def_alt] Theorem
⊢ ∀g. FiniteAbelianMonoid g ⇔
FiniteMonoid g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x
[GBAG_IMAGE_FILTER] Theorem
⊢ AbelianMonoid g ⇒
∀b. FINITE_BAG b ⇒
IMAGE f (SET_OF_BAG b ∩ P) ⊆ G ⇒
GBAG g (BAG_IMAGE f (BAG_FILTER P b)) =
GBAG g (BAG_IMAGE (λx. if P x then f x else #e) b)
[GBAG_IMAGE_PARTITION] Theorem
⊢ AbelianMonoid g ∧ FINITE s ⇒
∀b. FINITE_BAG b ⇒
IMAGE f (SET_OF_BAG b) ⊆ G ∧ (∀x. x ⋲ b ⇒ ∃P. P ∈ s ∧ P x) ∧
(∀x P1 P2. x ⋲ b ∧ P1 ∈ s ∧ P2 ∈ s ∧ P1 x ∧ P2 x ⇒ P1 = P2) ⇒
GBAG g
(BAG_IMAGE (λP. GBAG g (BAG_IMAGE f (BAG_FILTER P b)))
(BAG_OF_SET s)) =
GBAG g (BAG_IMAGE f b)
[GBAG_INSERT] Theorem
⊢ AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ∧ x ∈ G ⇒
GBAG g (BAG_INSERT x b) = x * GBAG g b
[GBAG_PARTITION] Theorem
⊢ AbelianMonoid g ∧ FINITE s ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ∧
(∀x. x ⋲ b ⇒ ∃P. P ∈ s ∧ P x) ∧
(∀x P1 P2. x ⋲ b ∧ P1 ∈ s ∧ P2 ∈ s ∧ P1 x ∧ P2 x ⇒ P1 = P2) ⇒
GBAG g (BAG_IMAGE (λP. GBAG g (BAG_FILTER P b)) (BAG_OF_SET s)) =
GBAG g b
[GBAG_UNION] Theorem
⊢ AbelianMonoid g ∧ FINITE_BAG b1 ∧ FINITE_BAG b2 ∧
SET_OF_BAG b1 ⊆ G ∧ SET_OF_BAG b2 ⊆ G ⇒
GBAG g (b1 ⊎ b2) = GBAG g b1 * GBAG g b2
[GBAG_in_carrier] Theorem
⊢ ∀g b.
AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ⇒ GBAG g b ∈ G
[GITBAG_BAG_IMAGE_op] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀b. FINITE_BAG b ⇒
∀p q a.
IMAGE p (SET_OF_BAG b) ⊆ G ∧ IMAGE q (SET_OF_BAG b) ⊆ G ∧
a ∈ G ⇒
GITBAG g (BAG_IMAGE (λx. p x * q x) b) a =
GITBAG g (BAG_IMAGE p b) a * GBAG g (BAG_IMAGE q b)
[GITBAG_CONG] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀b. FINITE_BAG b ⇒
∀b' a a'.
FINITE_BAG b' ∧ a ∈ G ∧ SET_OF_BAG b ⊆ G ∧
SET_OF_BAG b' ⊆ G ∧
(∀x. x ⋲ b ⊎ b' ∧ x ≠ #e ⇒ b x = b' x) ⇒
GITBAG g b a = GITBAG g b' a
[GITBAG_EMPTY] Theorem
⊢ ∀g a. GITBAG g {||} a = a
[GITBAG_GBAG] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀b. FINITE_BAG b ⇒
∀a. a ∈ G ∧ SET_OF_BAG b ⊆ G ⇒ GITBAG g b a = a * GBAG g b
[GITBAG_INSERT] Theorem
⊢ ∀b. FINITE_BAG b ⇒
∀g x a.
GITBAG g (BAG_INSERT x b) a =
GITBAG g (BAG_REST (BAG_INSERT x b))
(BAG_CHOICE (BAG_INSERT x b) * a)
[GITBAG_INSERT_THM] Theorem
⊢ ∀g b x a.
(AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G) ∧ x ∈ G ∧
a ∈ G ⇒
GITBAG g (BAG_INSERT x b) a = GITBAG g b (x * a)
[GITBAG_THM] Theorem
⊢ ∀g b acc.
FINITE_BAG b ⇒
GITBAG g b acc =
if b = {||} then acc
else GITBAG g (BAG_REST b) (BAG_CHOICE b * acc)
[GITBAG_UNION] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀b1.
FINITE_BAG b1 ⇒
∀b2.
FINITE_BAG b2 ∧ SET_OF_BAG b1 ⊆ G ∧ SET_OF_BAG b2 ⊆ G ⇒
∀a. a ∈ G ⇒
GITBAG g (b1 ⊎ b2) a = GITBAG g b2 (GITBAG g b1 a)
[GITBAG_in_carrier] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀b. FINITE_BAG b ⇒
∀a. SET_OF_BAG b ⊆ G ∧ a ∈ G ⇒ GITBAG g b a ∈ G
[GITBAG_same_op] Theorem
⊢ g1.op = g2.op ⇒
∀b. FINITE_BAG b ⇒ ∀a. GITBAG g1 b a = GITBAG g2 b a
[GITSET_EMPTY] Theorem
⊢ ∀g b. GITSET g ∅ b = b
[GITSET_INSERT] Theorem
⊢ ∀s. FINITE s ⇒
∀x g b.
GITSET g (x INSERT s) b =
GITSET g (REST (x INSERT s)) (CHOICE (x INSERT s) * b)
[GITSET_PROPERTY] Theorem
⊢ ∀g s.
FINITE s ∧ s ≠ ∅ ⇒
∀b. GITSET g s b = GITSET g (REST s) (CHOICE s * b)
[GITSET_THM] Theorem
⊢ ∀s g b.
FINITE s ⇒
GITSET g s b =
if s = ∅ then b else GITSET g (REST s) (CHOICE s * b)
[GPROD_SET_EMPTY] Theorem
⊢ ∀g s. GPROD_SET g ∅ = #e
[GPROD_SET_PROPERTY] Theorem
⊢ ∀g s. AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒ GPROD_SET g s ∈ G
[GPROD_SET_SING] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ GPROD_SET g {x} = x
[GPROD_SET_THM] Theorem
⊢ ∀g s.
GPROD_SET g ∅ = #e ∧
(AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
∀x::G. GPROD_SET g (x INSERT s) = x * GPROD_SET g (s DELETE x))
[IMP_GBAG_EQ_EXP] Theorem
⊢ AbelianMonoid g ∧ x ∈ G ∧ SET_OF_BAG b ⊆ {x} ⇒ GBAG g b = x ** b x
[IMP_GBAG_EQ_ID] Theorem
⊢ AbelianMonoid g ⇒ ∀b. BAG_EVERY ($= #e) b ⇒ GBAG g b = #e
[Invertibles_carrier] Theorem
⊢ ∀g. (Invertibles g).carrier = G*
[Invertibles_order] Theorem
⊢ ∀g x. order (Invertibles g) x = ord x
[Invertibles_property] Theorem
⊢ ∀g. (Invertibles g).carrier = G* ∧ (Invertibles g).op = $* ∧
(Invertibles g).id = #e ∧ (Invertibles g).exp = $**
[Invertibles_subset] Theorem
⊢ ∀g. (Invertibles g).carrier ⊆ G
[MonoidHomo_GBAG] Theorem
⊢ AbelianMonoid g ∧ AbelianMonoid h ∧ MonoidHomo f g h ∧
FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ⇒
f (GBAG g b) = GBAG h (BAG_IMAGE f b)
[SUBSET_COMMUTING_ITBAG_INSERT] Theorem
⊢ ∀f b t.
SET_OF_BAG b ⊆ t ∧ closure_comm_assoc_fun f t ∧ FINITE_BAG b ⇒
∀x a::t. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)
[abelian_monoid_op_closure_comm_assoc_fun] Theorem
⊢ ∀g. AbelianMonoid g ⇒ closure_comm_assoc_fun $* G
[abelian_monoid_order_common] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ⇒
∃z. z ∈ G ∧ ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)
[abelian_monoid_order_common_coprime] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ coprime (ord x) (ord y) ⇒
∃z. z ∈ G ∧ ord z = ord x * ord y
[abelian_monoid_order_lcm] Theorem
⊢ ∀g. AbelianMonoid g ⇒
∀x y. x ∈ G ∧ y ∈ G ⇒ ∃z. z ∈ G ∧ ord z = lcm (ord x) (ord y)
[addition_monoid_abelian_monoid] Theorem
⊢ AbelianMonoid addition_monoid
[addition_monoid_monoid] Theorem
⊢ Monoid addition_monoid
[addition_monoid_property] Theorem
⊢ addition_monoid.carrier = 𝕌(:num) ∧ addition_monoid.op = $+ ∧
addition_monoid.id = 0
[datatype_monoid] Theorem
⊢ DATATYPE (record monoid carrier op id)
[extend_carrier] Theorem
⊢ (extend m).carrier = 𝕌(:α)
[extend_id] Theorem
⊢ (extend m).id = m.id
[extend_is_monoid] Theorem
⊢ ∀m. Monoid m ⇒ Monoid (extend m)
[extend_op] Theorem
⊢ x ∈ m.carrier ∧ y ∈ m.carrier ⇒ (extend m).op x y = m.op x y
[finite_monoid_exp_not_distinct] Theorem
⊢ ∀g. FiniteMonoid g ⇒ ∀x. x ∈ G ⇒ ∃h k. x ** h = x ** k ∧ h ≠ k
[homo_monoid_I] Theorem
⊢ ∀g. MonoidIso I (homo_monoid g I) g
[homo_monoid_abelian_monoid] Theorem
⊢ ∀g f.
AbelianMonoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
AbelianMonoid (homo_monoid g f)
[homo_monoid_assoc] Theorem
⊢ ∀g f.
Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
∀x y z. x ∈ fG ∧ y ∈ fG ∧ z ∈ fG ⇒ (x ∘ y) ∘ z = x ∘ y ∘ z
[homo_monoid_by_inj] Theorem
⊢ ∀g f. Monoid g ∧ INJ f G 𝕌(:β) ⇒ MonoidHomo f g (homo_monoid g f)
[homo_monoid_closure] Theorem
⊢ ∀g f.
Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y ∈ fG
[homo_monoid_comm] Theorem
⊢ ∀g f.
AbelianMonoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y = y ∘ x
[homo_monoid_element] Theorem
⊢ ∀g f x. x ∈ G ⇒ f x ∈ fG
[homo_monoid_id] Theorem
⊢ ∀g f. f #e = #i
[homo_monoid_id_property] Theorem
⊢ ∀g f.
Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
#i ∈ fG ∧ ∀x. x ∈ fG ⇒ #i ∘ x = x ∧ x ∘ #i = x
[homo_monoid_monoid] Theorem
⊢ ∀g f.
Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
Monoid (homo_monoid g f)
[homo_monoid_op_inj] Theorem
⊢ ∀g f. INJ f G 𝕌(:β) ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ f (x * y) = f x ∘ f y
[homo_monoid_property] Theorem
⊢ ∀g f.
fG = IMAGE f G ∧
(∀x y.
x ∈ fG ∧ y ∈ fG ⇒
x ∘ y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y))) ∧
#i = f #e
[image_op_inj] Theorem
⊢ ∀g f.
INJ f G 𝕌(:β) ⇒
∀x y. x ∈ G ∧ y ∈ G ⇒ image_op g f (f x) (f y) = f (x * y)
[lists_monoid] Theorem
⊢ Monoid lists
[maximal_order_alt] Theorem
⊢ ∀g. maximal_order g = MAX_SET {ord z | z | z ∈ G}
[monoid_11] Theorem
⊢ ∀a0 a1 a2 a0' a1' a2'.
monoid a0 a1 a2 = monoid a0' a1' a2' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
[monoid_Axiom] Theorem
⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (monoid a0 a1 a2) = f a0 a1 a2
[monoid_accessors] Theorem
⊢ (∀f f0 a. (monoid f f0 a).carrier = f) ∧
(∀f f0 a. (monoid f f0 a).op = f0) ∧
∀f f0 a. (monoid f f0 a).id = a
[monoid_accfupds] Theorem
⊢ (∀m f. (m with op updated_by f).carrier = m.carrier) ∧
(∀m f. (m with id updated_by f).carrier = m.carrier) ∧
(∀m f. (m with carrier updated_by f).op = m.op) ∧
(∀m f. (m with id updated_by f).op = m.op) ∧
(∀m f. (m with carrier updated_by f).id = m.id) ∧
(∀m f. (m with op updated_by f).id = m.id) ∧
(∀m f. (m with carrier updated_by f).carrier = f m.carrier) ∧
(∀m f. (m with op updated_by f).op = f m.op) ∧
∀m f. (m with id updated_by f).id = f m.id
[monoid_assoc] Theorem
⊢ ∀g. Monoid g ⇒
∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * y * z = x * (y * z)
[monoid_auto_I] Theorem
⊢ ∀g. MonoidAuto I g
[monoid_auto_bij] Theorem
⊢ ∀g f. MonoidAuto f g ⇒ f PERMUTES G
[monoid_auto_compose] Theorem
⊢ ∀g f1 f2.
MonoidAuto f1 g ∧ MonoidAuto f2 g ⇒ MonoidAuto (f1 ∘ f2) g
[monoid_auto_element] Theorem
⊢ ∀f g. MonoidAuto f g ⇒ ∀x. x ∈ G ⇒ f x ∈ G
[monoid_auto_exp] Theorem
⊢ ∀f g.
Monoid g ∧ MonoidAuto f g ⇒ ∀x. x ∈ G ⇒ ∀n. f (x ** n) = f x ** n
[monoid_auto_id] Theorem
⊢ ∀f g. MonoidAuto f g ⇒ f #e = #e
[monoid_auto_linv_auto] Theorem
⊢ ∀g f. Monoid g ∧ MonoidAuto f g ⇒ MonoidAuto (LINV f G) g
[monoid_auto_order] Theorem
⊢ ∀g f. Monoid g ∧ MonoidAuto f g ⇒ ∀x. x ∈ G ⇒ ord (f x) = ord x
[monoid_carrier_nonempty] Theorem
⊢ ∀g. Monoid g ⇒ G ≠ ∅
[monoid_case_cong] Theorem
⊢ ∀M M' f.
M = M' ∧
(∀a0 a1 a2. M' = monoid a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
monoid_CASE M f = monoid_CASE M' f'
[monoid_case_eq] Theorem
⊢ monoid_CASE x f = v ⇔ ∃f' f0 a. x = monoid f' f0 a ∧ f f' f0 a = v
[monoid_comm_exp] Theorem
⊢ ∀g. Monoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ⇒ x * y = y * x ⇒ ∀n. x ** n * y = y * x ** n
[monoid_comm_exp_exp] Theorem
⊢ ∀g. Monoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
∀n m. x ** n * y ** m = y ** m * x ** n
[monoid_comm_op_exp] Theorem
⊢ ∀g. Monoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
∀n. (x * y) ** n = x ** n * y ** n
[monoid_component_equality] Theorem
⊢ ∀m1 m2.
m1 = m2 ⇔ m1.carrier = m2.carrier ∧ m1.op = m2.op ∧ m1.id = m2.id
[monoid_exp_0] Theorem
⊢ ∀g x. x ** 0 = #e
[monoid_exp_1] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ x ** 1 = x
[monoid_exp_SUC] Theorem
⊢ ∀g x n. x ** SUC n = x * x ** n
[monoid_exp_add] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀n k. x ** (n + k) = x ** n * x ** k
[monoid_exp_comm] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** n * x = x * x ** n
[monoid_exp_element] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** n ∈ G
[monoid_exp_mod_order] Theorem
⊢ ∀g. Monoid g ⇒
∀x. x ∈ G ∧ 0 < ord x ⇒ ∀n. x ** n = x ** (n MOD ord x)
[monoid_exp_mult] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀n k. x ** (n * k) = (x ** n) ** k
[monoid_exp_mult_comm] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀m n. (x ** m) ** n = (x ** n) ** m
[monoid_exp_suc] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** SUC n = x ** n * x
[monoid_fn_updates] Theorem
⊢ (∀f1 f f0 a.
monoid f f0 a with carrier updated_by f1 = monoid (f1 f) f0 a) ∧
(∀f1 f f0 a.
monoid f f0 a with op updated_by f1 = monoid f (f1 f0) a) ∧
∀f1 f f0 a.
monoid f f0 a with id updated_by f1 = monoid f f0 (f1 a)
[monoid_fupdcanon] Theorem
⊢ (∀m g f.
m with <|op updated_by f; carrier updated_by g|> =
m with <|carrier updated_by g; op updated_by f|>) ∧
(∀m g f.
m with <|id updated_by f; carrier updated_by g|> =
m with <|carrier updated_by g; id updated_by f|>) ∧
∀m g f.
m with <|id updated_by f; op updated_by g|> =
m with <|op updated_by g; id updated_by f|>
[monoid_fupdcanon_comp] Theorem
⊢ ((∀g f. op_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ op_fupd f) ∧
∀h g f.
op_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd g ∘ op_fupd f ∘ h) ∧
((∀g f. id_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ id_fupd f) ∧
∀h g f.
id_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd g ∘ id_fupd f ∘ h) ∧
(∀g f. id_fupd f ∘ op_fupd g = op_fupd g ∘ id_fupd f) ∧
∀h g f. id_fupd f ∘ op_fupd g ∘ h = op_fupd g ∘ id_fupd f ∘ h
[monoid_fupdfupds] Theorem
⊢ (∀m g f.
m with <|carrier updated_by f; carrier updated_by g|> =
m with carrier updated_by f ∘ g) ∧
(∀m g f.
m with <|op updated_by f; op updated_by g|> =
m with op updated_by f ∘ g) ∧
∀m g f.
m with <|id updated_by f; id updated_by g|> =
m with id updated_by f ∘ g
[monoid_fupdfupds_comp] Theorem
⊢ ((∀g f. carrier_fupd f ∘ carrier_fupd g = carrier_fupd (f ∘ g)) ∧
∀h g f.
carrier_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd (f ∘ g) ∘ h) ∧
((∀g f. op_fupd f ∘ op_fupd g = op_fupd (f ∘ g)) ∧
∀h g f. op_fupd f ∘ op_fupd g ∘ h = op_fupd (f ∘ g) ∘ h) ∧
(∀g f. id_fupd f ∘ id_fupd g = id_fupd (f ∘ g)) ∧
∀h g f. id_fupd f ∘ id_fupd g ∘ h = id_fupd (f ∘ g) ∘ h
[monoid_homo_I_refl] Theorem
⊢ ∀g. MonoidHomo I g g
[monoid_homo_compose] Theorem
⊢ ∀g h k f1 f2.
MonoidHomo f1 g h ∧ MonoidHomo f2 h k ⇒ MonoidHomo (f2 ∘ f1) g k
[monoid_homo_cong] Theorem
⊢ ∀g h f1 f2.
Monoid g ∧ Monoid h ∧ (∀x. x ∈ G ⇒ f1 x = f2 x) ⇒
(MonoidHomo f1 g h ⇔ MonoidHomo f2 g h)
[monoid_homo_element] Theorem
⊢ ∀f g h. MonoidHomo f g h ⇒ ∀x. x ∈ G ⇒ f x ∈ h.carrier
[monoid_homo_exp] Theorem
⊢ ∀g h f.
Monoid g ∧ MonoidHomo f g h ⇒
∀x. x ∈ G ⇒ ∀n. f (x ** n) = h.exp (f x) n
[monoid_homo_id] Theorem
⊢ ∀f g h. MonoidHomo f g h ⇒ f #e = h.id
[monoid_homo_sym] Theorem
⊢ ∀g h f.
Monoid g ∧ MonoidHomo f g h ∧ BIJ f G h.carrier ⇒
MonoidHomo (LINV f G) h g
[monoid_homo_sym_any] Theorem
⊢ Monoid g ∧ MonoidHomo f g h ∧
(∀x. x ∈ h.carrier ⇒ i x ∈ G ∧ f (i x) = x) ∧
(∀x. x ∈ G ⇒ i (f x) = x) ⇒
MonoidHomo i h g
[monoid_homo_trans] Theorem
⊢ ∀g h k f1 f2.
MonoidHomo f1 g h ∧ MonoidHomo f2 h k ⇒ MonoidHomo (f2 ∘ f1) g k
[monoid_id] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ #e * x = x ∧ x * #e = x
[monoid_id_element] Theorem
⊢ ∀g. Monoid g ⇒ #e ∈ G
[monoid_id_exp] Theorem
⊢ ∀g. Monoid g ⇒ ∀n. #e ** n = #e
[monoid_id_id] Theorem
⊢ ∀g. Monoid g ⇒ #e * #e = #e
[monoid_id_invertible] Theorem
⊢ ∀g. Monoid g ⇒ #e ∈ G*
[monoid_id_unique] Theorem
⊢ ∀g. Monoid g ⇒
∀e. e ∈ G ⇒ ((∀x. x ∈ G ⇒ x * e = x ∧ e * x = x) ⇔ e = #e)
[monoid_induction] Theorem
⊢ ∀P. (∀f f0 a. P (monoid f f0 a)) ⇒ ∀m. P m
[monoid_inj_image_abelian_monoid] Theorem
⊢ ∀g f.
AbelianMonoid g ∧ INJ f G 𝕌(:β) ⇒
AbelianMonoid (monoid_inj_image g f)
[monoid_inj_image_monoid] Theorem
⊢ ∀g f. Monoid g ∧ INJ f G 𝕌(:β) ⇒ Monoid (monoid_inj_image g f)
[monoid_inj_image_monoid_homo] Theorem
⊢ ∀g f. INJ f G 𝕌(:β) ⇒ MonoidHomo f g (monoid_inj_image g f)
[monoid_intersect_element] Theorem
⊢ ∀g h x. x ∈ (g mINTER h).carrier ⇒ x ∈ G ∧ x ∈ H
[monoid_intersect_id] Theorem
⊢ ∀g h. (g mINTER h).id = #e
[monoid_intersect_property] Theorem
⊢ ∀g h.
(g mINTER h).carrier = G ∩ H ∧ (g mINTER h).op = $* ∧
(g mINTER h).id = #e
[monoid_inv_def_alt] Theorem
⊢ ∀g. Monoid g ⇒
∀x. x ∈ G* ⇔ x ∈ G ∧ |/ x ∈ G ∧ x * |/ x = #e ∧ |/ x * x = #e
[monoid_inv_element] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G* ⇒ x ∈ G
[monoid_inv_from_invertibles] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G* ⇒ ∃y. y ∈ G ∧ x * y = #e ∧ y * x = #e
[monoid_inv_invertible] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G* ⇒ |/ x ∈ G*
[monoid_inv_op_invertible] Theorem
⊢ ∀g. Monoid g ⇒ ∀x y. x ∈ G* ∧ y ∈ G* ⇒ x * y ∈ G*
[monoid_invertibles_element] Theorem
⊢ ∀g x. x ∈ G* ⇔ x ∈ G ∧ ∃y. y ∈ G ∧ x * y = #e ∧ y * x = #e
[monoid_invertibles_is_monoid] Theorem
⊢ ∀g. Monoid g ⇒ Monoid (Invertibles g)
[monoid_iso_I_refl] Theorem
⊢ ∀g. MonoidIso I g g
[monoid_iso_bij] Theorem
⊢ ∀g h f. MonoidIso f g h ⇒ BIJ f G h.carrier
[monoid_iso_card_eq] Theorem
⊢ ∀g h f. MonoidIso f g h ∧ FINITE G ⇒ CARD G = CARD h.carrier
[monoid_iso_compose] Theorem
⊢ ∀g h k f1 f2.
MonoidIso f1 g h ∧ MonoidIso f2 h k ⇒ MonoidIso (f2 ∘ f1) g k
[monoid_iso_element] Theorem
⊢ ∀f g h. MonoidIso f g h ⇒ ∀x. x ∈ G ⇒ f x ∈ h.carrier
[monoid_iso_eq_id] Theorem
⊢ ∀g h f.
Monoid g ∧ Monoid h ∧ MonoidIso f g h ⇒
∀x. x ∈ G ⇒ (f x = h.id ⇔ x = #e)
[monoid_iso_exp] Theorem
⊢ ∀g h f.
Monoid g ∧ MonoidIso f g h ⇒
∀x. x ∈ G ⇒ ∀n. f (x ** n) = h.exp (f x) n
[monoid_iso_id] Theorem
⊢ ∀f g h. MonoidIso f g h ⇒ f #e = h.id
[monoid_iso_linv_iso] Theorem
⊢ ∀g h f. Monoid g ∧ MonoidIso f g h ⇒ MonoidIso (LINV f G) h g
[monoid_iso_monoid] Theorem
⊢ ∀g h f. Monoid g ∧ MonoidIso f g h ⇒ Monoid h
[monoid_iso_order] Theorem
⊢ ∀g h f.
Monoid g ∧ Monoid h ∧ MonoidIso f g h ⇒
∀x. x ∈ G ⇒ order h (f x) = ord x
[monoid_iso_property] Theorem
⊢ ∀f g h.
MonoidIso f g h ⇔
MonoidHomo f g h ∧ ∀y. y ∈ h.carrier ⇒ ∃!x. x ∈ G ∧ f x = y
[monoid_iso_sym] Theorem
⊢ ∀g h f. Monoid g ∧ MonoidIso f g h ⇒ MonoidIso (LINV f G) h g
[monoid_iso_trans] Theorem
⊢ ∀g h k f1 f2.
MonoidIso f1 g h ∧ MonoidIso f2 h k ⇒ MonoidIso (f2 ∘ f1) g k
[monoid_lid] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ #e * x = x
[monoid_lid_unique] Theorem
⊢ ∀g. Monoid g ⇒ ∀e. e ∈ G ⇒ (∀x. x ∈ G ⇒ e * x = x) ⇒ e = #e
[monoid_literal_11] Theorem
⊢ ∀f01 f1 a1 f02 f2 a2.
<|carrier := f01; op := f1; id := a1|> =
<|carrier := f02; op := f2; id := a2|> ⇔
f01 = f02 ∧ f1 = f2 ∧ a1 = a2
[monoid_literal_nchotomy] Theorem
⊢ ∀m. ∃f0 f a. m = <|carrier := f0; op := f; id := a|>
[monoid_nchotomy] Theorem
⊢ ∀mm. ∃f f0 a. mm = monoid f f0 a
[monoid_op_element] Theorem
⊢ ∀g. Monoid g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y ∈ G
[monoid_order_cofactor] Theorem
⊢ ∀g. Monoid g ⇒
∀x n.
x ∈ G ∧ 0 < ord x ∧ n divides ord x ⇒
ord (x ** (ord x DIV n)) = n
[monoid_order_common] Theorem
⊢ ∀g. Monoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
∃z. z ∈ G ∧ ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)
[monoid_order_common_coprime] Theorem
⊢ ∀g. Monoid g ⇒
∀x y.
x ∈ G ∧ y ∈ G ∧ x * y = y * x ∧ coprime (ord x) (ord y) ⇒
∃z. z ∈ G ∧ ord z = ord x * ord y
[monoid_order_condition] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀m. x ** m = #e ⇔ ord x divides m
[monoid_order_divides_exp] Theorem
⊢ ∀g. Monoid g ⇒ ∀x n. x ∈ G ⇒ (x ** n = #e ⇔ ord x divides n)
[monoid_order_divides_maximal] Theorem
⊢ ∀g. FiniteAbelianMonoid g ⇒
∀x. x ∈ G ∧ 0 < ord x ⇒ ord x divides maximal_order g
[monoid_order_divisor] Theorem
⊢ ∀g. Monoid g ⇒
∀x m.
x ∈ G ∧ 0 < ord x ∧ m divides ord x ⇒ ∃y. y ∈ G ∧ ord y = m
[monoid_order_eq_1] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ (ord x = 1 ⇔ x = #e)
[monoid_order_id] Theorem
⊢ ∀g. Monoid g ⇒ ord #e = 1
[monoid_order_nonzero] Theorem
⊢ ∀g x. Monoid g ∧ x ∈ G ∧ 0 < ord x ⇒ x ∈ G*
[monoid_order_power] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀k. ord (x ** k) * gcd (ord x) k = ord x
[monoid_order_power_coprime] Theorem
⊢ ∀g. Monoid g ⇒
∀x. x ∈ G ⇒ ∀n. coprime n (ord x) ⇒ ord (x ** n) = ord x
[monoid_order_power_eq_0] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀k. ord (x ** k) = 0 ⇔ 0 < k ∧ ord x = 0
[monoid_order_power_eqn] Theorem
⊢ ∀g. Monoid g ⇒
∀x k. x ∈ G ∧ 0 < k ⇒ ord (x ** k) = ord x DIV gcd k (ord x)
[monoid_rid] Theorem
⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ x * #e = x
[monoid_rid_unique] Theorem
⊢ ∀g. Monoid g ⇒ ∀e. e ∈ G ⇒ (∀x. x ∈ G ⇒ x * e = x) ⇒ e = #e
[monoid_updates_eq_literal] Theorem
⊢ ∀m f0 f a.
m with <|carrier := f0; op := f; id := a|> =
<|carrier := f0; op := f; id := a|>
[monoid_weak_iso_id] Theorem
⊢ ∀f g h. Monoid g ∧ Monoid h ∧ WeakIso f g h ⇒ f #e = h.id
[multiplication_monoid_abelian_monoid] Theorem
⊢ AbelianMonoid multiplication_monoid
[multiplication_monoid_monoid] Theorem
⊢ Monoid multiplication_monoid
[multiplication_monoid_property] Theorem
⊢ multiplication_monoid.carrier = 𝕌(:num) ∧
multiplication_monoid.op = $* ∧ multiplication_monoid.id = 1
[order_alt] Theorem
⊢ ∀g x.
ord x =
case OLEAST k. 0 < k ∧ x ** k = #e of NONE => 0 | SOME k => k
[order_eq_0] Theorem
⊢ ∀g x. ord x = 0 ⇔ ∀n. 0 < n ⇒ x ** n ≠ #e
[order_minimal] Theorem
⊢ ∀g x n. 0 < n ∧ n < ord x ⇒ x ** n ≠ #e
[order_period] Theorem
⊢ ∀g x. 0 < ord x ⇒ period g x (ord x)
[order_property] Theorem
⊢ ∀g x. x ** ord x = #e
[order_thm] Theorem
⊢ ∀g x n.
0 < n ⇒
(ord x = n ⇔ x ** n = #e ∧ ∀m. 0 < m ∧ m < n ⇒ x ** m ≠ #e)
[orders_element] Theorem
⊢ ∀g x n. x ∈ orders g n ⇔ x ∈ G ∧ ord x = n
[orders_eq_1] Theorem
⊢ ∀g. Monoid g ⇒ orders g 1 = {#e}
[orders_finite] Theorem
⊢ ∀g. FINITE G ⇒ ∀n. FINITE (orders g n)
[orders_subset] Theorem
⊢ ∀g n. orders g n ⊆ G
[plus_mod_abelian_monoid] Theorem
⊢ ∀n. 0 < n ⇒ AbelianMonoid (plus_mod n)
[plus_mod_exp] Theorem
⊢ ∀n. 0 < n ⇒ ∀x k. (plus_mod n).exp x k = (k * x) MOD n
[plus_mod_finite] Theorem
⊢ ∀n. FINITE (plus_mod n).carrier
[plus_mod_finite_abelian_monoid] Theorem
⊢ ∀n. 0 < n ⇒ FiniteAbelianMonoid (plus_mod n)
[plus_mod_finite_monoid] Theorem
⊢ ∀n. 0 < n ⇒ FiniteMonoid (plus_mod n)
[plus_mod_monoid] Theorem
⊢ ∀n. 0 < n ⇒ Monoid (plus_mod n)
[plus_mod_property] Theorem
⊢ ∀n. (plus_mod n).carrier = count n ∧
(plus_mod n).op = (λi j. (i + j) MOD n) ∧ (plus_mod n).id = 0 ∧
(∀x. x ∈ (plus_mod n).carrier ⇒ x < n) ∧
FINITE (plus_mod n).carrier ∧ CARD (plus_mod n).carrier = n
[power_monoid_abelian_monoid] Theorem
⊢ ∀b. AbelianMonoid (power_monoid b)
[power_monoid_monoid] Theorem
⊢ ∀b. Monoid (power_monoid b)
[power_monoid_property] Theorem
⊢ ∀b. (power_monoid b).carrier = {b ** j | j ∈ 𝕌(:num)} ∧
(power_monoid b).op = $* ∧ (power_monoid b).id = 1
[power_to_addition_homo] Theorem
⊢ ∀b. 1 < b ⇒ MonoidHomo (LOG b) (power_monoid b) addition_monoid
[power_to_addition_iso] Theorem
⊢ ∀b. 1 < b ⇒ MonoidIso (LOG b) (power_monoid b) addition_monoid
[set_inter_abelian_monoid] Theorem
⊢ AbelianMonoid set_inter
[set_inter_monoid] Theorem
⊢ Monoid set_inter
[set_union_abelian_monoid] Theorem
⊢ AbelianMonoid set_union
[set_union_monoid] Theorem
⊢ Monoid set_union
[submonoid_I_antisym] Theorem
⊢ ∀g h. submonoid h g ∧ submonoid g h ⇒ MonoidIso I h g
[submonoid_alt] Theorem
⊢ ∀g. Monoid g ⇒
∀h. h << g ⇔
H ⊆ G ∧ (∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y ∈ H) ∧ #i ∈ H ∧
$o = $* ∧ #i = #e
[submonoid_antisymmetric] Theorem
⊢ ∀g h. h << g ∧ g << h ⇒ h = g
[submonoid_big_intersect_element] Theorem
⊢ ∀g x. x ∈ (smbINTER g).carrier ⇔ ∀h. h << g ⇒ x ∈ H
[submonoid_big_intersect_has_id] Theorem
⊢ ∀g. (smbINTER g).id ∈ (smbINTER g).carrier
[submonoid_big_intersect_monoid] Theorem
⊢ ∀g. Monoid g ⇒ Monoid (smbINTER g)
[submonoid_big_intersect_op_element] Theorem
⊢ ∀g x y.
x ∈ (smbINTER g).carrier ∧ y ∈ (smbINTER g).carrier ⇒
(smbINTER g).op x y ∈ (smbINTER g).carrier
[submonoid_big_intersect_property] Theorem
⊢ ∀g. (smbINTER g).carrier = BIGINTER (IMAGE (λh. H) {h | h << g}) ∧
(∀x y.
x ∈ (smbINTER g).carrier ∧ y ∈ (smbINTER g).carrier ⇒
(smbINTER g).op x y = x * y) ∧ (smbINTER g).id = #e
[submonoid_big_intersect_submonoid] Theorem
⊢ ∀g. Monoid g ⇒ smbINTER g << g
[submonoid_big_intersect_subset] Theorem
⊢ ∀g. Monoid g ⇒ (smbINTER g).carrier ⊆ G
[submonoid_carrier_antisym] Theorem
⊢ ∀g h. submonoid h g ∧ G ⊆ H ⇒ MonoidIso I h g
[submonoid_carrier_subset] Theorem
⊢ ∀g h. h << g ⇒ H ⊆ G
[submonoid_element] Theorem
⊢ ∀g h. h << g ⇒ ∀x. x ∈ H ⇒ x ∈ G
[submonoid_eqn] Theorem
⊢ ∀g h.
submonoid h g ⇔
H ⊆ G ∧ (∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y) ∧ #i = #e
[submonoid_exp] Theorem
⊢ ∀g h. h << g ⇒ ∀x. x ∈ H ⇒ ∀n. h.exp x n = x ** n
[submonoid_homo_homo] Theorem
⊢ ∀g h k f. submonoid h g ∧ MonoidHomo f g k ⇒ MonoidHomo f h k
[submonoid_homomorphism] Theorem
⊢ ∀g h. h << g ⇒ Monoid h ∧ Monoid g ∧ submonoid h g
[submonoid_id] Theorem
⊢ ∀g h. h << g ⇒ #i = #e
[submonoid_intersect_monoid] Theorem
⊢ ∀g h k. h << g ∧ k << g ⇒ Monoid (h mINTER k)
[submonoid_intersect_property] Theorem
⊢ ∀g h k.
h << g ∧ k << g ⇒
(h mINTER k).carrier = H ∩ K ∧
(∀x y. x ∈ H ∩ K ∧ y ∈ H ∩ K ⇒ (h mINTER k).op x y = x * y) ∧
(h mINTER k).id = #e
[submonoid_intersect_submonoid] Theorem
⊢ ∀g h k. h << g ∧ k << g ⇒ (h mINTER k) << g
[submonoid_monoid] Theorem
⊢ ∀g h. h << g ⇒ Monoid h
[submonoid_op] Theorem
⊢ ∀g h. h << g ⇒ $o = $*
[submonoid_order] Theorem
⊢ ∀g h. h << g ⇒ ∀x. x ∈ H ⇒ order h x = ord x
[submonoid_order_eqn] Theorem
⊢ ∀g h.
Monoid g ∧ Monoid h ∧ submonoid h g ⇒
∀x. x ∈ H ⇒ order h x = ord x
[submonoid_property] Theorem
⊢ ∀g h.
h << g ⇒
Monoid h ∧ Monoid g ∧ H ⊆ G ∧
(∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y) ∧ #i = #e
[submonoid_refl] Theorem
⊢ ∀g. submonoid g g
[submonoid_reflexive] Theorem
⊢ ∀g. Monoid g ⇒ g << g
[submonoid_subset] Theorem
⊢ ∀g h. submonoid h g ⇒ H ⊆ G
[submonoid_trans] Theorem
⊢ ∀g h k. submonoid g h ∧ submonoid h k ⇒ submonoid g k
[submonoid_transitive] Theorem
⊢ ∀g h k. k << h ∧ h << g ⇒ k << g
[times_mod_abelian_monoid] Theorem
⊢ ∀n. 0 < n ⇒ AbelianMonoid (times_mod n)
[times_mod_eval] Theorem
⊢ ∀n. (times_mod n).carrier = count n ∧
(∀x y. (times_mod n).op x y = (x * y) MOD n) ∧
(times_mod n).id = if n = 1 then 0 else 1
[times_mod_exp] Theorem
⊢ ∀n. 0 < n ⇒ ∀x k. (times_mod n).exp x k = (x MOD n) ** k MOD n
[times_mod_finite] Theorem
⊢ ∀n. FINITE (times_mod n).carrier
[times_mod_finite_abelian_monoid] Theorem
⊢ ∀n. 0 < n ⇒ FiniteAbelianMonoid (times_mod n)
[times_mod_finite_monoid] Theorem
⊢ ∀n. 0 < n ⇒ FiniteMonoid (times_mod n)
[times_mod_monoid] Theorem
⊢ ∀n. 0 < n ⇒ Monoid (times_mod n)
[times_mod_property] Theorem
⊢ ∀n. (times_mod n).carrier = count n ∧
(times_mod n).op = (λi j. (i * j) MOD n) ∧
(times_mod n).id = (if n = 1 then 0 else 1) ∧
(∀x. x ∈ (times_mod n).carrier ⇒ x < n) ∧
FINITE (times_mod n).carrier ∧ CARD (times_mod n).carrier = n
[trivial_monoid] Theorem
⊢ ∀e. FiniteAbelianMonoid (trivial_monoid e)
*)
end
HOL 4, Trindemossen-2