(def-constant left%trans
"lambda(g:gg,a:sets[gg],
indic{h:gg, forsome(i:gg, (i in a) and h=g mul i)})"
(theory groups))
(def-constant right%trans
"lambda(a:sets[gg],g:gg,
indic{h:gg, forsome(i:gg, (i in a) and h=i mul g)})"
(theory groups))
(def-constant set%mul
"lambda(a,b:sets[gg],
indic{g:gg, forsome(h,i:gg, (h in a) and (i in b) and g=h mul i)})"
(theory groups))
(def-constant set%conjugate
"lambda(a:sets[gg],g:gg, right%trans(left%trans(inv(g),a),g))"
(theory groups))
(def-theorem left%trans-is-total
"total_q{left%trans,[gg,sets[gg],sets[gg]]}"
(theory groups)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally left%trans)
simplify-insistently
)))
(def-theorem right%trans-is-total
"total_q{right%trans,[sets[gg],gg,sets[gg]]}"
(theory groups)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally right%trans)
simplify-insistently
)))
(def-theorem set%mul-is-total
"total_q{set%mul,[sets[gg],sets[gg],sets[gg]]}"
(theory groups)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally set%mul)
simplify-insistently
)))
(def-theorem set%conjugate-is-total
"total_q{set%conjugate,[sets[gg],gg,sets[gg]]}"
(theory groups)
(usages d-r-convergence)
(proof
(
(unfold-single-defined-constant-globally set%conjugate)
simplify-insistently
)))
(def-theorem left%trans->right%trans-obligation
"lambda(g:gg,a:sets[gg],right%trans(a,g))=
lambda(g:gg,a:sets[gg],lambda(x:gg,
if(forsome(i_$0:gg, i_$0 in a and x=i_$0 mul g),
an%individual,
?unit%sort)))"
lemma
(theory groups)
(proof
(
(unfold-single-defined-constant-globally right%trans)
extensionality
simplify
)))
(def-theorem right%trans->left%trans-obligation
"lambda(a:sets[gg],g:gg,left%trans(g,a))=
lambda(a:sets[gg],g:gg,lambda(x:gg,
if(forsome(i_$0:gg, i_$0 in a and x=g mul i_$0),
an%individual,
?unit%sort)))"
lemma
(theory groups)
(proof
(
(unfold-single-defined-constant-globally left%trans)
extensionality
simplify
)))
(def-theorem subgroup->subgroup-obligation
"subgroup =
lambda(a:sets[gg],
nonempty_indic_q{a}
and
forall(g,h:gg,g in a and h in a implies (h mul g) in a)
and
forall(g:gg,g in a implies inv(g) in a))"
lemma
(theory groups)
(proof
(
(unfold-single-defined-constant-globally subgroup)
extensionality
simplify
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent
"with(p:prop, forall(g,h:gg, p))" ("h" "g"))
(instantiate-universal-antecedent
"with(p:prop, forall(g:gg, p))" ("g"))
(instantiate-universal-antecedent
"with(p:prop, forall(g,h:gg, p))" ("h" "g"))
)))
(def-translation left%trans<->right%trans
(source groups)
(target groups)
(fixed-theories h-o-real-arithmetic)
(constant-pairs
(mul "lambda(x,y:gg, y mul x)")
(left%trans "lambda(g:gg,a:sets[gg], right%trans(a,g))")
(right%trans "lambda(a:sets[gg],g:gg, left%trans(g,a))")
(subgroup subgroup))
force-under-quick-load
(theory-interpretation-check using-simplification))
(def-theorem trivial-left-translation
"forall(a:sets[gg], left%trans(e,a)=a)"
(theory groups)
(usages rewrite transportable-macete)
(proof
(
(unfold-single-defined-constant-globally left%trans)
direct-inference
extensionality
direct-inference
simplify
(case-split-on-conditionals (0))
)))
(def-theorem left%trans-associativity
"forall(g,h:gg,a:sets[gg],
left%trans(h mul g,a) = left%trans(h,(left%trans(g,a))))"
(theory groups)
(usages transportable-macete)
(proof; 28 nodes
(
(unfold-single-defined-constant-globally left%trans)
direct-inference
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
(instantiate-existential ("g mul i_$0"))
(instantiate-existential ("i_$0")))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (1 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("i"))
simplify)
)))
(def-theorem trivial-right-translation
trivial-left-translation
(theory groups)
(usages rewrite transportable-macete)
(translation left%trans<->right%trans)
(proof existing-theorem))
(def-theorem right%trans-associativity
left%trans-associativity
(theory groups)
(usages transportable-macete)
(translation left%trans<->right%trans)
(proof existing-theorem))
(def-translation act->left%trans
(source group-actions)
(target groups)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu "sets[gg]"))
(constant-pairs
(mul "lambda(x,y:gg, y mul x)")
(act "lambda(a:sets[gg],g:gg, left%trans(g,a))"))
(theory-interpretation-check using-simplification))
(def-translation act->right%trans
(source group-actions)
(target groups)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu "sets[gg]"))
(constant-pairs
(act "right%trans"))
(theory-interpretation-check using-simplification))
(def-theorem left%trans-right%trans-associativity
"forall(a:sets[gg], g,h:gg,
left%trans(g,right%trans(a,h)) = right%trans(left%trans(g,a),h))"
(theory groups)
(usages transportable-macete)
(proof; 43 nodes
(
unfold-defined-constants
direct-inference
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (0 0 0 0 0)")
(instantiate-existential ("g mul i_$0 mul inv(h)"))
(block
(script-comment "node added by `instantiate-existential' at (0 0)")
(instantiate-existential ("i_$1"))
(force-substitution "i_$0" "i_$1 mul h" (0))
(weaken (0 1 2))
simplify)
(block
(script-comment "node added by `instantiate-existential' at (0 1)")
(weaken (0 1 2))
simplify))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (1 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("inv(g) mul i_$0 mul h"))
(block
(script-comment "node added by `instantiate-existential' at (0 0)")
(instantiate-existential ("i"))
(force-substitution "i_$0" "g mul i" (0))
(weaken (0 1 2))
simplify)
(block
(script-comment "node added by `instantiate-existential' at (0 1)")
(weaken (0 2 3))
simplify))
)))
(def-theorem right%trans-left%trans-associativity
left%trans-right%trans-associativity
(theory groups)
(usages transportable-macete)
(translation left%trans<->right%trans)
(proof existing-theorem))
(def-theorem trivial-conjugation
"forall(a:sets[gg], set%conjugate(a,e)=a)"
(theory groups)
(usages rewrite transportable-macete)
(proof
(
(unfold-single-defined-constant-globally set%conjugate)
simplify
)))
(def-theorem set%conjugate-associativity
"forall(a:sets[gg],g,h:gg,
set%conjugate(a,g mul h)=set%conjugate(set%conjugate(a,g),h))"
(theory groups)
(usages transportable-macete)
(proof; macete menu takes some time here
(
(unfold-single-defined-constant-globally set%conjugate)
simplify
(apply-macete-with-minor-premises left%trans-associativity)
(apply-macete-with-minor-premises right%trans-associativity)
(apply-macete-with-minor-premises left%trans-right%trans-associativity)
direct-inference
)))
(def-translation act->set%conjugate
(source group-actions)
(target groups)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu "sets[gg]"))
(constant-pairs
(act "set%conjugate"))
(theory-interpretation-check using-simplification))
(def-theorem left-left%trans-inv
right-act-inv
(theory groups)
(usages rewrite transportable-macete)
(translation act->left%trans)
(proof existing-theorem))
(def-theorem right-left%trans-inv
left-act-inv
(theory groups)
(usages rewrite transportable-macete)
(translation act->left%trans)
(proof existing-theorem))
(def-theorem left-right%trans-inv
left-act-inv
(theory groups)
(usages rewrite transportable-macete)
(translation act->right%trans)
(proof existing-theorem))
(def-theorem right-right%trans-inv
right-act-inv
(theory groups)
(usages rewrite transportable-macete)
(translation act->right%trans)
(proof existing-theorem))
(def-theorem reverse-left%trans-associativity
reverse-act-associativity
(theory groups)
(usages transportable-macete)
(translation act->left%trans)
(proof existing-theorem))
(def-theorem reverse-right%trans-associativity
reverse-act-associativity
(theory groups)
(usages transportable-macete)
(translation act->right%trans)
(proof existing-theorem))
(def-theorem reverse-set%conjugate-associativity
reverse-act-associativity
(theory groups)
(usages transportable-macete)
(translation act->set%conjugate)
(proof existing-theorem))
(def-compound-macete simplify-set-translations
(series
(repeat
reverse-left%trans-associativity
reverse-right%trans-associativity
reverse-set%conjugate-associativity)
simplify))
(def-theorem left-translation-macete
action-macete
reverse
(theory groups)
(usages transportable-macete)
(translation act->left%trans)
(proof existing-theorem))
(def-theorem right-translation-macete
action-macete
reverse
(theory groups)
(usages transportable-macete)
(translation act->right%trans)
(proof existing-theorem))
(def-theorem subgroup-is-left%trans-stabilizer
"forall(a:sets[gg],g:gg, subgroup(a) implies left%trans(g,a) = a iff g in a)"
(theory groups)
(usages transportable-macete)
(proof; 32 nodes
(
(unfold-single-defined-constant-globally left%trans)
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
(contrapose "with(a,f:sets[gg],f=a);")
extensionality
(instantiate-existential ("g"))
simplify-insistently
(instantiate-existential ("e"))
(apply-macete-with-minor-premises subgroup-membership)
simplify)
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 1)")
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
(cut-with-single-formula "x_0 in a")
simplify
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
(force-substitution "x_0" "g mul i" (0))
(apply-macete-with-minor-premises subgroup-membership)))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (1)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("inv(g) mul x_0"))
(apply-macete-with-minor-premises subgroup-membership)
simplify))
)))
(def-theorem subgroup-is-right%trans-stabilizer
subgroup-is-left%trans-stabilizer
(theory groups)
(translation left%trans<->right%trans)
(proof existing-theorem))
(def-theorem set%mul-associativity
"forall(a,b,c:sets[gg],g:gg,
(a set%mul b) set%mul c = a set%mul (b set%mul c))"
(theory groups)
(usages transportable-macete)
(proof; 52 nodes
(
(unfold-single-defined-constant-globally set%mul)
direct-inference
extensionality
simplify-insistently
direct-inference
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (0 0 0 0 0)")
(instantiate-existential ("i mul i_$0" "h"))
(instantiate-existential ("i_$0" "i"))
(block
(script-comment "node added by `instantiate-existential' at (0 2)")
(force-substitution "x_0" "h_$0 mul i_$0" (0))
(force-substitution "h_$0" "h mul i" (0))
(weaken (0 1 2 3 4 5))
simplify))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (1 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("i_$1" "h_$0 mul h_$1"))
(instantiate-existential ("h_$1" "h_$0"))
(block
(script-comment "node added by `instantiate-existential' at (0 2)")
(force-substitution "x_0" "h_$0 mul i_$0" (0))
(force-substitution "i_$0" "h_$1 mul i_$1" (0))
(weaken (0 1 2 3 4 5))
simplify))
)))
(def-theorem idempotence-of-subgroups
"forall(a:sets[gg], subgroup(a) implies a set%mul a = a)"
(theory groups)
(usages transportable-macete)
(proof; 25 nodes
(
(unfold-single-defined-constant-globally set%mul)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "e in a")
(block
(script-comment "node added by `cut-with-single-formula' at (0)")
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
(cut-with-single-formula "x_0 in a")
simplify
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
(force-substitution "x_0" "h_$0 mul i_$0" (0))
(apply-macete-with-minor-premises subgroup-membership)))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (1)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("e" "x_0"))
simplify))
(apply-macete-with-minor-premises subgroup-membership)
)))
(def-theorem set%mul-right%trans-associativity
"forall(a,b:sets[gg],g:gg,
a set%mul right%trans(b,g) = right%trans(a set%mul b, g))"
(theory groups)
(usages transportable-macete)
(proof; 44 nodes
(
unfold-defined-constants
direct-inference
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (0 0 0 0 0)")
(instantiate-existential ("h_$0 mul i"))
(instantiate-existential ("i" "h_$0"))
simplify)
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (1 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("i mul g" "h"))
(instantiate-existential ("i"))
(block
(script-comment "node added by `instantiate-existential' at (0 2)")
(force-substitution "x_0" "i_$0 mul g" (0))
(force-substitution "i_$0" "h mul i" (0))
(weaken (0 1 2 3 4))
simplify))
)))
(def-theorem right%trans-set%mul-associativity
"forall(a,b:sets[gg],g:gg,
right%trans(a,g) set%mul b = a set%mul left%trans(g,b))"
(theory groups)
(usages transportable-macete)
(proof; 47 nodes
(
unfold-defined-constants
direct-inference
extensionality
direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (0 0 0 0 0)")
(instantiate-existential ("g mul i_$0" "i"))
(instantiate-existential ("i_$0"))
(block
(script-comment "node added by `instantiate-existential' at (0 2)")
(force-substitution "x_0" "h_$0 mul i_$0" (0))
(force-substitution "h_$0" "i mul g" (0))
(weaken (0 1 2 3 4))
simplify))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (1 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("i" "h_$0 mul g"))
(instantiate-existential ("h_$0"))
(block
(script-comment "node added by `instantiate-existential' at (0 2)")
(force-substitution "x_0" "h_$0 mul i_$0" (0))
simplify))
)))
(def-theorem overlapping-right-cosets
"forall(a:sets[gg],g,h:gg,
subgroup(a)
implies
(right%trans(a,g) = right%trans(a,h)
or
right%trans(a,g) disj right%trans(a,h)))"
(theory groups)
(usages transportable-macete)
(proof; 49 nodes
(
(unfold-single-defined-constant-globally right%trans)
insistent-direct-inference-strategy
(contrapose "with(p:prop,not(p));")
extensionality
direct-inference
(incorporate-antecedent
"with(x,h:gg,a:sets[gg],
x in indic{h_$0:gg,
forsome(i_$0:gg, i_$0 in a and h_$0=i_$0 mul h)});")
(incorporate-antecedent "with(x:gg,f:sets[gg],x in f);")
simplify-insistently
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (0 0 0 0 0 0 0 0 0)")
(instantiate-existential ("i mul g mul inv(h)"))
(block
(script-comment "node added by `instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises mul-associativity)
(apply-macete-with-minor-premises subgroups-closed-under-mul)
simplify
(force-substitution "h" "inv(i_$0) mul x" (0))
(block
(script-comment "node added by `force-substitution' at (0)")
(force-substitution "g" "inv(i_$1) mul x" (0))
(block
(script-comment "node added by `force-substitution' at (0)")
(weaken (0 5))
simplify
(apply-macete-with-minor-premises subgroup-membership))
(block
(script-comment "node added by `force-substitution' at (1)")
(force-substitution "x" "i_$1 mul g" (0))
(weaken (0))
simplify))
(block
(script-comment "node added by `force-substitution' at (1)")
(force-substitution "x" "i_$0 mul h" (0))
(weaken (5))
simplify))
simplify)
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy'
at (0 0 1 0 0 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("i_$0 mul h mul inv(g)"))
(block
(script-comment "node added by `instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises mul-associativity)
(apply-macete-with-minor-premises subgroups-closed-under-mul)
simplify
(force-substitution "h" "inv(i_$1) mul x" (0))
(block
(script-comment "node added by `force-substitution' at (0)")
(force-substitution "g" "inv(i) mul x" (0))
(block
(script-comment "node added by `force-substitution' at (0)")
simplify
(apply-macete-with-minor-premises subgroup-membership))
(block
(script-comment "node added by `force-substitution' at (1)")
(force-substitution "x" "i mul g" (0))
(weaken (5))
simplify))
(block
(script-comment "node added by `force-substitution' at (1)")
(force-substitution "x" "i_$1 mul h" (0))
(weaken (1))
simplify))
simplify)
)))