Re: [isabelle] Case distinction with Recursion Induction



Dear Makarius,

That was very helpful. The theory "Common_Patterns.thy" is very
instructive! Especially
the "note" command when using "case" patterns in induction.

Best!

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
>
> or
>
>  have "A" and "B" by fact+
>
> or
>
>  note `A` and `B`
>
> etc.
>
>
>        Makarius
>



-- 
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 MHonArc.