src/HOL/ex/MonoidGroup.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 41460 ea56b98aee83
child 58889 5b7a9633cfa8
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
wenzelm@5199
     1
(*  Title:      HOL/ex/MonoidGroup.thy
wenzelm@5199
     2
    Author:     Markus Wenzel
wenzelm@5199
     3
*)
wenzelm@5199
     4
wenzelm@17388
     5
header {* Monoids and Groups as predicates over record schemes *}
wenzelm@10357
     6
haftmann@16417
     7
theory MonoidGroup imports Main begin
wenzelm@5199
     8
wenzelm@5199
     9
record 'a monoid_sig =
wenzelm@11019
    10
  times :: "'a => 'a => 'a"
wenzelm@5199
    11
  one :: 'a
wenzelm@5199
    12
wenzelm@9297
    13
record 'a group_sig = "'a monoid_sig" +
wenzelm@5199
    14
  inv :: "'a => 'a"
wenzelm@5199
    15
wenzelm@19736
    16
definition
wenzelm@21404
    17
  monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where
wenzelm@19736
    18
  "monoid M = (\<forall>x y z.
wenzelm@11019
    19
    times M (times M x y) z = times M x (times M y z) \<and>
wenzelm@19736
    20
    times M (one M) x = x \<and> times M x (one M) = x)"
wenzelm@5199
    21
wenzelm@21404
    22
definition
wenzelm@21404
    23
  group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where
wenzelm@19736
    24
  "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
wenzelm@5199
    25
wenzelm@21404
    26
definition
wenzelm@11939
    27
  reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
wenzelm@21404
    28
    (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where
wenzelm@19736
    29
  "reverse M = M (| times := \<lambda>x y. times M y x |)"
wenzelm@5199
    30
wenzelm@5199
    31
end