|
13957
|
1 |
(* Title: ComplexBin.thy
|
|
|
2 |
Author: Jacques D. Fleuriot
|
|
|
3 |
Copyright: 2001 University of Edinburgh
|
|
|
4 |
Descrition: Binary arithmetic for the complex numbers
|
|
|
5 |
This case is reduced to that for the reals.
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
ComplexBin = Complex +
|
|
|
9 |
|
|
|
10 |
|
|
|
11 |
instance
|
|
|
12 |
complex :: number
|
|
|
13 |
|
|
|
14 |
instance complex :: plus_ac0(complex_add_commute,complex_add_assoc,complex_add_zero_left)
|
|
|
15 |
|
|
|
16 |
|
|
|
17 |
defs
|
|
|
18 |
complex_number_of_def
|
|
|
19 |
"number_of v == complex_of_real (number_of v)"
|
|
|
20 |
(*::bin=>complex ::bin=>complex*)
|
|
|
21 |
|
|
|
22 |
end
|