text‹
Groups over signature ‹(* :: \ \ \ \ \, 1 :: \, inverse :: \ \ \)\ are
defined as an axiomatic type class as follows. Note that the parent classes 🍋‹times›, 🍋‹one›, 🍋‹inverse› is provided by the basic HOL theory. ›
group = times + one + inverse +
assumes group_assoc: "(x * y) * z = x * (y * z)"
and group_left_one: "1 * x = x"
and group_left_inverse: "inverse x * x = 1"
‹
The group axioms only state the properties of left one and inverse, the
right versions may be derived as follows. ›
(in group) group_right_inverse: "x * inverse x = 1"
-
have "x * inverse x = 1 * (x * inverse x)"
by (simp only: group_left_one)
also have "… = 1 * x * inverse x"
by (simp only: group_assoc)
also have "… = inverse (inverse x) * inverse x * x * inverse x"
by (simp only: group_left_inverse)
also have "… = inverse (inverse x) * (inverse x * x) * inverse x"
by (simp only: group_assoc)
also have "… = inverse (inverse x) * 1 * inverse x"
by (simp only: group_left_inverse)
also have "… = inverse (inverse x) * (1 * inverse x)"
by (simp only: group_assoc)
also have "… = inverse (inverse x) * inverse x"
by (simp only: group_left_one)
also have "… = 1"
by (simp only: group_left_inverse)
finally show ?thesis .
‹
With ‹group_right_inverse› already available, ‹group_right_one›
is now established much easier. ›
(in group) group_right_one: "x * 1 = x"
-
have "x * 1 = x * (inverse x * x)"
by (simp only: group_left_inverse)
also have "… = x * inverse x * x"
by (simp only: group_assoc)
also have "… = 1 * x"
by (simp only: group_right_inverse)
also have "… = x"
by (simp only: group_left_one)
finally show ?thesis .
‹ 🪙
The calculational proof style above follows typical presentations given in
any introductory course on algebra. The basic technique is to form a
transitive chain of equations, which in turn are established by simplifying
with appropriate rules. The low-level logical details of equational
reasoning are left implicit.
Note that ``‹…›'' is just a special term variable that is bound
automatically to the argument🪙‹The argument of a curried infix expression
happens to be its right-hand side.› of the last fact achieved by any local
assumption or proven statement. In contrast to ‹?thesis›, the ``‹…›''
variable is bound 🪙‹after› the proof is finished.
There are only two separate Isar language elements for calculational proofs:
``🪙‹also›'' for initial or intermediate calculational steps, and
``🪙‹finally›'' for exhibiting the result of a calculation. These constructs
are not hardwired into Isabelle/Isar, but defined on top of the basic
Isar/VM interpreter. Expanding the 🪙‹also› and 🪙‹finally› derived language
elements, calculations may be simulated by hand as demonstrated below. ›
(in group) "x * 1 = x"
-
have "x * 1 = x * (inverse x * x)"
by (simp only: group_left_inverse)
have "… = x * inverse x * x"
by (simp only: group_assoc)
note calculation = trans [OF calculation this]
― ‹general calculational step: compose with transitivity rule›
have "… = 1 * x"
by (simp only: group_right_inverse)
note calculation = trans [OF calculation this]
― ‹general calculational step: compose with transitivity rule›
have "… = x"
by (simp only: group_left_one)
note calculation = trans [OF calculation this]
― ‹final calculational step: compose with transitivity rule \dots›
from calculation
― ‹\dots\ and pick up the final result›
show ?thesis .
‹
Note that this scheme of calculations is not restricted to plain
transitivity. Rules like anti-symmetry, or even forward and backward
substitution work as well. For the actual implementation of 🪙‹also› and 🪙‹finally›, Isabelle/Isar maintains separate context information of
``transitivity'' rules. Rule selection takes place automatically by
higher-order unification. ›
‹Groups as monoids›
‹
Monoids over signature ‹(* :: \ \ \ \ \, 1 :: \)\ are defined like this. ›
monoid = times + one +
assumes monoid_assoc: "(x * y) * z = x * (y * z)"
and monoid_left_one: "1 * x = x"
and monoid_right_one: "x * 1 = x"
‹
Groups are 🪙‹not› yet monoids directly from the definition. For monoids, ‹right_one› had to be included as an axiom, but for groups both ‹right_one›
and ‹right_inverse› are derivable from the other axioms. With ‹group_right_one› derived as a theorem of group theory (see @{thm
group_right_one}), we may still instantiate ‹group ⊆ monoid› properly as
follows. ›
group ⊆ monoid
by intro_classes
(rule group_assoc,
rule group_left_one,
rule group_right_one)
‹
The 🪙‹instance› command actually is a version of 🪙‹theorem›, setting up a
goal that reflects the intended class relation (or type constructor arity).
Thus any Isar proof language element may be involved to establish this
statement. When concluding the proof, the result is transformed into the
intended type signature extension behind the scenes. ›
‹More theorems of group theory›
‹
The one element is already uniquely determined by preserving an 🪙‹arbitrary›
group element. ›
(in group) group_one_equality:
assumes eq: "e * x = x"
shows "1 = e"
-
have "1 = x * inverse x"
by (simp only: group_right_inverse)
also have "… = (e * x) * inverse x"
by (simp only: eq)
also have "… = e * (x * inverse x)"
by (simp only: group_assoc)
also have "… = e * 1"
by (simp only: group_right_inverse)
also have "… = e"
by (simp only: group_right_one)
finally show ?thesis .
‹
Likewise, the inverse is already determined by the cancel property. ›
(in group) group_inverse_equality:
assumes eq: "x' * x = 1"
shows "inverse x = x'"
-
have "inverse x = 1 * inverse x"
by (simp only: group_left_one)
also have "… = (x' * x) * inverse x"
by (simp only: eq)
also have "… = x' * (x * inverse x)"
by (simp only: group_assoc)
also have "… = x' * 1"
by (simp only: group_right_inverse)
also have "… = x'"
by (simp only: group_right_one)
finally show ?thesis .
‹
The inverse operation has some further characteristic properties. ›
(in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"
(rule group_inverse_equality)
show "(inverse y * inverse x) * (x * y) = 1"
proof -
have "(inverse y * inverse x) * (x * y) =
(inverse y * (inverse x * x)) * y"
by (simp only: group_assoc)
also have "… = (inverse y * 1) * y"
by (simp only: group_left_inverse)
also have "… = inverse y * y"
by (simp only: group_right_one)
also have "… = 1"
by (simp only: group_left_inverse)
finally show ?thesis .
qed
(in group) inverse_inverse: "inverse (inverse x) = x"
(rule group_inverse_equality)
show "x * inverse x = one"
by (simp only: group_right_inverse)
(in group) inverse_inject:
assumes eq: "inverse x = inverse y"
shows "x = y"
-
have "x = x * 1"
by (simp only: group_right_one)
also have "… = x * (inverse y * y)"
by (simp only: group_left_inverse)
also have "… = x * (inverse x * y)"
by (simp only: eq)
also have "… = (x * inverse x) * y"
by (simp only: group_assoc)
also have "… = 1 * y"
by (simp only: group_right_inverse)
also have "… = y"
by (simp only: group_left_one)
finally show ?thesis .
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
