(def-language group-action-language (embedded-language groups-language) (base-types uu) (constants (act"[uu,gg,uu]")))

(def-theory group-actions (language group-action-language) (component-theories groups) (axioms (act-id"forall(alpha:uu,g:gg, act(alpha,e) = alpha)"rewrite transportable-macete) (act-associativity"forall(alpha:uu,g,h:gg, act(alpha,g mul h) = act(act(alpha,g),h))"transportable-macete)))

(def-constant orbit"lambda(alpha:uu, indic{beta:uu, forsome(g:gg, beta = act(alpha,g))})"(theory group-actions))

(def-constant stabilizer"lambda(alpha:uu, indic{g:gg, act(alpha,g)=alpha})"(theory group-actions))

(def-theorem act-is-total"total_q(act,[uu,gg,uu])"(theory group-actions) (usages d-r-convergence transportable-macete) (proof ( insistent-direct-inference (instantiate-theorem act-associativity ("x_0""x_1""e")) )))

(def-theorem orbit-is-total"total_q(orbit,[uu,sets[uu]])"(theory group-actions) (usages d-r-convergence transportable-macete) (proof ( (unfold-single-defined-constant-globally orbit) simplify-insistently )))

(def-theorem stabilizer-is-total"total_q(stabilizer,[uu,sets[gg]])"(theory group-actions) (usages d-r-convergence transportable-macete) (proof ( (unfold-single-defined-constant-globally stabilizer) simplify-insistently )))

(def-theorem reverse-act-associativity"forall(alpha:uu,g,h:gg, act(act(alpha,g),h) = act(alpha,g mul h))"(theory group-actions) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises act-associativity) simplify )))

(def-theorem action-by-stabilizer-member"forall(alpha:uu,g:gg, g in stabilizer(alpha) implies act(alpha,g)=alpha)"(theory group-actions) (usages transportable-macete) (proof ( (unfold-single-defined-constant-globally stabilizer) simplify )))

(def-theorem left-act-inv"forall(alpha:uu,g:gg, act(act(alpha,inv(g)),g) = alpha)"(theory group-actions) (usages rewrite transportable-macete) (proof ( (apply-macete-with-minor-premises reverse-act-associativity) simplify )))

(def-theorem right-act-inv"forall(alpha:uu,g:gg, act(act(alpha,g),inv(g)) = alpha)"(theory group-actions) (usages rewrite transportable-macete) (proof ( (apply-macete-with-minor-premises reverse-act-associativity) simplify )))

(def-compound-macete simplify-actions (series (repeat reverse-act-associativity) simplify))

(def-translation act->left-mul (source group-actions) (target groups) (fixed-theories h-o-real-arithmetic) (sort-pairs (uu"gg")) (constant-pairs (mul"lambda(x,y:gg, y mul x)") (act"lambda(x,y:gg, y mul x)")) force-under-quick-load (theory-interpretation-check using-simplification))

(def-translation act->right-mul (source group-actions) (target groups) (fixed-theories h-o-real-arithmetic) (sort-pairs (uu"gg")) (constant-pairs (act"mul")) force-under-quick-load (theory-interpretation-check using-simplification))

(def-translation act->conjugate (source group-actions) (target groups) (fixed-theories h-o-real-arithmetic) (sort-pairs (uu"gg")) (constant-pairs (act"lambda(g,h:gg, (inv(h) mul g) mul h)")) force-under-quick-load (theory-interpretation-check using-simplification))

(def-theorem action-macete"forall(alpha,beta:uu,g:gg, alpha=beta iff act(alpha,g) = act(beta,g))"reverse (theory group-actions) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem act-associativity ("alpha""g""inv(g)")) (contrapose"with(g,h:gg,alpha,beta:uu, act(alpha,g)=act(beta,h))") (force-substitution"act(alpha,g)""act(beta,g)"(0)) simplify )))

(def-theorem stabilizers-are-subgroups"forall(alpha:uu, subgroup(stabilizer(alpha)))"(theory group-actions) (usages transportable-macete) (proof ( unfold-defined-constants simplify-insistently direct-and-antecedent-inference-strategy (instantiate-existential ("e")) simplify (apply-macete-with-minor-premises act-associativity) simplify (apply-macete-with-minor-premises action-macete) (instantiate-existential ("g_$0")) simplify )))