Case distinction for propositional logic

Question

I would like to prove

P ==> P

by case distinction, to understand the latter.

lemma "P ⟹ P"
proof (cases P)

goal (2 subgoals):
1. P ⟹ P ⟹ P
2. P ⟹ ¬ P ⟹ P

I am not quite sure if I want these. I wanted to assume that P is true and then show P is true by assumption, then assume not P and prove not P by assumption. Like in a truth table.

The not P in the second subgoal seems strange, is that provable at all?

 assume P then show P by assumption

 Successful attempt to solve goal by exported rule:
 (P) ⟹ P 

next

goal (1 subgoal):
 1. P ⟹ ¬ P ⟹ P

 assume P assume "¬P" then show "¬P" by (rule HOL.FalseE)

This went completely bad.

How can I take P and not P as the cases?

P ==> ~P ==> Q is always true, because the assumptions are contradictory. — Lars Noschinski

Ben Keks Ben Keks · Accepted Answer · 2015-07-29T10:30:47

P and not P already are your cases. If you write "cases P", Isabelle copys the current goal and adds P to the assumptions of the first and ¬ P to the assumption of the second new subgoal. The right-hand side of the goals is not affected by the cases method if used in this way.

In your case, you don't have to prove the ¬ P in the second subgoal, but you may use it as the additional assumption, introduced by the case destinction.

Obviously you can't prove P from ¬ P in the second subgoal. Luckily, the global assumption P is still there, so that both cases still prove P from P, which is as trviial as it already is without the case destinction ;).

If you want to prove something by having Isabelle insert the possible values of a variable directly, you could try:

  lemma "P ⟹ P"
  proof (induct P) 

  goal (2 subgoals):
  1. True ⟹ True
  2. False ⟹ False

Case distinction for propositional logic

1 Answers