1structure intSimps :> intSimps = 2struct 3 4open HolKernel boolLib integerTheory intSyntax simpLib 5 6val ERR = mk_HOL_ERR "intSimps"; 7 8open intReduce 9 10(* ---------------------------------------------------------------------- 11 integer normalisations 12 ---------------------------------------------------------------------- *) 13 14 15local 16 open intSyntax integerTheory GenPolyCanon 17 val assoc = INT_ADD_ASSOC 18 val comm = INT_ADD_COMM 19 fun is_good t = let 20 val (l,r) = dest_mult t 21 in 22 is_int_literal l 23 end handle HOL_ERR _ => false 24 fun non_coeff t = if is_good t then rand t 25 else if is_negated t then rand t 26 else t 27 fun add_coeff t = 28 if is_good t then ALL_CONV t 29 else if is_negated t then REWR_CONV INT_NEG_MINUS1 t 30 else REWR_CONV (GSYM INT_MUL_LID) t 31 val distrib = GSYM INT_RDISTRIB 32 fun merge t = let 33 val (l,r) = dest_plus t 34 in 35 if is_int_literal l andalso is_int_literal r then 36 REDUCE_CONV 37 else BINOP_CONV add_coeff THENC 38 REWR_CONV distrib THENC 39 LAND_CONV REDUCE_CONV 40 end t 41in 42 val lintadd_gci = 43 GCI { dest = dest_plus, 44 assoc_mode = L, 45 is_literal = is_int_literal, 46 assoc = assoc, 47 symassoc = GSYM assoc, 48 comm = comm, 49 l_asscomm = derive_l_asscomm assoc comm, 50 r_asscomm = derive_r_asscomm assoc comm, 51 non_coeff = non_coeff, 52 merge = merge, 53 postnorm = REWR_CONV INT_MUL_LZERO ORELSEC 54 REWR_CONV INT_MUL_LID ORELSEC 55 TRY_CONV (REWR_CONV (GSYM INT_NEG_MINUS1)), 56 left_id = INT_ADD_LID, 57 right_id = INT_ADD_RID, 58 reducer = REDUCE_CONV } 59 val rintadd_gci = update_mode R lintadd_gci 60 val ADDL_CANON_CONV = gencanon lintadd_gci 61 val ADDR_CANON_CONV = gencanon rintadd_gci 62end 63 64 65 66(*---------------------------------------------------------------------------*) 67(* Support for ordered AC rewriting *) 68(*---------------------------------------------------------------------------*) 69 70val INT_ADD_AC_ss = ac_ss [(INT_ADD_ASSOC,INT_ADD_COMM)] 71val INT_MUL_AC_ss = ac_ss [(INT_MUL_ASSOC,INT_MUL_COMM)] 72val INT_AC_ss = merge_ss [INT_ADD_AC_ss,INT_MUL_AC_ss] 73 74 75(*---------------------------------------------------------------------------*) 76(* Standard simplifications for the integers. Does not use the integer *) 77(* decision procedure. *) 78(*---------------------------------------------------------------------------*) 79 80val INT_RWTS_ss = BasicProvers.thy_ssfrag "integer" 81 82val int_ss = 83 boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++ 84 sumSimps.SUM_ss ++ combinSimps.COMBIN_ss ++ 85 numSimps.REDUCE_ss ++ numSimps.ARITH_ss ++ INT_REDUCE_ss ++ 86 INT_RWTS_ss; 87 88(* Formerly the following underpowered version was used: 89 val int_ss = boolSimps.bool_ss ++ INT_REDUCE_ss; 90*) 91 92(* ---------------------------------------------------------------------- 93 INT_ARITH_ss 94 95 embedding Omega into a simpset fragment. 96 Derived from code to do the same for the natural numbers, which is in 97 src/num/arith/src/numSimps.sml 98 and 99 src/num/arith/src/Gen_arith.sml 100 ---------------------------------------------------------------------- *) 101 102fun contains_var tm = 103 if is_var tm then true 104 else if is_int_literal tm then false 105 else let 106 val (l, r) = dest_plus tm 107 handle HOL_ERR _ => 108 dest_mult tm 109 handle HOL_ERR _ => dest_minus tm 110 in 111 contains_var l orelse contains_var r 112 end handle HOL_ERR _ => contains_var (dest_absval tm) 113 handle HOL_ERR _ => true 114 (* final default value is true because the term in question must be a 115 complicated non-presburger thing that will get treated as a variable 116 anyway. *) 117 118fun is_linear_mult tm = let 119 val (l,r) = dest_mult tm 120in 121 not (contains_var l andalso contains_var r) 122end 123 124fun arg1 tm = rand (rator tm) 125val arg2 = rand 126 127val non_presburger_subterms = IntDP_Munge.non_presburger_subterms 128 129fun is_arith tm = 130 List.all (fn t => type_of t = int_ty) (non_presburger_subterms tm) 131 132fun contains_forall sense tm = 133 if is_conj tm orelse is_disj tm then 134 List.exists (contains_forall sense) (#2 (strip_comb tm)) 135 else if is_neg tm then 136 contains_forall (not sense) (rand tm) 137 else if is_imp tm then 138 contains_forall (not sense) (rand (rator tm)) orelse 139 contains_forall sense (rand tm) 140 else if is_forall tm then 141 sense orelse contains_forall sense (#2 (dest_forall tm)) 142 else if is_exists tm then 143 not sense orelse contains_forall sense (#2 (dest_exists tm)) 144 else false 145 146fun is_arith_thm thm = 147 not (null (hyp thm)) andalso is_arith (concl thm) 148 149val is_arith_asm = is_arith_thm o ASSUME 150 151open Trace Cache Traverse 152fun CTXT_ARITH DP DPname thms tm = let 153 val context = map concl thms 154 fun try gl = let 155 val gl' = list_mk_imp(context,gl) 156 val _ = trace (5, LZ_TEXT (fn () => "Trying cached arithmetic d.p. on "^ 157 term_to_string gl')) 158 in 159 rev_itlist (C MP) thms (DP gl') 160 end 161 val thm = EQT_INTRO (try tm) 162 handle (e as HOL_ERR _) => 163 if not (Feq tm) then EQF_INTRO (try(mk_neg tm)) else raise e 164in 165 trace(1,PRODUCE(tm,DPname,thm)); thm 166end 167 168fun crossprod (ll : 'a list list) : 'a list list = 169 case ll of 170 [] => [[]] 171 | h::t => let 172 val c = crossprod t 173 in 174 List.concat (map (fn hel => map (cons hel) c) h) 175 end 176fun prim_dest_const t = let 177 val {Thy,Name,...} = dest_thy_const t 178in 179 (Thy,Name) 180end 181 182fun dpvars t = let 183 fun recurse bnds acc t = let 184 val (f, args) = strip_comb t 185 fun go2() = let 186 val (t1, t2) = (hd args, hd (tl args)) 187 in 188 recurse bnds (recurse bnds acc t1) t2 189 end 190 fun go1 () = recurse bnds acc (hd args) 191 in 192 case Lib.total prim_dest_const f of 193 SOME ("bool", "~") => go1() 194 | SOME ("bool", "/\\") => go2() 195 | SOME ("bool", "\\/") => go2() 196 | SOME ("min", "==>") => go2() 197 | SOME ("min", "=") => go2() 198 | SOME ("bool", "COND") => let 199 val (t1,t2,t3) = (hd args, hd (tl args), hd (tl (tl args))) 200 in 201 recurse bnds (recurse bnds (recurse bnds acc t1) t2) t3 202 end 203 | SOME ("integer", "int_add") => go2() 204 | SOME ("integer", "int_sub") => go2() 205 | SOME ("integer", "int_gt") => go2() 206 | SOME ("integer", "int_lt") => go2() 207 | SOME ("integer", "int_le") => go2() 208 | SOME ("integer", "int_ge") => go2() 209 | SOME ("integer", "int_mod") => go2() 210 | SOME ("integer", "int_div") => go2() 211 | SOME ("integer", "int_neg") => go1() 212 | SOME ("integer", "ABS") => go1() 213 | SOME ("integer", "int_mul") => let 214 val args = intSyntax.strip_mult t 215 val arg_vs = map (HOLset.listItems o recurse bnds empty_tmset) args 216 val cs = crossprod (filter (not o null) arg_vs) 217 in 218 case cs of 219 [] => acc 220 | [[]] => acc 221 | _ => let 222 val var_ts = map (intSyntax.list_mk_mult o 223 Listsort.sort Term.compare) cs 224 in 225 List.foldl (fn (t,acc)=>HOLset.add(acc,t)) acc var_ts 226 end 227 end 228 | SOME ("bool", "!") => let 229 val (v, bod) = dest_abs (hd args) 230 in 231 recurse (HOLset.add(bnds, v)) acc bod 232 end 233 | SOME ("bool", "?") => let 234 val (v, bod) = dest_abs (hd args) 235 in 236 recurse (HOLset.add(bnds, v)) acc bod 237 end 238 | SOME _ => if is_int_literal t then acc 239 else HOLset.add(acc, t) 240 | NONE => if is_var t then if HOLset.member(bnds, t) then acc 241 else HOLset.add(acc, t) 242 else HOLset.add(acc, t) 243 end 244in 245 HOLset.listItems (recurse empty_tmset empty_tmset t) 246end 247 248 249fun mkSS DPname DP = let 250 val (CDP, cache) = let 251 fun check tm = 252 type_of tm = Type.bool andalso is_arith tm andalso not (Teq tm) 253 in 254 RCACHE (dpvars,check,CTXT_ARITH DP DPname) 255 (* the check function determines whether or not a term might be handled 256 by the decision procedure -- we want to handle F, because it's possible 257 that we have accumulated a contradictory context. *) 258 end 259 val ARITH_REDUCER = let 260 exception CTXT of thm list 261 fun get_ctxt e = (raise e) handle CTXT c => c 262 fun add_ctxt(ctxt, newthms) = let 263 val addthese = filter (fn th => is_arith_thm th andalso 264 not (Feq (concl th))) 265 (flatten (map CONJUNCTS newthms)) 266 in 267 CTXT (addthese @ get_ctxt ctxt) 268 end 269 in 270 REDUCER {name = SOME DPname, 271 addcontext = add_ctxt, 272 apply = fn args => CDP (get_ctxt (#context args)), 273 initial = CTXT []} 274 end 275in 276 (SSFRAG {name=SOME (DPname ^ "_ss"), 277 convs = [], rewrs = [], congs = [], 278 filter = NONE, ac = [], dprocs = [ARITH_REDUCER]}, 279 cache) 280end 281 282val (OMEGA_ss, omega_cache) = mkSS "OMEGA" Omega.OMEGA_PROVE 283val (COOPER_ss, cooper_cache) = mkSS "COOPER" Cooper.COOPER_PROVE 284val INT_ARITH_ss = OMEGA_ss 285 286 287end 288