|
1 (* Title: HOL/Tools/Presburger/cooper.ML |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb, TU Muenchen |
|
4 *) |
|
5 |
|
6 signature COOPER = |
|
7 sig |
|
8 val cooper_conv : Proof.context -> Conv.conv |
|
9 exception COOPER of string * exn |
|
10 end; |
|
11 |
|
12 structure Cooper: COOPER = |
|
13 struct |
|
14 open Conv; |
|
15 open Normalizer; |
|
16 |
|
17 exception COOPER of string * exn; |
|
18 val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms); |
|
19 |
|
20 fun C f x y = f y x; |
|
21 |
|
22 val FWD = C (fold (C implies_elim)); |
|
23 |
|
24 val true_tm = @{cterm "True"}; |
|
25 val false_tm = @{cterm "False"}; |
|
26 val zdvd1_eq = @{thm "zdvd1_eq"}; |
|
27 val presburger_ss = @{simpset} addsimps [zdvd1_eq]; |
|
28 val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::zadd_ac); |
|
29 (* Some types and constants *) |
|
30 val iT = HOLogic.intT |
|
31 val bT = HOLogic.boolT; |
|
32 val dest_numeral = HOLogic.dest_number #> snd; |
|
33 |
|
34 val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] = |
|
35 map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"}; |
|
36 |
|
37 val [infDconj, infDdisj, infDdvd,infDndvd,infDP] = |
|
38 map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"}; |
|
39 |
|
40 val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] = |
|
41 map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"}; |
|
42 |
|
43 val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP]; |
|
44 |
|
45 val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP; |
|
46 |
|
47 val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle, |
|
48 asetgt, asetge, asetdvd, asetndvd,asetP], |
|
49 [bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle, |
|
50 bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}]; |
|
51 |
|
52 val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"}, |
|
53 @{thm "plusinfinity"}, @{thm "cppi"}]; |
|
54 |
|
55 val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"}; |
|
56 |
|
57 val [zdvd_mono,simp_from_to,all_not_ex] = |
|
58 [@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}]; |
|
59 |
|
60 val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"}; |
|
61 |
|
62 val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv]; |
|
63 val eval_conv = Simplifier.rewrite eval_ss; |
|
64 |
|
65 (* recongnising cterm without moving to terms *) |
|
66 |
|
67 datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm |
|
68 | Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm |
|
69 | Dvd of cterm*cterm | NDvd of cterm*cterm | Nox |
|
70 |
|
71 fun whatis x ct = |
|
72 ( case (term_of ct) of |
|
73 Const("op &",_)$_$_ => And (Thm.dest_binop ct) |
|
74 | Const ("op |",_)$_$_ => Or (Thm.dest_binop ct) |
|
75 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox |
|
76 | Const("Not",_) $ (Const ("op =",_)$y$_) => |
|
77 if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox |
|
78 | Const ("Orderings.ord_class.less",_)$y$z => |
|
79 if term_of x aconv y then Lt (Thm.dest_arg ct) |
|
80 else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
|
81 | Const ("Orderings.ord_class.less_eq",_)$y$z => |
|
82 if term_of x aconv y then Le (Thm.dest_arg ct) |
|
83 else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
|
84 | Const ("Divides.dvd",_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) => |
|
85 if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
|
86 | Const("Not",_) $ (Const ("Divides.dvd",_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) => |
|
87 if term_of x aconv y then |
|
88 NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
|
89 | _ => Nox) |
|
90 handle CTERM _ => Nox; |
|
91 |
|
92 fun get_pmi_term t = |
|
93 let val (x,eq) = |
|
94 (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg) |
|
95 (Thm.dest_arg t) |
|
96 in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end; |
|
97 |
|
98 val get_pmi = get_pmi_term o cprop_of; |
|
99 |
|
100 val p_v' = @{cpat "?P' :: int => bool"}; |
|
101 val q_v' = @{cpat "?Q' :: int => bool"}; |
|
102 val p_v = @{cpat "?P:: int => bool"}; |
|
103 val q_v = @{cpat "?Q:: int => bool"}; |
|
104 |
|
105 fun myfwd (th1, th2, th3) p q |
|
106 [(th_1,th_2,th_3), (th_1',th_2',th_3')] = |
|
107 let |
|
108 val (mp', mq') = (get_pmi th_1, get_pmi th_1') |
|
109 val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) |
|
110 [th_1, th_1'] |
|
111 val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] |
|
112 val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2'] |
|
113 in (mi_th, set_th, infD_th) |
|
114 end; |
|
115 |
|
116 val inst' = fn cts => instantiate' [] (map SOME cts); |
|
117 val infDTrue = instantiate' [] [SOME true_tm] infDP; |
|
118 val infDFalse = instantiate' [] [SOME false_tm] infDP; |
|
119 |
|
120 val cadd = @{cterm "op + :: int => _"} |
|
121 val cmulC = @{cterm "op * :: int => _"} |
|
122 val cminus = @{cterm "op - :: int => _"} |
|
123 val cone = @{cterm "1:: int"} |
|
124 val cneg = @{cterm "uminus :: int => _"} |
|
125 val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg] |
|
126 val [zero, one] = [@{term "0::int"}, @{term "1::int"}]; |
|
127 |
|
128 val is_numeral = can dest_numeral; |
|
129 |
|
130 fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n)); |
|
131 fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n)); |
|
132 |
|
133 val [minus1,plus1] = |
|
134 map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd]; |
|
135 |
|
136 fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, |
|
137 asetgt, asetge,asetdvd,asetndvd,asetP, |
|
138 infDdvd, infDndvd, asetconj, |
|
139 asetdisj, infDconj, infDdisj] cp = |
|
140 case (whatis x cp) of |
|
141 And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q)) |
|
142 | Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q)) |
|
143 | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse)) |
|
144 | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue)) |
|
145 | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse)) |
|
146 | Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse)) |
|
147 | Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue)) |
|
148 | Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue)) |
|
149 | Dvd (d,s) => |
|
150 ([],let val dd = dvd d |
|
151 in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end) |
|
152 | NDvd(d,s) => ([],let val dd = dvd d |
|
153 in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) |
|
154 | _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP)); |
|
155 |
|
156 fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt, |
|
157 bsetge,bsetdvd,bsetndvd,bsetP, |
|
158 infDdvd, infDndvd, bsetconj, |
|
159 bsetdisj, infDconj, infDdisj] cp = |
|
160 case (whatis x cp) of |
|
161 And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q)) |
|
162 | Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q)) |
|
163 | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse)) |
|
164 | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue)) |
|
165 | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue)) |
|
166 | Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue)) |
|
167 | Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse)) |
|
168 | Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse)) |
|
169 | Dvd (d,s) => ([],let val dd = dvd d |
|
170 in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end) |
|
171 | NDvd (d,s) => ([],let val dd = dvd d |
|
172 in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) |
|
173 | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP)) |
|
174 |
|
175 (* Canonical linear form for terms, formulae etc.. *) |
|
176 fun provelin ctxt t = Goal.prove ctxt [] [] t |
|
177 (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac 1)]); |
|
178 fun linear_cmul 0 tm = zero |
|
179 | linear_cmul n tm = |
|
180 case tm of |
|
181 Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b) |
|
182 | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 ((curry (op *)) n) c)$x |
|
183 | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b) |
|
184 | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a) |
|
185 | _ => numeral1 ((curry (op *)) n) tm; |
|
186 fun earlier [] x y = false |
|
187 | earlier (h::t) x y = |
|
188 if h aconv y then false else if h aconv x then true else earlier t x y; |
|
189 |
|
190 fun linear_add vars tm1 tm2 = |
|
191 case (tm1,tm2) of |
|
192 (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1, |
|
193 Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => |
|
194 if x1 = x2 then |
|
195 let val c = numeral2 (curry (op +)) c1 c2 |
|
196 in if c = zero then linear_add vars r1 r2 |
|
197 else addC$(mulC$c$x1)$(linear_add vars r1 r2) |
|
198 end |
|
199 else if earlier vars x1 x2 then addC$(mulC$ c1 $ x1)$(linear_add vars r1 tm2) |
|
200 else addC$(mulC$c2$x2)$(linear_add vars tm1 r2) |
|
201 | (Const("HOL.plus_class.plus",_) $ (Const("HOL.times_class.times",_)$c1$x1)$r1 ,_) => |
|
202 addC$(mulC$c1$x1)$(linear_add vars r1 tm2) |
|
203 | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => |
|
204 addC$(mulC$c2$x2)$(linear_add vars tm1 r2) |
|
205 | (_,_) => numeral2 (curry (op +)) tm1 tm2; |
|
206 |
|
207 fun linear_neg tm = linear_cmul ~1 tm; |
|
208 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); |
|
209 |
|
210 |
|
211 fun lint vars tm = |
|
212 if is_numeral tm then tm |
|
213 else case tm of |
|
214 Const("HOL.minus_class.uminus",_)$t => linear_neg (lint vars t) |
|
215 | Const("HOL.plus_class.plus",_) $ s $ t => linear_add vars (lint vars s) (lint vars t) |
|
216 | Const("HOL.minus_class.minus",_) $ s $ t => linear_sub vars (lint vars s) (lint vars t) |
|
217 | Const ("HOL.times_class.times",_) $ s $ t => |
|
218 let val s' = lint vars s |
|
219 val t' = lint vars t |
|
220 in if is_numeral s' then (linear_cmul (dest_numeral s') t') |
|
221 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
|
222 else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm])) |
|
223 end |
|
224 | _ => addC$(mulC$one$tm)$zero; |
|
225 |
|
226 fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) = |
|
227 lin vs (Const("Orderings.ord_class.less_eq",T)$t$s) |
|
228 | lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) = |
|
229 lin vs (Const("Orderings.ord_class.less",T)$t$s) |
|
230 | lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t) |
|
231 | lin (vs as x::_) (Const("Divides.dvd",_)$d$t) = |
|
232 HOLogic.mk_binrel "Divides.dvd" (numeral1 abs d, lint vs t) |
|
233 | lin (vs as x::_) ((b as Const("op =",_))$s$t) = |
|
234 (case lint vs (subC$t$s) of |
|
235 (t as a$(m$c$y)$r) => |
|
236 if x <> y then b$zero$t |
|
237 else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r |
|
238 else b$(m$c$y)$(linear_neg r) |
|
239 | t => b$zero$t) |
|
240 | lin (vs as x::_) (b$s$t) = |
|
241 (case lint vs (subC$t$s) of |
|
242 (t as a$(m$c$y)$r) => |
|
243 if x <> y then b$zero$t |
|
244 else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r |
|
245 else b$(linear_neg r)$(m$c$y) |
|
246 | t => b$zero$t) |
|
247 | lin vs fm = fm; |
|
248 |
|
249 fun lint_conv ctxt vs ct = |
|
250 let val t = term_of ct |
|
251 in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop)) |
|
252 RS eq_reflection |
|
253 end; |
|
254 |
|
255 fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT |
|
256 | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT |
|
257 | is_intrel _ = false; |
|
258 |
|
259 fun linearize_conv ctxt vs ct = |
|
260 case (term_of ct) of |
|
261 Const("Divides.dvd",_)$d$t => |
|
262 let |
|
263 val th = binop_conv (lint_conv ctxt vs) ct |
|
264 val (d',t') = Thm.dest_binop (Thm.rhs_of th) |
|
265 val (dt',tt') = (term_of d', term_of t') |
|
266 in if is_numeral dt' andalso is_numeral tt' |
|
267 then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th |
|
268 else |
|
269 let |
|
270 val dth = |
|
271 ((if dest_numeral (term_of d') < 0 then |
|
272 Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs))) |
|
273 (Thm.transitive th (inst' [d',t'] dvd_uminus)) |
|
274 else th) handle TERM _ => th) |
|
275 val d'' = Thm.rhs_of dth |> Thm.dest_arg1 |
|
276 in |
|
277 case tt' of |
|
278 Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$_)$_ => |
|
279 let val x = dest_numeral c |
|
280 in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs))) |
|
281 (Thm.transitive dth (inst' [d'',t'] dvd_uminus')) |
|
282 else dth end |
|
283 | _ => dth |
|
284 end |
|
285 end |
|
286 | Const("Not",_)$(Const("Divides.dvd",_)$_$_) => arg_conv (linearize_conv ctxt vs) ct |
|
287 | t => if is_intrel t |
|
288 then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) |
|
289 RS eq_reflection |
|
290 else reflexive ct; |
|
291 |
|
292 val dvdc = @{cterm "op dvd :: int => _"}; |
|
293 |
|
294 fun unify ctxt q = |
|
295 let |
|
296 val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE |
|
297 val x = term_of cx |
|
298 val ins = insert (op = : int*int -> bool) |
|
299 fun h (acc,dacc) t = |
|
300 case (term_of t) of |
|
301 Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => |
|
302 if x aconv y |
|
303 andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] |
|
304 then (ins (dest_numeral c) acc,dacc) else (acc,dacc) |
|
305 | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => |
|
306 if x aconv y |
|
307 andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] |
|
308 then (ins (dest_numeral c) acc, dacc) else (acc,dacc) |
|
309 | Const("Divides.dvd",_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) => |
|
310 if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) |
|
311 | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
|
312 | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
|
313 | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t) |
|
314 | _ => (acc, dacc) |
|
315 val (cs,ds) = h ([],[]) p |
|
316 val l = fold (curry lcm) (cs union ds) 1 |
|
317 fun cv k ct = |
|
318 let val (tm as b$s$t) = term_of ct |
|
319 in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) |
|
320 |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end |
|
321 fun nzprop x = |
|
322 let |
|
323 val th = |
|
324 Simplifier.rewrite lin_ss |
|
325 (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} |
|
326 (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (mk_cnumber @{ctyp "int"} x)) |
|
327 @{cterm "0::int"}))) |
|
328 in equal_elim (Thm.symmetric th) TrueI end; |
|
329 val notz = let val tab = fold Inttab.update |
|
330 (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty |
|
331 in |
|
332 (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) |
|
333 handle Option => (writeln "noz: Theorems-Table contains no entry for"; |
|
334 print_cterm ct ; raise Option))) |
|
335 end |
|
336 fun unit_conv t = |
|
337 case (term_of t) of |
|
338 Const("op &",_)$_$_ => binop_conv unit_conv t |
|
339 | Const("op |",_)$_$_ => binop_conv unit_conv t |
|
340 | Const("Not",_)$_ => arg_conv unit_conv t |
|
341 | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => |
|
342 if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] |
|
343 then cv (l div (dest_numeral c)) t else Thm.reflexive t |
|
344 | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => |
|
345 if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] |
|
346 then cv (l div (dest_numeral c)) t else Thm.reflexive t |
|
347 | Const("Divides.dvd",_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => |
|
348 if x=y then |
|
349 let |
|
350 val k = l div (dest_numeral c) |
|
351 val kt = HOLogic.mk_number iT k |
|
352 val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
|
353 ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono) |
|
354 val (d',t') = (mulC$kt$d, mulC$kt$r) |
|
355 val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop)) |
|
356 RS eq_reflection |
|
357 val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop)) |
|
358 RS eq_reflection |
|
359 in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end |
|
360 else Thm.reflexive t |
|
361 | _ => Thm.reflexive t |
|
362 val uth = unit_conv p |
|
363 val clt = mk_cnumber @{ctyp "int"} l |
|
364 val ltx = Thm.capply (Thm.capply cmulC clt) cx |
|
365 val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth) |
|
366 val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex |
|
367 val thf = transitive th |
|
368 (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th') |
|
369 val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true |
|
370 ||> beta_conversion true |>> Thm.symmetric |
|
371 in transitive (transitive lth thf) rth end; |
|
372 |
|
373 |
|
374 val emptyIS = @{cterm "{}::int set"}; |
|
375 val insert_tm = @{cterm "insert :: int => _"}; |
|
376 val mem_tm = Const("op :",[iT , HOLogic.mk_setT iT] ---> bT); |
|
377 fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS; |
|
378 val cTrp = @{cterm "Trueprop"}; |
|
379 val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1; |
|
380 val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg |
|
381 |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg) |
|
382 [asetP,bsetP]; |
|
383 |
|
384 val D_tm = @{cpat "?D::int"}; |
|
385 |
|
386 val int_eq = (op =):int*int -> bool; |
|
387 fun cooperex_conv ctxt vs q = |
|
388 let |
|
389 |
|
390 val uth = unify ctxt q |
|
391 val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth)) |
|
392 val ins = insert (op aconvc) |
|
393 fun h t (bacc,aacc,dacc) = |
|
394 case (whatis x t) of |
|
395 And (p,q) => h q (h p (bacc,aacc,dacc)) |
|
396 | Or (p,q) => h q (h p (bacc,aacc,dacc)) |
|
397 | Eq t => (ins (minus1 t) bacc, |
|
398 ins (plus1 t) aacc,dacc) |
|
399 | NEq t => (ins t bacc, |
|
400 ins t aacc, dacc) |
|
401 | Lt t => (bacc, ins t aacc, dacc) |
|
402 | Le t => (bacc, ins (plus1 t) aacc,dacc) |
|
403 | Gt t => (ins t bacc, aacc,dacc) |
|
404 | Ge t => (ins (minus1 t) bacc, aacc,dacc) |
|
405 | Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc) |
|
406 | NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc) |
|
407 | _ => (bacc, aacc, dacc) |
|
408 val (b0,a0,ds) = h p ([],[],[]) |
|
409 val d = fold (curry lcm) ds 1 |
|
410 val cd = mk_cnumber @{ctyp "int"} d |
|
411 val dt = term_of cd |
|
412 fun divprop x = |
|
413 let |
|
414 val th = |
|
415 Simplifier.rewrite lin_ss |
|
416 (Thm.capply @{cterm Trueprop} |
|
417 (Thm.capply (Thm.capply dvdc (mk_cnumber @{ctyp "int"} x)) cd)) |
|
418 in equal_elim (Thm.symmetric th) TrueI end; |
|
419 val dvd = let val tab = fold Inttab.update |
|
420 (ds ~~ (map divprop ds)) Inttab.empty in |
|
421 (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) |
|
422 handle Option => (writeln "dvd: Theorems-Table contains no entry for"; |
|
423 print_cterm ct ; raise Option))) |
|
424 end |
|
425 val dp = |
|
426 let val th = Simplifier.rewrite lin_ss |
|
427 (Thm.capply @{cterm Trueprop} |
|
428 (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd)) |
|
429 in equal_elim (Thm.symmetric th) TrueI end; |
|
430 (* A and B set *) |
|
431 local |
|
432 val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"} |
|
433 val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"} |
|
434 in |
|
435 fun provein x S = |
|
436 case term_of S of |
|
437 Const("{}",_) => error "Unexpected error in Cooper please email Amine Chaieb" |
|
438 | Const("insert",_)$y$_ => |
|
439 let val (cy,S') = Thm.dest_binop S |
|
440 in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 |
|
441 else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
|
442 (provein x S') |
|
443 end |
|
444 end |
|
445 |
|
446 val al = map (lint vs o term_of) a0 |
|
447 val bl = map (lint vs o term_of) b0 |
|
448 val (sl,s0,f,abths,cpth) = |
|
449 if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) |
|
450 then |
|
451 (bl,b0,decomp_minf, |
|
452 fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) |
|
453 [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ |
|
454 (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) |
|
455 [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, |
|
456 bsetdisj,infDconj, infDdisj]), |
|
457 cpmi) |
|
458 else (al,a0,decomp_pinf,fn A => |
|
459 (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) |
|
460 [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ |
|
461 (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) |
|
462 [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, |
|
463 asetdisj,infDconj, infDdisj]),cppi) |
|
464 val cpth = |
|
465 let |
|
466 val sths = map (fn (tl,t0) => |
|
467 if tl = term_of t0 |
|
468 then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl |
|
469 else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0) |
|
470 |> HOLogic.mk_Trueprop)) |
|
471 (sl ~~ s0) |
|
472 val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths) |
|
473 val S = mkISet csl |
|
474 val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab) |
|
475 csl Termtab.empty |
|
476 val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp |
|
477 val inS = |
|
478 let |
|
479 fun transmem th0 th1 = |
|
480 Thm.equal_elim |
|
481 (Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule |
|
482 ((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1 |
|
483 val tab = fold Termtab.update |
|
484 (map (fn eq => |
|
485 let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop |
|
486 val th = if term_of s = term_of t |
|
487 then valOf(Termtab.lookup inStab (term_of s)) |
|
488 else FWD (instantiate' [] [SOME s, SOME t] eqelem_th) |
|
489 [eq, valOf(Termtab.lookup inStab (term_of s))] |
|
490 in (term_of t, th) end) |
|
491 sths) Termtab.empty |
|
492 in fn ct => |
|
493 (valOf (Termtab.lookup tab (term_of ct)) |
|
494 handle Option => (writeln "inS: No theorem for " ; print_cterm ct ; raise Option)) |
|
495 end |
|
496 val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p |
|
497 in [dp, inf, nb, pd] MRS cpth |
|
498 end |
|
499 val cpth' = Thm.transitive uth (cpth RS eq_reflection) |
|
500 in Thm.transitive cpth' ((simp_thms_conv then_conv eval_conv) (Thm.rhs_of cpth')) |
|
501 end; |
|
502 |
|
503 fun literals_conv bops uops env cv = |
|
504 let fun h t = |
|
505 case (term_of t) of |
|
506 b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t |
|
507 | u$_ => if member (op aconv) uops u then arg_conv h t else cv env t |
|
508 | _ => cv env t |
|
509 in h end; |
|
510 |
|
511 fun integer_nnf_conv ctxt env = |
|
512 nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt); |
|
513 |
|
514 (* val my_term = ref (@{cterm "NOTHING"}); *) |
|
515 local |
|
516 val pcv = Simplifier.rewrite |
|
517 (HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4)) |
|
518 @ [not_all,all_not_ex, ex_disj_distrib])) |
|
519 val postcv = Simplifier.rewrite presburger_ss |
|
520 fun conv ctxt p = |
|
521 let val _ = () (* my_term := p *) |
|
522 in |
|
523 Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) |
|
524 (term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) |
|
525 (cooperex_conv ctxt) p |
|
526 end |
|
527 handle CTERM s => raise COOPER ("Cooper Failed", CTERM s) |
|
528 | THM s => raise COOPER ("Cooper Failed", THM s) |
|
529 in val cooper_conv = conv |
|
530 end; |
|
531 end; |
|
532 |
|
533 |
|
534 |
|
535 structure Coopereif = |
|
536 struct |
|
537 |
|
538 open GeneratedCooper; |
|
539 fun cooper s = raise Cooper.COOPER ("Cooper Oracle Failed", ERROR s); |
|
540 fun i_of_term vs t = |
|
541 case t of |
|
542 Free(xn,xT) => (case AList.lookup (op aconv) vs t of |
|
543 NONE => cooper "Variable not found in the list!!" |
|
544 | SOME n => Bound n) |
|
545 | @{term "0::int"} => C 0 |
|
546 | @{term "1::int"} => C 1 |
|
547 | Term.Bound i => Bound i |
|
548 | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t') |
|
549 | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) |
|
550 | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) |
|
551 | Const(@{const_name "HOL.times"},_)$t1$t2 => |
|
552 (Mul (HOLogic.dest_number t1 |> snd,i_of_term vs t2) |
|
553 handle TERM _ => |
|
554 (Mul (HOLogic.dest_number t2 |> snd,i_of_term vs t1) |
|
555 handle TERM _ => cooper "i_of_term: Unsupported kind of multiplication")) |
|
556 | _ => (C (HOLogic.dest_number t |> snd) |
|
557 handle TERM _ => cooper "i_of_term: unknown term"); |
|
558 |
|
559 fun qf_of_term ps vs t = |
|
560 case t of |
|
561 Const("True",_) => T |
|
562 | Const("False",_) => F |
|
563 | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2)) |
|
564 | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2)) |
|
565 | Const(@{const_name "Divides.dvd"},_)$t1$t2 => |
|
566 (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "qf_of_term: unsupported dvd") |
|
567 | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2)) |
|
568 | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
569 | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
570 | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
571 | Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
572 | Const("Not",_)$t' => NOT(qf_of_term ps vs t') |
|
573 | Const("Ex",_)$Abs(xn,xT,p) => |
|
574 let val (xn',p') = variant_abs (xn,xT,p) |
|
575 val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1+ n)) vs) |
|
576 in E (qf_of_term ps vs' p') |
|
577 end |
|
578 | Const("All",_)$Abs(xn,xT,p) => |
|
579 let val (xn',p') = variant_abs (xn,xT,p) |
|
580 val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1+ n)) vs) |
|
581 in A (qf_of_term ps vs' p') |
|
582 end |
|
583 | _ =>(case AList.lookup (op aconv) ps t of |
|
584 NONE => cooper "qf_of_term ps : unknown term!" |
|
585 | SOME n => Closed n); |
|
586 |
|
587 local |
|
588 val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"}, |
|
589 @{term "op = :: int => _"}, @{term "op < :: int => _"}, |
|
590 @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"}, |
|
591 @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}] |
|
592 fun ty t = Bool.not (fastype_of t = HOLogic.boolT) |
|
593 in |
|
594 fun term_bools acc t = |
|
595 case t of |
|
596 (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b |
|
597 else insert (op aconv) t acc |
|
598 | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a |
|
599 else insert (op aconv) t acc |
|
600 | Abs p => term_bools acc (snd (variant_abs p)) |
|
601 | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc |
|
602 end; |
|
603 |
|
604 |
|
605 fun start_vs t = |
|
606 let |
|
607 val fs = term_frees t |
|
608 val ps = term_bools [] t |
|
609 in (fs ~~ (0 upto (length fs - 1)), ps ~~ (0 upto (length ps - 1))) |
|
610 end ; |
|
611 |
|
612 val iT = HOLogic.intT; |
|
613 val bT = HOLogic.boolT; |
|
614 fun myassoc2 l v = |
|
615 case l of |
|
616 [] => NONE |
|
617 | (x,v')::xs => if v = v' then SOME x |
|
618 else myassoc2 xs v; |
|
619 |
|
620 fun term_of_i vs t = |
|
621 case t of |
|
622 C i => HOLogic.mk_number HOLogic.intT i |
|
623 | Bound n => valOf (myassoc2 vs n) |
|
624 | Neg t' => @{term "uminus :: int => _"}$(term_of_i vs t') |
|
625 | Add(t1,t2) => @{term "op +:: int => _"}$ (term_of_i vs t1)$(term_of_i vs t2) |
|
626 | Sub(t1,t2) => Const(@{const_name "HOL.minus"},[iT,iT] ---> iT)$ |
|
627 (term_of_i vs t1)$(term_of_i vs t2) |
|
628 | Mul(i,t2) => Const(@{const_name "HOL.times"},[iT,iT] ---> iT)$ |
|
629 (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t2) |
|
630 | CX(i,t')=> term_of_i vs (Add(Mul (i,Bound (nat 0)),t')); |
|
631 |
|
632 fun term_of_qf ps vs t = |
|
633 case t of |
|
634 T => HOLogic.true_const |
|
635 | F => HOLogic.false_const |
|
636 | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} |
|
637 | Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"} |
|
638 | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' |
|
639 | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' |
|
640 | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} |
|
641 | NEq t' => term_of_qf ps vs (NOT(Eq t')) |
|
642 | Dvd(i,t') => @{term "op dvd :: int => _ "}$ |
|
643 (HOLogic.mk_number HOLogic.intT i)$(term_of_i vs t') |
|
644 | NDvd(i,t')=> term_of_qf ps vs (NOT(Dvd(i,t'))) |
|
645 | NOT t' => HOLogic.Not$(term_of_qf ps vs t') |
|
646 | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
647 | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
648 | Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
649 | Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf ps vs t1)$ (term_of_qf ps vs t2) |
|
650 | Closed n => valOf (myassoc2 ps n) |
|
651 | NClosed n => term_of_qf ps vs (NOT (Closed n)) |
|
652 | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!"; |
|
653 |
|
654 (* The oracle *) |
|
655 fun cooper_oracle thy t = |
|
656 let val (vs,ps) = start_vs t |
|
657 in (equals propT) $ (HOLogic.mk_Trueprop t) $ |
|
658 (HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))) |
|
659 end; |
|
660 |
|
661 end; |