[isabelle-dev] unit :: complete_boolean_algebra – 697e0fad9337

[Andreas Lochbihler]

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
>