Hi Florian,
the simproc unit_eq in
http://isabelle.in.tum.de/repos/isabelle/file/697e0fad9337/src/HOL/Product_Type.thy#l78
rewrites anything of type unit to (), so there's no need to declare the definitions
introduced in 697e0fad9337 as [simp]. One could declare sup_unit_def, inf_unit_def,
Sup_unit_def, and Inf_unit_def as [abs_def, simp] such that they get unfolded even if they
are applied only partially, but I don't know whether that is a good thing to have.
(Admittedly, the definition of uminus has this [simp] declaration, so it's a bit
unconsistent at the moment).
Andreas
On 10/06/14 23:02, Florian Haftmann wrote:
Hi Andreas,
I'm wondering whether there is a deliberate reason to declare top, bot
etc. on unit not as simp by default. Since there is only one element of
unit, proof goals after simp should be trivial…
Florian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
