Re: [isabelle] How powerful are trans rules?


Am Mittwoch, den 14.05.2014, 22:57 +0200 schrieb Makarius:
> In some sense the side conditions are deferred to the very end, and thus 
> displaced.  The final "by simp" can make this feel a bit wobbly, since it 
> dilutes the application of the last fact, with the solving of the side 
> conditions.
> This can be refined: a "." merely abbreviates "by this", and the latter 
> can have a terminal method for the solving of the remainder:
>    ...
>    finally show ?thesis by this simp_all
> or
>    ...
>    finally show ?thesis by this auto
> The proof method "this" does not appear very often under its proper name 
> in Isar proofs, but it is a perfectly normal structured method like 
> "rule".

that’s a good suggestion. I now use

        finally show ?thesis by this (intro cont2cont)+

everywhere, and (at least to the adept reader), this signals „The
conclusion of the calculation is used unmodified, while the accumulated
side conditions are all of the form "cont something" and solved using
the usual cont2cont rules.

This even composes well with the few cases where I had
        finally show ?thesis by (rule foobar)
which now simply become
        finally show ?thesis by (rule foobar) (intro cont2cont)+

(I am a big fan of "intro"; I find it the most predictable method beyond
single-stepping with rule and subst).


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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