1structure NumRelNorms :> NumRelNorms = 2struct 3 4open HolKernel boolLib 5 6(* ---------------------------------------------------------------------- 7 basic canonisers 8 ---------------------------------------------------------------------- *) 9 10(* first define the records containing the necessary information for the 11 generic canoniser *) 12 13(* for addition - right-associated for backwards compatibility *) 14local 15 open numSyntax arithmeticTheory GenPolyCanon 16 fun is_good t = let 17 val (l,r) = dest_mult t 18 in 19 is_numeral l 20 end handle HOL_ERR _ => false 21 fun non_coeff t = if is_good t then rand t 22 else if is_numeral t then mk_var(" ", num) 23 else t 24 fun add_coeff (t:term) : thm = if is_good t then ALL_CONV t 25 else REWR_CONV (GSYM MULT_LEFT_1) t 26 val distrib = GSYM RIGHT_ADD_DISTRIB 27 fun merge t = let 28 val (l,r) = dest_plus t 29 in 30 if is_numeral l andalso is_numeral r then 31 reduceLib.REDUCE_CONV 32 else 33 Conv.BINOP_CONV add_coeff THENC 34 REWR_CONV distrib THENC LAND_CONV reduceLib.REDUCE_CONV 35 end t 36in 37 val rnatadd_gci = 38 GCI { dest = dest_plus, 39 assoc_mode = R, 40 assoc = ADD_ASSOC, 41 symassoc = GSYM ADD_ASSOC, 42 comm = ADD_COMM, 43 r_asscomm = derive_r_asscomm ADD_ASSOC ADD_COMM, 44 l_asscomm = derive_l_asscomm ADD_ASSOC ADD_COMM, 45 is_literal = is_numeral, 46 non_coeff = non_coeff, merge = merge, 47 postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL MULT)) ORELSEC 48 TRY_CONV (REWR_CONV MULT_LEFT_1), 49 left_id = CONJUNCT1 ADD, 50 right_id = ADD_0, 51 reducer = reduceLib.REDUCE_CONV} 52 val lnatadd_gci = 53 GCI { dest = dest_plus, 54 assoc_mode = L, 55 assoc = ADD_ASSOC, 56 symassoc = GSYM ADD_ASSOC, 57 comm = ADD_COMM, 58 r_asscomm = derive_r_asscomm ADD_ASSOC ADD_COMM, 59 l_asscomm = derive_l_asscomm ADD_ASSOC ADD_COMM, 60 is_literal = is_numeral, 61 non_coeff = non_coeff, merge = merge, 62 postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL MULT)) ORELSEC 63 TRY_CONV (REWR_CONV MULT_LEFT_1), 64 left_id = CONJUNCT1 ADD, 65 right_id = ADD_0, 66 reducer = reduceLib.REDUCE_CONV} 67end 68 69val ADDL_CANON_CONV = GenPolyCanon.gencanon lnatadd_gci 70val ADDR_CANON_CONV = GenPolyCanon.gencanon rnatadd_gci 71 72 73 74 75 76(* multiplication *) 77val lcnatmult_gci = let 78 open GenPolyCanon numSyntax arithmeticTheory 79 fun is_good t = let 80 val (l,r) = dest_exp t 81 in 82 is_numeral r 83 end handle HOL_ERR _ => false 84 fun non_coeff t = if is_good t then rand (rator t) 85 else if is_numeral t then mk_numeral Arbnum.one 86 else t 87 fun add_coeff t = if is_good t then ALL_CONV t 88 else REWR_CONV (GSYM (CONJUNCT2 (SPEC_ALL EXP_1))) t 89 val distrib = GSYM EXP_ADD 90 fun merge t = let 91 val (l,r) = dest_mult t 92 in 93 if is_numeral l andalso is_numeral r then reduceLib.REDUCE_CONV 94 else Conv.BINOP_CONV add_coeff THENC REWR_CONV distrib THENC 95 reduceLib.REDUCE_CONV 96 end t 97in 98 GCI { dest = dest_mult, 99 is_literal = is_numeral, 100 assoc_mode = L_Cflipped, 101 assoc = MULT_ASSOC, 102 symassoc = GSYM MULT_ASSOC, 103 comm = MULT_COMM, 104 r_asscomm = derive_r_asscomm MULT_ASSOC MULT_COMM, 105 l_asscomm = derive_l_asscomm MULT_ASSOC MULT_COMM, 106 non_coeff = non_coeff, 107 merge = merge, 108 postnorm = REWR_CONV (CONJUNCT1 (SPEC_ALL EXP)) ORELSEC 109 TRY_CONV (REWR_CONV (CONJUNCT2 (SPEC_ALL EXP_1))), 110 right_id = MULT_RIGHT_1, 111 left_id = MULT_LEFT_1, 112 reducer = reduceLib.REDUCE_CONV} 113end 114 115val MUL_CANON_CONV = GenPolyCanon.gencanon lcnatmult_gci 116 117 118 119(* normalisation of sums over relational operators *) 120structure NumRel_Base = 121struct 122 open numSyntax Abbrev 123 type t = Arbint.int 124 val dest = dest_plus 125 val zero = Arbint.zero 126 val one = Arbint.one 127 val one_t = mk_numeral (Arbint.toNat one) 128 val mk = mk_plus 129 val listmk = list_mk_plus 130 fun toNat t = Arbint.fromNat (dest_numeral t) 131 fun destf t = let 132 val (l,r) = dest_mult t 133 in 134 (toNat l, r) 135 end handle HOL_ERR _ => if is_numeral t then (toNat t, one_t) 136 else (Arbint.one, t) 137 fun mkf (i,t) = let 138 val i_t = mk_numeral(Arbint.toNat i) 139 in 140 if aconv t one_t then i_t else mk_mult(i_t, t) 141 end 142 val canon = ADDR_CANON_CONV 143 val addid = REWR_CONV (GSYM arithmeticTheory.ADD_0) 144 val op+ = Arbint.+ 145 val op- = Arbint.- 146 val op~ = Arbint.~ 147 val op < = Arbint.< 148end 149 150structure LEQ_NREL : RelNorm_Input = struct 151 open NumRel_Base 152 val destrel = dest_leq 153 val opr = leq_tm 154 val rwt = arithmeticTheory.LE_ADD_LCANCEL 155end 156 157structure LT_NREL : RelNorm_Input = struct 158 open NumRel_Base 159 val destrel = dest_less 160 val opr = less_tm 161 val rwt = arithmeticTheory.LT_ADD_LCANCEL 162end 163 164structure EQ_NREL : RelNorm_Input = struct 165 open NumRel_Base 166 val destrel = dest_eq 167 val opr = mk_thy_const{Name = "=", Thy = "min", Ty = num --> num --> bool} 168 val rwt = arithmeticTheory.EQ_ADD_LCANCEL 169end 170 171structure NumLEQNorm = GenRelNorm (LEQ_NREL); 172structure NumLTNorm = GenRelNorm (LT_NREL); 173structure NumEQNorm = GenRelNorm (EQ_NREL); 174 175val sum_leq_norm = NumLEQNorm.gen_relnorm 176val sum_lt_norm = NumLTNorm.gen_relnorm 177val sum_eq_norm = NumEQNorm.gen_relnorm 178 179 180end; 181