From: Mamoun FILALI-AMINE <mamoun.filali@irit.fr>

Hello,

Currently, when using the induct rule, an automated goal split is generated with cases to be selected and pasted, for instance:

theorem example:

assumes a: "A /\ C”

assumes b: "B /\ D”

shows "A /\ B /\ C /\ D”

proof (induct rule: conjI)

- A
- B /\ C /\ D

Proof outline with cases:

case 1 then show ?case sorry

next

case 2 then show ?case sorry

qed

Would it be possible to generate the proof outline to be selected and pasted.

For instance we would have:

theorem example:

assumes a: "A /\ C”

assumes b: "B /\ D”

shows "A /\ B /\ C /\ D" proof (induct rule: conjI)

- A
- B /\ C /\ D

Proof outline with cases:

case 1 (* A *) then show ?case sorry

next

case 2 (* B /\ C /\ D *) then show ?case sorry

qed

Thanks

Mamoun

PS 1. Essentially, the same message was also posted on Stackoverflow.

PS 2. Peter Zeller and Javier Diaz have kindly suggested that we can generate comments

by changing the name of the cases through case_namesor goal_cases.

But I was thinking that having the actual text of the goal to prove was

more meaningful in order to read the proof afterwards.

These texts are in fact already present before the proof outline.

I would like that they appear together with the concerned case (as comments)

in order to see what is actually proved and not just the label.

Last updated: Jan 25 2022 at 01:11 UTC