Re: [isabelle] Case distinction with Recursion Induction
That was very helpful. The theory "Common_Patterns.thy" is very
the "note" command when using "case" patterns in induction.
On Wed, May 16, 2012 at 10:18 AM, Makarius <makarius at sketis.net> wrote:
> 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
> have "A" and "B" by fact+
> note `A` and `B`
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and