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