Re: [isabelle] How powerful are trans rules?



On Wed, 14 May 2014, Joachim Breitner wrote:

If the final "by simp" (or "by simp_all") for accumulated side-conditions does the job, why not use it? If all Isar calculations were to end with "." I could have omitted that flexibility in the language.

I think my annoyance is purely aesthetically, and – picky as I get – the aesthetics of the intermediate calculations. To me, the "cont" side conditions above feel out of place, as they hold already by the types and simple rule of composition.

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


	Makarius


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