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

[Florian Haftmann]

Hi Andreas,

see now http://isabelle.in.tum.de/reports/Isabelle/rev/8fcbfce2a2a9

for a uniform approach.

Hope this fits,
	Florian

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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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