在归纳规则生成的文本中添加注释

如何解决在归纳规则生成的文本中添加注释

当前，使用归纳规则时，会自动生成目标划分：

例如：

定理示例：

假设一个：“ A”

假设b：“ B”

显示“ A∧B”

证明（归纳规则：conjI）

自动生成以下带有证明大纲的文本，其中要包含的案例 选择并粘贴：

1. A

2. B

带有案例的证明大纲：

案例1

然后显示？对不起

下一个

案例2

然后显示？对不起

qed

是否可以生成带有注释案例的证明大纲 进行选择和粘贴：例如，我们将：

1. A

2. B

带有案例的证明大纲：

情况1（* A *）

然后显示？对不起？

下一个

情况2（* B *）

然后显示？对不起

已确认

谢谢。

Mamoun

解决方法

我不知道如何在不修改Isabelle本身的情况下为案件生成评论的方法。 但是您可以使用case_names或goal_cases来更改案件名称：

lemma myConjI[case_names left right]: 
  assumes a: "A"
  assumes b: "B"
  shows "A ∧ B"
  using assms by auto


theorem example1:
  assumes a: "A"
  assumes b: "B"
  shows "A ∧ B"
proof (induct rule: myConjI)
  case left
  then show ?case sorry
next
  case right
  then show ?case sorry
qed


theorem example2:
  assumes a: "A"
  assumes b: "B"
  shows "A ∧ B"
proof (rule conjI,goal_cases Bla Blub)
  case Bla
  then show ?case sorry
next
  case Blub
  then show ?case sorry
qed