Add comments to the text generated by induct rule

Question

Currently, when using the induct rule, an automated goal split is generated:

for instance:

theorem example:

assumes a: "A"

assumes b: "B"

shows "A ∧ B"

proof (induct rule: conjI)

generates automatically the following text with the proof outline with cases to be selected and pasted:

A
B

Proof outline with cases:

case 1

then show ?case sorry

qed

Would it it be possible to generate the proof outline with commented cases to be selected and pasted: For instance we would have:

A
B

Proof outline with cases:

case 1 (* A *)

then show ?case sorry

qed

Thank you.

Mamoun

Peter Zeller Peter Zeller · Accepted Answer · 2020-08-20T10:00:33

I am not aware of a way to generate comments for cases without modifying Isabelle itself. But you can change the name of the cases using case_names or 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

Add comments to the text generated by induct rule

1 Answers