325 by smt |
325 by smt |
326 |
326 |
327 |
327 |
328 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt |
328 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt |
329 |
329 |
330 lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)" by smt |
330 lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)" |
331 |
331 using [[z3_with_extensions]] |
332 lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" by smt |
332 by smt |
|
333 |
|
334 lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" |
|
335 using [[z3_with_extensions]] |
|
336 by smt |
333 |
337 |
334 lemma |
338 lemma |
335 assumes "x \<noteq> (0::real)" |
339 assumes "x \<noteq> (0::real)" |
336 shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not>P then 4 else 2) * x" |
340 shows "x + x \<noteq> (let P = (abs x > 1) in if P \<or> \<not>P then 4 else 2) * x" |
337 using assms by smt |
341 using assms by smt |
338 |
342 |
339 lemma |
343 lemma |
340 assumes "(n + m) mod 2 = 0" and "n mod 4 = 3" |
344 assumes "(n + m) mod 2 = 0" and "n mod 4 = 3" |
341 shows "n mod 2 = 1 & m mod 2 = (1::int)" |
345 shows "n mod 2 = 1 & m mod 2 = (1::int)" |
342 using assms by smt |
346 using assms [[z3_with_extensions]] by smt |
343 |
347 |
344 |
348 |
345 |
349 |
346 subsection {* Linear arithmetic with quantifiers *} |
350 subsection {* Linear arithmetic with quantifiers *} |
347 |
351 |
391 |
395 |
392 |
396 |
393 subsection {* Non-linear arithmetic over integers and reals *} |
397 subsection {* Non-linear arithmetic over integers and reals *} |
394 |
398 |
395 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0" |
399 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0" |
396 using [[smt_oracle=true]] |
400 using [[smt_oracle, z3_with_extensions]] |
397 by smt |
401 by smt |
398 |
402 |
399 lemma "(a::int) * (x + 1 + y) = a * x + a * (y + 1)" |
403 lemma "(a::int) * (x + 1 + y) = a * x + a * (y + 1)" |
|
404 using [[z3_with_extensions]] |
400 by smt |
405 by smt |
401 |
406 |
402 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)" |
407 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)" |
|
408 using [[z3_with_extensions]] |
403 by smt |
409 by smt |
404 |
410 |
405 lemma |
411 lemma |
406 "(U::int) + (1 + p) * (b + e) + p * d = |
412 "(U::int) + (1 + p) * (b + e) + p * d = |
407 U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)" |
413 U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)" |
|
414 using [[z3_with_extensions]] |
408 by smt |
415 by smt |
409 |
416 |
410 lemma [z3_rule]: |
417 lemma [z3_rule]: |
411 fixes x :: "int" |
418 fixes x :: "int" |
412 assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0" |
419 assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0" |
413 shows False |
420 shows False |
414 using assms by (metis mult_le_0_iff) |
421 using assms by (metis mult_le_0_iff) |
415 |
422 |
416 lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt |
423 lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" |
|
424 using [[z3_with_extensions]] |
|
425 by smt |
417 |
426 |
418 |
427 |
419 |
428 |
420 subsection {* Linear arithmetic for natural numbers *} |
429 subsection {* Linear arithmetic for natural numbers *} |
421 |
430 |
496 "(eval_dioph ks xs = l) = |
505 "(eval_dioph ks xs = l) = |
497 (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and> |
506 (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and> |
498 eval_dioph ks (map (\<lambda>x. x div 2) xs) = |
507 eval_dioph ks (map (\<lambda>x. x div 2) xs) = |
499 (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)" |
508 (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)" |
500 using [[smt_oracle=true]] (*FIXME*) |
509 using [[smt_oracle=true]] (*FIXME*) |
|
510 using [[z3_with_extensions]] |
501 by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2]) |
511 by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2]) |
502 |
512 |
503 |
513 |
504 context complete_lattice |
514 context complete_lattice |
505 begin |
515 begin |