114 (* ------------------------------------------------------------------------- *) |
114 (* ------------------------------------------------------------------------- *) |
115 |
115 |
116 |
116 |
117 fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in |
117 fun linear_cmul n tm = if n = 0 then zero else let fun times n k = n*k in |
118 ( case tm of |
118 ( case tm of |
119 (Const("op +",T) $ (Const ("op *",T1 ) $c1 $ x1) $ rest) => |
119 (Const("HOL.plus",T) $ (Const ("HOL.times",T1 ) $c1 $ x1) $ rest) => |
120 Const("op +",T) $ ((Const("op *",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) |
120 Const("HOL.plus",T) $ ((Const("HOL.times",T1) $ (numeral1 (times n) c1) $ x1)) $ (linear_cmul n rest) |
121 |_ => numeral1 (times n) tm) |
121 |_ => numeral1 (times n) tm) |
122 end ; |
122 end ; |
123 |
123 |
124 |
124 |
125 |
125 |
137 |
137 |
138 |
138 |
139 fun linear_add vars tm1 tm2 = |
139 fun linear_add vars tm1 tm2 = |
140 let fun addwith x y = x + y in |
140 let fun addwith x y = x + y in |
141 (case (tm1,tm2) of |
141 (case (tm1,tm2) of |
142 ((Const ("op +",T1) $ ( Const("op *",T2) $ c1 $ x1) $ rest1),(Const |
142 ((Const ("HOL.plus",T1) $ ( Const("HOL.times",T2) $ c1 $ x1) $ rest1),(Const |
143 ("op +",T3)$( Const("op *",T4) $ c2 $ x2) $ rest2)) => |
143 ("HOL.plus",T3)$( Const("HOL.times",T4) $ c2 $ x2) $ rest2)) => |
144 if x1 = x2 then |
144 if x1 = x2 then |
145 let val c = (numeral2 (addwith) c1 c2) |
145 let val c = (numeral2 (addwith) c1 c2) |
146 in |
146 in |
147 if c = zero then (linear_add vars rest1 rest2) |
147 if c = zero then (linear_add vars rest1 rest2) |
148 else (Const("op +",T1) $ (Const("op *",T2) $ c $ x1) $ (linear_add vars rest1 rest2)) |
148 else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c $ x1) $ (linear_add vars rest1 rest2)) |
149 end |
149 end |
150 else |
150 else |
151 if earlierv vars x1 x2 then (Const("op +",T1) $ |
151 if earlierv vars x1 x2 then (Const("HOL.plus",T1) $ |
152 (Const("op *",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) |
152 (Const("HOL.times",T2)$ c1 $ x1) $ (linear_add vars rest1 tm2)) |
153 else (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) |
153 else (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 rest2)) |
154 |((Const("op +",T1) $ (Const("op *",T2) $ c1 $ x1) $ rest1) ,_) => |
154 |((Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c1 $ x1) $ rest1) ,_) => |
155 (Const("op +",T1)$ (Const("op *",T2) $ c1 $ x1) $ (linear_add vars |
155 (Const("HOL.plus",T1)$ (Const("HOL.times",T2) $ c1 $ x1) $ (linear_add vars |
156 rest1 tm2)) |
156 rest1 tm2)) |
157 |(_, (Const("op +",T1) $(Const("op *",T2) $ c2 $ x2) $ rest2)) => |
157 |(_, (Const("HOL.plus",T1) $(Const("HOL.times",T2) $ c2 $ x2) $ rest2)) => |
158 (Const("op +",T1) $ (Const("op *",T2) $ c2 $ x2) $ (linear_add vars tm1 |
158 (Const("HOL.plus",T1) $ (Const("HOL.times",T2) $ c2 $ x2) $ (linear_add vars tm1 |
159 rest2)) |
159 rest2)) |
160 | (_,_) => numeral2 (addwith) tm1 tm2) |
160 | (_,_) => numeral2 (addwith) tm1 tm2) |
161 |
161 |
162 end; |
162 end; |
163 |
163 |
178 After this fuction the all expressions containig ths variable will have the form |
178 After this fuction the all expressions containig ths variable will have the form |
179 c*Free(x,T) + t where c is a constant ant t is a Term which is not containing |
179 c*Free(x,T) + t where c is a constant ant t is a Term which is not containing |
180 Free(x,T)*) |
180 Free(x,T)*) |
181 |
181 |
182 fun lint vars tm = if is_numeral tm then tm else case tm of |
182 fun lint vars tm = if is_numeral tm then tm else case tm of |
183 (Free (x,T)) => (HOLogic.mk_binop "op +" ((HOLogic.mk_binop "op *" ((mk_numeral 1),Free (x,T))), zero)) |
183 (Free (x,T)) => (HOLogic.mk_binop "HOL.plus" ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1),Free (x,T))), zero)) |
184 |(Bound i) => (Const("op +",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ |
184 |(Bound i) => (Const("HOL.plus",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ |
185 (Const("op *",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) |
185 (Const("HOL.times",HOLogic.intT -->HOLogic.intT -->HOLogic.intT) $ (mk_numeral 1) $ (Bound i)) $ zero) |
186 |(Const("uminus",_) $ t ) => (linear_neg (lint vars t)) |
186 |(Const("HOL.uminus",_) $ t ) => (linear_neg (lint vars t)) |
187 |(Const("op +",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) |
187 |(Const("HOL.plus",_) $ s $ t) => (linear_add vars (lint vars s) (lint vars t)) |
188 |(Const("op -",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) |
188 |(Const("HOL.minus",_) $ s $ t) => (linear_sub vars (lint vars s) (lint vars t)) |
189 |(Const ("op *",_) $ s $ t) => |
189 |(Const ("HOL.times",_) $ s $ t) => |
190 let val s' = lint vars s |
190 let val s' = lint vars s |
191 val t' = lint vars t |
191 val t' = lint vars t |
192 in |
192 in |
193 if is_numeral s' then (linear_cmul (dest_numeral s') t') |
193 if is_numeral s' then (linear_cmul (dest_numeral s') t') |
194 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
194 else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
210 let val c' = (mk_numeral(abs(dest_numeral c))) |
210 let val c' = (mk_numeral(abs(dest_numeral c))) |
211 in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) |
211 in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) |
212 end |
212 end |
213 else (warning "Nonlinear term --- Non numeral leftside at dvd" |
213 else (warning "Nonlinear term --- Non numeral leftside at dvd" |
214 ;raise COOPER) |
214 ;raise COOPER) |
215 |linform vars (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) |
215 |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) ) |
216 |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s)) |
216 |linform vars (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s)) |
217 |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) |
217 |linform vars (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) |
218 |linform vars (Const("op <=",_)$ s $ t ) = |
218 |linform vars (Const("op <=",_)$ s $ t ) = |
219 (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) |
219 (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $t $(mk_numeral 1)) $ s)) |
220 |linform vars (Const("op >=",_)$ s $ t ) = |
220 |linform vars (Const("op >=",_)$ s $ t ) = |
221 (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> |
221 (mkatom vars "op <" (Const ("HOL.minus",HOLogic.intT --> HOLogic.intT --> |
222 HOLogic.intT) $ (Const("op +",HOLogic.intT --> HOLogic.intT --> |
222 HOLogic.intT) $ (Const("HOL.plus",HOLogic.intT --> HOLogic.intT --> |
223 HOLogic.intT) $s $(mk_numeral 1)) $ t)) |
223 HOLogic.intT) $s $(mk_numeral 1)) $ t)) |
224 |
224 |
225 |linform vars fm = fm; |
225 |linform vars fm = fm; |
226 |
226 |
227 (* ------------------------------------------------------------------------- *) |
227 (* ------------------------------------------------------------------------- *) |
244 (*BEWARE: replaces Library.gcd!! There is also Library.lcm!*) |
244 (*BEWARE: replaces Library.gcd!! There is also Library.lcm!*) |
245 fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; |
245 fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; |
246 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); |
246 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); |
247 |
247 |
248 fun formlcm x fm = case fm of |
248 fun formlcm x fm = case fm of |
249 (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) => if |
249 (Const (p,_)$ _ $(Const ("HOL.plus", _)$(Const ("HOL.times",_)$ c $ y ) $z ) ) => if |
250 (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1 |
250 (is_arith_rel fm) andalso (x = y) then (abs(dest_numeral c)) else 1 |
251 | ( Const ("Not", _) $p) => formlcm x p |
251 | ( Const ("Not", _) $p) => formlcm x p |
252 | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) |
252 | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) |
253 | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) |
253 | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) |
254 | _ => 1; |
254 | _ => 1; |
257 (* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *) |
257 (* Adjust all coefficients of x in formula; fold in reduction to +/- 1. *) |
258 (* ------------------------------------------------------------------------- *) |
258 (* ------------------------------------------------------------------------- *) |
259 |
259 |
260 fun adjustcoeff x l fm = |
260 fun adjustcoeff x l fm = |
261 case fm of |
261 case fm of |
262 (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ |
262 (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
263 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
263 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
264 let val m = l div (dest_numeral c) |
264 let val m = l div (dest_numeral c) |
265 val n = (if p = "op <" then abs(m) else m) |
265 val n = (if p = "op <" then abs(m) else m) |
266 val xtm = HOLogic.mk_binop "op *" ((mk_numeral (m div n)), x) |
266 val xtm = HOLogic.mk_binop "HOL.times" ((mk_numeral (m div n)), x) |
267 in |
267 in |
268 (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) |
268 (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
269 end |
269 end |
270 else fm |
270 else fm |
271 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) |
271 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeff x l p) |
272 |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeff x l p) $(adjustcoeff x l q) |
272 |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeff x l p) $(adjustcoeff x l q) |
273 |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeff x l p)$ (adjustcoeff x l q) |
273 |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeff x l p)$ (adjustcoeff x l q) |
280 fun unitycoeff x fm = |
280 fun unitycoeff x fm = |
281 let val l = formlcm x fm |
281 let val l = formlcm x fm |
282 val fm' = adjustcoeff x l fm in |
282 val fm' = adjustcoeff x l fm in |
283 if l = 1 then fm' |
283 if l = 1 then fm' |
284 else |
284 else |
285 let val xp = (HOLogic.mk_binop "op +" |
285 let val xp = (HOLogic.mk_binop "HOL.plus" |
286 ((HOLogic.mk_binop "op *" ((mk_numeral 1), x )), zero)) |
286 ((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero)) |
287 in |
287 in |
288 HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) |
288 HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm) |
289 end |
289 end |
290 end; |
290 end; |
291 |
291 |
292 (* adjustcoeffeq l fm adjusts the coeffitients c_i of x overall in fm to l*) |
292 (* adjustcoeffeq l fm adjusts the coeffitients c_i of x overall in fm to l*) |
293 (* Here l must be a multiple of all c_i otherwise the obtained formula is not equivalent*) |
293 (* Here l must be a multiple of all c_i otherwise the obtained formula is not equivalent*) |
294 (* |
294 (* |
295 fun adjustcoeffeq x l fm = |
295 fun adjustcoeffeq x l fm = |
296 case fm of |
296 case fm of |
297 (Const(p,_) $d $( Const ("op +", _)$(Const ("op *",_) $ |
297 (Const(p,_) $d $( Const ("HOL.plus", _)$(Const ("HOL.times",_) $ |
298 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
298 c $ y ) $z )) => if (is_arith_rel fm) andalso (x = y) then |
299 let val m = l div (dest_numeral c) |
299 let val m = l div (dest_numeral c) |
300 val n = (if p = "op <" then abs(m) else m) |
300 val n = (if p = "op <" then abs(m) else m) |
301 val xtm = (HOLogic.mk_binop "op *" ((mk_numeral ((m div n)*l) ), x)) |
301 val xtm = (HOLogic.mk_binop "HOL.times" ((mk_numeral ((m div n)*l) ), x)) |
302 in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "op +" ( xtm ,( linear_cmul n z) )))) |
302 in (HOLogic.mk_binrel p ((linear_cmul n d),(HOLogic.mk_binop "HOL.plus" ( xtm ,( linear_cmul n z) )))) |
303 end |
303 end |
304 else fm |
304 else fm |
305 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) |
305 |( Const ("Not", _) $ p) => HOLogic.Not $ (adjustcoeffeq x l p) |
306 |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeffeq x l p) $(adjustcoeffeq x l q) |
306 |( Const ("op &",_) $ p $ q) => HOLogic.conj$(adjustcoeffeq x l p) $(adjustcoeffeq x l q) |
307 |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeffeq x l p)$ (adjustcoeffeq x l q) |
307 |( Const ("op |",_) $ p $ q) => HOLogic.disj $(adjustcoeffeq x l p)$ (adjustcoeffeq x l q) |
313 (* ------------------------------------------------------------------------- *) |
313 (* ------------------------------------------------------------------------- *) |
314 (* The "minus infinity" version. *) |
314 (* The "minus infinity" version. *) |
315 (* ------------------------------------------------------------------------- *) |
315 (* ------------------------------------------------------------------------- *) |
316 |
316 |
317 fun minusinf x fm = case fm of |
317 fun minusinf x fm = case fm of |
318 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) => |
318 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
319 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const |
319 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const |
320 else fm |
320 else fm |
321 |
321 |
322 |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z |
322 |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z |
323 )) => if (x = y) |
323 )) => if (x = y) |
324 then if (pm1 = one) andalso (c = zero) then HOLogic.false_const |
324 then if (pm1 = one) andalso (c = zero) then HOLogic.false_const |
325 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const |
325 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const |
326 else error "minusinf : term not in normal form!!!" |
326 else error "minusinf : term not in normal form!!!" |
327 else fm |
327 else fm |
334 (* ------------------------------------------------------------------------- *) |
334 (* ------------------------------------------------------------------------- *) |
335 (* The "Plus infinity" version. *) |
335 (* The "Plus infinity" version. *) |
336 (* ------------------------------------------------------------------------- *) |
336 (* ------------------------------------------------------------------------- *) |
337 |
337 |
338 fun plusinf x fm = case fm of |
338 fun plusinf x fm = case fm of |
339 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) => |
339 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ (c1 ) $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ c2 $ y) $z)) => |
340 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const |
340 if (is_arith_rel fm) andalso (x=y) andalso (c2 = one) andalso (c1 =zero) then HOLogic.false_const |
341 else fm |
341 else fm |
342 |
342 |
343 |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z |
343 |(Const("op <",_) $ c $(Const ("HOL.plus", _) $(Const ("HOL.times",_) $ pm1 $ y ) $ z |
344 )) => if (x = y) |
344 )) => if (x = y) |
345 then if (pm1 = one) andalso (c = zero) then HOLogic.true_const |
345 then if (pm1 = one) andalso (c = zero) then HOLogic.true_const |
346 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const |
346 else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const |
347 else error "plusinf : term not in normal form!!!" |
347 else error "plusinf : term not in normal form!!!" |
348 else fm |
348 else fm |
354 |
354 |
355 (* ------------------------------------------------------------------------- *) |
355 (* ------------------------------------------------------------------------- *) |
356 (* The LCM of all the divisors that involve x. *) |
356 (* The LCM of all the divisors that involve x. *) |
357 (* ------------------------------------------------------------------------- *) |
357 (* ------------------------------------------------------------------------- *) |
358 |
358 |
359 fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z ) ) = |
359 fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) = |
360 if x = y then abs(dest_numeral d) else 1 |
360 if x = y then abs(dest_numeral d) else 1 |
361 |divlcm x ( Const ("Not", _) $ p) = divlcm x p |
361 |divlcm x ( Const ("Not", _) $ p) = divlcm x p |
362 |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) |
362 |divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q) |
363 |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) |
363 |divlcm x ( Const ("op |",_) $ p $ q ) = lcm_num (divlcm x p) (divlcm x q) |
364 |divlcm x _ = 1; |
364 |divlcm x _ = 1; |
368 (* ------------------------------------------------------------------------- *) |
368 (* ------------------------------------------------------------------------- *) |
369 |
369 |
370 fun bset x fm = case fm of |
370 fun bset x fm = case fm of |
371 (Const ("Not", _) $ p) => if (is_arith_rel p) then |
371 (Const ("Not", _) $ p) => if (is_arith_rel p) then |
372 (case p of |
372 (case p of |
373 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) ) |
373 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) ) |
374 => if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero) |
374 => if (is_arith_rel p) andalso (x= y) andalso (c2 = one) andalso (c1 = zero) |
375 then [linear_neg a] |
375 then [linear_neg a] |
376 else bset x p |
376 else bset x p |
377 |_ =>[]) |
377 |_ =>[]) |
378 |
378 |
379 else bset x p |
379 else bset x p |
380 |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg(linear_add [] a (mk_numeral 1))] else [] |
380 |(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 [] |
381 |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] |
381 |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_neg a] else [] |
382 |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) |
382 |(Const ("op &",_) $ p $ q) => (bset x p) union (bset x q) |
383 |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) |
383 |(Const ("op |",_) $ p $ q) => (bset x p) union (bset x q) |
384 |_ => []; |
384 |_ => []; |
385 |
385 |
386 (* ------------------------------------------------------------------------- *) |
386 (* ------------------------------------------------------------------------- *) |
388 (* ------------------------------------------------------------------------- *) |
388 (* ------------------------------------------------------------------------- *) |
389 |
389 |
390 fun aset x fm = case fm of |
390 fun aset x fm = case fm of |
391 (Const ("Not", _) $ p) => if (is_arith_rel p) then |
391 (Const ("Not", _) $ p) => if (is_arith_rel p) then |
392 (case p of |
392 (case p of |
393 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $c2 $y) $a ) ) |
393 (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("HOL.plus", _) $(Const ("HOL.times",_) $c2 $y) $a ) ) |
394 => if (x= y) andalso (c2 = one) andalso (c1 = zero) |
394 => if (x= y) andalso (c2 = one) andalso (c1 = zero) |
395 then [linear_neg a] |
395 then [linear_neg a] |
396 else [] |
396 else [] |
397 |_ =>[]) |
397 |_ =>[]) |
398 |
398 |
399 else aset x p |
399 else aset x p |
400 |(Const ("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +",_) $ (Const ("op *",_) $c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = one) then [linear_sub [] (mk_numeral 1) a] else [] |
400 |(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 [] |
401 |(Const ("op <",_) $ c1$ (Const ("op +",_) $(Const ("op *",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else [] |
401 |(Const ("op <",_) $ c1$ (Const ("HOL.plus",_) $(Const ("HOL.times",_)$ c2 $ x) $ a)) => if (c1 =zero) andalso (c2 = (mk_numeral (~1))) then [a] else [] |
402 |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q) |
402 |(Const ("op &",_) $ p $ q) => (aset x p) union (aset x q) |
403 |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q) |
403 |(Const ("op |",_) $ p $ q) => (aset x p) union (aset x q) |
404 |_ => []; |
404 |_ => []; |
405 |
405 |
406 |
406 |
407 (* ------------------------------------------------------------------------- *) |
407 (* ------------------------------------------------------------------------- *) |
408 (* Replace top variable with another linear form, retaining canonicality. *) |
408 (* Replace top variable with another linear form, retaining canonicality. *) |
409 (* ------------------------------------------------------------------------- *) |
409 (* ------------------------------------------------------------------------- *) |
410 |
410 |
411 fun linrep vars x t fm = case fm of |
411 fun linrep vars x t fm = case fm of |
412 ((Const(p,_)$ d $ (Const("op +",_)$(Const("op *",_)$ c $ y) $ z))) => |
412 ((Const(p,_)$ d $ (Const("HOL.plus",_)$(Const("HOL.times",_)$ c $ y) $ z))) => |
413 if (x = y) andalso (is_arith_rel fm) |
413 if (x = y) andalso (is_arith_rel fm) |
414 then |
414 then |
415 let val ct = linear_cmul (dest_numeral c) t |
415 let val ct = linear_cmul (dest_numeral c) t |
416 in (HOLogic.mk_binrel p (d, linear_add vars ct z)) |
416 in (HOLogic.mk_binrel p (d, linear_add vars ct z)) |
417 end |
417 end |
433 if not(is_numeral d) then raise DVD_UNKNOWN |
433 if not(is_numeral d) then raise DVD_UNKNOWN |
434 else let |
434 else let |
435 val dn = dest_numeral d |
435 val dn = dest_numeral d |
436 fun coeffs_of x = case x of |
436 fun coeffs_of x = case x of |
437 Const(p,_) $ tl $ tr => |
437 Const(p,_) $ tl $ tr => |
438 if p = "op +" then (coeffs_of tl) union (coeffs_of tr) |
438 if p = "HOL.plus" then (coeffs_of tl) union (coeffs_of tr) |
439 else if p = "op *" |
439 else if p = "HOL.times" |
440 then if (is_numeral tr) |
440 then if (is_numeral tr) |
441 then [(dest_numeral tr) * (dest_numeral tl)] |
441 then [(dest_numeral tr) * (dest_numeral tl)] |
442 else [dest_numeral tl] |
442 else [dest_numeral tl] |
443 else [] |
443 else [] |
444 |_ => if (is_numeral t) then [dest_numeral t] else [] |
444 |_ => if (is_numeral t) then [dest_numeral t] else [] |