[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


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).


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