(def-constant subgroup 
    "lambda(a:sets[gg], 
          nonempty_indic_q{a} and
          forall(g,h:gg, ((g in a) and (h in a)) implies ((g mul h) in a)) and
          forall(g:gg, (g in a) implies (inv(g) in a)))"
    (theory groups))

(def-constant gg%subgroup  
    "sort_to_indic(gg)" 
    (theory groups))

(def-constant e%subgroup  
    "singleton{e}"
    (theory groups))

(def-theorem gg-is-a-subgroup 
    "subgroup(gg%subgroup)"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        unfold-defined-constants
        simplify
        (instantiate-existential ("e"))
        simplify
        )))

(def-theorem singleton-e-is-a-subgroup 
    "subgroup(e%subgroup)"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        unfold-defined-constants
        simplify-insistently
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        )))

(def-theorem subgroups-are-subsets-of-gg%subgroup 
    "forall(a:sets[gg], subgroup(a) implies a subseteq gg%subgroup)"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        simplify
        )))

(def-theorem subgroups-are-nonempty 
    "forall(a:sets[gg], subgroup(a) implies nonempty_indic_q{a})"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        (unfold-single-defined-constant-globally subgroup)
        simplify
        )))

(def-theorem subgroups-closed-under-mul 
    "forall(a:sets[gg], subgroup(a) 
        implies 
      forall(g,h:gg, (g in a) and (h in a) implies (g mul h) in a))"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        (unfold-single-defined-constant-globally subgroup)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop, forall(g,h:gg,p))" ("g" "h"))
        )))

(def-theorem subgroups-closed-under-inv 
    "forall(a:sets[gg], subgroup(a) 
        implies 
      forall(g,h:gg, (g in a) implies inv(g) in a))"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        (unfold-single-defined-constant-globally subgroup)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop, forall(g:gg,p))" ("g"))
        )))
    

(def-theorem subgroups-contain-e 
    "forall(a:sets[gg], subgroup(a) implies (e in a))"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem subgroups-are-nonempty ("a"))
        (force-substitution "e" "x mul inv(x)" (0))
        (apply-macete-with-minor-premises subgroups-closed-under-mul)
        simplify
        (apply-macete-with-minor-premises subgroups-closed-under-inv)
        simplify
        simplify
        simplify
        )))

(def-compound-macete subgroup-membership 
    (series
      (repeat 
        subgroups-closed-under-mul
        subgroups-closed-under-inv
        subgroups-contain-e)
      simplify))

(def-theorem subgroups-are-groups 
    "forall(a:sets[gg], subgroup(a) implies group{a,mul,e,inv})"
    (theory groups)
    (usages transportable-macete)
    (proof
      (
        insistent-direct-inference-strategy
        (apply-macete-with-minor-premises subgroup-membership)
        (apply-macete-with-minor-premises subgroup-membership)
        (apply-macete-with-minor-premises subgroup-membership)
        simplify
        simplify
        simplify
        simplify
        simplify
        )))

(def-theorem groups->subgroup-obl-1 
    "forall(a:sets[gg],
          nonempty_indic_q{a}
            and 
          forall(g,h:gg,g in a and h in a implies (g mul h) in a)
            and 
          forall(g:gg,g in a implies inv(g) in a)
            implies 
          e in a)"
    lemma
    (theory groups)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
          "with(a:sets[gg], forall(g,h:gg,g in a and h in a implies (g mul h) in a));" 
          ("x" "inv(x)"))
        (instantiate-universal-antecedent 
          "with(a:sets[gg],forall(g:gg,g in a implies inv(g) in a));" 
          ("x"))
        (incorporate-antecedent "with(x:gg,a:sets[gg],(x mul inv(x)) in a);")
        simplify
        )))

(def-theorem groups->subgroup-obl-2 
    "forall(a:sets[gg],
          nonempty_indic_q{a}
            and 
          forall(g,h:gg,g in a and h in a implies (g mul h) in a)
            and 
          forall(g:gg,g in a implies inv(g) in a)
            implies 
          forall(x:gg,x in a implies if(e in a, x, ?gg)=x))"
    lemma
    (theory groups)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem groups->subgroup-obl-1 ("a"))
        (contrapose "with(a:sets[gg],empty_indic_q{a});")
        auto-instantiate-existential
        simplify
        )))

(def-translation groups->subgroup 
    (source groups)
    (target groups)
    (assumptions 
      "with(a:sets[gg], nonempty_indic_q{a})"
      "with(a:sets[gg], forall(g,h:gg, (g in a) and (h in a) implies (g mul h) in a))"
      "with(a:sets[gg], forall(g:gg, (g in a) implies (inv(g) in a)))")
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs
      (gg (indic "with(a:sets[gg], a)")))
    (constant-pairs
      (mul "with(a:sets[gg], lambda(x,y:gg, if((x in a) and (y in a), x mul y, ?gg)))")
      (inv "with(a:sets[gg], lambda(x:gg, if(x in a, inv(x), ?gg)))"))
    force-under-quick-load
    (theory-interpretation-check using-simplification))