CODEWITHSUNDEEP
isabelle
Mamoun FILALI-AMINE
Mamoun FILALI-AMINE

Reputation: 11

Add comments to the text generated by induct rule

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:

  1. A

  2. B

Proof outline with cases:

case 1

then show ?case sorry

next

case 2

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:

  1. A

  2. B

Proof outline with cases:

case 1 (* A *)

then show ?case sorry

next

case 2 (* B *)

then show ?case sorry

qed

Thank you.

Mamoun

Upvotes: 1

Views: 51

Answers (1)

Peter Zeller
Peter Zeller

Reputation: 2276

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

Upvotes: 1

Related Questions