[isabelle] z3 proof reconstruction failure
when trying to proof the following (with z3):
lemma "x * y ≤ (0 :: int) ⟹ x ≤ 0 ∨ y ≤ 0"
I get a proof reconstruction failure:
Z3 found a proof, but proof reconstruction failed at the following subgoal:
x * y ≤ 0
¬ y ≤ 0
¬ x ≤ 0
Adding a rule to the lemma group "z3_rule" might solve this problem.
I tried to add an appropriate lemma to the group z3_rule, but without
success. Does anyone have an idea of how to make proof reconstruction
succeed in this case?
This archive was generated by a fusion of
Pipermail (Mailman edition) and