Дело различия для логики

Question

Я хотел бы доказать

P ==> P 

прецедентным различием, чтобы понять последние.

lemma "P ⟹ P" 
proof (cases P) 

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

Я не совсем уверен, хочу ли я их. Я хотел предположить, что P истинно, а затем показать, что P истинно по предположению, а затем предположить не P и доказать не P по предположению. Как в таблице истины.

Не P во втором подцеле кажется странным, это вообще что-то доказуемо?

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) 

Это пошло совсем плохо.

Как я могу взять P, а не P в качестве случаев?

Answer 1

P и не P уже являются вашими случаями. Если вы пишете «случаи P», Изабель копирует текущую цель и добавляет P к предположениям первого и ¬ P к предположению о втором новом подцеле. Правая часть целей не зависит от метода case, если используется таким образом.

В вашем случае вам не нужно доказывать ¬ P во втором подцеле, но вы можете использовать его в качестве дополнительного предположения, введенного в случае дезактивации дела.

Очевидно, вы не можете доказать P из ¬ P во втором подцеле. К счастью, глобальное предположение P все еще существует, так что оба случая все еще доказывают P из P, что так же трогательно, как и уже без разбора случая;).

Если вы хотите что-то доказать, имея Isabelle вставки возможные значения переменной напрямую, вы можете попробовать:

lemma "P ⟹ P" 
    proof (induct P) 

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