equal
deleted
inserted
replaced
397 |
397 |
398 |
398 |
399 subsection {* Non-linear arithmetic over integers and reals *} |
399 subsection {* Non-linear arithmetic over integers and reals *} |
400 |
400 |
401 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0" |
401 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0" |
402 using zero_less_mult_pos |
402 using [[smt_oracle=true]] |
403 by smt |
403 by smt |
404 |
404 |
405 lemma "(a::int) * (x + 1 + y) = a * x + a * (y + 1)" |
405 lemma "(a::int) * (x + 1 + y) = a * x + a * (y + 1)" |
406 using right_distrib |
|
407 by smt |
406 by smt |
408 |
407 |
409 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)" |
408 lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)" |
410 sorry (* FIXME: Z3 could solve this directly *) |
409 by smt |
411 |
410 |
412 lemma |
411 lemma |
413 "(U::int) + (1 + p) * (b + e) + p * d = |
412 "(U::int) + (1 + p) * (b + e) + p * d = |
414 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)" |
415 sorry (* FIXME: Z3 could solve this directly *) |
414 by smt |
416 |
415 |
417 |
416 |
418 subsection {* Linear arithmetic for natural numbers *} |
417 subsection {* Linear arithmetic for natural numbers *} |
419 |
418 |
420 lemma "2 * (x::nat) ~= 1" by smt |
419 lemma "2 * (x::nat) ~= 1" by smt |