equal
deleted
inserted
replaced
11 |
11 |
12 record 'a semigroup = |
12 record 'a semigroup = |
13 carrier :: "'a set" |
13 carrier :: "'a set" |
14 sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>\<index>" 65) |
14 sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>\<index>" 65) |
15 |
15 |
16 locale semigroup = |
16 locale semigroup = struct S + |
17 fixes S (structure) |
|
18 assumes sum_funcset: "sum S \<in> carrier S \<rightarrow> carrier S \<rightarrow> carrier S" |
17 assumes sum_funcset: "sum S \<in> carrier S \<rightarrow> carrier S \<rightarrow> carrier S" |
19 and sum_assoc: |
18 and sum_assoc: |
20 "[|x \<in> carrier S; y \<in> carrier S; z \<in> carrier S|] |
19 "[|x \<in> carrier S; y \<in> carrier S; z \<in> carrier S|] |
21 ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
20 ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)" |
22 |
21 |