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