I would like to complete this proof.
How can I easily/elegantly use the values found by nitpick? (What to write at the ... part?)
Alternatively, how can I use the fact that nitpick found a counterexample to finish the proof?
lemma Nitpick_test: "¬(((a+b) = 5) ∧ ((a-b) = (1::int)))" (is "?P")
proof (rule ccontr)
assume "¬ ?P"
nitpick
(* Nitpicking formula...
Nitpick found a counterexample:
Free variables:
a = 3
b = 2
*)
show "False" by ...
qed
The theorem does not hold as stated, because if a = 3 and b = 2, the statement evaluates to False. For other values of a and b, however, the statement does hold. Thus, as a and b are implicitly universally quantified, you cannot prove the theorem as stated.
If you want to instead prove
theorem "EX a b. a + b = 5 & a - b = (1 :: int)"
you can use rule exI[where x="..."] to provide the witness ... for the existential quantifier, so 3 and 2 in this case.