Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Add comments to the text generated by induct rule

Email Gateway (Aug 27 2020 at 12:43):

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)

1. A
2. 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)

1. A
2. 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: Jul 15 2022 at 23:21 UTC