*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] How powerful are trans rules?*From*: Joachim Breitner <breitner at kit.edu>*Date*: Wed, 14 May 2014 22:46:35 +0200*In-reply-to*: <alpine.LNX.2.00.1405142048560.25666@lxbroy10.informatik.tu-muenchen.de>*References*: <1400078255.4064.17.camel@kirk> <alpine.LNX.2.00.1405142048560.25666@lxbroy10.informatik.tu-muenchen.de>

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. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] How powerful are trans rules?***From:*Makarius

**References**:**[isabelle] How powerful are trans rules?***From:*Joachim Breitner

**Re: [isabelle] How powerful are trans rules?***From:*Makarius

- Previous by Date: Re: [isabelle] How powerful are trans rules?
- Next by Date: Re: [isabelle] How powerful are trans rules?
- Previous by Thread: Re: [isabelle] How powerful are trans rules?
- Next by Thread: Re: [isabelle] How powerful are trans rules?
- Cl-isabelle-users May 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list