equal
deleted
inserted
replaced
412 lemma |
412 lemma |
413 "(U::int) + (1 + p) * (b + e) + p * d = |
413 "(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)" |
414 U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)" |
415 by smt |
415 by smt |
416 |
416 |
|
417 lemma [z3_rule]: |
|
418 fixes x :: "int" |
|
419 assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0" |
|
420 shows False |
|
421 using assms by (metis mult_le_0_iff) |
|
422 |
|
423 lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt |
|
424 |
|
425 |
417 |
426 |
418 subsection {* Linear arithmetic for natural numbers *} |
427 subsection {* Linear arithmetic for natural numbers *} |
419 |
428 |
420 lemma "2 * (x::nat) ~= 1" by smt |
429 lemma "2 * (x::nat) ~= 1" by smt |
421 |
430 |