命题逻辑的大小写区分

Question

我想证明

P ==> P

按大小写区分，理解后者。

lemma "P ⟹ P"
proof (cases P)

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

我不太确定我是否想要这些。我想假设 P 为真，然后通过假设证明 P 为真，然后假设 P 不成立并通过假设证明 P 不成立。说实话 table.

第二个子目标中的非 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当成case而不是P当成case呢？

Answer 1

P 而不是 P 已经你的情况。如果你写 "cases P"，伊莎贝尔复制当前目标并将 P 添加到第一个假设和 ¬ P 添加到第二个新子目标的假设。如果以这种方式使用，则目标的右侧不受 cases 方法的影响。

在您的案例中，您不必证明第二个子目标中的 ¬ P，但您可以将其用作案例目标引入的附加假设。

显然你不能在第二个子目标中从 ¬ P 证明 P。幸运的是，全局假设 P 仍然存在，因此这两种情况仍然可以从 P 证明 P，这与没有案例目的地一样简单 ;).

如果您想通过让伊莎贝尔直接插入变量的可能值来证明某事，您可以尝试：

  lemma "P ⟹ P"
  proof (induct P) 

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

命题逻辑的大小写区分

Case distinction for propositional logic

logic

isabelle