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
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
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
have "A" and "B" by fact+
note `A` and `B`
This archive was generated by a fusion of
Pipermail (Mailman edition) and