Search code examples
isabelle

How to test for falsity in implications?

In a complex lemma which is basically an implication one may mistakenly form an antecedent that turns out to be falsity. Is there any support in Isabelle for avoiding this situation?

Solution

  • You can use quickcheck for that. In a proof where you suspect your antecedents don't hold, locally try to prove False:

    lemma "P ∧ ¬ P ⟹ foobar"
proof -
  have False
    quickcheck

    In case it's an antecedent that you need frequently, you can also do it like this:

    context
  assumes "P ∧ ¬ P"
begin

lemma False
  nitpick
  quickcheck

end

    The context command opens a new unnamed context with local hypotheses. When you exit the context, the assumption gets added to all theorems. There, you can also use nitpick to find problems.