(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
        )))