[isabelle-dev] unit :: complete_boolean_algebra – 697e0fad9337
florian.haftmann at informatik.tu-muenchen.de
Thu Jun 12 10:40:42 CEST 2014
see now http://isabelle.in.tum.de/reports/Isabelle/rev/8fcbfce2a2a9
for a uniform approach.
Hope this fits,
On 11.06.2014 09:22, Andreas Lochbihler wrote:
> 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…
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev