Re: [isabelle] Case distinction with Recursion Induction



On Tue, 15 May 2012, Alfio Martini wrote:

However, when using this I will always insert a comment next to the corresponding case so as to avoid impairing the clarity of the proof.

Comments can be very confusion, because they tend to diverge quickly from the formally checked text, when that is changed a few times in its natural life cycle.

Clarity of proofs means to put the right amount of explicit propositions in the text, not too little, not too much. Isar allows some flexibilty here. If you take a look at src/HOL/Induct/Command_Patterns.thy, for example, there are some illustrative patterns that use symbolic 'case' statements together with concrete propositions.

So an invocation of

  case Foo

that introduces some local facts A and B and more in an opaque manner can later be elucidated by saying

  have "A" by fact
  have "B" by fact

or

  have "A" and "B" by fact+

or

  note `A` and `B`

etc.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.