(* Title: HOL/ex/MonoidGroup.thy Author: Markus Wenzel *)
section‹Monoids and Groups as predicates over record schemes›
theory MonoidGroup imports Main begin
record 'a monoid_sig =
times :: "'a => 'a => 'a"
one :: 'a
record 'a group_sig = "'a monoid_sig" +
inv :: "'a => 'a"
definition
monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool"where "monoid M = (∀x y z. times M (times M x y) z = times M x (times M y z) ∧ times M (one M) x = x ∧ times M x (one M) = x)"
definition
group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool"where "group G = (monoid G ∧ (∀x. times G (inv G x) x = one G))"
definition
reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)"where "reverse M = M (| times := λx y. times M y x |)"
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-04-26)
¤
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.
