Re: [isabelle] How powerful are trans rules?

Dear Makarius,

Am Mittwoch, den 14.05.2014, 20:56 +0200 schrieb Makarius:
> On Wed, 14 May 2014, Joachim Breitner wrote:
> > One thing I tried was to use
> >
> >        lemma strong_trans[trans]:
> >          "a ⊑ f x ⟹ x ⊑ y ⟹ cont f ⟹ a ⊑ f y " sorry
> >
> > This way, the calculation above become
> >
> >        cont (Rep_cfun f) ⟹ cont (λa. f⋅(g⋅a)) ⟹ a ⊑ f⋅(g⋅d)
> >
> > so using "by simp" instead of "." finishes this. But I find this
> > annoying (I really like to finish with "finally ?something.").
> 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’m not sure. Last time I tried it I was not satisfied for some reason,
although that reason did not show up when preparing the small example
for my mailing list mail. Maybe I should simply re-evaluate that option.

> Formally, you did not explain the annoyance nor why you like to do it only 
> like that.  There can be technical problems in some situations, but if 
> that is the case here it needs to be made specific.

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.

Also, to the reader, a "by simp" at the end could potentially do many
things, where a "finally show ?thesis." tells the reader that nothing
fancy is happening at the end.

But as I said, its mostly code aesthetics: worth asking if there is a
nicer way – not worth worrying about if there is not.

> > as the calculation at the end will be the unhelpful theorem
> >
> >          cont (λa. a) ⟹ cont (λa. a) ⟹ a ⊑ a.
> >
> > can I avoid that?
> Did you try to specify some particular rules for particular 'also' steps? 
> There is a notation with round parenthese described in the isar-ref 
> manual.

Thanks, I didn’t know that before (and I must have overread that part in
the docs). I think I’ll play around with that.


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.