*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] How powerful are trans rules?*From*: Makarius <makarius at sketis.net>*Date*: Wed, 14 May 2014 20:56:39 +0200 (CEST)*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1400078255.4064.17.camel@kirk>*References*: <1400078255.4064.17.camel@kirk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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

Is there a way to have the side-condition already checked by "trans" (bysolving it with "intro cont2cont", for example), so that that they nevershow up to the user?

That rule also breaks antisymmetry proofs like notepad begin fix a b c :: "'a ::cpo" have "a ⊑ b" sorry also have "b ⊑ c" sorry also have "c ⊑ a" sorry finally have "a = c". end as the calculation at the end will be the unhelpful theorem cont (λa. a) ⟹ cont (λa. a) ⟹ a ⊑ a. can I avoid that?

Makarius

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

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

- Previous by Date: [isabelle] CFP: WFLP 2014 - Workshop on Functional and (Constraint) Logic Programming
- Next by Date: Re: [isabelle] How powerful are trans rules?
- Previous by Thread: [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