Email Gateway (Aug 23 2022 at 08:38): Email Gateway (Aug 23 2022 at 08:38):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Hi,
I was revisiting Real_Vector_Spaces.thy in Isabelle2020-RC1 and I found the following lemma:
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y"
by (simp add: of_real_def mult.commute)
I do not understand why "mult.commute" is added to the simplifier.
Indeed, I did the following experiment in order to check whether or not "mult.commute" was essential in this proof.
hide_const of_real
hide_fact of_real_mult
definition of_Real :: "real ⇒ 'a::real_algebra_1"
where "of_Real r = scaleR r 1"
lemma of_Real_mult [simp]: "of_Real (x * y) = of_Real x * of_Real y"
by (simp add: of_Real_def)
If this is the case, could it be possible to automatically check proof-by-proof (in all the libraries of Isabelle/HOL using sledgehammer) if all the one-line proofs are optimal, i.e., there are not unnecessary assumptions?
Kind regards,
José M.
Email Gateway (Aug 23 2022 at 08:38):From: Lawrence Paulson <lp15@cam.ac.uk>
Without any doubt, there must be numerous proofs can be simplified in this way.
Much more useful however would be to identify theorems that include unnecessary preconditions or where the type class constraints are needlessly strong. I’m not aware of any practical way of doing this.
Thanks for pointing out this example!
Larry
Last updated: Apr 19 2024 at 08:19 UTC