*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] How powerful are trans rules?*From*: Joachim Breitner <breitner at kit.edu>*Date*: Wed, 14 May 2014 16:37:35 +0200

Hi, I’m quite fond of "also ... also ... finally" chains, as they tend to remove a lot of distracting technicalities from a proof. When working with HOLCF proofs, I would like to do proofs like this: notepad begin fix a b c d f g have "a ⊑ f ⋅ b" sorry also have "b ⊑ g ⋅ c" sorry also have "c ⊑ d" sorry finally have "a ⊑ f ⋅ (g ⋅ d)". end I currently do that by hard-coding all the variants of the trans rule that I need: lemma [trans]: "a ⊑ f ⋅ b ⟹ b ⊑ c ⟹ a ⊑ f ⋅ c" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) lemma [trans]: "a ⊑ f ⋅ b ⟹ f ⊑ g ⟹ a ⊑ g ⋅ b" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) lemma [trans]: "a ⊑ f ⋅ (g ⋅ b) ⟹ b ⊑ c ⟹ a ⊑ f ⋅ (g ⋅ c)" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) lemma [trans]: "a ⊑ f ⋅ b ⋅ c ⋅ d ⟹ b ⊑ b' ⟹ a ⊑ f ⋅ b' ⋅ c ⋅ d" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) lemma [trans]: "a ⊑ f ⋅ b ⋅ c ⋅ d ⟹ c ⊑ c' ⟹ a ⊑ f ⋅ b ⋅ c' ⋅ d" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) lemma [trans]: "a ⊑ f ⋅ (g ⋅ b) ⋅ c ⋅ d ⟹ g ⊑ g' ⟹ a ⊑ f ⋅ (g' ⋅ b) ⋅ c ⋅ d" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) lemma [trans]: "a ⊑ f ⋅ b ⋅ (g ⋅ c ⋅ d) ⋅ e ⟹ d ⊑ d' ⟹ a ⊑ f ⋅ b ⋅ (g ⋅ c ⋅ d') ⋅ e" by (erule below_trans) (intro monofun_cfun_fun monofun_cfun_arg) This works, but is rather inflexible and does not scale. And note that all those trans rules are solved by the same set of rules. How can I improve that? 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" (by solving it with "intro cont2cont", for example), so that that they never show 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? Thanks 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

- Previous by Date: Re: [isabelle] sorry in innocent blue?
- Next by Date: [isabelle] CFP: WFLP 2014 - Workshop on Functional and (Constraint) Logic Programming
- Previous by Thread: Re: [isabelle] »strict« or »sequential« mode in Isabelle/jEdit?
- 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