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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Jun 12 10:40:42 CEST 2014

Hi Andreas,

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


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140612/7230dc4e/attachment.sig>

More information about the isabelle-dev mailing list