22317
|
1 |
structure ROOT =
|
|
2 |
struct
|
|
3 |
|
|
4 |
structure Nat =
|
|
5 |
struct
|
|
6 |
|
|
7 |
datatype nat = Zero_nat | Suc of nat;
|
|
8 |
|
|
9 |
end; (*struct Nat*)
|
|
10 |
|
|
11 |
structure Integer =
|
|
12 |
struct
|
|
13 |
|
|
14 |
fun nat_aux n i =
|
|
15 |
(if IntInf.<= (i, (0 : IntInf.int)) then n
|
|
16 |
else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
|
|
17 |
|
|
18 |
fun nat i = nat_aux Nat.Zero_nat i;
|
|
19 |
|
|
20 |
end; (*struct Integer*)
|
|
21 |
|
|
22 |
structure Classes =
|
|
23 |
struct
|
|
24 |
|
22479
|
25 |
type 'a semigroup = {mult : 'a -> 'a -> 'a};
|
|
26 |
fun mult (A_:'a semigroup) = #mult A_;
|
22317
|
27 |
|
|
28 |
type 'a monoidl =
|
22479
|
29 |
{Classes__monoidl_semigroup : 'a semigroup, neutral : 'a};
|
22317
|
30 |
fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_;
|
22479
|
31 |
fun neutral (A_:'a monoidl) = #neutral A_;
|
22317
|
32 |
|
22479
|
33 |
type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a};
|
22317
|
34 |
fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_;
|
22479
|
35 |
fun inverse (A_:'a group) = #inverse A_;
|
22317
|
36 |
|
|
37 |
fun inverse_int i = IntInf.~ i;
|
|
38 |
|
|
39 |
val neutral_int : IntInf.int = (0 : IntInf.int);
|
|
40 |
|
|
41 |
fun mult_int i j = IntInf.+ (i, j);
|
|
42 |
|
22479
|
43 |
val semigroup_int = {mult = mult_int} : IntInf.int semigroup;
|
22317
|
44 |
|
|
45 |
val monoidl_int =
|
22479
|
46 |
{Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} :
|
|
47 |
IntInf.int monoidl;
|
22317
|
48 |
|
|
49 |
val group_int =
|
22479
|
50 |
{Classes__group_monoidl = monoidl_int, inverse = inverse_int} :
|
22317
|
51 |
IntInf.int group;
|
|
52 |
|
|
53 |
fun pow_nat A_ (Nat.Suc n) x =
|
|
54 |
mult (monoidl_semigroup A_) x (pow_nat A_ n x)
|
|
55 |
| pow_nat A_ Nat.Zero_nat x = neutral A_;
|
|
56 |
|
|
57 |
fun pow_int A_ k x =
|
|
58 |
(if IntInf.<= ((0 : IntInf.int), k)
|
|
59 |
then pow_nat (group_monoidl A_) (Integer.nat k) x
|
|
60 |
else inverse A_
|
|
61 |
(pow_nat (group_monoidl A_) (Integer.nat (IntInf.~ k)) x));
|
|
62 |
|
|
63 |
val example : IntInf.int =
|
|
64 |
pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);
|
|
65 |
|
|
66 |
end; (*struct Classes*)
|
|
67 |
|
|
68 |
end; (*struct ROOT*)
|