Re: [isabelle] How powerful are trans rules?
On Wed, 14 May 2014, Joachim Breitner wrote:
One thing I tried was to use
"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
This archive was generated by a fusion of
Pipermail (Mailman edition) and