| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/ex/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 944 B |
|
Quelle MonoidGroup.thySprache: Isabelle |
|||||||||||||||
|
(* 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 |) => "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
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-06-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09