74 (*Function is_arith_rel returns true if and only if the term is an operation of the |
74 (*Function is_arith_rel returns true if and only if the term is an operation of the |
75 form [int,int]---> int*) |
75 form [int,int]---> int*) |
76 |
76 |
77 (*Transform a natural number to a term*) |
77 (*Transform a natural number to a term*) |
78 |
78 |
79 fun mk_numeral 0 = Const("HOL.zero",HOLogic.intT) |
79 fun mk_number 0 = Const("HOL.zero",HOLogic.intT) |
80 |mk_numeral 1 = Const("HOL.one",HOLogic.intT) |
80 |mk_number 1 = Const("HOL.one",HOLogic.intT) |
81 |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); |
81 |mk_number n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_numeral n); |
82 |
82 |
83 (*Transform an Term to an natural number*) |
83 (*Transform an Term to an natural number*) |
84 |
84 |
85 fun dest_numeral (Const("HOL.zero",Type ("IntDef.int", []))) = 0 |
85 fun dest_number (Const("HOL.zero",Type ("IntDef.int", []))) = 0 |
86 |dest_numeral (Const("HOL.one",Type ("IntDef.int", []))) = 1 |
86 |dest_number (Const("HOL.one",Type ("IntDef.int", []))) = 1 |
87 |dest_numeral (Const ("Numeral.number_of",_) $ n) = |
87 |dest_number (Const ("Numeral.number_of",_) $ n) = |
88 HOLogic.dest_binum n; |
88 HOLogic.dest_numeral n; |
89 (*Some terms often used for pattern matching*) |
89 (*Some terms often used for pattern matching*) |
90 |
90 |
91 val zero = mk_numeral 0; |
91 val zero = mk_number 0; |
92 val one = mk_numeral 1; |
92 val one = mk_number 1; |
93 |
93 |
94 (*Tests if a Term is representing a number*) |
94 (*Tests if a Term is representing a number*) |
95 |
95 |
96 fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_numeral t); |
96 fun is_numeral t = (t = zero) orelse (t = one) orelse (can dest_number t); |
97 |
97 |
98 (*maps a unary natural function on a term containing an natural number*) |
98 (*maps a unary natural function on a term containing an natural number*) |
99 |
99 |
100 fun numeral1 f n = mk_numeral (f(dest_numeral n)); |
100 fun numeral1 f n = mk_number (f(dest_number n)); |
101 |
101 |
102 (*maps a binary natural function on 2 term containing natural numbers*) |
102 (*maps a binary natural function on 2 term containing natural numbers*) |
103 |
103 |
104 fun numeral2 f m n = mk_numeral(f(dest_numeral m) (dest_numeral n)); |
104 fun numeral2 f m n = mk_number(f(dest_number m) (dest_number n)); |
105 |
105 |
106 (* ------------------------------------------------------------------------- *) |
106 (* ------------------------------------------------------------------------- *) |
107 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *) |
107 (* Operations on canonical linear terms c1 * x1 + ... + cn * xn + k *) |
108 (* *) |
108 (* *) |
109 (* Note that we're quite strict: the ci must be present even if 1 *) |
109 (* Note that we're quite strict: the ci must be present even if 1 *) |
176 After this fuction the all expressions containig ths variable will have the form |
176 After this fuction the all expressions containig ths variable will have the form |
177 c*Free(x,T) + t where c is a constant ant t is a Term which is not containing |
177 c*Free(x,T) + t where c is a constant ant t is a Term which is not containing |
178 Free(x,T)*) |
178 Free(x,T)*) |
179 |
179 |
180 fun lint vars tm = if is_numeral tm then tm else case tm of |
180 fun lint vars tm = if is_numeral tm then tm else case tm of |
181 (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) |
181 (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_number 1),Free (x,T))), zero)) |
182 |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ |
182 |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ |
183 (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) |
183 (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_number 1) $ (Bound i)) $ zero) |
184 |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) |
184 |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) |
185 |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) |
185 |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) |
186 |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) |
186 |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) |
187 |(Const ("HOL.times",_) $ s $ t) => |
187 |(Const ("HOL.times",_) $ s $ t) => |
188 let val s' = lint vars s |
188 let val s' = lint vars s |
189 val t' = lint vars t |
189 val t' = lint vars t |
190 in |
190 in |
191 if is_numeral s' then (linear_cmul (dest_numeral s') t') |
191 if is_numeral s' then (linear_cmul (dest_number s') t') |
192 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
192 else if is_numeral t' then (linear_cmul (dest_number t') s') |
193 |
193 |
194 else raise COOPER |
194 else raise COOPER |
195 end |
195 end |
196 |_ => raise COOPER; |
196 |_ => raise COOPER; |
197 |
197 |
203 |
203 |
204 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); |
204 fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); |
205 |
205 |
206 fun linform vars (Const ("Divides.dvd",_) $ c $ t) = |
206 fun linform vars (Const ("Divides.dvd",_) $ c $ t) = |
207 if is_numeral c then |
207 if is_numeral c then |
208 let val c' = (mk_numeral(abs(dest_numeral c))) |
208 let val c' = (mk_number(abs(dest_number c))) |
209 in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) |
209 in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t)) |
210 end |
210 end |
211 else (warning "Nonlinear term --- Non numeral leftside at dvd" |
211 else (warning "Nonlinear term --- Non numeral leftside at dvd" |
212 ;raise COOPER) |
212 ;raise COOPER) |
213 |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) |
213 |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) |
214 |linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s)) |
214 |linform vars (Const("Orderings.less",_)$ s $t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s)) |
215 |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) |
215 |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) |
216 |linform vars (Const("Orderings.less_eq",_)$ s $ t ) = |
216 |linform vars (Const("Orderings.less_eq",_)$ s $ t ) = |
217 (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) |
217 (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_number 1)) $ s)) |
218 |linform vars (Const("op >=",_)$ s $ t ) = |
218 |linform vars (Const("op >=",_)$ s $ t ) = |
219 (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> |
219 (mkatom vars "Orderings.less" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> |
220 HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> |
220 HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> |
221 HOLogic.intT) $s $(mk_numeral 1)) $ t)) |
221 HOLogic.intT) $s $(mk_number 1)) $ t)) |
222 |
222 |
223 |linform vars fm = fm; |
223 |linform vars fm = fm; |
224 |
224 |
225 (* ------------------------------------------------------------------------- *) |
225 (* ------------------------------------------------------------------------- *) |
226 (* Post-NNF transformation eliminating negated inequalities. *) |
226 (* Post-NNF transformation eliminating negated inequalities. *) |
227 (* ------------------------------------------------------------------------- *) |
227 (* ------------------------------------------------------------------------- *) |
228 |
228 |
229 fun posineq fm = case fm of |
229 fun posineq fm = case fm of |
230 (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) => |
230 (Const ("Not",_)$(Const("Orderings.less",_)$ c $ t)) => |
231 (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_numeral 1) (linear_add [] c t ) ))) |
231 (HOLogic.mk_binrel "Orderings.less" (zero , (linear_sub [] (mk_number 1) (linear_add [] c t ) ))) |
232 | ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q) |
232 | ( Const ("op &",_) $ p $ q) => HOLogic.mk_conj (posineq p,posineq q) |
233 | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q) |
233 | ( Const ("op |",_) $ p $ q ) => HOLogic.mk_disj (posineq p,posineq q) |
234 | _ => fm; |
234 | _ => fm; |
235 |
235 |
236 |
236 |
243 fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; |
243 fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; |
244 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); |
244 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); |
245 |
245 |
246 fun formlcm x fm = case fm of |
246 fun formlcm x fm = case fm of |
247 (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if |
247 (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if |
248 (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1 |
248 (is_arith_rel fm) andalso (x = y) then (abs(dest_number c)) else 1 |
249 | ( Const ("Not", _) $p) => formlcm x p |
249 | ( Const ("Not", _) $p) => formlcm x p |
250 | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) |
250 | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) |
251 | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) |
251 | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) |
252 | _ => 1; |
252 | _ => 1; |
253 |
253 |
257 |
257 |
258 fun adjustcoeff x l fm = |
258 fun adjustcoeff x l fm = |
259 case fm of |
259 case fm of |
260 (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
260 (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
261 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
261 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
262 let val m = l div (dest_numeral c) |
262 let val m = l div (dest_number c) |
263 val n = (if p = "Orderings.less" then abs(m) else m) |
263 val n = (if p = "Orderings.less" then abs(m) else m) |
264 val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) |
264 val xtm = HOLogic.mk_binop "HOL.times" ((mk_number (m div n)), x) |
265 in |
265 in |
266 (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
266 (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
267 end |
267 end |
268 else fm |
268 else fm |
269 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) |
269 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) |
279 let val l = formlcm x fm |
279 let val l = formlcm x fm |
280 val fm' = adjustcoeff x l fm in |
280 val fm' = adjustcoeff x l fm in |
281 if l = 1 then fm' |
281 if l = 1 then fm' |
282 else |
282 else |
283 let val xp = (HOLogic.mk_binop "HOL.plus" |
283 let val xp = (HOLogic.mk_binop "HOL.plus" |
284 ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero)) |
284 ((HOLogic.mk_binop "HOL.times" ((mk_number 1), x )), zero)) |
285 in |
285 in |
286 HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) |
286 HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_number l) , xp )) $ (adjustcoeff x l fm) |
287 end |
287 end |
288 end; |
288 end; |
289 |
289 |
290 (* adjustcoeffeq l fm adjusts the coeffitients c_i of x overall in fm to l*) |
290 (* adjustcoeffeq l fm adjusts the coeffitients c_i of x overall in fm to l*) |
291 (* Here l must be a multiple of all c_i otherwise the obtained formula is not equivalent*) |
291 (* Here l must be a multiple of all c_i otherwise the obtained formula is not equivalent*) |
292 (* |
292 (* |
293 fun adjustcoeffeq x l fm = |
293 fun adjustcoeffeq x l fm = |
294 case fm of |
294 case fm of |
295 (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
295 (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
296 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
296 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
297 let val m = l div (dest_numeral c) |
297 let val m = l div (dest_number c) |
298 val n = (if p = "Orderings.less" then abs(m) else m) |
298 val n = (if p = "Orderings.less" then abs(m) else m) |
299 val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) |
299 val xtm = (HOLogic.mk_binop "HOL.times" ((mk_number ((m div n)*l) ), x)) |
300 in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
300 in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
301 end |
301 end |
302 else fm |
302 else fm |
303 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) |
303 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) |
304 |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeffeq x l p) $(adjustcoeffeq x l q) |
304 |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeffeq x l p) $(adjustcoeffeq x l q) |
318 else fm |
318 else fm |
319 |
319 |
320 |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z |
320 |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z |
321 )) => if (x = y) |
321 )) => if (x = y) |
322 then if (pm1 = one) andalso (c = zero) then HOLogic.false_const |
322 then if (pm1 = one) andalso (c = zero) then HOLogic.false_const |
323 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const |
323 else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.true_const |
324 else error "minusinf : term not in normal form!!!" |
324 else error "minusinf : term not in normal form!!!" |
325 else fm |
325 else fm |
326 |
326 |
327 |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) |
327 |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) |
328 |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) |
328 |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) |
339 else fm |
339 else fm |
340 |
340 |
341 |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z |
341 |(Const("Orderings.less",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z |
342 )) => if (x = y) |
342 )) => if (x = y) |
343 then if (pm1 = one) andalso (c = zero) then HOLogic.true_const |
343 then if (pm1 = one) andalso (c = zero) then HOLogic.true_const |
344 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const |
344 else if (dest_number pm1 = ~1) andalso (c = zero) then HOLogic.false_const |
345 else error "plusinf : term not in normal form!!!" |
345 else error "plusinf : term not in normal form!!!" |
346 else fm |
346 else fm |
347 |
347 |
348 |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p) |
348 |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p) |
349 |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q) |
349 |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q) |
353 (* ------------------------------------------------------------------------- *) |
353 (* ------------------------------------------------------------------------- *) |
354 (* The LCM of all the divisors that involve x. *) |
354 (* The LCM of all the divisors that involve x. *) |
355 (* ------------------------------------------------------------------------- *) |
355 (* ------------------------------------------------------------------------- *) |
356 |
356 |
357 fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) = |
357 fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) = |
358 if x = y then abs(dest_numeral d) else 1 |
358 if x = y then abs(dest_number d) else 1 |
359 |divlcm x ( Const ("Not", _) $ p) = divlcm x p |
359 |divlcm x ( Const ("Not", _) $ p) = divlcm x p |
360 |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) |
360 |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) |
361 |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) |
361 |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) |
362 |divlcm x _ = 1; |
362 |divlcm x _ = 1; |
363 |
363 |
373 then [linear_neg a] |
373 then [linear_neg a] |
374 else bset x p |
374 else bset x p |
375 |_ =>[]) |
375 |_ =>[]) |
376 |
376 |
377 else bset x p |
377 else bset x p |
378 |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else [] |
378 |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_number 1))] else [] |
379 |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] |
379 |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] |
380 |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) |
380 |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) |
381 |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) |
381 |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) |
382 |_ => []; |
382 |_ => []; |
383 |
383 |
393 then [linear_neg a] |
393 then [linear_neg a] |
394 else [] |
394 else [] |
395 |_ =>[]) |
395 |_ =>[]) |
396 |
396 |
397 else aset x p |
397 else aset x p |
398 |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else [] |
398 |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_number 1) a] else [] |
399 |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else [] |
399 |(Const ("Orderings.less",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_number (~1))) then [a] else [] |
400 |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q) |
400 |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q) |
401 |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q) |
401 |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q) |
402 |_ => []; |
402 |_ => []; |
403 |
403 |
404 |
404 |
408 |
408 |
409 fun linrep vars x t fm = case fm of |
409 fun linrep vars x t fm = case fm of |
410 ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => |
410 ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => |
411 if (x = y) andalso (is_arith_rel fm) |
411 if (x = y) andalso (is_arith_rel fm) |
412 then |
412 then |
413 let val ct = linear_cmul (dest_numeral c) t |
413 let val ct = linear_cmul (dest_number c) t |
414 in (HOLogic.mk_binrel p (d, linear_add vars ct z)) |
414 in (HOLogic.mk_binrel p (d, linear_add vars ct z)) |
415 end |
415 end |
416 else fm |
416 else fm |
417 |(Const ("Not", _) $ p) => HOLogic.Not $ (linrep vars x t p) |
417 |(Const ("Not", _) $ p) => HOLogic.Not $ (linrep vars x t p) |
418 |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (linrep vars x t p) $ (linrep vars x t q) |
418 |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (linrep vars x t p) $ (linrep vars x t q) |
428 exception DVD_UNKNOWN |
428 exception DVD_UNKNOWN |
429 |
429 |
430 fun dvd_op (d, t) = |
430 fun dvd_op (d, t) = |
431 if not(is_numeral d) then raise DVD_UNKNOWN |
431 if not(is_numeral d) then raise DVD_UNKNOWN |
432 else let |
432 else let |
433 val dn = dest_numeral d |
433 val dn = dest_number d |
434 fun coeffs_of x = case x of |
434 fun coeffs_of x = case x of |
435 Const(p,_) $ tl $ tr => |
435 Const(p,_) $ tl $ tr => |
436 if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr) |
436 if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr) |
437 else if p = "HOL.times" |
437 else if p = "HOL.times" |
438 then if (is_numeral tr) |
438 then if (is_numeral tr) |
439 then [(dest_numeral tr) * (dest_numeral tl)] |
439 then [(dest_number tr) * (dest_number tl)] |
440 else [dest_numeral tl] |
440 else [dest_number tl] |
441 else [] |
441 else [] |
442 |_ => if (is_numeral t) then [dest_numeral t] else [] |
442 |_ => if (is_numeral t) then [dest_number t] else [] |
443 val ts = coeffs_of t |
443 val ts = coeffs_of t |
444 in case ts of |
444 in case ts of |
445 [] => raise DVD_UNKNOWN |
445 [] => raise DVD_UNKNOWN |
446 |_ => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true |
446 |_ => fold_rev (fn k => fn r => r andalso (k mod dn = 0)) ts true |
447 end; |
447 end; |
464 ((if dvd_op(s,t) then HOLogic.true_const |
464 ((if dvd_op(s,t) then HOLogic.true_const |
465 else HOLogic.false_const) |
465 else HOLogic.false_const) |
466 handle _ => at) |
466 handle _ => at) |
467 else |
467 else |
468 case AList.lookup (op =) operations p of |
468 case AList.lookup (op =) operations p of |
469 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const) |
469 SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const else HOLogic.false_const) |
470 handle _ => at) |
470 handle _ => at) |
471 | _ => at) |
471 | _ => at) |
472 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
472 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
473 case AList.lookup (op =) operations p of |
473 case AList.lookup (op =) operations p of |
474 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then |
474 SOME f => ((if (f ((dest_number s),(dest_number t))) then |
475 HOLogic.false_const else HOLogic.true_const) |
475 HOLogic.false_const else HOLogic.true_const) |
476 handle _ => at) |
476 handle _ => at) |
477 | _ => at) |
477 | _ => at) |
478 | _ => at; |
478 | _ => at; |
479 |
479 |
480 *) |
480 *) |
481 |
481 |
482 fun evalc_atom at = case at of |
482 fun evalc_atom at = case at of |
483 (Const (p,_) $ s $ t) => |
483 (Const (p,_) $ s $ t) => |
484 ( case AList.lookup (op =) operations p of |
484 ( case AList.lookup (op =) operations p of |
485 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const |
485 SOME f => ((if (f ((dest_number s),(dest_number t))) then HOLogic.true_const |
486 else HOLogic.false_const) |
486 else HOLogic.false_const) |
487 handle _ => at) |
487 handle _ => at) |
488 | _ => at) |
488 | _ => at) |
489 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
489 |Const("Not",_)$(Const (p,_) $ s $ t) =>( |
490 case AList.lookup (op =) operations p of |
490 case AList.lookup (op =) operations p of |
491 SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) |
491 SOME f => ((if (f ((dest_number s),(dest_number t))) |
492 then HOLogic.false_const else HOLogic.true_const) |
492 then HOLogic.false_const else HOLogic.true_const) |
493 handle _ => at) |
493 handle _ => at) |
494 | _ => at) |
494 | _ => at) |
495 | _ => at; |
495 | _ => at; |
496 |
496 |
657 Free (name,_) => Free (name,T) $ (mk_uni_vars T rest) |
657 Free (name,_) => Free (name,T) $ (mk_uni_vars T rest) |
658 |_=> (mk_uni_vars T node) $ (mk_uni_vars T rest ) ) |
658 |_=> (mk_uni_vars T node) $ (mk_uni_vars T rest ) ) |
659 |mk_uni_vars T (Free (v,_)) = Free (v,T) |
659 |mk_uni_vars T (Free (v,_)) = Free (v,T) |
660 |mk_uni_vars T tm = tm; |
660 |mk_uni_vars T tm = tm; |
661 |
661 |
662 fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_numeral 0) else (Const ("HOL.zero",T2)) |
662 fun mk_uni_int T (Const ("HOL.zero",T2)) = if T = T2 then (mk_number 0) else (Const ("HOL.zero",T2)) |
663 |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_numeral 1) else (Const ("HOL.one",T2)) |
663 |mk_uni_int T (Const ("HOL.one",T2)) = if T = T2 then (mk_number 1) else (Const ("HOL.one",T2)) |
664 |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest ) |
664 |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest ) |
665 |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) |
665 |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) |
666 |mk_uni_int T tm = tm; |
666 |mk_uni_int T tm = tm; |
667 |
667 |
668 |
668 |
678 val vars = (xn::vars1) |
678 val vars = (xn::vars1) |
679 val p = unitycoeff x (posineq (simpl p1)) |
679 val p = unitycoeff x (posineq (simpl p1)) |
680 val p_inf = simpl (minusinf x p) |
680 val p_inf = simpl (minusinf x p) |
681 val bset = bset x p |
681 val bset = bset x p |
682 val js = myupto 1 (divlcm x p) |
682 val js = myupto 1 (divlcm x p) |
683 fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p |
683 fun p_element j b = linrep vars x (linear_add vars b (mk_number j)) p |
684 fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset) |
684 fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) bset) |
685 in (list_disj (map stage js)) |
685 in (list_disj (map stage js)) |
686 end |
686 end |
687 | _ => error "cooper: not an existential formula"; |
687 | _ => error "cooper: not an existential formula"; |
688 |
688 |
689 |
689 |
697 val vars = (xn::vars1) |
697 val vars = (xn::vars1) |
698 val p = unitycoeff x (posineq (simpl p1)) |
698 val p = unitycoeff x (posineq (simpl p1)) |
699 val p_inf = simpl (plusinf x p) |
699 val p_inf = simpl (plusinf x p) |
700 val aset = aset x p |
700 val aset = aset x p |
701 val js = myupto 1 (divlcm x p) |
701 val js = myupto 1 (divlcm x p) |
702 fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p |
702 fun p_element j a = linrep vars x (linear_sub vars a (mk_number j)) p |
703 fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset) |
703 fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) aset) |
704 in (list_disj (map stage js)) |
704 in (list_disj (map stage js)) |
705 end |
705 end |
706 | _ => error "cooper: not an existential formula"; |
706 | _ => error "cooper: not an existential formula"; |
707 |
707 |
708 |
708 |
709 (* Try to find a withness for the formula *) |
709 (* Try to find a withness for the formula *) |
710 |
710 |
711 fun inf_w mi d vars x p = |
711 fun inf_w mi d vars x p = |
712 let val f = if mi then minusinf else plusinf in |
712 let val f = if mi then minusinf else plusinf in |
713 case (simpl (minusinf x p)) of |
713 case (simpl (minusinf x p)) of |
714 Const("True",_) => (SOME (mk_numeral 1), HOLogic.true_const) |
714 Const("True",_) => (SOME (mk_number 1), HOLogic.true_const) |
715 |Const("False",_) => (NONE,HOLogic.false_const) |
715 |Const("False",_) => (NONE,HOLogic.false_const) |
716 |F => |
716 |F => |
717 let |
717 let |
718 fun h n = |
718 fun h n = |
719 case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of |
719 case ((simpl o evalc) (linrep vars x (mk_number n) F)) of |
720 Const("True",_) => (SOME (mk_numeral n),HOLogic.true_const) |
720 Const("True",_) => (SOME (mk_number n),HOLogic.true_const) |
721 |F' => if n=1 then (NONE,F') |
721 |F' => if n=1 then (NONE,F') |
722 else let val (rw,rf) = h (n-1) in |
722 else let val (rw,rf) = h (n-1) in |
723 (rw,HOLogic.mk_disj(F',rf)) |
723 (rw,HOLogic.mk_disj(F',rf)) |
724 end |
724 end |
725 |
725 |
734 Const("True",_) => (SOME n,HOLogic.true_const) |
734 Const("True",_) => (SOME n,HOLogic.true_const) |
735 |F' => let val (rw,rf) = h nl |
735 |F' => let val (rw,rf) = h nl |
736 in (rw,HOLogic.mk_disj(F',rf)) |
736 in (rw,HOLogic.mk_disj(F',rf)) |
737 end) |
737 end) |
738 val f = if b then linear_add else linear_sub |
738 val f = if b then linear_add else linear_sub |
739 val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_numeral i)) st)) (myupto 1 d) [] |
739 val p_elements = fold_rev (fn i => fn l => l union (map (fn e => f [] e (mk_number i)) st)) (myupto 1 d) [] |
740 in h p_elements |
740 in h p_elements |
741 end; |
741 end; |
742 |
742 |
743 fun withness d b st vars x p = case (inf_w b d vars x p) of |
743 fun withness d b st vars x p = case (inf_w b d vars x p) of |
744 (SOME n,_) => (SOME n,HOLogic.true_const) |
744 (SOME n,_) => (SOME n,HOLogic.true_const) |
767 val js = myupto 1 (divlcm x p) |
767 val js = myupto 1 (divlcm x p) |
768 val (p_inf,f,S ) = |
768 val (p_inf,f,S ) = |
769 if (length bst) <= (length ast) |
769 if (length bst) <= (length ast) |
770 then (simpl (minusinf x p),linear_add,bst) |
770 then (simpl (minusinf x p),linear_add,bst) |
771 else (simpl (plusinf x p), linear_sub,ast) |
771 else (simpl (plusinf x p), linear_sub,ast) |
772 fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p |
772 fun p_element j a = linrep vars x (f vars a (mk_number j)) p |
773 fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S) |
773 fun stage j = list_disj (linrep vars x (mk_number j) p_inf :: map (p_element j) S) |
774 fun stageh n = ((if n = 0 then [] |
774 fun stageh n = ((if n = 0 then [] |
775 else |
775 else |
776 let |
776 let |
777 val nth_stage = simpl (evalc (stage n)) |
777 val nth_stage = simpl (evalc (stage n)) |
778 in |
778 in |