[isabelle-dev] unit :: complete_boolean_algebra – 697e0fad9337
Andreas Lochbihler
andreas.lochbihler at inf.ethz.ch
Wed Jun 11 09:22:22 CEST 2014
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
>
More information about the isabelle-dev
mailing list