src/HOL/ex/MonoidGroup.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 41460 ea56b98aee83 child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
```     1 (*  Title:      HOL/ex/MonoidGroup.thy
```
```     2     Author:     Markus Wenzel
```
```     3 *)
```
```     4
```
```     5 header {* Monoids and Groups as predicates over record schemes *}
```
```     6
```
```     7 theory MonoidGroup imports Main begin
```
```     8
```
```     9 record 'a monoid_sig =
```
```    10   times :: "'a => 'a => 'a"
```
```    11   one :: 'a
```
```    12
```
```    13 record 'a group_sig = "'a monoid_sig" +
```
```    14   inv :: "'a => 'a"
```
```    15
```
```    16 definition
```
```    17   monoid :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) => bool" where
```
```    18   "monoid M = (\<forall>x y z.
```
```    19     times M (times M x y) z = times M x (times M y z) \<and>
```
```    20     times M (one M) x = x \<and> times M x (one M) = x)"
```
```    21
```
```    22 definition
```
```    23   group :: "(| times :: 'a => 'a => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'b |) => bool" where
```
```    24   "group G = (monoid G \<and> (\<forall>x. times G (inv G x) x = one G))"
```
```    25
```
```    26 definition
```
```    27   reverse :: "(| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |) =>
```
```    28     (| times :: 'a => 'a => 'a, one :: 'a, ... :: 'b |)" where
```
```    29   "reverse M = M (| times := \<lambda>x y. times M y x |)"
```
```    30
```
```    31 end
```