1structure CSimp :> CSimp = 2struct 3 4open HolKernel boolLib CooperThms intSyntax integerTheory int_arithTheory 5 6(* Fix the grammar used by this file *) 7structure Parse = struct 8 open Parse 9 val (Type,Term) = parse_from_grammars boolTheory.bool_grammars 10end 11open Parse 12 13val lhand = rand o rator 14 15fun has_atom dthis is_other t = let 16 val (t1, t2) = dthis t 17in 18 has_atom dthis is_other t1 orelse has_atom dthis is_other t2 19end handle HOL_ERR _ => not (is_other t) 20 21fun find_atom ASSOC COMM dthis is_other t = let 22 val find_atom = find_atom ASSOC COMM dthis is_other 23 val is_this = can dthis 24 fun move_atom_from_left t = 25 if is_this (lhand t) then REWR_CONV (GSYM ASSOC) t 26 else ALL_CONV t 27 val move_atom_from_right = REWR_CONV COMM THENC move_atom_from_left 28 val (t1, t2) = dthis t 29in 30 if has_atom dthis is_other t1 then 31 LAND_CONV find_atom THENC move_atom_from_left 32 else 33 RAND_CONV find_atom THENC move_atom_from_right 34end t handle (e as HOL_ERR _) => if is_other t then raise e else ALL_CONV t 35 36datatype matchmode = NOMATCH | NEGATED | POSITIVE 37fun compare_pair accmode eqnp tp = 38 if rand eqnp <> rand tp then NOMATCH 39 else let 40 val e_coeff = lhand eqnp 41 val t_coeff = lhand tp 42 val (e_negged, e_core) = 43 if is_negated e_coeff then (true, rand e_coeff) 44 else (false, e_coeff) 45 val (t_negged, t_core) = 46 if is_negated t_coeff then (true, rand t_coeff) 47 else (false, t_coeff) 48 val possible_mode = 49 if e_negged <> t_negged then NEGATED else POSITIVE 50 in 51 if accmode = NOMATCH orelse possible_mode = accmode then 52 if e_core = t_core then possible_mode 53 else NOMATCH 54 else NOMATCH 55 end 56fun determine_match accmode eqnpart tpart = 57 case (is_plus eqnpart, is_plus tpart) of 58 (true, true) => let 59 in 60 case compare_pair accmode (rand eqnpart) (rand tpart) of 61 NOMATCH => NOMATCH 62 | newacc => determine_match newacc (lhand eqnpart) (lhand tpart) 63 end 64 | (false, false) => compare_pair accmode eqnpart tpart 65 | _ => NOMATCH 66 67val cvar = mk_var("c", intSyntax.int_ty) 68val xvar = mk_var("x", intSyntax.int_ty) 69val yvar = mk_var("y", intSyntax.int_ty) 70val gv = genvar int_ty 71val handle_negs = PURE_REWRITE_RULE [INT_NEG_ADD, INT_NEG_LMUL, INT_NEGNEG, 72 INT_NEG_0] 73fun EQRWT eqn = let 74 val (varpart, numpart) = dest_plus (rand (concl eqn)) 75 val eq1 = MP (INST [cvar |-> varpart, xvar |-> numpart, yvar |-> gv] 76 eq_context_rwt1) eqn 77 val eq2 = handle_negs (MP (INST [cvar |-> varpart, xvar |-> numpart, 78 yvar |-> gv] 79 eq_context_rwt2) eqn) 80in 81 (fn t => 82 if is_eq t then 83 case determine_match NOMATCH varpart (lhand (rand t)) of 84 NOMATCH => ALL_CONV t 85 | POSITIVE => (LAND_CONV (K eqn) THENC REWR_CONV INT_EQ_LADD THENC 86 CooperMath.REDUCE_CONV) t 87 | NEGATED => raise Fail "EQRWT : should never happen" 88 else if is_leq t then 89 case determine_match NOMATCH varpart (lhand (rand t)) of 90 NOMATCH => ALL_CONV t 91 | POSITIVE => (K (INST [gv |-> rand (rand t)] eq1) THENC 92 CooperMath.REDUCE_CONV) t 93 | NEGATED => (K (INST [gv |-> rand (rand t)] eq2) THENC 94 CooperMath.REDUCE_CONV) t 95 else ALL_CONV t) 96end 97 98 99fun LTRWT ltthm = let 100 val (varpart, numpart) = dest_plus (rand (concl ltthm)) 101 val n = int_of_term numpart 102 val rwt1 = MP (INST [cvar |-> varpart, xvar |-> numpart, 103 yvar |-> gv] le_context_rwt1) ltthm 104 val rwt2 = handle_negs (MP (INST [cvar |-> varpart, xvar |-> numpart, 105 yvar |-> gv] le_context_rwt2) ltthm) 106 val rwt3 = MP (INST [cvar |-> varpart, xvar |-> numpart, 107 yvar |-> gv] le_context_rwt3) ltthm 108 val rwt4 = handle_negs (MP (INST [cvar |-> varpart, xvar |-> numpart, 109 yvar |-> gv] le_context_rwt4) ltthm) 110 val rwt5 = CONV_RULE (RAND_CONV (TRY_CONV OmegaMath.leaf_normalise)) 111 (handle_negs (MP (INST [cvar |-> varpart, 112 xvar |-> numpart] 113 le_context_rwt5) 114 ltthm)) 115in 116 (fn t => 117 if is_eq t then 118 case determine_match NOMATCH varpart (lhand (rand t)) of 119 NOMATCH => ALL_CONV t 120 | POSITIVE => let val tnumpart = rand (rand t) 121 in 122 if Arbint.<(n, int_of_term tnumpart) then 123 MP (CONV_RULE (LAND_CONV CooperMath.REDUCE_CONV) 124 (INST [gv |-> tnumpart] rwt3)) TRUTH 125 else ALL_CONV t 126 end 127 | NEGATED => let val tnumpart = rand (rand t) 128 in 129 if Arbint.<(n, Arbint.~(int_of_term tnumpart)) then 130 MP (CONV_RULE (LAND_CONV CooperMath.REDUCE_CONV) 131 (INST [gv |-> tnumpart] rwt4)) TRUTH 132 else ALL_CONV t 133 end 134 else if is_leq t then 135 case determine_match NOMATCH varpart (lhand (rand t)) of 136 NOMATCH => ALL_CONV t 137 | POSITIVE => let val tnumpart = rand (rand t) 138 in 139 if Arbint.<=(n, int_of_term tnumpart) then 140 MP (CONV_RULE (LAND_CONV CooperMath.REDUCE_CONV) 141 (INST [gv |-> tnumpart] rwt1)) TRUTH 142 else 143 ALL_CONV t 144 end 145 | NEGATIVE => let val tnumpart = rand (rand t) 146 open Arbint 147 in 148 case compare(int_of_term tnumpart, ~ n) of 149 LESS => MP (CONV_RULE 150 (LAND_CONV CooperMath.REDUCE_CONV) 151 (INST [gv |-> tnumpart] rwt2)) 152 TRUTH 153 | EQUAL => rwt5 154 | GREATER => ALL_CONV t 155 end 156 else ALL_CONV t) 157end 158 159 160fun disj_cong0 t = let 161 val (d1, d2) = dest_disj t 162 val notd1_t = mk_neg d1 163 val notd1_th = ASSUME notd1_t 164 val d2_rewritten = 165 if is_neg d1 then 166 DISCH notd1_t 167 (REWRITE_CONV [CONV_RULE (REWR_CONV NOT_NOT_P) notd1_th] d2) 168 else if is_divides d1 orelse is_eq d1 then 169 DISCH notd1_t (REWRITE_CONV [notd1_th] d2) 170 else let 171 val notd1_thm = CONV_RULE OmegaMath.leaf_normalise notd1_th 172 in 173 DISCH notd1_t (CooperMath.BLEAF_CONV (op THENC) (LTRWT notd1_thm) d2) 174 end 175in 176 K (MATCH_MP simple_disj_congruence d2_rewritten) THENC 177 TRY_CONV (REWR_CONV T_or_r ORELSEC REWR_CONV F_or_r) 178end t 179 180val disj_cong = 181 REWR_CONV T_or_l ORELSEC REWR_CONV F_or_l ORELSEC disj_cong0 182 183fun conj_cong0 t = let 184 val (c1, c2) = dest_conj t 185 val c1_thm = ASSUME c1 186 val c2_rewritten = 187 if is_eq c1 then 188 DISCH c1 (CooperMath.BLEAF_CONV (op THENC) (EQRWT c1_thm) c2) 189 else if is_leq c1 then 190 DISCH c1 (CooperMath.BLEAF_CONV (op THENC) (LTRWT c1_thm) c2) 191 else 192 DISCH c1 (REWRITE_CONV [EQT_INTRO c1_thm 193 handle HOL_ERR _ => EQF_INTRO c1_thm] c2) 194in 195 K (MATCH_MP simple_conj_congruence c2_rewritten) THENC 196 TRY_CONV (REWR_CONV T_and_r ORELSEC REWR_CONV F_and_r) 197end t 198 199val conj_cong = 200 REWR_CONV T_and_l ORELSEC REWR_CONV F_and_l ORELSEC conj_cong0 201 202fun IFP is c tm = if is tm then c tm else ALL_CONV tm 203 204fun csimp tm = let 205in 206 if is_disj tm then 207 if has_atom dest_disj is_conj tm then 208 find_atom DISJ_ASSOC DISJ_COMM dest_disj is_conj THENC 209 disj_cong THENC IFP is_disj (RAND_CONV csimp) 210 else BINOP_CONV csimp 211 else if is_conj tm then 212 if has_atom dest_conj is_disj tm then 213 find_atom CONJ_ASSOC CONJ_COMM dest_conj is_disj THENC 214 conj_cong THENC IFP is_conj (RAND_CONV csimp) 215 else BINOP_CONV csimp 216 else ALL_CONV 217end tm 218 219end (* struct *) 220