1(*=========================================================================== 2== LIBRARY: reduce (part II) == 3== == 4== DESCRIPTION: Conversions to reduce arithmetic constant expressions == 5== == 6== AUTHOR: Michael Norrish == 7== University of Cambridge Computer Laboratory == 8== New Museums Site == 9== Pembroke Street == 10== Cambridge CB2 3QG == 11== England. == 12== == 13== mn200@cl.cam.ac.uk == 14== == 15== DATE: January 1999 == 16== == 17== NOTE: The original functionality in this file was provided by == 18== carefully written CONVs. With the use of proper numerals == 19== (see numeralTheory), this is no longer necessary, and == 20== simple rewriting can be used for most tasks. == 21== It is the (untested) claim that this will be as efficient. == 22============================================================================*) 23 24structure Arithconv :> Arithconv = 25struct 26 27open HolKernel boolTheory boolLib Parse Rsyntax 28 Num_conv numSyntax arithmeticTheory numeralTheory; 29 30val ambient_grammars = Parse.current_grammars(); 31val _ = Parse.temp_set_grammars arithmeticTheory.arithmetic_grammars 32 33val ERR = mk_HOL_ERR "Arithconv" 34fun failwith function = raise (ERR function "") 35 36 37(*--------------------------------------------------------------------------- 38 A "conv-al" that takes a conv and makes it fail if the 39 result is not either true, false or a numeral. 40 ---------------------------------------------------------------------------*) 41 42fun TFN_CONV c t = 43 let val result = c t 44 val result_t = rhs (concl result) 45 in 46 if aconv result_t T orelse aconv result_t F orelse 47 Literal.is_numeral result_t 48 then 49 result 50 else failwith "TFN_CONV" 51end 52 53 54(*-----------------------------------------------------------------------*) 55(* NEQ_CONV "[x] = [y]" = |- ([x] = [y]) = [x=y -> T | F] *) 56(*-----------------------------------------------------------------------*) 57 58local 59 val NEQ_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_eq]) 60 val REFL_CLAUSE_num = INST_TYPE [alpha |-> num] REFL_CLAUSE 61in 62fun NEQ_CONV tm = 63 case total boolLib.dest_eq tm 64 of NONE => failwith "NEQ_CONV" 65 | SOME (n1,n2) => 66 if is_numeral n1 andalso is_numeral n2 then 67 if aconv n1 n2 then SPEC n1 REFL_CLAUSE_num 68 else with_exn NEQ_RW tm (ERR "NEQ_CONV" "") 69 else failwith "NEQ_CONV" 70end; 71 72(*-----------------------------------------------------------------------*) 73(* LT_CONV "[x] < [y]" = |- ([x] < [y]) = [x<y -> T | F] *) 74(*-----------------------------------------------------------------------*) 75 76local val LT_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_lt]) 77in 78fun LT_CONV tm = 79 if is_less tm then with_exn LT_RW tm (ERR "LT_CONV" "") 80 else failwith "LT_CONV" 81end; 82 83(*-----------------------------------------------------------------------*) 84(* GT_CONV "[x] > [y]" = |- ([x] > [y]) = [x>y -> T | F] *) 85(*-----------------------------------------------------------------------*) 86 87local val GT_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_lt]) 88in 89fun GT_CONV tm = 90 if is_greater tm then with_exn GT_RW tm (ERR "GT_CONV" "") 91 else failwith "GT_CONV" 92end; 93 94(*-----------------------------------------------------------------------*) 95(* LE_CONV "[x] <= [y]" = |- ([x]<=> [y]) = [x<=y -> T | F] *) 96(*-----------------------------------------------------------------------*) 97 98local val LE_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_lte]) 99in 100fun LE_CONV tm = 101 if is_leq tm then with_exn LE_RW tm (ERR "LE_CONV" "") else failwith "LE_CONV" 102end; 103 104(*-----------------------------------------------------------------------*) 105(* GE_CONV "[x] >= [y]" = |- ([x] >= [y]) = [x>=y -> T | F] *) 106(*-----------------------------------------------------------------------*) 107 108local val GE_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_lte]) 109in 110fun GE_CONV tm = 111 if is_geq tm then with_exn GE_RW tm (ERR "GE_CONV" "") 112 else failwith "GE_CONV" 113end; 114 115(*-----------------------------------------------------------------------*) 116(* EVEN_CONV "EVEN [x]" = |- EVEN [x] = [ x divisible by 2 -> T | F ] *) 117(*-----------------------------------------------------------------------*) 118 119local val EC = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_evenodd]) 120in 121fun EVEN_CONV tm = 122 if is_even tm then with_exn EC tm (ERR "EVEN_CONV" "") 123 else failwith "EVEN_CONV" 124end 125 126(*-----------------------------------------------------------------------*) 127(* ODD_CONV "ODD [x]" = |- ODD [x] = [ x divisible by 2 -> F | T ] *) 128(*-----------------------------------------------------------------------*) 129 130local val OC = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_evenodd]) 131in 132fun ODD_CONV tm = 133 if is_odd tm then with_exn OC tm (ERR "ODD_CONV" "") else failwith "ODD_CONV" 134end 135 136(*-----------------------------------------------------------------------*) 137(* SUC_CONV "SUC [x]" = |- SUC [x] = [x+1] *) 138(*-----------------------------------------------------------------------*) 139 140local val SUC_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_suc]) 141in 142fun SUC_CONV tm = 143 if is_suc tm then with_exn SUC_RW tm (ERR "SUC_CONV" "") 144 else failwith "SUC_CONV" 145end; 146 147(*-----------------------------------------------------------------------*) 148(* PRE_CONV "PRE [n]" = |- PRE [n] = [n-1] *) 149(*-----------------------------------------------------------------------*) 150 151local 152 val PRE_RW = TFN_CONV (REWRITE_CONV [numeral_distrib, numeral_pre,NORM_0]) 153in 154fun PRE_CONV tm = 155 if is_pre tm then with_exn PRE_RW tm (ERR "PRE_CONV" "") 156 else failwith "PRE_CONV" 157end; 158 159(*-----------------------------------------------------------------------*) 160(* SBC_CONV "[x] - [y]" = |- ([x] - [y]) = [x - y] *) 161(*-----------------------------------------------------------------------*) 162 163local 164 val SBC_RW = 165 TFN_CONV (REWRITE_CONV 166 [numeral_distrib, numeral_sub,iSUB_THM, 167 iDUB_removal,numeral_pre, numeral_lt]) 168in 169fun SBC_CONV tm = 170 if is_minus tm then with_exn SBC_RW tm (ERR "SBC_CONV" "") 171 else failwith "SBC_CONV" 172end; 173 174(*-----------------------------------------------------------------------*) 175(* ADD_CONV "[x] + [y]" = |- [x] + [y] = [x+y] *) 176(*-----------------------------------------------------------------------*) 177 178local 179 val ADD_RW = 180 TFN_CONV (REWRITE_CONV 181 [numeral_distrib, numeral_add,numeral_suc, numeral_iisuc]) 182in 183fun ADD_CONV tm = 184 if is_plus tm then with_exn ADD_RW tm (ERR "ADD_CONV" "") 185 else failwith "ADD_CONV" 186end; 187 188(*-----------------------------------------------------------------------*) 189(* MUL_CONV "[x] * [y]" = |- [x] * [y] = [x * y] *) 190(*-----------------------------------------------------------------------*) 191 192local 193 val MUL_RW = 194 TFN_CONV (REWRITE_CONV 195 [numeral_distrib, numeral_add, numeral_suc, 196 numeral_iisuc, numeral_mult, iDUB_removal, numeral_pre]) 197in 198fun MUL_CONV tm = 199 if is_mult tm then with_exn MUL_RW tm (ERR "MUL_CONV" "") 200 else failwith "MUL_CONV" 201end; 202 203(*-----------------------------------------------------------------------*) 204(* EXP_CONV "[x] EXP [y]" = |- [x] EXP [y] = [x ** y] *) 205(*-----------------------------------------------------------------------*) 206 207local 208 val RW1 = REWRITE_CONV [numeral_distrib, numeral_exp] 209 val RW2 = REWRITE_CONV [numeral_add, numeral_suc, numeral_iisuc, 210 numeral_mult, iDUB_removal, numeral_pre, iSQR] 211 val EXP_RW = TFN_CONV (RW1 THENC RW2) 212in 213fun EXP_CONV tm = 214 if is_exp tm then with_exn EXP_RW tm (ERR "EXP_CONV" "") 215 else failwith "EXP_CONV" 216end; 217 218(*-----------------------------------------------------------------------*) 219(* DIV_CONV "[x] DIV [y]" = |- [x] DIV [y] = [x div y] *) 220(*-----------------------------------------------------------------------*) 221 222fun provelt x y = EQT_ELIM (LT_CONV (mk_less(mk_numeral x, mk_numeral y))) 223 224val xv = mk_var {Name= "x", Ty=num} 225val yv = mk_var {Name= "y", Ty=num} 226val zv = mk_var {Name= "z", Ty=num} 227val pv = mk_var {Name= "p", Ty=num} 228val qv = mk_var {Name= "q", Ty=num} 229val rv = mk_var {Name= "r", Ty=num}; 230 231local val divt = 232 prove((���(q * y = p) ==> (p + r = x) ==> (r < y) ==> (x DIV y = q)���), 233 REPEAT DISCH_TAC THEN 234 MATCH_MP_TAC (arithmeticTheory.DIV_UNIQUE) THEN 235 EXISTS_TAC (���r:num���) THEN ASM_REWRITE_TAC[]) 236in 237fun DIV_CONV tm = 238 let open Arbnum 239 val (xn,yn) = dest_div tm 240 val x = dest_numeral xn 241 and y = dest_numeral yn 242 val q = x div y 243 val p = q * y 244 val r = x - p 245 val pn = mk_numeral p 246 and qn = mk_numeral q 247 and rn = mk_numeral r 248 val p1 = MUL_CONV (mk_mult(qn,yn)) 249 and p2 = ADD_CONV (mk_plus(pn,rn)) 250 and p3 = provelt r y 251 and chain = INST [xv |-> xn, yv |-> yn, pv |-> pn, 252 qv |-> qn, rv |-> rn] divt 253 in 254 MP (MP (MP chain p1) p2) p3 255 end handle HOL_ERR _ => failwith "DIV_CONV" 256 | Div => raise ERR "DIV_CONV" "attempt to divide by zero" 257end; 258 259(*-----------------------------------------------------------------------*) 260(* MOD_CONV "[x] MOD [y]" = |- [x] MOD [y] = [x mod y] *) 261(*-----------------------------------------------------------------------*) 262 263local val modt = 264 prove(���(q * y = p) ==> (p + r = x) ==> (r < y) ==> (x MOD y = r)���, 265 REPEAT DISCH_TAC THEN 266 MATCH_MP_TAC arithmeticTheory.MOD_UNIQUE THEN 267 EXISTS_TAC ���q:num��� THEN ASM_REWRITE_TAC[]) 268in 269fun MOD_CONV tm = 270 let open Arbnum 271 val (xn,yn) = dest_mod tm 272 val x = dest_numeral xn 273 and y = dest_numeral yn 274 val q = x div y 275 val p = q * y 276 val r = x - p 277 val pn = mk_numeral p 278 and qn = mk_numeral q 279 and rn = mk_numeral r 280 val p1 = MUL_CONV (mk_mult(qn,yn)) 281 and p2 = ADD_CONV (mk_plus(pn,rn)) 282 and p3 = provelt r y 283 and chain = INST [xv |-> xn, yv |-> yn, pv |-> pn, 284 qv |-> qn, rv |-> rn] modt 285 in 286 MP (MP (MP chain p1) p2) p3 287 end handle HOL_ERR _ => failwith "MOD_CONV" 288 | Div => raise ERR "MOD_CONV" "attempt to take mod 0" 289end; 290 291val _ = Parse.temp_set_grammars ambient_grammars 292 293end 294