1(*****************************************************************************)
2(* Define complex rationals                                                  *)
3(*****************************************************************************)
4
5(*****************************************************************************)
6(* Ignore everything up to "END BOILERPLATE"                                 *)
7(*****************************************************************************)
8
9(*****************************************************************************)
10(* START BOILERPLATE NEEDED FOR COMPILATION                                  *)
11(*****************************************************************************)
12
13(******************************************************************************
14* Load theories
15******************************************************************************)
16(* The commented out stuff below should be loaded in interactive sessions
17quietdec := true;
18map
19 load
20 ["intLib","gcdTheory", "fracLib", "ratLib"];
21open intLib gcdTheory fracLib ratLib ratTheory;
22quietdec := false;
23*)
24
25(******************************************************************************
26* Boilerplate needed for compilation: open HOL4 systems modules
27******************************************************************************)
28open HolKernel Parse boolLib bossLib;
29
30(******************************************************************************
31* Open theories (including ratTheory from Jens Brandt)
32******************************************************************************)
33open gcdTheory fracLib ratLib ratTheory;
34
35(*****************************************************************************)
36(* END BOILERPLATE                                                           *)
37(*****************************************************************************)
38
39(*****************************************************************************)
40(* Start new theory "complex_rational"                                       *)
41(*****************************************************************************)
42val _ = new_theory "complex_rational";
43
44(*****************************************************************************)
45(* A complex rational x+yi is a pair of rational numbers.                    *)
46(* The type ``:complex_rational`` is a datatype isomorphic to                *)
47(* ``:rat # rat``, with curried constructor ``COMPLEX_RATIONAL``.            *)
48(*****************************************************************************)
49val _ = Hol_datatype `complex_rational = COMPLEX_RATIONAL of rat => rat`;
50
51(*****************************************************************************)
52(* Abbreviation for the complex rational constructor                         *)
53(*****************************************************************************)
54val _ = overload_on("com", ``COMPLEX_RATIONAL``);
55
56(*****************************************************************************)
57(* Complex rationals representing 0 and 1                                    *)
58(*****************************************************************************)
59val com_0_def = Define `com_0 = com rat_0 rat_0`
60and com_1_def = Define `com_1 = com rat_1 rat_0`;
61
62(*****************************************************************************)
63(* Define complex addition                                                   *)
64(*****************************************************************************)
65val COMPLEX_ADD_def =
66 Define
67  `COMPLEX_ADD (com a1 b1) (com a2 b2) =
68    com (a1+a2) (b1+b2)`;
69
70(*****************************************************************************)
71(* Overload "+" onto complex addition                                        *)
72(*****************************************************************************)
73val _ = overload_on("+", ``COMPLEX_ADD``);
74
75(*****************************************************************************)
76(* Define complex subtraction                                                *)
77(*****************************************************************************)
78val COMPLEX_SUB_def =
79 Define
80  `COMPLEX_SUB (com a1 b1) (com a2 b2) =
81    com (a1-a2) (b1-b2)`;
82
83(*****************************************************************************)
84(* Overload "-" onto complex subtraction                                     *)
85(*****************************************************************************)
86val _ = overload_on("-", ``COMPLEX_SUB``);
87
88(*****************************************************************************)
89(* Complex multiplication                                                    *)
90(*****************************************************************************)
91val COMPLEX_MULT_def =
92 Define
93  `COMPLEX_MULT (com a1 b1) (com a2 b2) =
94    com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
95
96(*****************************************************************************)
97(* Overload "*" onto complex multiplication                                  *)
98(*****************************************************************************)
99val _ = overload_on("*", ``COMPLEX_MULT``);
100
101(*****************************************************************************)
102(* Complex reciprocal (1/x)                                                  *)
103(*****************************************************************************)
104val COMPLEX_RECIPROCAL_def =
105 Define
106  `COMPLEX_RECIPROCAL (com a b) = com (a/(a*a + b*b)) ((~b)/(a*a + b*b))`;
107
108(*****************************************************************************)
109(* Complex comparisions                                                      *)
110(*****************************************************************************)
111
112val COMPLEX_LT_def =
113 Define
114  `COMPLEX_LT (com ra ia) (com rb ib) =
115    (ra < rb) \/ ((ra = rb) /\ (ia < ib))`;
116
117val COMPLEX_LE_def =
118 Define
119  `COMPLEX_LE (com ra ia) (com rb ib) =
120    (ra < rb) \/ ((ra = rb) /\ (ia <= ib))`;
121
122val COMPLEX_GT_def =
123 Define
124  `COMPLEX_GT (com ra ia) (com rb ib) =
125    (ra > rb) \/ ((ra = rb) /\ (ia > ib))`;
126
127val COMPLEX_GE_def =
128 Define
129  `COMPLEX_GE (com ra ia) (com rb ib) =
130    (ra > rb) \/ ((ra = rb) /\ (ia >= ib))`;
131
132(*****************************************************************************)
133(* Overload "<", ">", "<=",">=" onto complex comparisons                     *)
134(*****************************************************************************)
135
136val _ = overload_on("<",``COMPLEX_LT``);
137val _ = overload_on("<=",``COMPLEX_LE``);
138val _ = overload_on(">",``COMPLEX_GT``);
139val _ = overload_on(">=",``COMPLEX_GE``);
140
141(*****************************************************************************)
142(* Complex negation                                                          *)
143(*****************************************************************************)
144
145val COMPLEX_NEG_def = Define `COMPLEX_NEG a = com_0 - a`;
146
147(*****************************************************************************)
148(* Overload "~" onto complex negation                                        *)
149(*****************************************************************************)
150
151val _ = overload_on("~",``COMPLEX_NEG``);
152
153(*****************************************************************************)
154(* Complex division                                                          *)
155(*****************************************************************************)
156
157val COMPLEX_DIV_def = Define `COMPLEX_DIV a b = a * (COMPLEX_RECIPROCAL b)`;
158
159(*****************************************************************************)
160(* Overload "/" onto complex division                                        *)
161(*****************************************************************************)
162
163val _ = overload_on("/",``COMPLEX_DIV``);
164
165(*****************************************************************************)
166(* DIVIDES : int->int->bool  tests if first argument divides second argument *)
167(*                                                                           *)
168(* Uses:                                                                     *)
169(*  ABS     : int -> int          get absolute value                         *)
170(*  Num     : int -> num          convert non-negative integer to a natural  *)
171(*  MOD     : num -> num -> num   compute remainder (curried infix)          *)
172(*                                                                           *)
173(*****************************************************************************)
174val DIVIDES_def = Define `DIVIDES m n = (Num(ABS n) MOD Num(ABS m) = 0)`;
175
176(*****************************************************************************)
177(* Test if a complex rational is an integer                                  *)
178(*                                                                           *)
179(* Uses following auxiliary functions:                                       *)
180(*                                                                           *)
181(*  rat_nmr : rat->int          get numerator                                *)
182(*  rat_dnm : rat->int          get denominator                              *)
183(*                                                                           *)
184(*****************************************************************************)
185val IS_INT_def =
186 Define
187  `IS_INT(com a b) = DIVIDES (rat_dnm a) (rat_nmr a) /\ (b = rat_0)`;
188
189(*****************************************************************************)
190(* Need GCD to put a fraction in lowest terms for computing numerator and    *)
191(* denominator                                                               *)
192(*                                                                           *)
193(*    numerator(m/n) = m/(gcd m n)                                           *)
194(*  denominator(m/n) = n/(gcd m n)                                           *)
195(*****************************************************************************)
196
197(*****************************************************************************)
198(* Divide each component of a pair of integers by their gcd and return       *)
199(* the reduced pair: (x,y) |--> (x/(gcd x y), y/(gcd x y))                   *)
200(*****************************************************************************)
201val reduce_def =
202 Define
203  `reduce(x,y) =
204    let n = &(gcd (Num(ABS x)) (Num(ABS y))) in (x/n, y/n)`;
205
206(*****************************************************************************)
207(* Reduce a rational to lowest terms and return numerator as an integer      *)
208(*****************************************************************************)
209val reduced_nmr_def =
210 Define
211  `reduced_nmr r = FST(reduce(rep_frac(rep_rat r)))`;
212
213(*****************************************************************************)
214(* Reduce a rational to lowest terms and return denominator as an integer    *)
215(*****************************************************************************)
216val reduced_dnm_def =
217 Define
218  `reduced_dnm r = SND(reduce(rep_frac(rep_rat r)))`;
219
220(*****************************************************************************)
221(* Multiplication theorems for use in translation                            *)
222(*****************************************************************************)
223
224val COMPLEX_MULT_COMM =
225 store_thm
226   ("COMPLEX_MULT_COMM",
227    ``a * b = b * a:complex_rational``,
228    Cases_on `a` THEN Cases_on `b`
229     THEN RW_TAC std_ss [COMPLEX_MULT_def]
230     THEN METIS_TAC [RAT_MUL_COMM,RAT_ADD_COMM]);
231
232val COMPLEX_MULT_ASSOC =
233 store_thm
234  ("COMPLEX_MULT_ASSOC",
235   ``a * (b * c) = a * b * c:complex_rational``,
236   Cases_on `a` THEN Cases_on `b` THEN Cases_on `c`
237    THEN RW_TAC std_ss
238          [COMPLEX_MULT_def,RAT_LDISTRIB,RAT_RDISTRIB,
239           RAT_SUB_ADDAINV,GSYM RAT_AINV_LMUL,GSYM RAT_AINV_RMUL,
240           RAT_ADD_ASSOC,RAT_MUL_ASSOC,RAT_AINV_ADD]
241    THEN METIS_TAC
242          [RAT_MUL_COMM,RAT_MUL_ASSOC,RAT_ADD_COMM,RAT_ADD_ASSOC]);
243
244val COMPLEX_MULT_RID =
245 store_thm
246  ("COMPLEX_MULT_RID",
247   ``a * com_1 = a``,
248   Cases_on `a`
249    THEN RW_TAC std_ss
250          [com_1_def,COMPLEX_MULT_def,GSYM rat_0,rat_0_def,
251           GSYM rat_1,rat_1_def,RAT_MUL_RID,RAT_MUL_RZERO,
252           RAT_ADD_RID,RAT_SUB_RID]);
253
254val _ = export_theory();
255