Re: [isabelle] How powerful are trans rules?

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.

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.

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 is just the standard question about all structure proof elements: Is it sufficient to have some fixed scheme of rule application that is parameterized by facts from the library? Or is there a need to allow arbitrary tool implementations in that slot (in Isabelle/ML). 15 years ago the question was on the table, and the answer was that plain rules for 'also' are usually sufficient.

That rule also breaks antisymmetry proofs like

         fix a b c :: "'a ::cpo"
         have "a ⊑ b" sorry
         also have "b ⊑ c" sorry
         also have "c ⊑ a" sorry
         have "a = c".

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.


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