equal
deleted
inserted
replaced
9 theory Complex |
9 theory Complex |
10 imports Transcendental |
10 imports Transcendental |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 |
14 We use the @{text codatatype} command to define the type of complex numbers. This allows us to use |
15 We use the @{text codatatype}-command to define the type of complex numbers. This might look strange |
15 @{text primcorec} to define complex functions by defining their real and imaginary result |
16 at first, but allows us to use @{text primcorec} to define complex-functions by defining their |
16 separately. |
17 real and imaginary result separate. |
|
18 |
|
19 *} |
17 *} |
20 |
18 |
21 codatatype complex = Complex (Re: real) (Im: real) |
19 codatatype complex = Complex (Re: real) (Im: real) |
22 |
20 |
23 lemma complex_surj: "Complex (Re z) (Im z) = z" |
21 lemma complex_surj: "Complex (Re z) (Im z) = z" |