CODEWITHSUNDEEP
isabelletheorem-proving
TFuto
TFuto

Reputation: 1452

Isabelle - Nitpick counterexample usage

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

Upvotes: 1

Views: 308

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

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.

Upvotes: 3

Related Questions